Implement popcount in flattening back-end

We can avoid lowering, and eventually re-use this as part of other
algorithms.

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_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 zero_extension(bv_utils.popcount(op));
+}

src/solvers/flattening/bv_utils.cpp

@@ -3205,3 +3205,77 @@ 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)
+{
+  if(bv.empty())
+    return bvt();
+
+  // Determine the result width: log2(bv.size()) + 1
+  std::size_t result_width = address_bits(bv.size());
+  if(result_width == 0)
+    result_width = 1; // At least one bit for the result
+
+  // Start with the original bit vector
+  bvt x = bv;
+
+  // Apply the parallel bit counting algorithm from Hacker's Delight
+  // 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 < address_bits(x.size()); 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() < field_size)
+      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 = zeros(x.size());
+    bvt masked_shifted = zeros(x.size());
+
+    for(std::size_t i = 0; i < x.size(); i++)
+    {
+      masked_x[i] = prop.land(x[i], mask[i]);
+      masked_shifted[i] = prop.land(x_shifted[i], mask[i]);
+    }
+
+    // Add the masked vectors
+    x = add(masked_x, masked_shifted);
+  }
+
+  // Extract the result with the appropriate width
+  // The result is in the least significant bits of x
+  bvt result;
+  result.reserve(result_width);
+
+  for(std::size_t i = 0; i < result_width; i++)
+  {
+    if(i < x.size())
+      result.push_back(x[i]);
+    else
+      result.push_back(const_literal(false));
+  }
+
+  return result;
+}

src/solvers/flattening/bv_utils.h

@@ -222,6 +222,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 ∝