Skip to content

Commit a26d3fc

Browse files
committed
Optimise propositional encoding of object_size
Avoid creating equalities over the postponed bitvector when the object literals trivially aren't equal, and directly encode bitwise equality when the object literals are trivially equal (and stop searching for a matching object). In all other cases, avoid unnecessary Tseitin variables to encode the postponed bitvector equality. When running on various proofs done for AWS open-source projects, this changes the performance as follows (when comparing to diffblue#7021): with CaDiCaL as back-end, the total solver time for the hardest 46 proofs changes from 26779.7 to 22409.9 seconds (4369.8 seconds speed-up); with Minisat, however, the hardest 49 proofs take 28616.7 instead of 28420.4 seconds (196.3 seconds slow-down). Across these benchmarks, 11.7% of variables and 12.8% of clauses are removed.
1 parent 64034e0 commit a26d3fc

File tree

1 file changed

+17
-0
lines changed

1 file changed

+17
-0
lines changed

src/solvers/flattening/bv_pointers.cpp

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -958,9 +958,26 @@ void bv_pointerst::do_postponed(
958958
PRECONDITION(size_bv.size() == postponed.bv.size());
959959

960960
literalt l1=bv_utils.equal(bv, saved_bv);
961+
if(l1.is_true())
962+
{
963+
for(std::size_t i = 0; i < postponed.bv.size(); ++i)
964+
prop.set_equal(postponed.bv[i], size_bv[i]);
965+
break;
966+
}
967+
else if(l1.is_false())
968+
continue;
969+
#define COMPACT_OBJECT_SIZE_EQ
970+
#ifndef COMPACT_OBJECT_SIZE_EQ
961971
literalt l2=bv_utils.equal(postponed.bv, size_bv);
962972

963973
prop.l_set_to_true(prop.limplies(l1, l2));
974+
#else
975+
for(std::size_t i = 0; i < postponed.bv.size(); ++i)
976+
{
977+
prop.lcnf({!l1, !postponed.bv[i], size_bv[i]});
978+
prop.lcnf({!l1, postponed.bv[i], !size_bv[i]});
979+
}
980+
#endif
964981
}
965982
}
966983
else

0 commit comments

Comments
 (0)