Use propt::lcnf when cnf_handled_well is true

src/cprover/bv_pointers_wide.cpp

@@ -629,9 +629,30 @@
           difference, element_size_bv, bv_utilst::representationt::SIGNED);
       }
 
-      prop.l_set_to_true(prop.limplies(
-        prop.land(same_object_lit, prop.land(lhs_in_bounds, rhs_in_bounds)),
-        bv_utils.equal(difference, bv)));
+      if(prop.cnf_handled_well())
+      {
+        for(std::size_t i = 0; i < width; ++i)
+        {
+          prop.lcnf(
+            {!same_object_lit,
+             !lhs_in_bounds,
+             !rhs_in_bounds,
+             !difference[i],
+             bv[i]});
+          prop.lcnf(
+            {!same_object_lit,
+             !lhs_in_bounds,
+             !rhs_in_bounds,
+             difference[i],
+             !bv[i]});
+        }
+      }
+      else
+      {
+        prop.l_set_to_true(prop.limplies(
+          prop.land(same_object_lit, prop.land(lhs_in_bounds, rhs_in_bounds)),
+          bv_utils.equal(difference, bv)));
+      }
     }
 
     return bv;
@@ -892,7 +913,10 @@
       if(!is_dynamic)
         l2 = !l2;
 
-      prop.l_set_to_true(prop.limplies(l1, l2));
+      if(prop.cnf_handled_well())
+        prop.lcnf({!l1, l2});
+      else
+        prop.l_set_to_true(prop.limplies(l1, l2));
     }
   }
   else if(
@@ -933,7 +957,10 @@
       literalt l1 = bv_utils.equal(bv, saved_bv);
       literalt l2 = bv_utils.equal(postponed.bv, size_bv);
 
-      prop.l_set_to_true(prop.limplies(l1, l2));
+      if(prop.cnf_handled_well())
+        prop.lcnf({!l1, l2});
+      else
+        prop.l_set_to_true(prop.limplies(l1, l2));
     }
   }
   else

src/solvers/flattening/boolbv_bv_rel.cpp

@@ -73,10 +73,20 @@
         {
           literalt equal_lit = equality(lhs, rhs);
 
-          if(or_equal)
-            prop.l_set_to_true(prop.limplies(equal_lit, literal));
+          if(prop.cnf_handled_well())
+          {
+            if(or_equal)
+              prop.lcnf(!equal_lit, literal);
+            else
+              prop.lcnf(!equal_lit, !literal);
+          }
           else
-            prop.l_set_to_true(prop.limplies(equal_lit, !literal));
+          {
+            if(or_equal)
+              prop.l_set_to_true(prop.limplies(equal_lit, literal));
+            else
+              prop.l_set_to_true(prop.limplies(equal_lit, !literal));
+          }
         }
       }
 

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -142,9 +142,32 @@
           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)));
+        if(prop.cnf_handled_well())
+        {
+          literalt index_eq =
+            convert(equal_exprt(expr.offset(), from_integer(i, constant_type)));
+
+          for(std::size_t j = 0; j < width; j++)
+          {
+            if(offset + j >= op_bv.size())
+              break;
+
+            prop.lcnf({!index_eq, !bv[j], op_bv[offset + j]});
+            prop.lcnf({!index_eq, bv[j], !op_bv[offset + j]});
+          }
+        }
+        else
+        {
+          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);
+
+          prop.l_set_to_true(prop.limplies(
+            convert(equal_exprt(expr.offset(), from_integer(i, constant_type))),
+            prop.land(equal_bv)));
+        }
       }
     }
     else

src/solvers/flattening/boolbv_case.cpp

@@ -68,8 +68,10 @@
       {
         literalt value_literal=bv_utils.equal(bv, op);
 
-        prop.l_set_to_true(
-          prop.limplies(compare_literal, value_literal));
+        if(prop.cnf_handled_well())
+          prop.lcnf({!compare_literal, value_literal});
+        else
+          prop.l_set_to_true(prop.limplies(compare_literal, value_literal));
       }
 
       what=COMPARE;

src/solvers/flattening/boolbv_cond.cpp

@@ -45,9 +45,19 @@
       {
         const bvt &op = convert_bv(operand, bv.size());
 
-        literalt value_literal=bv_utils.equal(bv, op);
-
-        prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
+        if(prop.cnf_handled_well())
+        {
+          for(std::size_t i = 0; i < bv.size(); ++i)
+          {
+            prop.lcnf({!cond_literal, !bv[i], op[i]});
+            prop.lcnf({!cond_literal, bv[i], !op[i]});
+          }
+        }
+        else
+        {
+          literalt value_literal = bv_utils.equal(bv, op);
+          prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
+        }
       }
 
       condition=!condition;

src/solvers/flattening/boolbv_extractbit.cpp

