Make lower_popcount a method of popcount_exprt

Expression lowering may be useful well outside the solvers/ context.
Making it a method of the class being lowered also serves as a way of
describing the semantics of the expression.

This is mainly a refactoring, no changes in behaviour are intended.

scripts/expected_doxygen_warnings.txt

@@ -21,13 +21,13 @@
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'config.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'invariant.h' not generated, too many nodes (187), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'invariant.h' not generated, too many nodes (186), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'namespace.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/solvers/Makefile

@@ -141,7 +141,6 @@ SRC = $(BOOLEFORCE_SRC) \
       floatbv/float_approximation.cpp \
       lowering/byte_operators.cpp \
       lowering/functions.cpp \
-      lowering/popcount.cpp \
       bdd/miniBDD/miniBDD.cpp \
       prop/bdd_expr.cpp \
       prop/cover_goals.cpp \

src/solvers/flattening/boolbv.cpp

@@ -227,7 +227,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(lower_popcount(to_popcount_expr(expr), ns));
+    return convert_bv(to_popcount_expr(expr).lower());
 
   return conversion_failed(expr);
 }

src/solvers/lowering/expr_lowering.h

@@ -14,7 +14,6 @@ Author: Michael Tautschnig
 class byte_extract_exprt;
 class byte_update_exprt;
 class namespacet;
-class popcount_exprt;
 
 /// Rewrite a byte extract expression to more fundamental operations.
 /// \param src: Byte extract expression
@@ -44,10 +43,4 @@ exprt lower_byte_operators(const exprt &src, const namespacet &ns);
 
 bool has_byte_operator(const exprt &src);
 
-/// Lower a popcount_exprt to arithmetic and logic expressions
-/// \param expr: Input expression to be translated
-/// \param ns: Namespace for type lookups
-/// \return Semantically equivalent expression
-exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns);
-
 #endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */

src/solvers/smt2/smt2_conv.cpp

@@ -1984,8 +1984,7 @@ void smt2_convt::convert_expr(const exprt &expr)
   }
   else if(expr.id() == ID_popcount)
   {
-    exprt lowered = lower_popcount(to_popcount_expr(expr), ns);
-    convert_expr(lowered);
+    convert_expr(to_popcount_expr(expr).lower());
   }
   else
     INVARIANT_WITH_DIAGNOSTICS(

src/util/bitvector_expr.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "bitvector_expr.h"
 
 #include "arith_tools.h"
+#include "bitvector_types.h"
 #include "mathematical_types.h"
 
 shift_exprt::shift_exprt(
@@ -40,3 +41,49 @@ extractbits_exprt::extractbits_exprt(
     from_integer(_upper, integer_typet()),
     from_integer(_lower, integer_typet()));
 }
+
+exprt popcount_exprt::lower() const
+{
+  // Hacker's Delight, variant pop0:
+  // x = (x & 0x55555555) + ((x >> 1) & 0x55555555);
+  // x = (x & 0x33333333) + ((x >> 2) & 0x33333333);
+  // x = (x & 0x0F0F0F0F) + ((x >> 4) & 0x0F0F0F0F);
+  // x = (x & 0x00FF00FF) + ((x >> 8) & 0x00FF00FF);
+  // etc.
+  // return x;
+  // http://www.hackersdelight.org/permissions.htm
+
+  // make sure the operand width is a power of two
+  exprt x = op();
+  const auto x_width = to_bitvector_type(x.type()).get_width();
+  CHECK_RETURN(x_width >= 1);
+  const std::size_t bits = address_bits(x_width);
+  const std::size_t new_width = numeric_cast_v<std::size_t>(power(2, bits));
+
+  const bool need_typecast =
+    new_width > x_width || x.type().id() != ID_unsignedbv;
+
+  if(need_typecast)
+    x = typecast_exprt(x, unsignedbv_typet(new_width));
+
+  // repeatedly compute x = (x & bitmask) + ((x >> shift) & bitmask)
+  for(std::size_t shift = 1; shift < new_width; shift <<= 1)
+  {
+    // x >> shift
+    lshr_exprt shifted_x(
+      x, from_integer(shift, unsignedbv_typet(address_bits(shift) + 1)));
+    // bitmask is a string of alternating shift-many bits starting from lsb set
+    // to 1
+    std::string bitstring;
+    bitstring.reserve(new_width);
+    for(std::size_t i = 0; i < new_width / (2 * shift); ++i)
+      bitstring += std::string(shift, '0') + std::string(shift, '1');
+    const mp_integer value = binary2integer(bitstring, false);
+    const constant_exprt bitmask(integer2bvrep(value, new_width), x.type());
+    // build the expression
+    x = plus_exprt(bitand_exprt(x, bitmask), bitand_exprt(shifted_x, bitmask));
+  }
+
+  // the result is restricted to the result type
+  return typecast_exprt::conditional_cast(x, type());
+}

src/util/bitvector_expr.h

@@ -641,6 +641,10 @@ class popcount_exprt : public unary_exprt
     : unary_exprt(ID_popcount, _op, _op.type())
   {
   }
+
+  /// Lower a popcount_exprt to arithmetic and logic expressions.
+  /// \return Semantically equivalent expression
+  exprt lower() const;
 };
 
 template <>