Merge pull request #8717 from tautschnig/popcount-flattening

Implement popcount in flattening back-end

Author: tautschnig

src/solvers/Makefile

@@ -118,6 +118,7 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/boolbv_onehot.cpp \
       flattening/boolbv_overflow.cpp \
       flattening/boolbv_power.cpp \
+      flattening/boolbv_popcount.cpp \
       flattening/boolbv_quantifier.cpp \
       flattening/boolbv_reduction.cpp \
       flattening/boolbv_replication.cpp \

src/solvers/flattening/boolbv.cpp

@@ -235,7 +235,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_power)
      return convert_power(to_binary_expr(expr));
   else if(expr.id() == ID_popcount)
-    return convert_bv(simplify_expr(to_popcount_expr(expr).lower(), ns));
+     return convert_popcount(to_popcount_expr(expr));
   else if(expr.id() == ID_count_leading_zeros)
   {
     return convert_bv(

src/solvers/flattening/boolbv.h

@@ -37,6 +37,7 @@ class floatbv_round_to_integral_exprt;
 class floatbv_typecast_exprt;
 class ieee_float_op_exprt;
 class overflow_result_exprt;
+class popcount_exprt;
 class replication_exprt;
 class unary_overflow_exprt;
 class union_typet;
@@ -203,6 +204,7 @@ class boolbvt:public arrayst
   virtual bvt convert_bitreverse(const bitreverse_exprt &expr);
   virtual bvt convert_saturating_add_sub(const binary_exprt &expr);
   virtual bvt convert_overflow_result(const overflow_result_exprt &expr);
+  virtual bvt convert_popcount(const popcount_exprt &expr);
 
   bvt convert_update_bits(bvt src, const exprt &index, const bvt &new_value);
 

src/solvers/flattening/boolbv_popcount.cpp

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module:
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include <util/bitvector_expr.h>
+
+#include "boolbv.h"
+
+bvt boolbvt::convert_popcount(const popcount_exprt &expr)
+{
+  const std::size_t width = boolbv_width(expr.type());
+
+  bvt op = convert_bv(expr.op());
+
+  return bv_utils.zero_extension(bv_utils.popcount(op), width);
+}

src/solvers/flattening/bv_utils.cpp

@@ -8,6 +8,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "bv_utils.h"
 
+#include <util/arith_tools.h>
+
 #include <list>
 #include <utility>
 
@@ -1693,3 +1695,65 @@ bvt bv_utilst::verilog_bv_normal_bits(const bvt &src)
 
   return even_bits;
 }
+
+/// Symbolic implementation of popcount (count of 1 bits in a bit vector)
+/// Based on the pop0 algorithm from Hacker's Delight
+/// \param bv: The bit vector to count 1s in
+/// \return A bit vector representing the count
+bvt bv_utilst::popcount(const bvt &bv)
+{
+  PRECONDITION(!bv.empty());
+
+  // Determine the result width: log2(bv.size()) + 1
+  std::size_t log2 = address_bits(bv.size());
+  CHECK_RETURN(log2 >= 1);
+
+  // Start with the original bit vector
+  bvt x = bv;
+
+  // Apply the parallel bit counting algorithm from Hacker's Delight (pop0).
+  // The algorithm works by summing adjacent bit groups of increasing sizes.
+
+  // Iterate through the stages of the algorithm, doubling the field size each
+  // time
+  for(std::size_t stage = 0; stage < log2; ++stage)
+  {
+    std::size_t shift_amount = 1 << stage;     // 1, 2, 4, 8, 16, ...
+    std::size_t field_size = 2 * shift_amount; // 2, 4, 8, 16, 32, ...
+
+    // Skip if the bit vector is smaller than the field size
+    if(x.size() <= shift_amount)
+      break;
+
+    // Shift the bit vector
+    bvt x_shifted = shift(x, shiftt::SHIFT_LRIGHT, shift_amount);
+
+    // Create a mask with 'shift_amount' ones followed by 'shift_amount' zeros,
+    // repeated
+    bvt mask;
+    mask.reserve(x.size());
+    for(std::size_t i = 0; i < x.size(); i++)
+    {
+      if((i % field_size) < shift_amount)
+        mask.push_back(const_literal(true));
+      else
+        mask.push_back(const_literal(false));
+    }
+
+    // Apply the mask to both the original and shifted bit vectors
+    bvt masked_x, masked_shifted;
+    masked_x.reserve(x.size());
+    masked_shifted.reserve(x.size());
+
+    for(std::size_t i = 0; i < x.size(); i++)
+    {
+      masked_x.push_back(prop.land(x[i], mask[i]));
+      masked_shifted.push_back(prop.land(x_shifted[i], mask[i]));
+    }
+
+    // Add the masked vectors
+    x = add(masked_x, masked_shifted);
+  }
+
+  return x;
+}

src/solvers/flattening/bv_utils.h

@@ -218,6 +218,12 @@ class bv_utilst
   literalt verilog_bv_has_x_or_z(const bvt &);
   static bvt verilog_bv_normal_bits(const bvt &);
 
+  /// Symbolic implementation of popcount (count of 1 bits in a bit vector)
+  /// Based on the pop0 algorithm from Hacker's Delight
+  /// \param bv: The bit vector to count 1s in
+  /// \return A bit vector representing the count
+  bvt popcount(const bvt &bv);
+
 protected:
   propt ∝