From 900e793fe9aa33548a9e183607279ac1b5866784 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 11 Jul 2022 13:00:16 +0000 Subject: [PATCH] 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 #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. --- src/solvers/flattening/bv_pointers.cpp | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 0e10621a8f3..6e2be1ded4f 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -958,9 +958,26 @@ void bv_pointerst::do_postponed( PRECONDITION(size_bv.size() == postponed.bv.size()); literalt l1=bv_utils.equal(bv, saved_bv); + if(l1.is_true()) + { + for(std::size_t i = 0; i < postponed.bv.size(); ++i) + prop.set_equal(postponed.bv[i], size_bv[i]); + break; + } + else if(l1.is_false()) + continue; +#define COMPACT_OBJECT_SIZE_EQ +#ifndef COMPACT_OBJECT_SIZE_EQ literalt l2=bv_utils.equal(postponed.bv, size_bv); prop.l_set_to_true(prop.limplies(l1, l2)); +#else + for(std::size_t i = 0; i < postponed.bv.size(); ++i) + { + prop.lcnf({!l1, !postponed.bv[i], size_bv[i]}); + prop.lcnf({!l1, postponed.bv[i], !size_bv[i]}); + } +#endif } } else