@@ -65,8 +65,17 @@
       for(std::size_t i = 0; i < src_bv.size(); i++)
       {
         equal_exprt equality(index_casted, from_integer(i, index_type));
-        literalt equal = prop.lequal(literal, src_bv[i]);
-        prop.l_set_to_true(prop.limplies(convert(equality), equal));
+        if(prop.cnf_handled_well())
+        {
+          literalt index_eq = convert(equality);
+          prop.lcnf({!index_eq, !literal, src_bv[i]});
+          prop.lcnf({!index_eq, literal, !src_bv[i]});
+        }
+        else
+        {
+          literalt equal = prop.lequal(literal, src_bv[i]);
+          prop.l_set_to_true(prop.limplies(convert(equality), equal));
+        }
       }
 
       return literal;

src/solvers/flattening/boolbv_index.cpp

@@ -186,9 +186,18 @@
           "past the array's end");
 
         // Cache comparisons and equalities
-        prop.l_set_to_true(convert(implies_exprt(
-          equal_exprt(index, from_integer(i, index.type())),
-          equal_exprt(result, *it++))));
+        if(prop.cnf_handled_well())
+        {
+          prop.lcnf(
+            {!convert(equal_exprt(index, from_integer(i, index.type()))),
+             convert(equal_exprt(result, *it++))});
+        }
+        else
+        {
+          prop.l_set_to_true(convert(implies_exprt(
+            equal_exprt(index, from_integer(i, index.type())),
+            equal_exprt(result, *it++))));
+        }
       }
 
       return bv;
@@ -229,13 +238,33 @@
       {
         mp_integer offset=i*width;
 
-        for(std::size_t j=0; j<width; j++)
-          equal_bv[j] = prop.lequal(
-            bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
+        if(prop.cnf_handled_well())
+        {
+          literalt index_eq =
+            convert(equal_exprt(index, from_integer(i, index.type())));
+
+          for(std::size_t j = 0; j < width; j++)
+          {
+            prop.lcnf(
+              {!index_eq,
+               !bv[j],
+               array_bv[numeric_cast_v<std::size_t>(offset + j)]});
+            prop.lcnf(
+              {!index_eq,
+               bv[j],
+               !array_bv[numeric_cast_v<std::size_t>(offset + j)]});
+          }
+        }
+        else
+        {
+          for(std::size_t j = 0; j < width; j++)
+            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)));
+          prop.l_set_to_true(prop.limplies(
+            convert(equal_exprt(index, from_integer(i, index.type()))),
+            prop.land(equal_bv)));
+        }
       }
     }
     else

src/solvers/flattening/bv_pointers.cpp

@@ -697,8 +697,20 @@
           prop.lor(in_bounds, prop.land(lhs_in_bounds, rhs_in_bounds));
       }
 
-      prop.l_set_to_true(prop.limplies(
-        prop.land(same_object_lit, in_bounds), bv_utils.equal(difference, bv)));
+      if(prop.cnf_handled_well())
+      {
+        for(std::size_t i = 0; i < width; ++i)
+        {
+          prop.lcnf({!same_object_lit, !in_bounds, !difference[i], bv[i]});
+          prop.lcnf({!same_object_lit, !in_bounds, difference[i], !bv[i]});
+        }
+      }
+      else
+      {
+        prop.l_set_to_true(prop.limplies(
+          prop.land(same_object_lit, in_bounds),
+          bv_utils.equal(difference, bv)));
+      }
     }
 
     return bv;
@@ -1071,10 +1083,18 @@
       replace_expr(replacements, is_not_dyn);
 
       PRECONDITION(postponed.bv.size() == 1);
-      prop.l_set_to_true(
-        prop.limplies(convert_bv(is_dyn)[0], postponed.bv.front()));
-      prop.l_set_to_true(
-        prop.limplies(convert_bv(is_not_dyn)[0], !postponed.bv.front()));
+      if(prop.cnf_handled_well())
+      {
+        prop.lcnf({!convert_bv(is_dyn)[0], postponed.bv.front()});
+        prop.lcnf({!convert_bv(is_not_dyn)[0], !postponed.bv.front()});
+      }
+      else
+      {
+        prop.l_set_to_true(
+          prop.limplies(convert_bv(is_dyn)[0], postponed.bv.front()));
+        prop.l_set_to_true(
+          prop.limplies(convert_bv(is_not_dyn)[0], !postponed.bv.front()));
+      }
     }
     else if(
       const auto postponed_object_size =
@@ -1121,7 +1141,10 @@
 #ifndef COMPACT_OBJECT_SIZE_EQ
         literalt l2 = bv_utils.equal(postponed.bv, size_bv);
 
-        prop.l_set_to_true(prop.limplies(l1, l2));
+        if(prop.cnf_handled_well())
+          prop.lcnf({!l1, l2});
+        else
+          prop.l_set_to_true(prop.limplies(l1, l2));
 #else
         for(std::size_t i = 0; i < postponed.bv.size(); ++i)
         {