simplify_exprt::simplify_bitwise is now independent of bitvector representation

Author: Daniel Kroening

src/util/simplify_expr_int.cpp

@@ -717,9 +717,6 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
 
   while(expr.operands().size()>=2)
   {
-    const irep_idt &a_str=expr.op0().get(ID_value);
-    const irep_idt &b_str=expr.op1().get(ID_value);
-
     if(!expr.op0().is_constant())
       break;
 
@@ -732,32 +729,19 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
     if(expr.op1().type()!=expr.type())
       break;
 
-    INVARIANT(
-      a_str.size() == b_str.size(),
-      "bitvectors of the same type have the same size");
+    const auto a_val=bv2integer(id2string(to_constant_expr(expr.op0()).get_value()), false);
+    const auto b_val=bv2integer(id2string(to_constant_expr(expr.op1()).get_value()), false);
 
-    std::string new_value;
-    new_value.resize(width);
+    mp_integer new_value;
 
     if(expr.id()==ID_bitand)
-    {
-      for(std::size_t i=0; i<width; i++)
-        new_value[i]=(a_str[i]=='1' && b_str[i]=='1')?'1':'0';
-    }
+      new_value=bitwise_and(a_val, b_val);
     else if(expr.id()==ID_bitor)
-    {
-      for(std::size_t i=0; i<width; i++)
-        new_value[i]=(a_str[i]=='1' || b_str[i]=='1')?'1':'0';
-    }
+      new_value=bitwise_or(a_val, b_val);
     else if(expr.id()==ID_bitxor)
-    {
-      for(std::size_t i=0; i<width; i++)
-        new_value[i]=((a_str[i]=='1')!=(b_str[i]=='1'))?'1':'0';
-    }
-    else
-      break;
+      new_value=bitwise_xor(a_val, b_val);
 
-    constant_exprt new_op(new_value, expr.type());
+    constant_exprt new_op(integer2bv(new_value, width), expr.type());
 
     // erase first operand
     expr.operands().erase(expr.operands().begin());