Use propt::lcnf instead of propt::l_set_to{true,false}

l_set_to{true,false} will do one unnecessary call to lcnf; several
locations also permitted further optimisation as
l_set_to_true(limplies(a, b)) is lcnf(!a, b).

Author: tautschnig

src/solvers/flattening/arrays.cpp

@@ -253,7 +253,7 @@ void arrayst::add_array_constraint(const lazy_constraintt &lazy, bool refine)
   else
   {
     // add the constraint eagerly
-    prop.l_set_to_true(convert(lazy.lazy));
+    prop.lcnf(bvt(1, convert(lazy.lazy)));
   }
 }
 

src/solvers/flattening/boolbv_bv_rel.cpp

@@ -76,9 +76,9 @@ literalt boolbvt::convert_bv_rel(const exprt &expr)
             literalt equal_lit=equality(op0, op1);
 
             if(or_equal)
-              prop.l_set_to_true(prop.limplies(equal_lit, literal));
+              prop.lcnf(!equal_lit, literal);
             else
-              prop.l_set_to_true(prop.limplies(equal_lit, !literal));
+              prop.lcnf(!equal_lit, !literal);
           }
         }
 

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -129,24 +129,17 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 
       typet constant_type=offset.type(); // type of index operand
 
-      bvt equal_bv;
-      equal_bv.resize(width);
-
       for(std::size_t i=0; i<bytes; i++)
       {
         equality.rhs()=from_integer(i, constant_type);
+        const bvt &eq_bv = convert_bv(equality);
+        CHECK_RETURN(eq_bv.size() == 1);
+        literalt index_not_eq_lit = !eq_bv[0];
 
         std::size_t offset=i*byte_width;
 
-        for(std::size_t j=0; j<width; j++)
-          if(offset+j<op_bv.size())
-            equal_bv[j]=prop.lequal(bv[j], op_bv[offset+j]);
-          else
-            equal_bv[j]=const_literal(true);
-
-        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)));
+        for(std::size_t j=0; j<width && offset+j<op_bv.size(); j++)
+          prop.lcnf(index_not_eq_lit, prop.lequal(bv[j], op_bv[offset+j]));
       }
     }
     else

src/solvers/flattening/boolbv_case.cpp

@@ -73,8 +73,7 @@ bvt boolbvt::convert_case(const exprt &expr)
       {
         literalt value_literal=bv_utils.equal(bv, op);
 
-        prop.l_set_to_true(
-          prop.limplies(compare_literal, value_literal));
+        prop.lcnf(!compare_literal, value_literal);
       }
 
       what=COMPARE;

src/solvers/flattening/boolbv_cond.cpp

@@ -61,7 +61,7 @@ bvt boolbvt::convert_cond(const exprt &expr)
 
         literalt value_literal=bv_utils.equal(bv, op);
 
-        prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
+        prop.lcnf(!cond_literal, value_literal);
       }
 
       condition=!condition;

src/solvers/flattening/boolbv_extractbit.cpp

@@ -73,7 +73,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
         literalt equal=prop.lequal(l, bv0[i]);
         const bvt &eq_bv = convert_bv(equality);
         CHECK_RETURN(eq_bv.size() == 1);
-        prop.l_set_to_true(prop.limplies(eq_bv[0], equal));
+        prop.lcnf(!eq_bv[0], equal);
       }
 
       return l;

src/solvers/flattening/boolbv_index.cpp

@@ -135,7 +135,7 @@ bvt boolbvt::convert_index(const index_exprt &expr)
       simplify(implication, ns);
       const bvt &bv2 = convert_bv(implication);
       CHECK_RETURN(bv2.size() == 1);
-      prop.l_set_to_true(bv2[0]);
+      prop.lcnf(bv2);
 
       return bv;
     }
@@ -189,10 +189,11 @@ bvt boolbvt::convert_index(const index_exprt &expr)
         value_equality.rhs()=*it++;
 
         // Cache comparisons and equalities
-        const bvt &bv2 =
-          convert_bv(implies_exprt(index_equality, value_equality));
-        CHECK_RETURN(bv2.size() == 1);
-        prop.l_set_to_true(bv2[0]);
+        const bvt &bv_index_eq = convert_bv(index_equality);
+        CHECK_RETURN(bv_index_eq.size() == 1);
+        const bvt &bv_value_eq = convert_bv(value_equality);
+        CHECK_RETURN(bv_value_eq.size() == 1);
+        prop.lcnf(!bv_index_eq[0], bv_value_eq[0]);
       }
 
       return bv;
@@ -233,25 +234,26 @@ bvt boolbvt::convert_index(const index_exprt &expr)
       bv_utils.equal_const_register(convert_bv(index));  // Definitely
 #endif
 
-      bvt equal_bv;
-      equal_bv.resize(width);
-
       for(mp_integer i=0; i<array_size; i=i+1)
       {
         index_equality.rhs()=from_integer(i, index_equality.lhs().type());
 
         if(index_equality.rhs().is_nil())
           throw "number conversion failed (1)";
 
-        mp_integer offset=i*width;
-
-        for(std::size_t j=0; j<width; j++)
-          equal_bv[j]=prop.lequal(bv[j],
-                             array_bv[integer2size_t(offset+j)]);
-
         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)));
+        literalt index_not_eq_lit = !index_eq[0];
+
+        mp_integer offset=i*width;
+
+        bvt::const_iterator array_it =
+          array_bv.begin() + integer2size_t(offset);
+        for(const auto &bit : bv)
+        {
+          prop.lcnf(index_not_eq_lit, prop.lequal(bit, *array_it));
+          ++array_it;
+        }
       }
     }
     else

