boolbvt::convert_constant is now independent of bitvector representation

src/solvers/flattening/boolbv_constant.cpp

@@ -6,6 +6,7 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include <util/arith_tools.h>
 
 #include "boolbv.h"
 
@@ -78,9 +79,9 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
           expr_type.id()==ID_c_bit_field ||
           expr_type.id()==ID_incomplete_c_enum)
   {
-    const std::string &binary=id2string(expr.get_value());
+    const auto &value = expr.get_value();
 
-    if(binary.size()!=width)
+    if(value.size() != width)
     {
       error().source_location=expr.find_source_location();
       error() << "wrong value length in constant: "
@@ -90,7 +91,7 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
 
     for(std::size_t i=0; i<width; i++)
     {
-      bool bit=(binary[binary.size()-i-1]=='1');
+      const bool bit = get_bitvector_bit(value, i);
       bv[i]=const_literal(bit);
     }
 

src/util/arith_tools.cpp

@@ -262,3 +262,14 @@ void mp_max(mp_integer &a, const mp_integer &b)
   if(b>a)
     a=b;
 }
+
+/// Get a bit with given index from bit-vector representation.
+/// \param src: the bitvector representation
+/// \param bit_index: index (0 is the least significant)
+bool get_bitvector_bit(const irep_idt &src, std::size_t bit_index)
+{
+  // The representation is binary, using '0'/'1',
+  // most significant bit first.
+  PRECONDITION(bit_index < src.size());
+  return src[src.size() - 1 - bit_index] == '1';
+}

src/util/arith_tools.h

@@ -164,4 +164,6 @@ mp_integer power(const mp_integer &base, const mp_integer &exponent);
 void mp_min(mp_integer &a, const mp_integer &b);
 void mp_max(mp_integer &a, const mp_integer &b);
 
+bool get_bitvector_bit(const irep_idt &src, std::size_t bit_index);
+
 #endif // CPROVER_UTIL_ARITH_TOOLS_H

src/util/simplify_expr.cpp

@@ -135,25 +135,22 @@ bool simplify_exprt::simplify_popcount(popcount_exprt &expr)
 
   if(op.is_constant())
   {
-    const typet &type=ns.follow(op.type());
+    const typet &op_type = op.type();
 
-    if(type.id()==ID_signedbv ||
-       type.id()==ID_unsignedbv)
+    if(op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv)
     {
-      mp_integer value;
-      if(!to_integer(op, value))
-      {
-        std::size_t result;
+      const auto width = to_bitvector_type(op_type).get_width();
+      const auto &value = to_constant_expr(op).get_value();
+      std::size_t result = 0;
 
-        for(result=0; value!=0; value=value>>1)
-          if(value.is_odd())
-            result++;
+      for(std::size_t i = 0; i < width; i++)
+        if(get_bitvector_bit(value, i))
+          result++;
 
-        exprt simp_result = from_integer(result, expr.type());
-        expr.swap(simp_result);
+      auto result_expr = from_integer(result, expr.type());
+      expr.swap(result_expr);
 
-        return false;
-      }
+      return false;
     }
   }