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

@@ -161,9 +161,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(equal_exprt(expr.offset(), from_integer(i, constant_type))),
-          prop.land(equal_bv)));
+        const bvt &eq_bv = convert_bv(equal_exprt(expr.offset(), from_integer(i, constant_type)));
+        CHECK_RETURN(eq_bv.size() == 1);
+        prop.l_set_to_true(prop.limplies(eq_bv[0], prop.land(equal_bv)));
       }
     }
     else
@@ -173,8 +173,9 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 
       for(std::size_t i=0; i<bytes; i++)
       {
-        literalt e =
-          convert(equal_exprt(expr.offset(), from_integer(i, constant_type)));
+        const bvt &eq_bv = convert_bv(equal_exprt(expr.offset(), from_integer(i, constant_type)));
+        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

@@ -87,7 +87,9 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
     // index condition
     equal_exprt equality(
       offset_expr, 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];
 
     bv_endianness_mapt map_op(op.type(), little_endian, ns, boolbv_width);
     bv_endianness_mapt map_value(value.type(), little_endian, ns, boolbv_width);

src/solvers/flattening/boolbv_cond.cpp

@@ -41,7 +41,9 @@ bvt boolbvt::convert_cond(const cond_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);
@@ -70,7 +72,9 @@ bvt boolbvt::convert_cond(const cond_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, bv.size());
 

src/solvers/flattening/boolbv_extractbit.cpp

@@ -66,7 +66,9 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
       {
         equality.rhs()=from_integer(i, index_type);
         literalt equal = prop.lequal(literal, src_bv[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 literal;
@@ -78,7 +80,9 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
       for(std::size_t i = 0; i < src_bv.size(); i++)
       {
         equality.rhs()=from_integer(i, index_type);
-        literal = prop.lselect(convert(equality), src_bv[i], literal);
+        const bvt &eq_bv = convert_bv(equality);
+        CHECK_RETURN(eq_bv.size() == 1);
+        literal = prop.lselect(eq_bv[0], src_bv[i], literal);
       }
 
       return literal;

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 &true_case_bv = convert_bv(expr.true_case(), width);
   const bvt &false_case_bv = convert_bv(expr.false_case(), width);

src/solvers/flattening/boolbv_index.cpp

@@ -116,7 +116,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;
     }
@@ -159,9 +162,12 @@ bvt boolbvt::convert_index(const index_exprt &expr)
           "past the array's end");
 
         // Cache comparisons and equalities
-        prop.l_set_to_true(convert(implies_exprt(
+        const bvt &bv2 =
+          convert_bv(implies_exprt(
           equal_exprt(index, from_integer(i, index.type())),
-          equal_exprt(result, *it++))));
+          equal_exprt(result, *it++)));
+        CHECK_RETURN(bv2.size() == 1);
+        prop.l_set_to_true(bv2[0]);
       }
 
       return bv;
@@ -208,9 +214,9 @@ bvt boolbvt::convert_index(const index_exprt &expr)
           equal_bv[j] = prop.lequal(
             bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
 
-        prop.l_set_to_true(prop.limplies(
-          convert(equal_exprt(index, from_integer(i, index.type()))),
-          prop.land(equal_bv)));
+        const bvt &index_eq = convert_bv(equal_exprt(index, from_integer(i, index_type())));
+        CHECK_RETURN(index_eq.size() == 1);
+        prop.l_set_to_true(prop.limplies(index_eq[0], prop.land(equal_bv)));
       }
     }
     else
@@ -229,8 +235,9 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
       for(mp_integer i=0; i<array_size; i=i+1)
       {
-        literalt e =
-          convert(equal_exprt(index, from_integer(i, constant_type)));
+        const bvt &eq_bv = convert_bv(equal_exprt(index, from_integer(i, constant_type)));
+        CHECK_RETURN(eq_bv.size() == 1);
+        literalt e = eq_bv[0];
 
         mp_integer offset=i*width;
 

src/solvers/flattening/boolbv_with.cpp

@@ -167,7 +167,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];
 
     const std::size_t offset = numeric_cast_v<std::size_t>(i * op2_bv.size());
 
@@ -183,7 +185,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];
 
   if(const auto op1_value = numeric_cast<mp_integer>(op1))
   {
@@ -201,7 +205,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

@@ -197,7 +197,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;