added means to get a bit from bit-vector representation

Author: Daniel Kroening

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,9 @@ 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);
 
+/// get bit with given index from bit vector
+/// \param src: the bitvector representation
+/// \param bit_index: the index (0 is the least significant)
+bool get_bitvector_bit(const irep_idt &src, std::size_t bit_index);
+
 #endif // CPROVER_UTIL_ARITH_TOOLS_H