use 'bvrep' as terminology for 'bitvector representation'

Daniel Kroening · Daniel Kroening · commit 7235f233b2b5 · 2018-10-19T11:21:27.000+01:00
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -1814,7 +1814,7 @@ std::string expr2ct::convert_constant(
     const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
     const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
 
-    mp_integer int_value = bv2integer(value, width, is_signed);
+    mp_integer int_value = bvrep2integer(value, width, is_signed);
     mp_integer i=0;
 
     irep_idt int_value_string=integer2string(int_value);
@@ -1853,7 +1853,7 @@ std::string expr2ct::convert_constant(
     const auto width = to_bitvector_type(type).get_width();
 
     mp_integer int_value =
-      bv2integer(value, width, type.id() == ID_signedbv);
+      bvrep2integer(value, width, type.id() == ID_signedbv);
 
     const irep_idt &c_type=
       type.id()==ID_c_bit_field?type.subtype().get(ID_C_c_type):
diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
@@ -566,7 +566,7 @@ int linker_script_merget::ls_data2instructions(
     symbol_exprt lhs(d["sym"].value, pointer_type(char_type()));
 
     constant_exprt rhs(
-      integer2bv(
+      integer2bvrep(
         string2integer(id2string(symbol_value)),
         unsigned_int_type().get_width()),
       unsigned_int_type());
@@ -630,7 +630,7 @@ int linker_script_merget::ls_data2instructions(
     symbol_exprt lhs(d["sym"].value, pointer_type(char_type()));
 
     constant_exprt rhs;
-    rhs.set_value(integer2bv(
+    rhs.set_value(integer2bvrep(
       string2integer(d["val"].value), unsigned_int_type().get_width()));
     rhs.type()=unsigned_int_type();
 
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
@@ -140,7 +140,8 @@ static std::string numeric_representation(
 
   if(options.hex_representation)
   {
-    mp_integer value_int = bv2integer(id2string(value), value.size(), false);
+    const mp_integer value_int =
+      bvrep2integer(to_constant_expr(expr).get_value(), value.size(), false);
     result = integer2string(value_int, 16);
     prefix = "0x";
   }
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
@@ -383,7 +383,7 @@ void interpretert::evaluate(
     {
       const irep_idt &value=to_constant_expr(expr).get_value();
       const auto width = to_c_bool_type(expr.type()).get_width();
-      dest.push_back(bv2integer(value, width, false));
+      dest.push_back(bvrep2integer(value, width, false));
       return;
     }
     else if(expr.type().id()==ID_bool)
@@ -985,15 +985,15 @@ void interpretert::evaluate(
       else if(expr.type().id()==ID_signedbv)
       {
         const auto width = to_signedbv_type(expr.type()).get_width();
-        const auto s = integer2bv(value, width);
-        dest.push_back(bv2integer(s, width, true));
+        const auto s = integer2bvrep(value, width);
+        dest.push_back(bvrep2integer(s, width, true));
         return;
       }
       else if(expr.type().id()==ID_unsignedbv)
       {
         const auto width = to_unsignedbv_type(expr.type()).get_width();
-        const auto s = integer2bv(value, width);
-        dest.push_back(bv2integer(s, width, false));
+        const auto s = integer2bvrep(value, width);
+        dest.push_back(bvrep2integer(s, width, false));
         return;
       }
       else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool))
diff --git a/src/solvers/flattening/boolbv_constant.cpp b/src/solvers/flattening/boolbv_constant.cpp
@@ -91,7 +91,7 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
 
     for(std::size_t i=0; i<width; i++)
     {
-      const bool bit = get_bitvector_bit(value, width, i);
+      const bool bit = get_bvrep_bit(value, width, i);
       bv[i]=const_literal(bit);
     }
 
diff --git a/src/solvers/lowering/popcount.cpp b/src/solvers/lowering/popcount.cpp
@@ -48,7 +48,7 @@ exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
     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);
-    constant_exprt bitmask(integer2bv(value, new_width), x.type());
+    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));
   }
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
@@ -44,19 +44,19 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
   else if(type_id==ID_unsignedbv)
   {
     const auto width = to_unsignedbv_type(type).get_width();
-    int_value = bv2integer(value, width, false);
+    int_value = bvrep2integer(value, width, false);
     return false;
   }
   else if(type_id==ID_signedbv)
   {
     const auto width = to_signedbv_type(type).get_width();
-    int_value = bv2integer(value, width, true);
+    int_value = bvrep2integer(value, width, true);
     return false;
   }
   else if(type_id==ID_c_bool)
   {
     const auto width = to_c_bool_type(type).get_width();
-    int_value = bv2integer(value, width, false);
+    int_value = bvrep2integer(value, width, false);
     return false;
   }
   else if(type_id==ID_c_enum)
@@ -65,13 +65,13 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
     if(subtype.id()==ID_signedbv)
     {
       const auto width = to_signedbv_type(type).get_width();
-      int_value = bv2integer(value, width, true);
+      int_value = bvrep2integer(value, width, true);
       return false;
     }
     else if(subtype.id()==ID_unsignedbv)
     {
       const auto width = to_unsignedbv_type(type).get_width();
-      int_value = bv2integer(value, width, false);
+      int_value = bvrep2integer(value, width, false);
       return false;
     }
   }
@@ -83,17 +83,17 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
 
     if(subtype.id()==ID_signedbv)
     {
-      int_value = bv2integer(value, width, true);
+      int_value = bvrep2integer(value, width, true);
       return false;
     }
     else if(subtype.id()==ID_unsignedbv)
     {
-      int_value = bv2integer(value, width, false);
+      int_value = bvrep2integer(value, width, false);
       return false;
     }
     else if(subtype.id() == ID_c_bool)
     {
-      int_value = bv2integer(value, width, false);
+      int_value = bvrep2integer(value, width, false);
       return false;
     }
   }
@@ -136,28 +136,28 @@ constant_exprt from_integer(
   else if(type_id==ID_unsignedbv)
   {
     std::size_t width=to_unsignedbv_type(type).get_width();
-    return constant_exprt(integer2bv(int_value, width), type);
+    return constant_exprt(integer2bvrep(int_value, width), type);
   }
   else if(type_id==ID_bv)
   {
     std::size_t width=to_bv_type(type).get_width();
-    return constant_exprt(integer2bv(int_value, width), type);
+    return constant_exprt(integer2bvrep(int_value, width), type);
   }
   else if(type_id==ID_signedbv)
   {
     std::size_t width=to_signedbv_type(type).get_width();
-    return constant_exprt(integer2bv(int_value, width), type);
+    return constant_exprt(integer2bvrep(int_value, width), type);
   }
   else if(type_id==ID_c_enum)
   {
     const std::size_t width =
       to_c_enum_type(type).subtype().get_size_t(ID_width);
-    return constant_exprt(integer2bv(int_value, width), type);
+    return constant_exprt(integer2bvrep(int_value, width), type);
   }
   else if(type_id==ID_c_bool)
   {
     std::size_t width=to_c_bool_type(type).get_width();
-    return constant_exprt(integer2bv(int_value, width), type);
+    return constant_exprt(integer2bvrep(int_value, width), type);
   }
   else if(type_id==ID_bool)
   {
@@ -175,7 +175,7 @@ constant_exprt from_integer(
   else if(type_id==ID_c_bit_field)
   {
     std::size_t width=to_c_bit_field_type(type).get_width();
-    return constant_exprt(integer2bv(int_value, width), type);
+    return constant_exprt(integer2bvrep(int_value, width), type);
   }
   else if(type_id==ID_fixedbv)
   {
@@ -280,7 +280,7 @@ void mp_max(mp_integer &a, const mp_integer &b)
 /// \param src: the bitvector representation
 /// \param width: the number of bits in the bitvector
 /// \param bit_index: index (0 is the least significant)
-bool get_bitvector_bit(
+bool get_bvrep_bit(
   const irep_idt &src,
   std::size_t width,
   std::size_t bit_index)
@@ -314,14 +314,14 @@ make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)
 /// \param width: the width of the bit-vector
 /// \param f: the functor
 /// \returns new bitvector representation
-irep_idt bitvector_bitwise_op(
+irep_idt bvrep_bitwise_op(
   const irep_idt &a,
   const irep_idt &b,
   const std::size_t width,
   const std::function<bool(bool, bool)> f)
 {
   return make_bvrep(width, [&a, &b, &width, f](std::size_t i) {
-    return f(get_bitvector_bit(a, width, i), get_bitvector_bit(b, width, i));
+    return f(get_bvrep_bit(a, width, i), get_bvrep_bit(b, width, i));
   });
 }
 
@@ -331,25 +331,24 @@ irep_idt bitvector_bitwise_op(
 /// \param width: the width of the bit-vector
 /// \param f: the functor
 /// \returns new bitvector representation
-irep_idt bitvector_bitwise_op(
+irep_idt bvrep_bitwise_op(
   const irep_idt &a,
   const std::size_t width,
   const std::function<bool(bool)> f)
 {
   return make_bvrep(width, [&a, &width, f](std::size_t i) {
-    return f(get_bitvector_bit(a, width, i));
+    return f(get_bvrep_bit(a, width, i));
   });
 }
 
 /// convert an integer to bit-vector representation with given width
-irep_idt integer2bv(const mp_integer &src, std::size_t width)
+irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
 {
   return integer2binary(src, width);
 }
 
 /// convert a bit-vector representation (possibly signed) to integer
-mp_integer
-bv2integer(const irep_idt &src, std::size_t width, bool is_signed)
+mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
 {
   PRECONDITION(src.size() == width);
   return binary2integer(id2string(src), is_signed);
diff --git a/src/util/arith_tools.h b/src/util/arith_tools.h
@@ -164,15 +164,15 @@ 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(
+bool get_bvrep_bit(
   const irep_idt &src,
   std::size_t width,
   std::size_t bit_index);
 
 irep_idt
 make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f);
 
-irep_idt integer2bv(const mp_integer &, std::size_t width);
-mp_integer bv2integer(const irep_idt &, std::size_t width, bool is_signed);
+irep_idt integer2bvrep(const mp_integer &, std::size_t width);
+mp_integer bvrep2integer(const irep_idt &, std::size_t width, bool is_signed);
 
 #endif // CPROVER_UTIL_ARITH_TOOLS_H
diff --git a/src/util/bv_arithmetic.cpp b/src/util/bv_arithmetic.cpp
@@ -84,7 +84,7 @@ mp_integer bv_arithmetict::pack() const
 
 exprt bv_arithmetict::to_expr() const
 {
-  return constant_exprt(integer2bv(value, spec.width), spec.to_type());
+  return constant_exprt(integer2bvrep(value, spec.width), spec.to_type());
 }
 
 bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)
@@ -184,5 +184,6 @@ void bv_arithmetict::from_expr(const exprt &expr)
 {
   PRECONDITION(expr.is_constant());
   spec=bv_spect(expr.type());
-  value = bv2integer(to_constant_expr(expr).get_value(), spec.width, spec.is_signed);
+  value = bvrep2integer(
+    to_constant_expr(expr).get_value(), spec.width, spec.is_signed);
 }
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
@@ -251,7 +251,7 @@ bool exprt::is_one() const
     {
       const auto width = to_bitvector_type(type()).get_width();
       mp_integer int_value =
-        bv2integer(id2string(constant_expr.get_value()), width, false);
+        bvrep2integer(id2string(constant_expr.get_value()), width, false);
       if(int_value==1)
         return true;
     }
diff --git a/src/util/fixedbv.cpp b/src/util/fixedbv.cpp
@@ -26,7 +26,7 @@ fixedbvt::fixedbvt(const constant_exprt &expr)
 void fixedbvt::from_expr(const constant_exprt &expr)
 {
   spec=fixedbv_spect(to_fixedbv_type(expr.type()));
-  v = bv2integer(expr.get_value(), spec.width, true);
+  v = bvrep2integer(expr.get_value(), spec.width, true);
 }
 
 void fixedbvt::from_integer(const mp_integer &i)
@@ -46,7 +46,7 @@ constant_exprt fixedbvt::to_expr() const
   type.set_width(spec.width);
   type.set_integer_bits(spec.integer_bits);
   PRECONDITION(spec.width != 0);
-  return constant_exprt(integer2bv(v, spec.width), type);
+  return constant_exprt(integer2bvrep(v, spec.width), type);
 }
 
 void fixedbvt::round(const fixedbv_spect &dest_spec)
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
@@ -696,7 +696,7 @@ void ieee_floatt::divide_and_round(
 
 constant_exprt ieee_floatt::to_expr() const
 {
-  return constant_exprt(integer2bv(pack(), spec.width()), spec.to_type());
+  return constant_exprt(integer2bvrep(pack(), spec.width()), spec.to_type());
 }
 
 ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other)
@@ -1062,7 +1062,7 @@ void ieee_floatt::change_spec(const ieee_float_spect &dest_spec)
 void ieee_floatt::from_expr(const constant_exprt &expr)
 {
   spec=ieee_float_spect(to_floatbv_type(expr.type()));
-  unpack(bv2integer(expr.get_value(), spec.width(), false));
+  unpack(bvrep2integer(expr.get_value(), spec.width(), false));
 }
 
 mp_integer ieee_floatt::to_integer() const
diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp
@@ -220,7 +220,7 @@ json_objectt json(
 static std::string binary(const constant_exprt &src)
 {
   const auto width = to_bitvector_type(src.type()).get_width();
-  const auto int_val = bv2integer(src.get_value(), width, false);
+  const auto int_val = bvrep2integer(src.get_value(), width, false);
   return integer2binary(int_val, width);
 }
 
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
@@ -144,7 +144,7 @@ bool simplify_exprt::simplify_popcount(popcount_exprt &expr)
       std::size_t result = 0;
 
       for(std::size_t i = 0; i < width; i++)
-        if(get_bitvector_bit(value, width, i))
+        if(get_bvrep_bit(value, width, i))
           result++;
 
       auto result_expr = from_integer(result, expr.type());
@@ -670,7 +670,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
          expr_type_id==ID_floatbv)
       {
         const auto width = to_bv_type(op_type).get_width();
-        const auto int_value = bv2integer(value, width, false);
+        const auto int_value = bvrep2integer(value, width, false);
         expr=from_integer(int_value, expr_type);
         return false;
       }
@@ -1460,7 +1460,7 @@ exprt simplify_exprt::bits2expr(
     std::reverse(tmp.begin(), tmp.end());
 
     mp_integer i = binary2integer(tmp, false);
-    return constant_exprt(integer2bv(i, bits.size()), type);
+    return constant_exprt(integer2bvrep(i, bits.size()), type);
   }
   else if(type.id()==ID_c_enum)
   {
@@ -1577,7 +1577,7 @@ optionalt<std::string> simplify_exprt::expr2bits(
       std::string result(width, ' ');
 
       for(std::string::size_type i = 0; i < width; ++i)
-        result[map.map_bit(i)] = get_bitvector_bit(bvrep, width, i) ? '1' : '0';
+        result[map.map_bit(i)] = get_bvrep_bit(bvrep, width, i) ? '1' : '0';
 
       return result;
     }
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp

Original file line number	Diff line number	Diff line change
`@@ -140,7 +140,8 @@ static std::string numeric_representation(`
`140`	`140`
`141`	`141`	`if(options.hex_representation)`
`142`	`142`	`{`
`143`		`- mp_integer value_int = bv2integer(id2string(value), value.size(), false);`
	`143`	`+ const mp_integer value_int =`
	`144`	`+ bvrep2integer(to_constant_expr(expr).get_value(), value.size(), false);`
`144`	`145`	`result = integer2string(value_int, 16);`
`145`	`146`	`prefix = "0x";`
`146`	`147`	`}`
Original file line number	Diff line number	Diff line change
`@@ -383,7 +383,7 @@ void interpretert::evaluate(`
`383`	`383`	`{`
`384`	`384`	`const irep_idt &value=to_constant_expr(expr).get_value();`
`385`	`385`	`const auto width = to_c_bool_type(expr.type()).get_width();`
`386`		`- dest.push_back(bv2integer(value, width, false));`
	`386`	`+ dest.push_back(bvrep2integer(value, width, false));`
`387`	`387`	`return;`
`388`	`388`	`}`
`389`	`389`	`else if(expr.type().id()==ID_bool)`
`@@ -985,15 +985,15 @@ void interpretert::evaluate(`
`985`	`985`	`else if(expr.type().id()==ID_signedbv)`
`986`	`986`	`{`
`987`	`987`	`const auto width = to_signedbv_type(expr.type()).get_width();`
`988`		`- const auto s = integer2bv(value, width);`
`989`		`- dest.push_back(bv2integer(s, width, true));`
	`988`	`+ const auto s = integer2bvrep(value, width);`
	`989`	`+ dest.push_back(bvrep2integer(s, width, true));`
`990`	`990`	`return;`
`991`	`991`	`}`
`992`	`992`	`else if(expr.type().id()==ID_unsignedbv)`
`993`	`993`	`{`
`994`	`994`	`const auto width = to_unsignedbv_type(expr.type()).get_width();`
`995`		`- const auto s = integer2bv(value, width);`
`996`		`- dest.push_back(bv2integer(s, width, false));`
	`995`	`+ const auto s = integer2bvrep(value, width);`
	`996`	`+ dest.push_back(bvrep2integer(s, width, false));`
`997`	`997`	`return;`
`998`	`998`	`}`
`999`	`999`	`else if((expr.type().id()==ID_bool) \|\| (expr.type().id()==ID_c_bool))`
Original file line number	Diff line number	Diff line change
`@@ -91,7 +91,7 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)`
`91`	`91`
`92`	`92`	`for(std::size_t i=0; i<width; i++)`
`93`	`93`	`{`
`94`		`- const bool bit = get_bitvector_bit(value, width, i);`
	`94`	`+ const bool bit = get_bvrep_bit(value, width, i);`
`95`	`95`	`bv[i]=const_literal(bit);`
`96`	`96`	`}`
`97`	`97`
Original file line number	Diff line number	Diff line change
`@@ -48,7 +48,7 @@ exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)`
`48`	`48`	`for(std::size_t i = 0; i < new_width / (2 * shift); ++i)`
`49`	`49`	`bitstring += std::string(shift, '0') + std::string(shift, '1');`
`50`	`50`	`const mp_integer value = binary2integer(bitstring, false);`
`51`		`- constant_exprt bitmask(integer2bv(value, new_width), x.type());`
	`51`	`+ const constant_exprt bitmask(integer2bvrep(value, new_width), x.type());`
`52`	`52`	`// build the expression`
`53`	`53`	`x = plus_exprt(bitand_exprt(x, bitmask), bitand_exprt(shifted_x, bitmask));`
`54`	`54`	`}`
Original file line number	Diff line number	Diff line change
`@@ -44,19 +44,19 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)`
`44`	`44`	`else if(type_id==ID_unsignedbv)`
`45`	`45`	`{`
`46`	`46`	`const auto width = to_unsignedbv_type(type).get_width();`
`47`		`- int_value = bv2integer(value, width, false);`
	`47`	`+ int_value = bvrep2integer(value, width, false);`
`48`	`48`	`return false;`
`49`	`49`	`}`
`50`	`50`	`else if(type_id==ID_signedbv)`
`51`	`51`	`{`
`52`	`52`	`const auto width = to_signedbv_type(type).get_width();`
`53`		`- int_value = bv2integer(value, width, true);`
	`53`	`+ int_value = bvrep2integer(value, width, true);`
`54`	`54`	`return false;`
`55`	`55`	`}`
`56`	`56`	`else if(type_id==ID_c_bool)`
`57`	`57`	`{`
`58`	`58`	`const auto width = to_c_bool_type(type).get_width();`
`59`		`- int_value = bv2integer(value, width, false);`
	`59`	`+ int_value = bvrep2integer(value, width, false);`
`60`	`60`	`return false;`
`61`	`61`	`}`
`62`	`62`	`else if(type_id==ID_c_enum)`
`@@ -65,13 +65,13 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)`
`65`	`65`	`if(subtype.id()==ID_signedbv)`
`66`	`66`	`{`
`67`	`67`	`const auto width = to_signedbv_type(type).get_width();`
`68`		`- int_value = bv2integer(value, width, true);`
	`68`	`+ int_value = bvrep2integer(value, width, true);`
`69`	`69`	`return false;`
`70`	`70`	`}`
`71`	`71`	`else if(subtype.id()==ID_unsignedbv)`
`72`	`72`	`{`
`73`	`73`	`const auto width = to_unsignedbv_type(type).get_width();`
`74`		`- int_value = bv2integer(value, width, false);`
	`74`	`+ int_value = bvrep2integer(value, width, false);`
`75`	`75`	`return false;`
`76`	`76`	`}`
`77`	`77`	`}`
`@@ -83,17 +83,17 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)`
`83`	`83`
`84`	`84`	`if(subtype.id()==ID_signedbv)`
`85`	`85`	`{`
`86`		`- int_value = bv2integer(value, width, true);`
	`86`	`+ int_value = bvrep2integer(value, width, true);`
`87`	`87`	`return false;`
`88`	`88`	`}`
`89`	`89`	`else if(subtype.id()==ID_unsignedbv)`
`90`	`90`	`{`
`91`		`- int_value = bv2integer(value, width, false);`
	`91`	`+ int_value = bvrep2integer(value, width, false);`
`92`	`92`	`return false;`
`93`	`93`	`}`
`94`	`94`	`else if(subtype.id() == ID_c_bool)`
`95`	`95`	`{`
`96`		`- int_value = bv2integer(value, width, false);`
	`96`	`+ int_value = bvrep2integer(value, width, false);`
`97`	`97`	`return false;`
`98`	`98`	`}`
`99`	`99`	`}`
`@@ -136,28 +136,28 @@ constant_exprt from_integer(`
`136`	`136`	`else if(type_id==ID_unsignedbv)`
`137`	`137`	`{`
`138`	`138`	`std::size_t width=to_unsignedbv_type(type).get_width();`
`139`		`- return constant_exprt(integer2bv(int_value, width), type);`
	`139`	`+ return constant_exprt(integer2bvrep(int_value, width), type);`
`140`	`140`	`}`
`141`	`141`	`else if(type_id==ID_bv)`
`142`	`142`	`{`
`143`	`143`	`std::size_t width=to_bv_type(type).get_width();`
`144`		`- return constant_exprt(integer2bv(int_value, width), type);`
	`144`	`+ return constant_exprt(integer2bvrep(int_value, width), type);`
`145`	`145`	`}`
`146`	`146`	`else if(type_id==ID_signedbv)`
`147`	`147`	`{`
`148`	`148`	`std::size_t width=to_signedbv_type(type).get_width();`
`149`		`- return constant_exprt(integer2bv(int_value, width), type);`
	`149`	`+ return constant_exprt(integer2bvrep(int_value, width), type);`
`150`	`150`	`}`
`151`	`151`	`else if(type_id==ID_c_enum)`
`152`	`152`	`{`
`153`	`153`	`const std::size_t width =`
`154`	`154`	`to_c_enum_type(type).subtype().get_size_t(ID_width);`
`155`		`- return constant_exprt(integer2bv(int_value, width), type);`
	`155`	`+ return constant_exprt(integer2bvrep(int_value, width), type);`
`156`	`156`	`}`
`157`	`157`	`else if(type_id==ID_c_bool)`
`158`	`158`	`{`
`159`	`159`	`std::size_t width=to_c_bool_type(type).get_width();`
`160`		`- return constant_exprt(integer2bv(int_value, width), type);`
	`160`	`+ return constant_exprt(integer2bvrep(int_value, width), type);`
`161`	`161`	`}`
`162`	`162`	`else if(type_id==ID_bool)`
`163`	`163`	`{`
`@@ -175,7 +175,7 @@ constant_exprt from_integer(`
`175`	`175`	`else if(type_id==ID_c_bit_field)`
`176`	`176`	`{`
`177`	`177`	`std::size_t width=to_c_bit_field_type(type).get_width();`
`178`		`- return constant_exprt(integer2bv(int_value, width), type);`
	`178`	`+ return constant_exprt(integer2bvrep(int_value, width), type);`
`179`	`179`	`}`
`180`	`180`	`else if(type_id==ID_fixedbv)`
`181`	`181`	`{`
`@@ -280,7 +280,7 @@ void mp_max(mp_integer &a, const mp_integer &b)`
`280`	`280`	`/// \param src: the bitvector representation`
`281`	`281`	`/// \param width: the number of bits in the bitvector`
`282`	`282`	`/// \param bit_index: index (0 is the least significant)`
`283`		`-bool get_bitvector_bit(`
	`283`	`+bool get_bvrep_bit(`
`284`	`284`	`const irep_idt &src,`
`285`	`285`	`std::size_t width,`
`286`	`286`	`std::size_t bit_index)`
`@@ -314,14 +314,14 @@ make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)`
`314`	`314`	`/// \param width: the width of the bit-vector`
`315`	`315`	`/// \param f: the functor`
`316`	`316`	`/// \returns new bitvector representation`
`317`		`-irep_idt bitvector_bitwise_op(`
	`317`	`+irep_idt bvrep_bitwise_op(`
`318`	`318`	`const irep_idt &a,`
`319`	`319`	`const irep_idt &b,`
`320`	`320`	`const std::size_t width,`
`321`	`321`	`const std::function<bool(bool, bool)> f)`
`322`	`322`	`{`
`323`	`323`	`return make_bvrep(width, [&a, &b, &width, f](std::size_t i) {`
`324`		`- return f(get_bitvector_bit(a, width, i), get_bitvector_bit(b, width, i));`
	`324`	`+ return f(get_bvrep_bit(a, width, i), get_bvrep_bit(b, width, i));`
`325`	`325`	`});`
`326`	`326`	`}`
`327`	`327`
`@@ -331,25 +331,24 @@ irep_idt bitvector_bitwise_op(`
`331`	`331`	`/// \param width: the width of the bit-vector`
`332`	`332`	`/// \param f: the functor`
`333`	`333`	`/// \returns new bitvector representation`
`334`		`-irep_idt bitvector_bitwise_op(`
	`334`	`+irep_idt bvrep_bitwise_op(`
`335`	`335`	`const irep_idt &a,`
`336`	`336`	`const std::size_t width,`
`337`	`337`	`const std::function<bool(bool)> f)`
`338`	`338`	`{`
`339`	`339`	`return make_bvrep(width, [&a, &width, f](std::size_t i) {`
`340`		`- return f(get_bitvector_bit(a, width, i));`
	`340`	`+ return f(get_bvrep_bit(a, width, i));`
`341`	`341`	`});`
`342`	`342`	`}`
`343`	`343`
`344`	`344`	`/// convert an integer to bit-vector representation with given width`
`345`		`-irep_idt integer2bv(const mp_integer &src, std::size_t width)`
	`345`	`+irep_idt integer2bvrep(const mp_integer &src, std::size_t width)`
`346`	`346`	`{`
`347`	`347`	`return integer2binary(src, width);`
`348`	`348`	`}`
`349`	`349`
`350`	`350`	`/// convert a bit-vector representation (possibly signed) to integer`
`351`		`-mp_integer`
`352`		`-bv2integer(const irep_idt &src, std::size_t width, bool is_signed)`
	`351`	`+mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)`
`353`	`352`	`{`
`354`	`353`	`PRECONDITION(src.size() == width);`
`355`	`354`	`return binary2integer(id2string(src), is_signed);`
Original file line number	Diff line number	Diff line change
`@@ -84,7 +84,7 @@ mp_integer bv_arithmetict::pack() const`
`84`	`84`
`85`	`85`	`exprt bv_arithmetict::to_expr() const`
`86`	`86`	`{`
`87`		`- return constant_exprt(integer2bv(value, spec.width), spec.to_type());`
	`87`	`+ return constant_exprt(integer2bvrep(value, spec.width), spec.to_type());`
`88`	`88`	`}`
`89`	`89`
`90`	`90`	`bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)`
`@@ -184,5 +184,6 @@ void bv_arithmetict::from_expr(const exprt &expr)`
`184`	`184`	`{`
`185`	`185`	`PRECONDITION(expr.is_constant());`
`186`	`186`	`spec=bv_spect(expr.type());`
`187`		`- value = bv2integer(to_constant_expr(expr).get_value(), spec.width, spec.is_signed);`
	`187`	`+ value = bvrep2integer(`
	`188`	`+ to_constant_expr(expr).get_value(), spec.width, spec.is_signed);`
`188`	`189`	`}`
Original file line number	Diff line number	Diff line change
`@@ -251,7 +251,7 @@ bool exprt::is_one() const`
`251`	`251`	`{`
`252`	`252`	`const auto width = to_bitvector_type(type()).get_width();`
`253`	`253`	`mp_integer int_value =`
`254`		`- bv2integer(id2string(constant_expr.get_value()), width, false);`
	`254`	`+ bvrep2integer(id2string(constant_expr.get_value()), width, false);`
`255`	`255`	`if(int_value==1)`
`256`	`256`	`return true;`
`257`	`257`	`}`
Original file line number	Diff line number	Diff line change
`@@ -26,7 +26,7 @@ fixedbvt::fixedbvt(const constant_exprt &expr)`
`26`	`26`	`void fixedbvt::from_expr(const constant_exprt &expr)`
`27`	`27`	`{`
`28`	`28`	`spec=fixedbv_spect(to_fixedbv_type(expr.type()));`
`29`		`- v = bv2integer(expr.get_value(), spec.width, true);`
	`29`	`+ v = bvrep2integer(expr.get_value(), spec.width, true);`
`30`	`30`	`}`
`31`	`31`
`32`	`32`	`void fixedbvt::from_integer(const mp_integer &i)`
`@@ -46,7 +46,7 @@ constant_exprt fixedbvt::to_expr() const`
`46`	`46`	`type.set_width(spec.width);`
`47`	`47`	`type.set_integer_bits(spec.integer_bits);`
`48`	`48`	`PRECONDITION(spec.width != 0);`
`49`		`- return constant_exprt(integer2bv(v, spec.width), type);`
	`49`	`+ return constant_exprt(integer2bvrep(v, spec.width), type);`
`50`	`50`	`}`
`51`	`51`
`52`	`52`	`void fixedbvt::round(const fixedbv_spect &dest_spec)`
Original file line number	Diff line number	Diff line change
`@@ -696,7 +696,7 @@ void ieee_floatt::divide_and_round(`
`696`	`696`
`697`	`697`	`constant_exprt ieee_floatt::to_expr() const`
`698`	`698`	`{`
`699`		`- return constant_exprt(integer2bv(pack(), spec.width()), spec.to_type());`
	`699`	`+ return constant_exprt(integer2bvrep(pack(), spec.width()), spec.to_type());`
`700`	`700`	`}`
`701`	`701`
`702`	`702`	`ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other)`
`@@ -1062,7 +1062,7 @@ void ieee_floatt::change_spec(const ieee_float_spect &dest_spec)`
`1062`	`1062`	`void ieee_floatt::from_expr(const constant_exprt &expr)`
`1063`	`1063`	`{`
`1064`	`1064`	`spec=ieee_float_spect(to_floatbv_type(expr.type()));`
`1065`		`- unpack(bv2integer(expr.get_value(), spec.width(), false));`
	`1065`	`+ unpack(bvrep2integer(expr.get_value(), spec.width(), false));`
`1066`	`1066`	`}`
`1067`	`1067`
`1068`	`1068`	`mp_integer ieee_floatt::to_integer() const`
Original file line number	Diff line number	Diff line change
`@@ -220,7 +220,7 @@ json_objectt json(`
`220`	`220`	`static std::string binary(const constant_exprt &src)`
`221`	`221`	`{`
`222`	`222`	`const auto width = to_bitvector_type(src.type()).get_width();`
`223`		`- const auto int_val = bv2integer(src.get_value(), width, false);`
	`223`	`+ const auto int_val = bvrep2integer(src.get_value(), width, false);`
`224`	`224`	`return integer2binary(int_val, width);`
`225`	`225`	`}`
`226`	`226`