Consistently use convert_bv instead of convert

This will place all expressions in boolbvt's cache instead of sometimes
using prop_convt's cache.

Author: tautschnig

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -144,8 +144,9 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
           else
             equal_bv[j]=const_literal(true);
 
-        prop.l_set_to_true(
-          prop.limplies(convert(equality), prop.land(equal_bv)));
+        const bvt &eq_bv = convert_bv(equality);
+        CHECK_RETURN(eq_bv.size() == 1);
+        prop.l_set_to_true(prop.limplies(eq_bv[0], prop.land(equal_bv)));
       }
     }
     else
@@ -159,7 +160,9 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
       {
         equality.rhs()=from_integer(i, constant_type);
 
-        literalt e=convert(equality);
+        const bvt &eq_bv = convert_bv(equality);
+        CHECK_RETURN(eq_bv.size() == 1);
+        literalt e = eq_bv[0];
 
         std::size_t offset=i*byte_width;
 

src/solvers/flattening/boolbv_byte_update.cpp

@@ -91,7 +91,10 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
     equal_exprt equality;
     equality.lhs()=offset_expr;
     equality.rhs()=from_integer(offset/byte_width, offset_expr.type());
-    literalt equal=convert(equality);
+
+    const bvt &eq_bv = convert_bv(equality);
+    CHECK_RETURN(eq_bv.size() == 1);
+    literalt equal = eq_bv[0];
 
     endianness_mapt map_op(op.type(), little_endian, ns);
     endianness_mapt map_value(value.type(), little_endian, ns);

src/solvers/flattening/boolbv_cond.cpp

@@ -42,7 +42,9 @@ bvt boolbvt::convert_cond(const exprt &expr)
     {
       if(condition)
       {
-        cond_literal=convert(*it);
+        const bvt &cond_bv = convert_bv(*it);
+        CHECK_RETURN(cond_bv.size() == 1);
+        cond_literal = cond_bv[0];
         cond_literal=prop.land(!previous_cond, cond_literal);
 
         previous_cond=prop.lor(previous_cond, cond_literal);
@@ -74,7 +76,9 @@ bvt boolbvt::convert_cond(const exprt &expr)
       const exprt &cond=expr.operands()[i-2];
       const exprt &value=expr.operands()[i-1];
 
-      literalt cond_literal=convert(cond);
+      const bvt &cond_bv = convert_bv(cond);
+      CHECK_RETURN(cond_bv.size() == 1);
+      literalt cond_literal = cond_bv[0];
 
       const bvt &op=convert_bv(value);
 

src/solvers/flattening/boolbv_extractbit.cpp

@@ -71,7 +71,9 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
       {
         equality.rhs()=from_integer(i, index_type);
         literalt equal=prop.lequal(l, bv0[i]);
-        prop.l_set_to_true(prop.limplies(convert(equality), equal));
+        const bvt &eq_bv = convert_bv(equality);
+        CHECK_RETURN(eq_bv.size() == 1);
+        prop.l_set_to_true(prop.limplies(eq_bv[0], equal));
       }
 
       return l;
@@ -83,7 +85,9 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
       for(std::size_t i=0; i<bv0.size(); i++)
       {
         equality.rhs()=from_integer(i, index_type);
-        l=prop.lselect(convert(equality), bv0[i], l);
+        const bvt &eq_bv = convert_bv(equality);
+        CHECK_RETURN(eq_bv.size() == 1);
+        l=prop.lselect(eq_bv[0], bv0[i], l);
       }
 
       return l;

src/solvers/flattening/boolbv_if.cpp

@@ -16,7 +16,9 @@ bvt boolbvt::convert_if(const if_exprt &expr)
   if(width==0)
     return bvt(); // An empty bit-vector if.
 
-  literalt cond=convert(expr.cond());
+  const bvt &cond_bv = convert_bv(expr.cond());
+  CHECK_RETURN(cond_bv.size() == 1);
+  literalt cond = cond_bv[0];
 
   const bvt &op1_bv=convert_bv(expr.true_case());
   const bvt &op2_bv=convert_bv(expr.false_case());

src/solvers/flattening/boolbv_index.cpp

@@ -132,7 +132,10 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
       // Simplify may remove the lower bound if the type
       // is correct.
-      prop.l_set_to_true(convert(simplify_expr(implication, ns)));
+      simplify(implication, ns);
+      const bvt &bv2 = convert_bv(implication);
+      CHECK_RETURN(bv2.size() == 1);
+      prop.l_set_to_true(bv2[0]);
 
       return bv;
     }
@@ -186,8 +189,10 @@ bvt boolbvt::convert_index(const index_exprt &expr)
         value_equality.rhs()=*it++;
 
         // Cache comparisons and equalities
-        prop.l_set_to_true(convert(implies_exprt(index_equality,
-                                                 value_equality)));
+        const bvt &bv2 =
+          convert_bv(implies_exprt(index_equality, value_equality));
+        CHECK_RETURN(bv2.size() == 1);
+        prop.l_set_to_true(bv2[0]);
       }
 
       return bv;
@@ -244,8 +249,9 @@ bvt boolbvt::convert_index(const index_exprt &expr)
           equal_bv[j]=prop.lequal(bv[j],
                              array_bv[integer2size_t(offset+j)]);
 
-        prop.l_set_to_true(
-          prop.limplies(convert(index_equality), prop.land(equal_bv)));
+        const bvt &index_eq = convert_bv(index_equality);
+        CHECK_RETURN(index_eq.size() == 1);
+        prop.l_set_to_true(prop.limplies(index_eq[0], prop.land(equal_bv)));
       }
     }
     else
