Use propt::l_set_to_{true,false}

Avoids the lower-level l_set_to(..., {true,false}) and may then
highlight opportunities for further optimisation.

Author: tautschnig

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(bv_utils.overflow_negate(op_bv), false);
+      prop.l_set_to_false(bv_utils.overflow_negate(op_bv));
 
     if(no_overflow)
       return bv_utils.negate_no_overflow(op_bv);

src/solvers/flattening/bv_pointers.cpp

@@ -739,7 +739,7 @@ void bv_pointerst::do_postponed(
       if(!is_dynamic)
         l2=!l2;
 
-      prop.l_set_to(prop.limplies(l1, l2), true);
+      prop.l_set_to_true(prop.limplies(l1, l2));
     }
   }
   else if(postponed.expr.id()==ID_object_size)
@@ -791,7 +791,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(prop.limplies(l1, l2), true);
+      prop.l_set_to_true(prop.limplies(l1, l2));
     }
   }
   else

src/solvers/flattening/bv_utils.cpp

@@ -539,7 +539,7 @@ bvt bv_utilst::negate(const bvt &bv)
 
 bvt bv_utilst::negate_no_overflow(const bvt &bv)
 {
-  prop.l_set_to(overflow_negate(bv), false);
+  prop.l_set_to_false(overflow_negate(bv));
   return negate(bv);
 }
 
@@ -778,9 +778,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(
-    prop.limplies(cond, !overflow_negate(bv)),
-    true);
+  prop.l_set_to_true(prop.limplies(cond, !overflow_negate(bv)));
 
   return cond_negate(bv, cond);
 }
@@ -800,7 +798,7 @@ bvt bv_utilst::signed_multiplier_no_overflow(
 
   bvt result=unsigned_multiplier_no_overflow(neg0, neg1);
 
-  prop.l_set_to(result[result.size()-1], false);
+  prop.l_set_to_false(result[result.size()-1]);
 
   literalt result_sign=prop.lxor(sign0, sign1);
 

src/solvers/prop/aig_prop.cpp

@@ -591,7 +591,7 @@ void aig_prop_solvert::convert_aig()
 
   // 3. Do constraints
   for(const auto &c_it : aig.constraints)
-    solver.l_set_to(c_it, true);
+    solver.l_set_to_true(c_it);
 
   // HACK!
   aig.nodes.clear();

src/solvers/prop/aig_prop.h

@@ -41,7 +41,7 @@ class aig_prop_baset:public propt
   literalt lselect(literalt a, literalt b, literalt c) override; // a?b:c
   void set_equal(literalt a, literalt b) override;
 
-  void l_set_to(literalt a, bool value) override { assert(false); }
+  void l_set_to(literalt a, bool value) override = 0;
 
   literalt new_variable() override
   {