simplify_concatenation is now independent of bitvector representation

Author: Daniel Kroening

src/util/simplify_expr_int.cpp

@@ -883,8 +883,9 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
       exprt &op=*it;
       if(op.is_true() || op.is_false())
       {
-        bool value=op.is_true();
-        op=constant_exprt(value?ID_1:ID_0, unsignedbv_typet(1));
+        const bool value = op.is_true();
+        op = from_integer(value, unsignedbv_typet(1));
+        result = true;
       }
     }
 
@@ -902,10 +903,20 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
          is_bitvector_type(opn.type()))
       {
         // merge!
-        const std::string new_value=
-          opi.get_string(ID_value)+opn.get_string(ID_value);
-        opi.set(ID_value, new_value);
-        opi.type().set(ID_width, new_value.size());
+        const auto &value_i = to_constant_expr(opi).get_value();
+        const auto &value_n = to_constant_expr(opn).get_value();
+        const auto width_i = to_bitvector_type(opi.type()).get_width();
+        const auto width_n = to_bitvector_type(opn.type()).get_width();
+        const auto new_width = width_i + width_n;
+
+        const auto new_value =
+          make_bvrep(new_width, [&value_i, &value_n, width_n](std::size_t x) {
+            return x < width_n ? get_bitvector_bit(value_n, x)
+                               : get_bitvector_bit(value_i, x - width_n);
+          });
+
+        to_constant_expr(opi).set_value(new_value);
+        opi.type().set(ID_width, new_width);
         // erase opn
         expr.operands().erase(expr.operands().begin()+i+1);
         result=true;