src/solvers/flattening/boolbv_unary_minus.cpp

@@ -104,7 +104,7 @@ bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
           (bvtype==bvtypet::IS_SIGNED || bvtype==bvtypet::IS_UNSIGNED))
   {
     if(no_overflow)
-      prop.l_set_to_false(bv_utils.overflow_negate(op_bv));
+      prop.lcnf(bvt(1, !bv_utils.overflow_negate(op_bv)));
 
     if(no_overflow)
       return bv_utils.negate_no_overflow(op_bv);

src/solvers/flattening/bv_pointers.cpp

@@ -741,7 +741,7 @@ void bv_pointerst::do_postponed(
       if(!is_dynamic)
         l2=!l2;
 
-      prop.l_set_to_true(prop.limplies(l1, l2));
+      prop.lcnf(!l1, l2);
     }
   }
   else if(postponed.expr.id()==ID_object_size)
@@ -793,7 +793,7 @@ void bv_pointerst::do_postponed(
       bvt size_bv=bv_utils.build_constant(object_size, postponed.bv.size());
       literalt l2=bv_utils.equal(postponed.bv, size_bv);
 
-      prop.l_set_to_true(prop.limplies(l1, l2));
+      prop.lcnf(!l1, l2);
     }
   }
   else

src/solvers/flattening/bv_utils.cpp

@@ -434,8 +434,7 @@ void bv_utilst::adder_no_overflow(
     adder(sum, tmp_op, const_literal(subtract), carry);
 
     // result of addition in sum
-    prop.l_set_to_false(
-      prop.land(sign_the_same, prop.lxor(sum[sum.size()-1], old_sign)));
+    prop.lcnf(!sign_the_same, prop.lequal(sum[sum.size()-1], old_sign));
   }
   else if(rep==representationt::UNSIGNED)
   {
@@ -453,7 +452,7 @@ void bv_utilst::adder_no_overflow(bvt &sum, const bvt &op)
 
   adder(sum, op, carry_out, carry_out);
 
-  prop.l_set_to_false(carry_out); // enforce no overflow
+  prop.lcnf(bvt(1, !carry_out)); // enforce no overflow
 }
 
 bvt bv_utilst::shift(const bvt &op, const shiftt s, const bvt &dist)
@@ -539,7 +538,7 @@ bvt bv_utilst::negate(const bvt &bv)
 
 bvt bv_utilst::negate_no_overflow(const bvt &bv)
 {
-  prop.l_set_to_false(overflow_negate(bv));
+  prop.lcnf(bvt(1, !overflow_negate(bv)));
   return negate(bv);
 }
 
@@ -733,7 +732,7 @@ bvt bv_utilst::unsigned_multiplier_no_overflow(
       adder_no_overflow(product, tmpop);
 
       for(std::size_t idx=op1.size()-sum; idx<op1.size(); idx++)
-        prop.l_set_to_false(prop.land(op1[idx], op0[sum]));
+        prop.lcnf(!op1[idx], !op0[sum]);
     }
 
   return product;
@@ -778,7 +777,7 @@ bvt bv_utilst::absolute_value(const bvt &bv)
 
 bvt bv_utilst::cond_negate_no_overflow(const bvt &bv, literalt cond)
 {
-  prop.l_set_to_true(prop.limplies(cond, !overflow_negate(bv)));
+  prop.lcnf(!cond, !overflow_negate(bv));
 
   return cond_negate(bv, cond);
 }
@@ -798,7 +797,7 @@ bvt bv_utilst::signed_multiplier_no_overflow(
 
   bvt result=unsigned_multiplier_no_overflow(neg0, neg1);
 
-  prop.l_set_to_false(result[result.size()-1]);
+  prop.lcnf(bvt(1, !result[result.size()-1]));
 
   literalt result_sign=prop.lxor(sign0, sign1);
 
@@ -957,19 +956,15 @@ void bv_utilst::unsigned_divider(
 
   literalt is_equal=equal(sum, op0);
 
-  prop.l_set_to_true(prop.limplies(is_not_zero, is_equal));
+  prop.lcnf(!is_not_zero, is_equal);
 
   // op1!=0 => rem < op1
 
-  prop.l_set_to_true(
-    prop.limplies(
-      is_not_zero, lt_or_le(false, rem, op1, representationt::UNSIGNED)));
+  prop.lcnf(!is_not_zero, lt_or_le(false, rem, op1, representationt::UNSIGNED));
 
   // op1!=0 => res <= op0
 
-  prop.l_set_to_true(
-    prop.limplies(
-      is_not_zero, lt_or_le(true, res, op0, representationt::UNSIGNED)));
+  prop.lcnf(!is_not_zero, lt_or_le(true, res, op0, representationt::UNSIGNED));
 }
 
 
@@ -1174,7 +1169,7 @@ literalt bv_utilst::lt_or_le(
 
       // When comparing signs we are comparing the top bit
 #ifdef INCLUDE_REDUNDANT_CLAUSES
-      prop.l_set_to_true(compareBelow[start + 1])
+      prop.lcnf(compareBelow[start + 1])
 #endif
 
       // Four cases...
@@ -1192,7 +1187,7 @@ literalt bv_utilst::lt_or_le(
     {
       // Unsigned is much easier
       start = compareBelow.size() - 1;
-      prop.l_set_to_true(compareBelow[start]);
+      prop.lcnf(compareBelow[start]);
     }
 
     // Determine the output