@@ -267,7 +273,9 @@ bvt boolbvt::convert_index(const index_exprt &expr)
       {
         equality.op1()=from_integer(i, constant_type);
 
-        literalt e=convert(equality);
+        const bvt &eq_bv = convert_bv(equality);
+        CHECK_RETURN(eq_bv.size() == 1);
+        literalt e = eq_bv[0];
 
         mp_integer offset=i*width;
 

src/solvers/flattening/boolbv_with.cpp

@@ -160,7 +160,9 @@ void boolbvt::convert_with_array(
   {
     exprt counter=from_integer(i, counter_type);
 
-    literalt eq_lit=convert(equal_exprt(op1, counter));
+    const bvt &eq_bv = convert_bv(equal_exprt(op1, counter));
+    CHECK_RETURN(eq_bv.size() == 1);
+    literalt eq_lit = eq_bv[0];
 
     std::size_t offset=integer2unsigned(i*op2_bv.size());
 
@@ -177,7 +179,9 @@ void boolbvt::convert_with_bv(
   const bvt &prev_bv,
   bvt &next_bv)
 {
-  literalt l=convert(op2);
+  const bvt &bv = convert_bv(op2);
+  CHECK_RETURN(bv.size() == 1);
+  literalt l = bv[0];
 
   mp_integer op1_value;
   if(!to_integer(op1, op1_value))
@@ -196,7 +200,9 @@ void boolbvt::convert_with_bv(
   {
     exprt counter=from_integer(i, counter_type);
 
-    literalt eq_lit=convert(equal_exprt(op1, counter));
+    const bvt &eq_bv = convert_bv(equal_exprt(op1, counter));
+    CHECK_RETURN(eq_bv.size() == 1);
+    literalt eq_lit = eq_bv[0];
 
     next_bv[i]=prop.lselect(eq_lit, l, prev_bv[i]);
   }

src/solvers/flattening/bv_pointers.cpp

@@ -198,7 +198,9 @@ bool bv_pointerst::convert_address_of_rec(
   {
     const if_exprt &ifex=to_if_expr(expr);
 
-    literalt cond=convert(ifex.cond());
+    const bvt &cond_bv = convert_bv(ifex.cond());
+    CHECK_RETURN(cond_bv.size() == 1);
+    literalt cond = cond_bv[0];
 
     bvt bv1, bv2;