From fca4f1819433762ecaa5d6b4fcaebfc111582030 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 7 Dec 2022 12:47:30 +0100 Subject: [PATCH 01/44] p --- src/math/polysat/ule_constraint.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index 17ab00a7f..57cf4b0e6 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -202,12 +202,12 @@ namespace polysat { s.m_viable.intersect(p, q, sc); if (first && !is_positive) { - if (!p.is_val()) + if (!p.is_val()) // -1 > q s.add_clause(~sc, s.ult(q, -1), false); if (!q.is_val()) // p > 0 - s.add_clause(~sc, s.ult(0, q), false); + s.add_clause(~sc, s.ult(0, p), false); } } From 85715eb164e140fe200bbe9406880faced8529fb Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 7 Dec 2022 16:08:24 +0100 Subject: [PATCH 02/44] Update use of insert_eval and lemma scores to support propagation --- src/math/polysat/clause_builder.cpp | 9 +++--- src/math/polysat/clause_builder.h | 16 ++++++--- src/math/polysat/saturation.cpp | 50 ++++++++++++++++------------- src/math/polysat/solver.cpp | 40 ++++++++++++----------- src/math/polysat/solver.h | 18 +++++------ src/math/polysat/viable.cpp | 2 +- 6 files changed, 76 insertions(+), 59 deletions(-) diff --git a/src/math/polysat/clause_builder.cpp b/src/math/polysat/clause_builder.cpp index 6ce287189..511e341b4 100644 --- a/src/math/polysat/clause_builder.cpp +++ b/src/math/polysat/clause_builder.cpp @@ -75,13 +75,14 @@ namespace polysat { m_literals.push_back(c.blit()); } - void clause_builder::insert_eval(sat::literal lit) { - insert_eval(m_solver->lit2cnstr(lit)); + void clause_builder::insert_eval(sat::literal lit, bool status) { + insert_eval(m_solver->lit2cnstr(lit), status); } - void clause_builder::insert_eval(signed_constraint c) { + void clause_builder::insert_eval(signed_constraint c, bool status) { if (c.bvalue(*m_solver) == l_undef) { - m_solver->assign_eval(~c.blit()); + sat::literal lit = c.blit(); + m_solver->assign_eval(status ? lit : ~lit); } insert(c); } diff --git a/src/math/polysat/clause_builder.h b/src/math/polysat/clause_builder.h index b9eba6fca..4c6294138 100644 --- a/src/math/polysat/clause_builder.h +++ b/src/math/polysat/clause_builder.h @@ -51,11 +51,17 @@ namespace polysat { void insert(signed_constraint c); void insert(inequality const& i) { insert(i.as_signed_constraint()); } - /// Inserting constraints into the clause. - /// If they are not yet on the search stack, add them as evaluated to false. - /// \pre Constraint must be false in the current assignment. - void insert_eval(sat::literal lit); - void insert_eval(signed_constraint c); + /// Insert constraints into the clause. + /// If they are not yet on the search stack, add them as evaluated to the given status. + /// \pre Constraint must evaluate to true or false according to the given status in the current assignment. + void insert_eval(sat::literal lit, bool status); + void insert_eval(signed_constraint c, bool status); + + /// Insert constraints into the clause. + /// If they are not yet on the search stack, add them as evaluated to \b false. + /// \pre Constraint must be \b false in the current assignment. + void insert_eval(sat::literal lit) { insert_eval(lit, false); } + void insert_eval(signed_constraint c) { insert_eval(c, false); } void insert_eval(inequality const& i) { insert_eval(i.as_signed_constraint()); } using const_iterator = decltype(m_literals)::const_iterator; diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 2fd4caf86..78340d987 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -96,8 +96,7 @@ namespace polysat { SASSERT(all_of(m_lemma, [this](sat::literal lit) { return is_forced_false(s.lit2cnstr(lit)); })); - // NSB review question: insert_eval: Is this right? - m_lemma.insert_eval(c); + m_lemma.insert(c); core.add_lemma(m_rule, m_lemma.build()); return true; } @@ -514,20 +513,20 @@ namespace polysat { auto prop1 = [&](signed_constraint c) { m_lemma.reset(); - m_lemma.insert(~s.eq(b)); - m_lemma.insert(~s.eq(y)); - m_lemma.insert(x_eq_0); - m_lemma.insert(a_eq_0); + m_lemma.insert_eval(~s.eq(b)); + m_lemma.insert_eval(~s.eq(y)); + m_lemma.insert_eval(x_eq_0); + m_lemma.insert_eval(a_eq_0); return propagate(core, axb_l_y, c); }; auto prop2 = [&](signed_constraint ante, signed_constraint c) { m_lemma.reset(); - m_lemma.insert(~s.eq(b)); - m_lemma.insert(~s.eq(y)); - m_lemma.insert(x_eq_0); - m_lemma.insert(a_eq_0); - m_lemma.insert(~ante); + m_lemma.insert_eval(~s.eq(b)); + m_lemma.insert_eval(~s.eq(y)); + m_lemma.insert_eval(x_eq_0); + m_lemma.insert_eval(a_eq_0); + m_lemma.insert_eval(~ante); return propagate(core, axb_l_y, c); }; @@ -648,27 +647,34 @@ namespace polysat { signed_constraint b_is_odd = s.odd(b); signed_constraint a_is_odd = s.odd(a); signed_constraint x_is_odd = s.odd(X); +#if 0 + LOG_H1("try_parity: " << X << " on: " << lit_pp(s, axb_l_y.as_signed_constraint())); + LOG("y: " << y << " a: " << a << " b: " << b); + LOG("b_is_odd: " << lit_pp(s, b_is_odd)); + LOG("a_is_odd: " << lit_pp(s, a_is_odd)); + LOG("x_is_odd: " << lit_pp(s, x_is_odd)); +#endif if (!b_is_odd.is_currently_true(s)) { if (!a_is_odd.is_currently_true(s)) return false; if (!x_is_odd.is_currently_true(s)) return false; m_lemma.reset(); - m_lemma.insert(~s.eq(y)); - m_lemma.insert(~a_is_odd); - m_lemma.insert(~x_is_odd); + m_lemma.insert_eval(~s.eq(y)); + m_lemma.insert_eval(~a_is_odd); + m_lemma.insert_eval(~x_is_odd); if (propagate(core, axb_l_y, b_is_odd)) return true; return false; } m_lemma.reset(); - m_lemma.insert(~s.eq(y)); - m_lemma.insert(~b_is_odd); + m_lemma.insert_eval(~s.eq(y)); + m_lemma.insert_eval(~b_is_odd); if (propagate(core, axb_l_y, a_is_odd)) return true; m_lemma.reset(); - m_lemma.insert(~s.eq(y)); - m_lemma.insert(~b_is_odd); + m_lemma.insert_eval(~s.eq(y)); + m_lemma.insert_eval(~b_is_odd); if (propagate(core, axb_l_y, x_is_odd)) return true; return false; @@ -693,14 +699,14 @@ namespace polysat { if (!is_forced_diseq(a, 0, a_eq_0)) return false; m_lemma.reset(); - m_lemma.insert(s.eq(y)); - m_lemma.insert(~s.eq(b)); - m_lemma.insert(a_eq_0); + m_lemma.insert_eval(s.eq(y)); + m_lemma.insert_eval(~s.eq(b)); + m_lemma.insert_eval(a_eq_0); if (propagate(core, axb_l_y, s.even(X))) return true; if (!is_forced_diseq(X, 0, x_eq_0)) return false; - m_lemma.insert(x_eq_0); + m_lemma.insert_eval(x_eq_0); if (propagate(core, axb_l_y, s.even(a))) return true; return false; diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index bba0ab9b0..ca76f1c1f 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -824,17 +824,12 @@ namespace polysat { backjump_and_learn(max_jump_level); } - // - // NSB review: this code assumes that these lemmas are false. - // It does not allow saturation to add unit propagation into freshly created literals. - // std::optional solver::compute_lemma_score(clause const& lemma) { - unsigned max_level = 0; // highest level in lemma - unsigned lits_at_max_level = 0; // how many literals at the highest level in lemma - unsigned snd_level = 0; // second-highest level in lemma - bool is_propagation = false; + unsigned max_level = 0; // highest level in lemma + unsigned lits_at_max_level = 0; // how many literals at the highest level in lemma + unsigned snd_level = 0; // second-highest level in lemma + bool is_propagation = false; // whether there is an unassigned literal (at most one) for (sat::literal lit : lemma) { - SASSERT(m_bvars.is_assigned(lit)); // any new constraints should have been assign_eval'd if (m_bvars.is_true(lit)) // may happen if we only use the clause to justify a new constraint; it is not a real lemma return std::nullopt; if (!m_bvars.is_assigned(lit)) { @@ -861,15 +856,19 @@ namespace polysat { // Do the standard backjumping known from SAT solving (back to second-highest level in the lemma, propagate it there). // - Semantic split clause: multiple literals on the highest level in the lemma. // Backtrack to "highest level - 1" and split on the lemma there. - // For now, we follow the same convention for computing the jump levels. + // For now, we follow the same convention for computing the jump levels, + // but we support an additional type of clause: + // - Propagation clause: a single literal is unassigned and should be propagated after backjumping. + // backjump to max_level so we can propagate unsigned jump_level; + unsigned branching_factor = lits_at_max_level; if (is_propagation) - jump_level = max_level; - if (lits_at_max_level <= 1) + jump_level = max_level, branching_factor = 1; + else if (lits_at_max_level <= 1) jump_level = snd_level; else jump_level = (max_level == 0) ? 0 : (max_level - 1); - return {{jump_level, lits_at_max_level}}; + return {{jump_level, branching_factor}}; } void solver::backjump_and_learn(unsigned max_jump_level) { @@ -886,6 +885,10 @@ namespace polysat { auto appraise_lemma = [&](clause* lemma) { m_simplify_clause.apply(*lemma); auto score = compute_lemma_score(*lemma); + if (score) + LOG(" score: " << *score); + else + LOG(" score: "); if (score && *score < best_score) { best_score = *score; best_lemma = lemma; @@ -905,6 +908,9 @@ namespace polysat { unsigned const jump_level = std::max(best_score.jump_level(), base_level()); SASSERT(jump_level <= max_jump_level); + LOG("best_score: " << best_score); + LOG("best_lemma: " << *best_lemma); + m_conflict.reset(); backjump(jump_level); @@ -940,10 +946,7 @@ namespace polysat { SASSERT(!is_conflict()); } - LOG("best_score: " << best_score); - LOG("best_lemma: " << *best_lemma); - - if (best_score.literals_at_max_level() > 1) { + if (best_score.branching_factor() > 1) { // NOTE: at this point it is possible that the best_lemma is non-asserting. // We need to double-check, because the backjump level may not be exact (see comment on checking is_conflict above). bool const is_asserting = all_of(*best_lemma, [this](sat::literal lit) { return m_bvars.is_assigned(lit); }); @@ -1269,7 +1272,8 @@ namespace polysat { out << lpad(4, lit) << ": " << rpad(30, c); if (!c) return out; - out << " [ " << s.m_bvars.value(lit); + out << " [ b:" << rpad(7, s.m_bvars.value(lit)); + out << " p:" << rpad(7, c.eval(s)); if (s.m_bvars.is_assigned(lit)) { out << ' '; if (s.m_bvars.is_assumption(lit)) diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 7676ccec6..1af414a14 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -52,20 +52,19 @@ namespace polysat { * * Comparison criterion: * - Lowest jump level has priority, because otherwise, some of the accumulated lemmas may still be false after backjumping. - * - To break ties on jump level, choose clause with the fewest literals at its highest decision level; - * to limit case splits. + * - To break ties on jump level, choose clause with the lowest branching factor. */ class lemma_score { unsigned m_jump_level; - unsigned m_literals_at_max_level; + unsigned m_branching_factor; // how many literals will be unassigned after backjumping to jump_level public: - lemma_score(unsigned jump_level, unsigned at_max_level) - : m_jump_level(jump_level), m_literals_at_max_level(at_max_level) + lemma_score(unsigned jump_level, unsigned bf) + : m_jump_level(jump_level), m_branching_factor(bf) { } unsigned jump_level() const { return m_jump_level; } - unsigned literals_at_max_level() const { return m_literals_at_max_level; } + unsigned branching_factor() const { return m_branching_factor; } static lemma_score max() { return {UINT_MAX, UINT_MAX}; @@ -73,20 +72,20 @@ namespace polysat { bool operator==(lemma_score const& other) const { return m_jump_level == other.m_jump_level - && m_literals_at_max_level == other.m_literals_at_max_level; + && m_branching_factor == other.m_branching_factor; } bool operator!=(lemma_score const& other) const { return !operator==(other); } bool operator<(lemma_score const& other) const { return m_jump_level < other.m_jump_level - || (m_jump_level == other.m_jump_level && m_literals_at_max_level < other.m_literals_at_max_level); + || (m_jump_level == other.m_jump_level && m_branching_factor < other.m_branching_factor); } bool operator>(lemma_score const& other) const { return other.operator<(*this); } bool operator<=(lemma_score const& other) const { return operator==(other) || operator<(other); } bool operator>=(lemma_score const& other) const { return operator==(other) || operator>(other); } std::ostream& display(std::ostream& out) const { - return out << "jump_level=" << m_jump_level << " at_max_level=" << m_literals_at_max_level; + return out << "jump_level=" << m_jump_level << " branching_factor=" << m_branching_factor; } }; @@ -413,6 +412,7 @@ namespace polysat { signed_constraint eq(pdd const& p, unsigned q) { return eq(p - q); } signed_constraint odd(pdd const& p) { return ~even(p); } signed_constraint even(pdd const& p) { return parity(p, 1); } + /** parity(p) >= k (<=> p * 2^(K-k) == 0) */ signed_constraint parity(pdd const& p, unsigned k) { return eq(p*rational::power_of_two(p.manager().power_of_2() - k)); } signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); } signed_constraint diseq(pdd const& p, unsigned q) { return diseq(p - q); } diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index fbb9dd2c6..92d63173e 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -725,7 +725,7 @@ namespace polysat { } while (e != first); - SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false; })); + SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false || s.lit2cnstr(lit).is_currently_false(s); })); core.add_lemma("viable", lemma.build()); core.logger().log(inf_fi(*this, v)); return true; From 05a1f4d096be4eef34371ba6e43edcb36d9e357d Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 7 Dec 2022 16:09:10 +0100 Subject: [PATCH 03/44] Skip try_parity for x==y and y==x --- src/math/polysat/saturation.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 78340d987..ee7cc1973 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -644,6 +644,10 @@ namespace polysat { pdd X = s.var(x); if (!is_AxB_eq_0(x, axb_l_y, a, b, y)) return false; + if (a.is_max() && b.is_var()) // x == y, we propagate values in each direction and don't need a lemma + return false; + if (a.is_one() && (-b).is_var()) // y == x + return false; signed_constraint b_is_odd = s.odd(b); signed_constraint a_is_odd = s.odd(a); signed_constraint x_is_odd = s.odd(X); From 71acba20e2fff024c7cb89d8da6081f59e3a9be1 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 7 Dec 2022 16:13:24 +0100 Subject: [PATCH 04/44] Assertion was too strong (via test_ineq1) --- src/math/polysat/conflict.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 950729210..c1cf8b4d4 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -322,7 +322,11 @@ namespace polysat { lemma->set_redundant(true); for (sat::literal lit : *lemma) { LOG(lit_pp(s, lit)); - SASSERT(s.m_bvars.value(lit) != l_true); + // NOTE: it can happen that the literal's bvalue is l_true at this point. + // E.g., lit has been assigned to true on the search stack but not yet propagated. + // A propagation before lit will cause a conflict, and by chance the viable conflict will contain lit. + // (in that case, the evaluation of lit in the current assignment must be false, and it would have caused a conflict by itself when propagated.) + SASSERT(s.m_bvars.value(lit) != l_true || !s.lit2cnstr(lit).is_currently_true(s)); } m_lemmas.push_back(std::move(lemma)); // TODO: pass to inference_logger (with name) From a4adb63662f4ba3e1c5ac554f1c21467c043deec Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 7 Dec 2022 16:15:28 +0100 Subject: [PATCH 05/44] unit test updates --- src/test/polysat.cpp | 65 ++++++++++++++++++++------------------------ 1 file changed, 30 insertions(+), 35 deletions(-) diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 33de542fe..85f5c8c62 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -241,10 +241,9 @@ namespace polysat { public: scoped_solver(std::string name): solver(lim), m_name(name) { - if (collect_test_records) { - std::cout << m_name << ":"; - std::cout.flush(); - } else { + if (collect_test_records) + std::cout << m_name << std::flush; + else { std::cout << std::string(78, '#') << "\n\n"; std::cout << "START: " << m_name << "\n"; } @@ -266,10 +265,8 @@ namespace polysat { } void check() { - if (collect_test_records) { - std::cout << " ..."; - std::cout.flush(); - } + if (collect_test_records) + std::cout << " ..." << std::flush; auto* rec = test_records.active_or_new_record(); m_last_finished = nullptr; SASSERT(rec->m_answer == l_undef); @@ -287,7 +284,7 @@ namespace polysat { rec->m_finished = true; m_last_finished = rec; if (collect_test_records) - std::cout << " " << m_last_result; + std::cout << " " << m_last_result << std::flush; else std::cout << "DONE: " << m_name << ": " << m_last_result << "\n"; statistics st; @@ -1258,7 +1255,6 @@ namespace polysat { static void test_quot_rem_incomplete() { unsigned bw = 4; scoped_solver s(__func__); - s.set_max_conflicts(5); auto quot = s.var(s.add_var(bw)); auto rem = s.var(s.add_var(bw)); auto a = s.value(rational(2), bw); @@ -1278,7 +1274,6 @@ namespace polysat { static void test_quot_rem_fixed() { unsigned bw = 4; scoped_solver s(__func__); - s.set_max_conflicts(5); auto a = s.value(rational(2), bw); auto b = s.value(rational(5), bw); auto [quot, rem] = s.quot_rem(a, b); @@ -1289,24 +1284,22 @@ namespace polysat { static void test_quot_rem(unsigned bw = 32) { scoped_solver s(__func__); - s.set_max_conflicts(5); auto a = s.var(s.add_var(bw)); auto quot = s.var(s.add_var(bw)); auto rem = s.var(s.add_var(bw)); auto x = a * 123; auto y = 123; // quot = udiv(a*123, 123) - s.add_eq(quot * y + rem - x); - s.add_diseq(a - quot); - s.add_umul_noovfl(quot, y); - s.add_ult(rem, x); + s.add_eq(x, quot * y + rem); // 123*a = q*123 + r + s.add_diseq(a, quot); // a != quot + s.add_umul_noovfl(quot, y); // 123*quot < 2^K + s.add_ult(rem, x); // r < 123*a ??? s.check(); - s.expect_sat(); + s.expect_sat(); // dubious } static void test_quot_rem2(unsigned bw = 32) { scoped_solver s(__func__); - s.set_max_conflicts(5); auto q = s.var(s.add_var(bw)); auto r = s.var(s.add_var(bw)); auto idx = s.var(s.add_var(bw)); @@ -1593,12 +1586,12 @@ void tst_polysat() { #if 0 // Enable this block to run a single unit test with detailed output. collect_test_records = false; test_max_conflicts = 50; - test_polysat::test_band5(); + // test_polysat::test_band5(); // test_polysat::test_band5_clause(); // test_polysat::test_ineq_axiom1(32, 1); // test_polysat::test_pop_conflict(); // test_polysat::test_l2(); - // test_polysat::test_ineq1(); + test_polysat::test_ineq1(); // test_polysat::test_quot_rem(); // test_polysat::test_ineq_non_axiom1(32, 3); // test_polysat::test_monot_bounds_full(); @@ -1662,6 +1655,23 @@ void tst_polysat() { RUN(test_polysat::test_fixed_point_arith_mul_div_inverse()); RUN(test_polysat::test_fixed_point_arith_div_mul_inverse()); + RUN(test_polysat::test_quot_rem_incomplete()); + RUN(test_polysat::test_quot_rem_fixed()); + RUN(test_polysat::test_quot_rem()); + RUN(test_polysat::test_quot_rem2()); + + RUN(test_polysat::test_band1()); + RUN(test_polysat::test_band2()); + RUN(test_polysat::test_band3()); + RUN(test_polysat::test_band4()); + RUN(test_polysat::test_band5()); + RUN(test_polysat::test_band5_clause()); + + RUN(test_polysat::test_fi_zero()); + RUN(test_polysat::test_fi_nonzero()); + RUN(test_polysat::test_fi_nonmax()); + RUN(test_polysat::test_fi_disequal_mild()); + RUN(test_polysat::test_ineq_axiom1()); RUN(test_polysat::test_ineq_axiom2()); RUN(test_polysat::test_ineq_axiom3()); @@ -1671,21 +1681,6 @@ void tst_polysat() { RUN(test_polysat::test_ineq_non_axiom1()); RUN(test_polysat::test_ineq_non_axiom4()); - RUN(test_polysat::test_quot_rem_incomplete()); - RUN(test_polysat::test_quot_rem_fixed()); - RUN(test_polysat::test_band1()); - RUN(test_polysat::test_band2()); - RUN(test_polysat::test_band3()); - RUN(test_polysat::test_band4()); - RUN(test_polysat::test_band5()); - RUN(test_polysat::test_band5_clause()); - RUN(test_polysat::test_quot_rem()); - - RUN(test_polysat::test_fi_zero()); - RUN(test_polysat::test_fi_nonzero()); - RUN(test_polysat::test_fi_nonmax()); - RUN(test_polysat::test_fi_disequal_mild()); - // test_fi::exhaustive(); // test_fi::randomized(); From 93ee9c7f8e94fb41b7705674a9319f3273521bb8 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 7 Dec 2022 16:16:07 +0100 Subject: [PATCH 06/44] compile --- src/math/polysat/forbidden_intervals.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index f788eb3f2..960e55170 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -128,7 +128,7 @@ namespace polysat { return true; } - static char* _last_function = ""; + static char const* _last_function = ""; bool forbidden_intervals::get_interval_ule(signed_constraint const& c, pvar v, fi_record& fi) { From 45e94ae7dd5ff0b81968906ea83cd1f96f58e3e6 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 7 Dec 2022 18:41:42 +0100 Subject: [PATCH 07/44] insert_eval --- src/math/polysat/saturation.cpp | 21 ++++++++++----------- src/test/polysat.cpp | 3 ++- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index ee7cc1973..947beaad3 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -121,10 +121,9 @@ namespace polysat { if (!is_forced_false(c)) return false; - // TODO: ??? this means that c is already on the search stack, so presumably the lemma won't help. Should check whether this case occurs. - // if (c.bvalue(s) == l_true) - // return false; - SASSERT(c.bvalue(s) != l_true); + // Constraint c is already on the search stack, so the lemma will not derive anything new. + if (c.bvalue(s) == l_true) + return false; m_lemma.insert_eval(c); core.add_lemma(m_rule, m_lemma.build()); @@ -354,7 +353,7 @@ namespace polysat { if (!is_non_overflow(x, y, non_ovfl)) return false; m_lemma.reset(); - m_lemma.insert(~non_ovfl); + m_lemma.insert_eval(~non_ovfl); if (!xy_l_xz.is_strict()) m_lemma.insert_eval(s.eq(x)); return add_conflict(core, xy_l_xz, ineq(xy_l_xz.is_strict(), y, z)); @@ -397,7 +396,7 @@ namespace polysat { return false; pdd const& z_prime = l_y.lhs(); m_lemma.reset(); - m_lemma.insert(~non_ovfl); + m_lemma.insert_eval(~non_ovfl); return add_conflict(core, l_y, yx_l_zx, ineq(yx_l_zx.is_strict() || l_y.is_strict(), z_prime * x, z * x)); } @@ -437,7 +436,7 @@ namespace polysat { if (!is_non_overflow(x, y_prime, non_ovfl)) return false; m_lemma.reset(); - m_lemma.insert(~non_ovfl); + m_lemma.insert_eval(~non_ovfl); return add_conflict(core, yx_l_zx, z_l_y, ineq(z_l_y.is_strict() || yx_l_zx.is_strict(), y * x, y_prime * x)); } @@ -478,7 +477,7 @@ namespace polysat { if (!is_non_overflow(a, z, non_ovfl)) return false; m_lemma.reset(); - m_lemma.insert(~non_ovfl); + m_lemma.insert_eval(~non_ovfl); return add_conflict(core, y_l_ax, x_l_z, ineq(x_l_z.is_strict() || y_l_ax.is_strict(), y, a * z)); } @@ -602,9 +601,9 @@ namespace polysat { if (!is_non_overflow(a, X, non_ovfl)) return false; m_lemma.reset(); - m_lemma.insert(~s.eq(b, rational(-1))); - m_lemma.insert(~s.eq(y)); - m_lemma.insert(~non_ovfl); + m_lemma.insert_eval(~s.eq(b, rational(-1))); + m_lemma.insert_eval(~s.eq(y)); + m_lemma.insert_eval(~non_ovfl); if (propagate(core, axb_l_y, s.eq(X, 1))) return true; if (propagate(core, axb_l_y, s.eq(a, 1))) diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 85f5c8c62..f1d8707d6 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -1591,7 +1591,7 @@ void tst_polysat() { // test_polysat::test_ineq_axiom1(32, 1); // test_polysat::test_pop_conflict(); // test_polysat::test_l2(); - test_polysat::test_ineq1(); + // test_polysat::test_ineq1(); // test_polysat::test_quot_rem(); // test_polysat::test_ineq_non_axiom1(32, 3); // test_polysat::test_monot_bounds_full(); @@ -1599,6 +1599,7 @@ void tst_polysat() { // test_polysat::test_quot_rem_incomplete(); // test_polysat::test_monot(); // test_polysat::test_fixed_point_arith_div_mul_inverse(); + test_polysat::test_monot_bounds_simple(8); return; #endif From 55d691e16e595f6476c7ad1064faa8c3fb509134 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 7 Dec 2022 18:45:00 +0100 Subject: [PATCH 08/44] enable --- src/math/polysat/saturation.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 947beaad3..d7ba543eb 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -39,14 +39,10 @@ namespace polysat { if (c.is_currently_true(s)) continue; auto i = inequality::from_ule(c); -#if 0 if (try_mul_bounds(v, core, i)) return true; -#endif -#if 0 if (try_parity(v, core, i)) return true; -#endif if (try_ugt_x(v, core, i)) return true; if (try_ugt_y(v, core, i)) From 437f826e8bbb2575f42f5fc1ce19ca5f948225cb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Dec 2022 20:04:58 -0800 Subject: [PATCH 09/44] sketch parity generalization Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.cpp | 41 +++++++++++++++++ src/math/dd/dd_pdd.h | 2 + src/math/polysat/saturation.cpp | 82 ++++++++++++++++++++++++++------- src/math/polysat/solver.h | 10 +++- 4 files changed, 118 insertions(+), 17 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 1d784985c..8175a2dd8 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -165,6 +165,47 @@ namespace dd { return true; } + unsigned pdd_manager::min_parity(PDD p) { + if (m_semantics != mod2N_e) + return 0; + + if (is_val(p)) { + rational v = val(p); + if (v.is_zero()) + return m_power_of_2 + 1; + unsigned r = 0; + while (v.is_even() && v > 0) + r++, v /= 2; + return r; + } + PDD q = p; + while (!is_val(q)) + q = lo(q); + unsigned p2 = val(q).trailing_zeros(); + init_mark(); + if (p2 == 0) + return 0; + init_mark(); + m_todo.push_back(hi(p)); + while (!m_todo.empty() && p2 != 0) { + PDD r = m_todo.back(); + m_todo.pop_back(); + if (is_marked(r)) + continue; + set_mark(r); + if (!is_val(r)) { + m_todo.push_back(lo(r)); + m_todo.push_back(hi(r)); + } + else if (val(r).is_zero()) + continue; + else if (val(r).trailing_zeros() < p2) + p2 = val(r).trailing_zeros(); + } + m_todo.reset(); + return p2; + } + pdd pdd_manager::subst_val(pdd const& p, pdd const& s) { return pdd(apply(p.root, s.root, pdd_subst_val_op), this); } diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index e656cee35..4851626b2 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -255,6 +255,7 @@ namespace dd { inline bool is_var(PDD p) const { return !is_val(p) && is_zero(lo(p)) && is_one(hi(p)); } inline bool is_max(PDD p) const { SASSERT(m_semantics == mod2_e || m_semantics == mod2N_e); return is_val(p) && val(p) == max_value(); } bool is_never_zero(PDD p); + unsigned min_parity(PDD p); inline unsigned level(PDD p) const { return m_nodes[p].m_level; } inline unsigned var(PDD p) const { return m_level2var[level(p)]; } inline PDD lo(PDD p) const { return m_nodes[p].m_lo; } @@ -432,6 +433,7 @@ namespace dd { void get_univariate_coefficients(vector& coeff) const { m.get_univariate_coefficients(root, coeff); } vector get_univariate_coefficients() const { vector coeff; m.get_univariate_coefficients(root, coeff); return coeff; } bool is_never_zero() const { return m.is_never_zero(root); } + unsigned min_parity() const { return m.min_parity(root); } bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); } pdd operator-() const { return m.minus(*this); } diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index d7ba543eb..0884d9b9a 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -633,6 +633,7 @@ namespace polysat { bool saturation::try_parity(pvar x, conflict& core, inequality const& axb_l_y) { set_rule("[x] a*x + b = 0 => (odd(a) & odd(x) <=> odd(b))"); auto& m = s.var2pdd(x); + unsigned N = m.power_of_2(); pdd y = m.zero(); pdd a = m.zero(); pdd b = m.zero(); @@ -653,29 +654,78 @@ namespace polysat { LOG("a_is_odd: " << lit_pp(s, a_is_odd)); LOG("x_is_odd: " << lit_pp(s, x_is_odd)); #endif - if (!b_is_odd.is_currently_true(s)) { - if (!a_is_odd.is_currently_true(s)) - return false; - if (!x_is_odd.is_currently_true(s)) - return false; + if (a_is_odd.is_currently_true(s) && + x_is_odd.is_currently_true(s)) { m_lemma.reset(); m_lemma.insert_eval(~s.eq(y)); m_lemma.insert_eval(~a_is_odd); m_lemma.insert_eval(~x_is_odd); if (propagate(core, axb_l_y, b_is_odd)) return true; - return false; } - m_lemma.reset(); - m_lemma.insert_eval(~s.eq(y)); - m_lemma.insert_eval(~b_is_odd); - if (propagate(core, axb_l_y, a_is_odd)) - return true; - m_lemma.reset(); - m_lemma.insert_eval(~s.eq(y)); - m_lemma.insert_eval(~b_is_odd); - if (propagate(core, axb_l_y, x_is_odd)) - return true; + +#if 0 + // TODO - enable this code and test + // a is divisibly by 4, + // max divisor of x is k + // -> b has parity k + 4 + if ((~a_is_odd).is_currently_true(s) || + (~x_is_odd).is_currently_true(s)) { + unsigned a_parity = 0; + unsigned x_parity = 0; + while (a_parity <= N && s.parity(a, a_parity+1).is_currently_true(s)) + ++a_parity; + while (x_parity <= N && s.parity(X, x_parity+1).is_currently_true(s)) + ++x_parity; + SASSERT(a_parity > 0 || x_parity > 0); + unsigned b_parity = std::min(N + 1, a_parity + x_parity); + if (a_parity > 0) + m_lemma.insert_eval(~s.parity(a, a_parity)); + if (x_parity > 0) + m_lemma.insert_eval(~s.parity(X, x_parity)); + if (propagate(core, axb_l_y, s.parity(b, b_parity))) + return true; + } +#endif + + if (b_is_odd.is_currently_true(s)) { + m_lemma.reset(); + m_lemma.insert_eval(~s.eq(y)); + m_lemma.insert_eval(~b_is_odd); + if (propagate(core, axb_l_y, a_is_odd)) + return true; + m_lemma.reset(); + m_lemma.insert_eval(~s.eq(y)); + m_lemma.insert_eval(~b_is_odd); + if (propagate(core, axb_l_y, x_is_odd)) + return true; + } + +#if 0 + + // + // if b has at least b_parity, then a*x has at least b_parity + // establish lower bound on parity of b + // + if ((~b_is_odd).is_currently_true(s) && !is_forced_eq(b, 0)) { + unsigned b_parity = 1; + while (b_parity <= N && s.parity(b, b_parity+1).is_currently_true(s)) + ++b_parity; + SASSERT(b_parity <= N); + // TODO: + // something like this (but fixed) + for (unsigned i = 0; i <= b_parity; ++i) { + if (s.parity(a, b_parity - i).is_currently_false(s)) { + m_lemma.reset(); + m_lemma.insert_eval(~s.eq(y)); + m_lemma.insert_eval(~s.parity(b, b_parity)); + m_lemma.insert_eval(s.parity(a, b_parity - i)); + if (propagate(core, axb_l_y, s.parity(x, i))) + return true; + } + } + } +#endif return false; } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 1af414a14..aeeafba0e 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -413,7 +413,15 @@ namespace polysat { signed_constraint odd(pdd const& p) { return ~even(p); } signed_constraint even(pdd const& p) { return parity(p, 1); } /** parity(p) >= k (<=> p * 2^(K-k) == 0) */ - signed_constraint parity(pdd const& p, unsigned k) { return eq(p*rational::power_of_two(p.manager().power_of_2() - k)); } + signed_constraint parity(pdd const& p, unsigned k) { + unsigned N = p.manager().power_of_2(); + if (k > N) + return eq(p); + else if (k == 0) + return odd(p); + else + return eq(p*rational::power_of_two(N - k)); + } signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); } signed_constraint diseq(pdd const& p, unsigned q) { return diseq(p - q); } signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); } From acbd60799d1ef3ed6c1054ba0f84a1b7b6b20e71 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Dec 2022 20:12:19 -0800 Subject: [PATCH 10/44] add placeholder for factor equality Signed-off-by: Nikolaj Bjorner --- src/math/polysat/saturation.cpp | 17 +++++++++++++++++ src/math/polysat/saturation.h | 1 + 2 files changed, 18 insertions(+) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 0884d9b9a..780cb6cbf 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -43,6 +43,8 @@ namespace polysat { return true; if (try_parity(v, core, i)) return true; + if (try_factor_equality(v, core, i)) + return true; if (try_ugt_x(v, core, i)) return true; if (try_ugt_y(v, core, i)) @@ -761,6 +763,21 @@ namespace polysat { return false; } + /** + * [x] ax + p <= q, ax + r = 0 => -r + p <= q + * [x] p <= ax + q, ax + r = 0 => p <= -r + q + * generalizations + * [x] abx + p <= q, ax + r = 0 => -rb + p <= q + * [x] p <= abx + q, ax + r = 0 => p <= -rb + q + */ + + bool saturation::try_factor_equality(pvar x, conflict& core, inequality const& a_l_b) { + // search for abx+p pattern in a_l_b.lhs() + // search for ax + r = 0 equality in core (or in search but maybe not needed) + // replace abx by -rb in patterns on either a_l_b.lhs() or a_l_b.rhs() or both if available to form new implied + // literal wtihout occurrence of x + return false; + } /* * TODO * diff --git a/src/math/polysat/saturation.h b/src/math/polysat/saturation.h index f41c39ad0..a0f7e7fa8 100644 --- a/src/math/polysat/saturation.h +++ b/src/math/polysat/saturation.h @@ -48,6 +48,7 @@ namespace polysat { bool try_parity(pvar x, conflict& core, inequality const& axb_l_y); bool try_mul_bounds(pvar x, conflict& core, inequality const& axb_l_y); + bool try_factor_equality(pvar x, conflict& core, inequality const& a_l_b); bool try_mul_eq_1(pvar x, conflict& core, inequality const& axb_l_y); bool try_mul_odd(pvar x, conflict& core, inequality const& axb_l_y); bool try_tangent(pvar v, conflict& core, inequality const& c); From 28fb67219ea5e5d1ac830eaa485b979658f3e099 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 8 Dec 2022 07:13:31 -0800 Subject: [PATCH 11/44] fix new (and unused) function for extracting min parity of a polynomial Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 8175a2dd8..3886bbb0f 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -178,16 +178,16 @@ namespace dd { r++, v /= 2; return r; } + init_mark(); PDD q = p; - while (!is_val(q)) + m_todo.push_back(hi(q)); + while (!is_val(q)) { q = lo(q); + m_todo.push_back(hi(q)); + } unsigned p2 = val(q).trailing_zeros(); init_mark(); - if (p2 == 0) - return 0; - init_mark(); - m_todo.push_back(hi(p)); - while (!m_todo.empty() && p2 != 0) { + while (p2 != 0 && !m_todo.empty()) { PDD r = m_todo.back(); m_todo.pop_back(); if (is_marked(r)) From 85818612fbf2681d47c23101e9835ae0638ba4d9 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 8 Dec 2022 15:25:36 +0100 Subject: [PATCH 12/44] val_pp --- src/math/dd/dd_pdd.cpp | 18 +++++++++--------- src/math/dd/dd_pdd.h | 2 ++ 2 files changed, 11 insertions(+), 9 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 3886bbb0f..42d473657 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -1719,15 +1719,15 @@ namespace dd { unsigned pow; if (val.is_power_of_two(pow) && pow > 10) return out << "2^" << pow; - else if (val < m.max_value() && (val + 1).is_power_of_two(pow) && pow > 10) { - if (require_parens) - out << "("; - out << "2^" << pow << "-1"; - if (require_parens) - out << ")"; - return out; - } else - return out << m.normalize(val); + for (int offset : {-1, 1}) + if (val < m.max_value() && (val - offset).is_power_of_two(pow) && pow > 10) + return out << lparen() << "2^" << pow << (offset >= 0 ? "+" : "") << offset << rparen(); + rational neg_val = mod(-val, m.two_to_N()); + if (neg_val < val) { // keep this condition so we don't suddenly print negative values where we wouldn't otherwise + if (neg_val.is_power_of_two(pow) && pow > 10) + return out << "-2^" << pow; + } + return out << m.normalize(val); } bool pdd_manager::well_formed() { diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 4851626b2..de29ed600 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -556,6 +556,8 @@ namespace dd { pdd_manager const& m; rational const& val; bool require_parens; + char const* lparen() const { return require_parens ? "(" : ""; } + char const* rparen() const { return require_parens ? ")" : ""; } public: val_pp(pdd_manager const& m, rational const& val, bool require_parens): m(m), val(val), require_parens(require_parens) {} std::ostream& display(std::ostream& out) const; From 3fe8f4a0cd79b841d7f0aa86153cdc0695cf3838 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 8 Dec 2022 15:30:55 +0100 Subject: [PATCH 13/44] minor issue about narrow with first=true --- src/math/polysat/solver.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index ca76f1c1f..079574944 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -1052,6 +1052,10 @@ namespace polysat { } if (v != null_var) m_viable_fallback.push_constraint(v, c); + // TODO: we use narrow with first=true to add axioms about the constraint to the solver. + // However, constraints can be activated multiple times (e.g., if it comes from a lemma and is propagated at a non-base level). + // So the same axioms may be added multiple times. + // Maybe separate narrow/activate? And keep a flag in m_bvars to remember whether constraint has already been activated. c.narrow(*this, true); #if ENABLE_LINEAR_SOLVER m_linear_solver.activate_constraint(c); From a81e05e66015269aed535f2235d496b7c4b285df Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 8 Dec 2022 15:52:34 +0100 Subject: [PATCH 14/44] We shouldn't assume that v is assigned Happens if it is a viable conflict for v --- src/math/polysat/saturation.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 780cb6cbf..43f3d28f3 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -346,7 +346,7 @@ namespace polysat { if (!is_xY_l_xZ(v, xy_l_xz, y, z)) return false; - if (!xy_l_xz.is_strict() && s.get_value(v).is_zero()) + if (!xy_l_xz.is_strict() && s.is_assigned(v) && s.get_value(v).is_zero()) return false; if (!is_non_overflow(x, y, non_ovfl)) return false; From 676aa81c5a1e4dacc3e8ea57dab8a1675a1ab2f3 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 8 Dec 2022 16:08:21 +0100 Subject: [PATCH 15/44] Fix test_ineq2 --- src/test/polysat.cpp | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index f1d8707d6..17c92063a 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -324,7 +324,7 @@ namespace polysat { for (auto const& p : expected_assignment) { auto const& v_pdd = p.first; auto const expected_value = p.second; - SASSERT(v_pdd.is_monomial() && !v_pdd.is_val()); + SASSERT(v_pdd.is_var()); auto const v = v_pdd.var(); if (get_value(v) != expected_value) { rec->m_result = test_result::wrong_model; @@ -651,9 +651,10 @@ namespace polysat { /** * Check unsat of: - * n*q1 = a - b - * n*q2 + r2 = c*a - c*b - * n > r2 > 0 + * n*q1 = a - b 3*1 == 3 - 0 + * n*q2 + r2 = c*a - c*b 3*0 + 1 == 11*3 - 11*0 (= 33 = 1 mod 32) + * n > r2 > 0 3 > 1 > 0 + * It is actually satisfiable. */ static void test_ineq2() { scoped_solver s(__func__); @@ -669,10 +670,9 @@ namespace polysat { s.add_ult(r2, n); s.add_diseq(r2); s.check(); - s.expect_unsat(); + s.expect_sat({ {n, 3}, {q1, 1}, {a, 3}, {b, 0}, {c, 11}, {q2, 0}, {r2, 1} }); } - /** * Monotonicity example from certora * @@ -1592,6 +1592,7 @@ void tst_polysat() { // test_polysat::test_pop_conflict(); // test_polysat::test_l2(); // test_polysat::test_ineq1(); + test_polysat::test_ineq2(); // test_polysat::test_quot_rem(); // test_polysat::test_ineq_non_axiom1(32, 3); // test_polysat::test_monot_bounds_full(); @@ -1599,13 +1600,14 @@ void tst_polysat() { // test_polysat::test_quot_rem_incomplete(); // test_polysat::test_monot(); // test_polysat::test_fixed_point_arith_div_mul_inverse(); - test_polysat::test_monot_bounds_simple(8); + // test_polysat::test_monot_bounds_simple(8); + // test_polysat::test_ineq_non_axiom4(32, 7); return; #endif // If non-empty, only run tests whose name contains the run_filter run_filter = ""; - test_max_conflicts = 10; + test_max_conflicts = 20; collect_test_records = true; From 5ad961029d67bc1bf137502f72894b5f2d7a3086 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 8 Dec 2022 16:12:41 +0100 Subject: [PATCH 16/44] Rename revert_decision -> revert_pvar, and enable it. Also rename resolve_with_assignment to resolve_evaluated --- src/math/polysat/conflict.cpp | 16 +++++++--------- src/math/polysat/conflict.h | 8 ++++---- src/math/polysat/solver.cpp | 10 +++++++--- src/math/polysat/solver.h | 2 +- 4 files changed, 19 insertions(+), 17 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index c1cf8b4d4..71c7390ec 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -104,11 +104,11 @@ namespace polysat { } }; - struct inf_resolve_with_assignment : public inference { + struct inf_resolve_evaluated : public inference { solver& s; sat::literal lit; signed_constraint c; - inf_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {} + inf_resolve_evaluated(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {} std::ostream& display(std::ostream& out) const override { out << "Resolve upon " << lit << " with assignment:"; for (pvar v : c->vars()) @@ -251,15 +251,13 @@ namespace polysat { insert_vars(c); } SASSERT(!m_vars.contains(v)); - // TODO: apply conflict resolution plugins here too? } else { logger().begin_conflict(header_with_var("forbidden interval lemma for v", v)); VERIFY(s.m_viable.resolve(v, *this)); } - - // NSB TODO - disabled: revert_decision(v); SASSERT(!empty()); + revert_pvar(v); // at this point, v is not assigned } bool conflict::contains(sat::literal lit) const { @@ -368,7 +366,7 @@ namespace polysat { logger().log(inf_resolve_bool(lit, cl)); } - void conflict::resolve_with_assignment(sat::literal lit) { + void conflict::resolve_evaluated(sat::literal lit) { // The reason for lit is conceptually: // x1 = v1 /\ ... /\ xn = vn ==> lit @@ -400,10 +398,10 @@ namespace polysat { SASSERT(!contains(lit)); SASSERT(!contains(~lit)); - logger().log(inf_resolve_with_assignment(s, lit, c)); + logger().log(inf_resolve_evaluated(s, lit, c)); } - void conflict::revert_decision(pvar v) { + void conflict::revert_pvar(pvar v) { m_resolver->infer_lemmas_for_value(v, *this); } @@ -422,7 +420,7 @@ namespace polysat { } logger().log(inf_resolve_value(s, v)); - revert_decision(v); + revert_pvar(v); } clause_ref conflict::build_lemma() { diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index 9922b57d9..ac529b382 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -177,14 +177,14 @@ namespace polysat { /** Perform boolean resolution with the clause upon the given literal. */ void resolve_bool(sat::literal lit, clause const& cl); - /** lit was fully evaluated under the assignment. */ - void resolve_with_assignment(sat::literal lit); + /** lit was evaluated under the assignment. */ + void resolve_evaluated(sat::literal lit); /** Perform resolution with "v = value <- ..." */ void resolve_value(pvar v); - /** Revert decision, add auxiliary lemmas for the decision variable **/ - void revert_decision(pvar v); + /** Revert variable assignment, add auxiliary lemmas for the reverted variable */ + void revert_pvar(pvar v); /** Convert the core into a lemma to be learned. */ clause_ref build_lemma(); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 079574944..45c43cc22 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -770,7 +770,7 @@ namespace polysat { continue; } if (j.is_decision()) { - // NSB TODO - disabled m_conflict.revert_decision(v); + m_conflict.revert_pvar(v); revert_decision(v); return; } @@ -806,7 +806,7 @@ namespace polysat { // do we really want to resolve these eagerly? m_conflict.resolve_bool(lit, *m_bvars.reason(lit)); else - m_conflict.resolve_with_assignment(lit); + m_conflict.resolve_evaluated(lit); } } LOG("End of resolve_conflict loop"); @@ -929,6 +929,11 @@ namespace polysat { default: UNREACHABLE(); } + if (is_conflict()) { + // TODO: the remainder of the narrow_queue as well as the lemmas are forgotten. + // should we just insert them into the new conflict to carry them along? + return; + } } for (clause* lemma : lemmas) { @@ -943,7 +948,6 @@ namespace polysat { // TODO: we could also insert the remaining lemmas into the conflict and keep them for later. return; } - SASSERT(!is_conflict()); } if (best_score.branching_factor() > 1) { diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index aeeafba0e..29ad8f255 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -137,7 +137,7 @@ namespace polysat { friend class scoped_solverv; friend class test_polysat; friend class test_fi; - friend struct inf_resolve_with_assignment; + friend struct inf_resolve_evaluated; reslimit& m_lim; params_ref m_params; From 3c8718615a390d1ef853df58b84cb694e775e196 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 8 Dec 2022 16:15:54 +0100 Subject: [PATCH 17/44] yes, no need for plugins to be mutually exclusive --- src/math/polysat/conflict.cpp | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 71c7390ec..14d0fe2da 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -68,17 +68,9 @@ namespace polysat { , m_free_variable_elimination(s) {} - // - // NSB review: the plugins need not be mutually exclusive - // Shouldn't saturation and superposition be allowed independently? - // If they create propagations or conflict lemmas we select the - // tightest propagation as part of backjumping. - // void infer_lemmas_for_value(pvar v, conflict& core) { - if (m_poly_sup.perform(v, core)) - return; - if (m_saturation.perform(v, core)) - return; + (void)m_poly_sup.perform(v, core); + (void)m_saturation.perform(v, core); } // Analyse current conflict core to extract additional lemmas From 33902c7c9e6da5a4acaf79efada319db849478c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 8 Dec 2022 09:57:38 -0800 Subject: [PATCH 18/44] fix parity propagation code, add tail-spin unit tests. The unit tests diverge because conflict resolution removes conflicting literals from the conflict clause before the decision variable gets processed. We have to change how conflict resolution is processed for such conflict clauses Signed-off-by: Nikolaj Bjorner --- src/math/polysat/saturation.cpp | 111 +++++++++++++++++--------------- src/math/polysat/solver.h | 2 +- src/test/polysat.cpp | 49 +++++++++++++- 3 files changed, 107 insertions(+), 55 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 43f3d28f3..56aef30e4 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -634,6 +634,8 @@ namespace polysat { */ bool saturation::try_parity(pvar x, conflict& core, inequality const& axb_l_y) { set_rule("[x] a*x + b = 0 => (odd(a) & odd(x) <=> odd(b))"); + + // IF_VERBOSE(0, verbose_stream() << "try parity " << axb_l_y.as_signed_constraint() << "\n"); auto& m = s.var2pdd(x); unsigned N = m.power_of_2(); pdd y = m.zero(); @@ -649,6 +651,21 @@ namespace polysat { signed_constraint b_is_odd = s.odd(b); signed_constraint a_is_odd = s.odd(a); signed_constraint x_is_odd = s.odd(X); + + auto propagate1 = [&](signed_constraint premise, signed_constraint conseq) { + m_lemma.reset(); + m_lemma.insert_eval(~s.eq(y)); + m_lemma.insert_eval(~premise); + return propagate(core, axb_l_y, conseq); + }; + + auto propagate2 = [&](signed_constraint premise1, signed_constraint premise2, signed_constraint conseq) { + m_lemma.reset(); + m_lemma.insert_eval(~s.eq(y)); + m_lemma.insert_eval(~premise1); + m_lemma.insert_eval(~premise2); + return propagate(core, axb_l_y, conseq); + }; #if 0 LOG_H1("try_parity: " << X << " on: " << lit_pp(s, axb_l_y.as_signed_constraint())); LOG("y: " << y << " a: " << a << " b: " << b); @@ -657,77 +674,67 @@ namespace polysat { LOG("x_is_odd: " << lit_pp(s, x_is_odd)); #endif if (a_is_odd.is_currently_true(s) && - x_is_odd.is_currently_true(s)) { - m_lemma.reset(); - m_lemma.insert_eval(~s.eq(y)); - m_lemma.insert_eval(~a_is_odd); - m_lemma.insert_eval(~x_is_odd); - if (propagate(core, axb_l_y, b_is_odd)) + x_is_odd.is_currently_true(s) && + propagate2(a_is_odd, x_is_odd, b_is_odd)) + return true; + + + if (b_is_odd.is_currently_true(s)) { + if (propagate1(b_is_odd, a_is_odd)) + return true; + if (propagate1(b_is_odd, x_is_odd)) return true; } - -#if 0 - // TODO - enable this code and test + // a is divisibly by 4, // max divisor of x is k // -> b has parity k + 4 - if ((~a_is_odd).is_currently_true(s) || - (~x_is_odd).is_currently_true(s)) { - unsigned a_parity = 0; - unsigned x_parity = 0; - while (a_parity <= N && s.parity(a, a_parity+1).is_currently_true(s)) + unsigned a_parity = a_is_odd.is_currently_false(s) ? 1 : 0; + unsigned x_parity = x_is_odd.is_currently_false(s) ? 1 : 0; + + if ((a_parity > 0 || x_parity > 0) && !is_forced_eq(a, 0) && !is_forced_eq(X, 0)) { + while (a_parity < N && s.parity(a, a_parity+1).is_currently_true(s)) ++a_parity; - while (x_parity <= N && s.parity(X, x_parity+1).is_currently_true(s)) + while (x_parity < N && s.parity(X, x_parity+1).is_currently_true(s)) ++x_parity; - SASSERT(a_parity > 0 || x_parity > 0); - unsigned b_parity = std::min(N + 1, a_parity + x_parity); - if (a_parity > 0) - m_lemma.insert_eval(~s.parity(a, a_parity)); - if (x_parity > 0) - m_lemma.insert_eval(~s.parity(X, x_parity)); - if (propagate(core, axb_l_y, s.parity(b, b_parity))) + unsigned b_parity = std::min(N, a_parity + x_parity); + if (a_parity > 0 && x_parity > 0 && propagate2(s.parity(a, a_parity), s.parity(X, x_parity), s.parity(b, b_parity))) return true; - } -#endif - - if (b_is_odd.is_currently_true(s)) { - m_lemma.reset(); - m_lemma.insert_eval(~s.eq(y)); - m_lemma.insert_eval(~b_is_odd); - if (propagate(core, axb_l_y, a_is_odd)) + if (a_parity > 0 && x_parity == 0 && propagate1(s.parity(a, a_parity), s.parity(b, b_parity))) return true; - m_lemma.reset(); - m_lemma.insert_eval(~s.eq(y)); - m_lemma.insert_eval(~b_is_odd); - if (propagate(core, axb_l_y, x_is_odd)) + if (a_parity == 0 && x_parity > 0 && propagate1(s.parity(X, x_parity), s.parity(b, b_parity))) return true; } -#if 0 - // - // if b has at least b_parity, then a*x has at least b_parity - // establish lower bound on parity of b + // if b has at most b_parity, then a*x has at most b_parity // - if ((~b_is_odd).is_currently_true(s) && !is_forced_eq(b, 0)) { + else if (!is_forced_eq(b, 0)) { unsigned b_parity = 1; - while (b_parity <= N && s.parity(b, b_parity+1).is_currently_true(s)) - ++b_parity; - SASSERT(b_parity <= N); - // TODO: - // something like this (but fixed) - for (unsigned i = 0; i <= b_parity; ++i) { - if (s.parity(a, b_parity - i).is_currently_false(s)) { - m_lemma.reset(); - m_lemma.insert_eval(~s.eq(y)); - m_lemma.insert_eval(~s.parity(b, b_parity)); - m_lemma.insert_eval(s.parity(a, b_parity - i)); - if (propagate(core, axb_l_y, s.parity(x, i))) + bool found = false; + for (; b_parity < N; ++b_parity) { + if (s.parity(b, b_parity).is_currently_false(s)) { + found = true; + break; + } + } + if (found) { + if (propagate1(~s.parity(b, b_parity), ~s.parity(a, b_parity))) + return true; + if (propagate1(~s.parity(b, b_parity), ~s.parity(a, b_parity))) + return true; + + for (unsigned i = 1; i < N; ++i) { + if (s.parity(a, i).is_currently_true(s) && + propagate2(~s.parity(b, b_parity), s.parity(a, i), ~s.parity(X, b_parity - i))) return true; + + if (s.parity(X, i).is_currently_true(s) && + propagate2(~s.parity(b, b_parity), s.parity(X, i), ~s.parity(a, b_parity - i))) + return true; } } } -#endif return false; } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 29ad8f255..71acde22d 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -415,7 +415,7 @@ namespace polysat { /** parity(p) >= k (<=> p * 2^(K-k) == 0) */ signed_constraint parity(pdd const& p, unsigned k) { unsigned N = p.manager().power_of_2(); - if (k > N) + if (k >= N) return eq(p); else if (k == 0) return odd(p); diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 17c92063a..ba355af94 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -204,7 +204,7 @@ namespace polysat { for (test_record const* r : m_records) { if (!r->m_finished) continue; - r->display(out, max_name_len); + r->display(out, static_cast(max_name_len)); out << std::endl; if (r->m_result == test_result::ok && r->m_answer == l_true) n_sat++; @@ -629,6 +629,47 @@ namespace polysat { SASSERT(cl->size() == 2); } + // 8 * x + 3 == 0 is unsat + static void test_parity1() { + scoped_solver s(__func__); + simplify_clause simp(s); + clause_builder cb(s); + auto x = s.var(s.add_var(8)); + auto y = s.var(s.add_var(8)); + auto z = s.var(s.add_var(8)); + s.add_clause({s.eq(x * y + z), s.eq(x * y + 5)}, false); + s.add_eq(y, 8); + s.add_eq(z, 3); + s.check(); + s.expect_unsat(); + } + + // 8 * x + 4 == 0 is unsat + static void test_parity2() { + scoped_solver s(__func__); + simplify_clause simp(s); + clause_builder cb(s); + auto x = s.var(s.add_var(8)); + auto y = s.var(s.add_var(8)); + s.add_clause({ s.eq(x * y + 2), s.eq(x * y + 4) }, false); + s.add_eq(y, 8); + s.check(); + s.expect_unsat(); + } + + // x * y + 4 == 0 & 16 divides y is unsat + static void test_parity3() { + scoped_solver s(__func__); + simplify_clause simp(s); + clause_builder cb(s); + auto x = s.var(s.add_var(8)); + auto y = s.var(s.add_var(8)); + s.add_clause({ s.eq(x * y + 2), s.eq(x * y + 4) }, false); + s.add_eq(16 * y); + s.check(); + s.expect_unsat(); + } + /** * Check unsat of: @@ -1583,9 +1624,13 @@ static void STD_CALL polysat_on_ctrl_c(int) { void tst_polysat() { using namespace polysat; -#if 0 // Enable this block to run a single unit test with detailed output. +#if 1 // Enable this block to run a single unit test with detailed output. collect_test_records = false; test_max_conflicts = 50; + test_polysat::test_parity1(); +// test_polysat::test_parity2(); +// test_polysat::test_parity3(); + return; // test_polysat::test_band5(); // test_polysat::test_band5_clause(); // test_polysat::test_ineq_axiom1(32, 1); From a6b49d8b4e2c7eea7bcefe4d07fbaefecf2c6f2e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 8 Dec 2022 19:17:35 -0800 Subject: [PATCH 19/44] provide access to saturation for selected constraints --- src/math/polysat/conflict.cpp | 15 +++++++-- src/math/polysat/saturation.cpp | 56 ++++++++++++++++++--------------- src/math/polysat/saturation.h | 3 +- 3 files changed, 44 insertions(+), 30 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 14d0fe2da..e03ace554 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -73,6 +73,10 @@ namespace polysat { (void)m_saturation.perform(v, core); } + void infer_lemmas_for_value(pvar v, signed_constraint const& c, conflict& core) { + (void)m_saturation.perform(v, c, core); + } + // Analyse current conflict core to extract additional lemmas void find_extra_lemmas(conflict& core) { m_free_variable_elimination.find_lemma(core); @@ -381,10 +385,15 @@ namespace polysat { #endif if (!has_decision) { + for (pvar v : c->vars()) { + if (s.is_assigned(v) && s.get_level(v) <= lvl) { + m_vars.insert(v); +// TODO - figure out what to do with constraints from conflict lemma that disappear here. +// if (s.m_bvars.is_false(lit)) +// m_resolver->infer_lemmas_for_value(v, ~c, *this); + } + } remove(c); - for (pvar v : c->vars()) - if (s.is_assigned(v) && s.get_level(v) <= lvl) - m_vars.insert(v); } SASSERT(!contains(lit)); diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 56aef30e4..ae9b587a8 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -32,30 +32,35 @@ namespace polysat { saturation::saturation(solver& s) : s(s), m_lemma(s) {} - bool saturation::perform(pvar v, conflict& core) { - for (auto c : core) { - if (!c->is_ule()) - continue; - if (c.is_currently_true(s)) - continue; - auto i = inequality::from_ule(c); - if (try_mul_bounds(v, core, i)) - return true; - if (try_parity(v, core, i)) - return true; - if (try_factor_equality(v, core, i)) - return true; - if (try_ugt_x(v, core, i)) - return true; - if (try_ugt_y(v, core, i)) - return true; - if (try_ugt_z(v, core, i)) - return true; - if (try_y_l_ax_and_x_l_z(v, core, i)) - return true; - if (try_tangent(v, core, i)) - return true; - } + void saturation::perform(pvar v, conflict& core) { + for (auto c : core) + if (perform(v, c, core)) + return; + } + + bool saturation::perform(pvar v, signed_constraint const& c, conflict& core) { + IF_VERBOSE(0, verbose_stream() << v << " " << c << " " << c.is_currently_true(s) << "\n"); + if (!c->is_ule()) + return false; + if (c.is_currently_true(s)) + return false; + auto i = inequality::from_ule(c); + if (try_mul_bounds(v, core, i)) + return true; + if (try_parity(v, core, i)) + return true; + if (try_factor_equality(v, core, i)) + return true; + if (try_ugt_x(v, core, i)) + return true; + if (try_ugt_y(v, core, i)) + return true; + if (try_ugt_z(v, core, i)) + return true; + if (try_y_l_ax_and_x_l_z(v, core, i)) + return true; + if (try_tangent(v, core, i)) + return true; return false; } @@ -66,7 +71,6 @@ namespace polysat { return s.ule(lhs, rhs); } - bool saturation::propagate(conflict& core, inequality const& crit, signed_constraint c) { if (is_forced_true(c)) return false; @@ -635,7 +639,7 @@ namespace polysat { bool saturation::try_parity(pvar x, conflict& core, inequality const& axb_l_y) { set_rule("[x] a*x + b = 0 => (odd(a) & odd(x) <=> odd(b))"); - // IF_VERBOSE(0, verbose_stream() << "try parity " << axb_l_y.as_signed_constraint() << "\n"); + IF_VERBOSE(0, verbose_stream() << "try parity " << axb_l_y.as_signed_constraint() << "\n"); auto& m = s.var2pdd(x); unsigned N = m.power_of_2(); pdd y = m.zero(); diff --git a/src/math/polysat/saturation.h b/src/math/polysat/saturation.h index a0f7e7fa8..bb169bc44 100644 --- a/src/math/polysat/saturation.h +++ b/src/math/polysat/saturation.h @@ -113,7 +113,8 @@ namespace polysat { public: saturation(solver& s); - bool perform(pvar v, conflict& core); + void perform(pvar v, conflict& core); + bool perform(pvar v, signed_constraint const& sc, conflict& core); }; /* From e716e507d9f571a748da23cf129ca5f7af794ef2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 26 Nov 2022 17:16:03 +0700 Subject: [PATCH 20/44] investigate bench4 Signed-off-by: Nikolaj Bjorner --- src/test/polysat.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index ba355af94..24d6f55e8 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -1635,6 +1635,7 @@ void tst_polysat() { // test_polysat::test_band5_clause(); // test_polysat::test_ineq_axiom1(32, 1); // test_polysat::test_pop_conflict(); + test_polysat::test_ineq_basic4(); // test_polysat::test_l2(); // test_polysat::test_ineq1(); test_polysat::test_ineq2(); @@ -1662,6 +1663,8 @@ void tst_polysat() { set_log_enabled(false); } + return; + RUN(test_polysat::test_clause_simplify1()); RUN(test_polysat::test_add_conflicts()); From 8d13446537fe885faaab39f5b6a84e45baa30f34 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 9 Dec 2022 17:22:20 +0100 Subject: [PATCH 21/44] Solve boolean skeleton first --- src/math/polysat/solver.cpp | 30 +++++++++++++++++++++++ src/test/polysat.cpp | 48 ++++++++++++++++++------------------- src/util/util.h | 8 +++++++ 3 files changed, 61 insertions(+), 25 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 45c43cc22..366156989 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -278,6 +278,7 @@ namespace polysat { sc.narrow(*this, false); } else { // constraint state: active but unassigned (bvalue undef, but pwatch is set; e.g., new constraints generated for lemmas) +#if 1 if (c->vars().size() >= 2) { unsigned other_v = c->var(1 - idx); // Wait for the remaining variable to be assigned @@ -293,6 +294,19 @@ namespace polysat { SASSERT(sc.is_currently_false(*this)); assign_eval(~sc.blit()); } +#else + signed_constraint sc(c, true); + switch (sc.eval(*this)) { + case l_true: + assign_eval(sc.blit()); + break; + case l_false: + assign_eval(~sc.blit()); + break; + default: + break; + } +#endif } return false; } @@ -559,6 +573,22 @@ namespace polysat { void solver::decide() { LOG_H2("Decide"); SASSERT(can_decide()); +#if 1 + // Simple hack to try deciding the boolean skeleton first + if (!can_bdecide()) { + // enqueue all not-yet-true clauses + for (auto const& cls : m_constraints.clauses()) { + for (auto const& cl : cls) { + bool is_true = any_of(*cl, [&](sat::literal lit) { return m_bvars.is_true(lit); }); + if (is_true) + continue; + size_t undefs = count_if(*cl, [&](sat::literal lit) { return !m_bvars.is_assigned(lit); }); + if (undefs >= 2) + m_lemmas.push_back(cl.get()); + } + } + } +#endif if (can_bdecide()) bdecide(); else diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index ba355af94..04c567fef 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -632,8 +632,6 @@ namespace polysat { // 8 * x + 3 == 0 is unsat static void test_parity1() { scoped_solver s(__func__); - simplify_clause simp(s); - clause_builder cb(s); auto x = s.var(s.add_var(8)); auto y = s.var(s.add_var(8)); auto z = s.var(s.add_var(8)); @@ -644,11 +642,23 @@ namespace polysat { s.expect_unsat(); } + // 8 * u * x + 3 == 0 is unsat + static void test_parity1b() { + scoped_solver s(__func__); + auto u = s.var(s.add_var(8)); + auto x = s.var(s.add_var(8)); + auto y = s.var(s.add_var(8)); + auto z = s.var(s.add_var(8)); + s.add_clause({s.eq(u * x * y + z), s.eq(u * x * y + 5)}, false); + s.add_eq(y, 8); + s.add_eq(z, 3); + s.check(); + s.expect_unsat(); + } + // 8 * x + 4 == 0 is unsat static void test_parity2() { scoped_solver s(__func__); - simplify_clause simp(s); - clause_builder cb(s); auto x = s.var(s.add_var(8)); auto y = s.var(s.add_var(8)); s.add_clause({ s.eq(x * y + 2), s.eq(x * y + 4) }, false); @@ -660,8 +670,6 @@ namespace polysat { // x * y + 4 == 0 & 16 divides y is unsat static void test_parity3() { scoped_solver s(__func__); - simplify_clause simp(s); - clause_builder cb(s); auto x = s.var(s.add_var(8)); auto y = s.var(s.add_var(8)); s.add_clause({ s.eq(x * y + 2), s.eq(x * y + 4) }, false); @@ -1628,25 +1636,10 @@ void tst_polysat() { collect_test_records = false; test_max_conflicts = 50; test_polysat::test_parity1(); -// test_polysat::test_parity2(); -// test_polysat::test_parity3(); - return; - // test_polysat::test_band5(); - // test_polysat::test_band5_clause(); - // test_polysat::test_ineq_axiom1(32, 1); - // test_polysat::test_pop_conflict(); - // test_polysat::test_l2(); - // test_polysat::test_ineq1(); - test_polysat::test_ineq2(); - // test_polysat::test_quot_rem(); - // test_polysat::test_ineq_non_axiom1(32, 3); - // test_polysat::test_monot_bounds_full(); - // test_polysat::test_band2(); - // test_polysat::test_quot_rem_incomplete(); - // test_polysat::test_monot(); - // test_polysat::test_fixed_point_arith_div_mul_inverse(); - // test_polysat::test_monot_bounds_simple(8); - // test_polysat::test_ineq_non_axiom4(32, 7); + // test_polysat::test_parity1b(); + // test_polysat::test_parity2(); + // test_polysat::test_parity3(); + // test_polysat::test_ineq2(); return; #endif @@ -1662,6 +1655,11 @@ void tst_polysat() { set_log_enabled(false); } + RUN(test_polysat::test_parity1()); + RUN(test_polysat::test_parity1b()); + RUN(test_polysat::test_parity2()); + RUN(test_polysat::test_parity3()); + RUN(test_polysat::test_clause_simplify1()); RUN(test_polysat::test_add_conflicts()); diff --git a/src/util/util.h b/src/util/util.h index 351a3faa9..4ac65ccfd 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -385,6 +385,14 @@ bool all_of(Container const& c, Predicate p) return std::all_of(begin(c), end(c), std::forward(p)); } +/** Compact version of std::any_of */ +template +bool any_of(Container const& c, Predicate p) +{ + using std::begin, std::end; // allows begin(c) to also find c.begin() + return std::any_of(begin(c), end(c), std::forward(p)); +} + /** Compact version of std::count */ template std::size_t count(Container const& c, Item x) From 707577644f7d62d261d9c1816b3a800c7501614f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2022 09:33:24 -0800 Subject: [PATCH 22/44] assignment -> assignment_t for build Signed-off-by: Nikolaj Bjorner --- src/math/polysat/solver.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 71acde22d..a550f35c0 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -211,7 +211,7 @@ namespace polysat { dd::pdd_manager& sz2pdd(unsigned sz) const; dd::pdd_manager& var2pdd(pvar v) const; - assignment const& assignment() const { return m_search.assignment(); } + assignment_t const& assignment() const { return m_search.assignment(); } void push_level(); void pop_levels(unsigned num_levels); From 6e886114f90c7e9bc54644cc14c5928d54612d54 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2022 09:56:47 -0800 Subject: [PATCH 23/44] add parity4 Signed-off-by: Nikolaj Bjorner --- src/test/polysat.cpp | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 04c567fef..c1808d9a4 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -629,7 +629,7 @@ namespace polysat { SASSERT(cl->size() == 2); } - // 8 * x + 3 == 0 is unsat + // 8 * x + 3 == 0 or 8 * x + 5 == 0 is unsat static void test_parity1() { scoped_solver s(__func__); auto x = s.var(s.add_var(8)); @@ -642,7 +642,7 @@ namespace polysat { s.expect_unsat(); } - // 8 * u * x + 3 == 0 is unsat + // 8 * u * x + 3 == 0 or 8 * u * x + 5 == 0 is unsat static void test_parity1b() { scoped_solver s(__func__); auto u = s.var(s.add_var(8)); @@ -656,7 +656,7 @@ namespace polysat { s.expect_unsat(); } - // 8 * x + 4 == 0 is unsat + // 8 * x + 2 == 0 or 8 * x + 4 == 0 is unsat static void test_parity2() { scoped_solver s(__func__); auto x = s.var(s.add_var(8)); @@ -667,7 +667,7 @@ namespace polysat { s.expect_unsat(); } - // x * y + 4 == 0 & 16 divides y is unsat + // (x * y + 4 == 0 or x * y + 2 == 0) & 16 divides y is unsat static void test_parity3() { scoped_solver s(__func__); auto x = s.var(s.add_var(8)); @@ -678,6 +678,15 @@ namespace polysat { s.expect_unsat(); } + static void test_parity4() { + scoped_solver s(__func__); + auto x = s.var(s.add_var(8)); + auto y = s.var(s.add_var(8)); + s.add_eq(x * y + 2); + s.add_clause({ s.parity(y, 4), s.parity(y, 8) }, false); + s.check(); + s.expect_unsat(); + } /** * Check unsat of: @@ -1635,7 +1644,8 @@ void tst_polysat() { #if 1 // Enable this block to run a single unit test with detailed output. collect_test_records = false; test_max_conflicts = 50; - test_polysat::test_parity1(); + test_polysat::test_parity4(); +// test_polysat::test_parity1(); // test_polysat::test_parity1b(); // test_polysat::test_parity2(); // test_polysat::test_parity3(); From c27bd0d6508f3febcc8734622ba205e766ba843d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2022 14:58:37 -0800 Subject: [PATCH 24/44] added try_factor Signed-off-by: Nikolaj Bjorner --- src/math/polysat/saturation.cpp | 71 +++++++++++++++++++++++++++------ src/math/polysat/saturation.h | 4 ++ 2 files changed, 63 insertions(+), 12 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index ae9b587a8..e38ce22c7 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -34,12 +34,13 @@ namespace polysat { void saturation::perform(pvar v, conflict& core) { for (auto c : core) - if (perform(v, c, core)) - return; + if (perform(v, c, core)) { + IF_VERBOSE(0, verbose_stream() << m_rule << " v" << v << " " << c << "\n"); + return; + } } bool saturation::perform(pvar v, signed_constraint const& c, conflict& core) { - IF_VERBOSE(0, verbose_stream() << v << " " << c << " " << c.is_currently_true(s) << "\n"); if (!c->is_ule()) return false; if (c.is_currently_true(s)) @@ -223,6 +224,18 @@ namespace polysat { return i.rhs() == y && i.lhs() == a * s.var(x) + b; } + + bool saturation::is_Y_l_AxB(pvar x, inequality const& i, pdd& y, pdd& a, pdd& b) { + y = i.lhs(); + pdd aa = a, bb = b; + return i.rhs().degree(x) == 1 && (i.rhs().factor(x, 1, aa, bb), aa == a && bb == b); + } + + bool saturation::verify_Y_l_AxB(pvar x, inequality const& i, pdd const& y, pdd const& a, pdd& b) { + return i.lhs() == y && i.rhs() == a * s.var(x) + b; + } + + /** * Match [x] a*x + b <= y, val(y) = 0 */ @@ -561,7 +574,7 @@ namespace polysat { // // NSB review: should we handle cases where k_val >= 2^{K-1}, but exploit that x*y = 0 iff -x*y = 0? // - IF_VERBOSE(0, verbose_stream() << "mult-bounds2 " << Y << " " << axb_l_y.as_signed_constraint() << " " << u_l_k.as_signed_constraint() << " \n"); + // IF_VERBOSE(0, verbose_stream() << "mult-bounds2 " << Y << " " << axb_l_y.as_signed_constraint() << " " << u_l_k.as_signed_constraint() << " \n"); rational bound = ceil(rational::power_of_two(m.power_of_2()) / k_val); if (prop2(d, s.uge(Y, bound))) return true; @@ -569,8 +582,8 @@ namespace polysat { return true; } - IF_VERBOSE(0, verbose_stream() << "mult-bounds1 " << a << " " << axb_l_y.as_signed_constraint() << " \n"); - IF_VERBOSE(0, verbose_stream() << core << "\n"); + // IF_VERBOSE(0, verbose_stream() << "mult-bounds1 " << a << " " << axb_l_y.as_signed_constraint() << " \n"); + // IF_VERBOSE(0, verbose_stream() << core << "\n"); if (prop1(s.umul_ovfl(a, X))) return true; if (prop1(s.umul_ovfl(a, -X))) @@ -638,8 +651,6 @@ namespace polysat { */ bool saturation::try_parity(pvar x, conflict& core, inequality const& axb_l_y) { set_rule("[x] a*x + b = 0 => (odd(a) & odd(x) <=> odd(b))"); - - IF_VERBOSE(0, verbose_stream() << "try parity " << axb_l_y.as_signed_constraint() << "\n"); auto& m = s.var2pdd(x); unsigned N = m.power_of_2(); pdd y = m.zero(); @@ -652,6 +663,8 @@ namespace polysat { return false; if (a.is_one() && (-b).is_var()) // y == x return false; + if (a.is_one()) + return false; signed_constraint b_is_odd = s.odd(b); signed_constraint a_is_odd = s.odd(a); signed_constraint x_is_odd = s.odd(X); @@ -783,10 +796,44 @@ namespace polysat { */ bool saturation::try_factor_equality(pvar x, conflict& core, inequality const& a_l_b) { - // search for abx+p pattern in a_l_b.lhs() - // search for ax + r = 0 equality in core (or in search but maybe not needed) - // replace abx by -rb in patterns on either a_l_b.lhs() or a_l_b.rhs() or both if available to form new implied - // literal wtihout occurrence of x + auto& m = s.var2pdd(x); + unsigned N = m.power_of_2(); + pdd y = m.zero(); + pdd a = m.zero(); + pdd b = m.zero(); + pdd y2 = m.zero(); + pdd a2 = m.zero(); + pdd b2 = m.zero(); + pdd X = s.var(x); + bool is_axb_l_y = is_AxB_l_Y(x, a_l_b, a, b, y); + bool is_y_l_axb = !is_axb_l_y && is_Y_l_AxB(x, a_l_b, y, a, b); + + + if (!is_axb_l_y && !is_y_l_axb) + return false; + + if (a.is_val()) + return false; + + for (auto c : core) { + if (!c->is_ule()) + continue; + auto i = inequality::from_ule(c); + if (i.is_strict()) + continue; + if (!is_AxB_eq_0(x, i, a2, b2, y2)) + continue; + if (a != a2) { + IF_VERBOSE(0, verbose_stream() << "misaligned coefficients " << a << " vs " << a2 << "\n"); + continue; // punt on more general case for first iteration. + } + m_lemma.reset(); + m_lemma.insert(~s.eq(y2)); + m_lemma.insert(~c); + IF_VERBOSE(0, verbose_stream() << "factor equality " << a_l_b.as_signed_constraint() << "\n"); + if (propagate(core, a_l_b, is_axb_l_y ? s.ule(b - b2, y) : s.ule(y, b - b2))) + return true; + } return false; } /* diff --git a/src/math/polysat/saturation.h b/src/math/polysat/saturation.h index bb169bc44..ec53b89bc 100644 --- a/src/math/polysat/saturation.h +++ b/src/math/polysat/saturation.h @@ -79,6 +79,10 @@ namespace polysat { bool is_AxB_l_Y(pvar x, inequality const& c, pdd& a, pdd& b, pdd& y); bool verify_AxB_l_Y(pvar x, inequality const& c, pdd const& a, pdd const& b, pdd const& y); + // c := Y ~ Ax + B + bool is_Y_l_AxB(pvar x, inequality const& c, pdd& y, pdd& a, pdd& b); + bool verify_Y_l_AxB(pvar x, inequality const& c, pdd const& y, pdd const& a, pdd& b); + // c := Ax + B ~ Y, val(Y) = 0 bool is_AxB_eq_0(pvar x, inequality const& c, pdd& a, pdd& b, pdd& y); bool verify_AxB_eq_0(pvar x, inequality const& c, pdd const& a, pdd const& b, pdd const& y); From d09252373385c43f76088855307499fdd6d9dfde Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Dec 2022 10:51:21 -0800 Subject: [PATCH 25/44] bugfixes to try_factor_equality Signed-off-by: Nikolaj Bjorner --- src/math/polysat/constraint.h | 2 ++ src/math/polysat/saturation.cpp | 54 +++++++++++++++++++++------------ src/math/polysat/viable.cpp | 3 ++ 3 files changed, 39 insertions(+), 20 deletions(-) diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 90d86f4f6..a54f649a7 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -234,4 +234,6 @@ namespace polysat { inline std::ostream& operator<<(std::ostream& out, constraint_pp const& p) { return p.display(out); } + inline std::ostream& operator<<(std::ostream& out, inequality const& i) { return out << i.as_signed_constraint(); } + } diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index e38ce22c7..7e877c8ba 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -574,7 +574,7 @@ namespace polysat { // // NSB review: should we handle cases where k_val >= 2^{K-1}, but exploit that x*y = 0 iff -x*y = 0? // - // IF_VERBOSE(0, verbose_stream() << "mult-bounds2 " << Y << " " << axb_l_y.as_signed_constraint() << " " << u_l_k.as_signed_constraint() << " \n"); + // IF_VERBOSE(0, verbose_stream() << "mult-bounds2 " << Y << " " << axb_l_y << " " << u_l_k<< " \n"); rational bound = ceil(rational::power_of_two(m.power_of_2()) / k_val); if (prop2(d, s.uge(Y, bound))) return true; @@ -582,7 +582,7 @@ namespace polysat { return true; } - // IF_VERBOSE(0, verbose_stream() << "mult-bounds1 " << a << " " << axb_l_y.as_signed_constraint() << " \n"); + // IF_VERBOSE(0, verbose_stream() << "mult-bounds1 " << a << " " << axb_l_y << " \n"); // IF_VERBOSE(0, verbose_stream() << core << "\n"); if (prop1(s.umul_ovfl(a, X))) return true; @@ -798,21 +798,20 @@ namespace polysat { bool saturation::try_factor_equality(pvar x, conflict& core, inequality const& a_l_b) { auto& m = s.var2pdd(x); unsigned N = m.power_of_2(); - pdd y = m.zero(); - pdd a = m.zero(); - pdd b = m.zero(); - pdd y2 = m.zero(); - pdd a2 = m.zero(); - pdd b2 = m.zero(); - pdd X = s.var(x); - bool is_axb_l_y = is_AxB_l_Y(x, a_l_b, a, b, y); - bool is_y_l_axb = !is_axb_l_y && is_Y_l_AxB(x, a_l_b, y, a, b); - + pdd y1 = m.zero(); + pdd a1 = m.zero(); + pdd b1 = m.zero(); + pdd a2 = a1, b2 = b1, y2 = y1, a3 = a2, b3 = b2, y3 = y2; + bool is_axb_l_y = is_AxB_l_Y(x, a_l_b, a1, b1, y1); + bool is_y_l_axb = is_Y_l_AxB(x, a_l_b, y2, a2, b2); + if (!a_l_b.is_strict() && a_l_b.rhs().is_zero()) + return false; + if (!is_axb_l_y && !is_y_l_axb) return false; - if (a.is_val()) + if (a1.is_val() && a2.is_val()) return false; for (auto c : core) { @@ -821,17 +820,32 @@ namespace polysat { auto i = inequality::from_ule(c); if (i.is_strict()) continue; - if (!is_AxB_eq_0(x, i, a2, b2, y2)) + if (!is_AxB_eq_0(x, i, a3, b3, y3)) continue; - if (a != a2) { - IF_VERBOSE(0, verbose_stream() << "misaligned coefficients " << a << " vs " << a2 << "\n"); - continue; // punt on more general case for first iteration. + if (c == a_l_b.as_signed_constraint()) + continue; + pdd lhs = i.lhs(); + pdd rhs = i.rhs(); + bool change = false; + + if (is_axb_l_y && a1 == a3) { + change = true; + lhs = b3 - b1; } + if (is_y_l_axb && a2 == a3) { + change = true; + rhs = b3 - b2; + } + if (!change) { + IF_VERBOSE(0, verbose_stream() << "missed factor equality " << c << " " << a_l_b << "\n"); + continue; + } + signed_constraint conseq = i.is_strict() ? s.ult(lhs, rhs) : s.ule(lhs, rhs); m_lemma.reset(); - m_lemma.insert(~s.eq(y2)); + m_lemma.insert(~s.eq(y3)); m_lemma.insert(~c); - IF_VERBOSE(0, verbose_stream() << "factor equality " << a_l_b.as_signed_constraint() << "\n"); - if (propagate(core, a_l_b, is_axb_l_y ? s.ule(b - b2, y) : s.ule(y, b - b2))) + IF_VERBOSE(0, verbose_stream() << "factor equality " << a_l_b << "\n"); + if (propagate(core, a_l_b, conseq)) return true; } return false; diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 92d63173e..617495f20 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -707,6 +707,8 @@ namespace polysat { n = n1; } + verbose_stream() << e->interval << " " << e->side_cond << " " << e->src << ";\n"; + if (!e->interval.is_full()) { auto const& hi = e->interval.hi(); auto const& next_lo = n->interval.lo(); @@ -726,6 +728,7 @@ namespace polysat { while (e != first); SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false || s.lit2cnstr(lit).is_currently_false(s); })); + core.add_lemma("viable", lemma.build()); core.logger().log(inf_fi(*this, v)); return true; From 5a27ae6b5366aa529d6215550881d783b52daa19 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Dec 2022 12:56:21 -0800 Subject: [PATCH 26/44] disable tangent lemma, which appears to be counter-productive Signed-off-by: Nikolaj Bjorner --- src/math/polysat/saturation.cpp | 2 +- src/math/polysat/viable.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 7e877c8ba..40ecdb547 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -60,7 +60,7 @@ namespace polysat { return true; if (try_y_l_ax_and_x_l_z(v, core, i)) return true; - if (try_tangent(v, core, i)) + if (false && try_tangent(v, core, i)) return true; return false; } diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 617495f20..56ff926d7 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -707,7 +707,7 @@ namespace polysat { n = n1; } - verbose_stream() << e->interval << " " << e->side_cond << " " << e->src << ";\n"; + // verbose_stream() << e->interval << " " << e->side_cond << " " << e->src << ";\n"; if (!e->interval.is_full()) { auto const& hi = e->interval.hi(); From 9feefa4c0a57907d6f02e155cfb2a21db29bcb16 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 12 Dec 2022 11:47:27 +0100 Subject: [PATCH 27/44] Remove clause methods that should not be used --- src/math/polysat/clause.cpp | 14 -------------- src/math/polysat/clause.h | 4 ---- 2 files changed, 18 deletions(-) diff --git a/src/math/polysat/clause.cpp b/src/math/polysat/clause.cpp index e0604f807..0c3df0704 100644 --- a/src/math/polysat/clause.cpp +++ b/src/math/polysat/clause.cpp @@ -28,20 +28,6 @@ namespace polysat { return alloc(clause, std::move(literals)); } - bool clause::is_always_false(solver& s) const { - return all_of(m_literals, [&s](sat::literal lit) { - signed_constraint c = s.m_constraints.lookup(lit); - return c.is_always_false(); - }); - } - - bool clause::is_currently_false(solver& s) const { - return all_of(m_literals, [&s](sat::literal lit) { - signed_constraint c = s.m_constraints.lookup(lit); - return c.is_currently_false(s); - }); - } - std::ostream& clause::display(std::ostream& out) const { bool first = true; for (auto lit : *this) { diff --git a/src/math/polysat/clause.h b/src/math/polysat/clause.h index 029df4b7a..6103ef7d6 100644 --- a/src/math/polysat/clause.h +++ b/src/math/polysat/clause.h @@ -68,10 +68,6 @@ namespace polysat { const_iterator begin() const { return m_literals.begin(); } const_iterator end() const { return m_literals.end(); } - // evaluates under pvar assignment - bool is_always_false(solver& s) const; - bool is_currently_false(solver& s) const; - std::ostream& display(std::ostream& out) const; void set_redundant(bool r) { m_redundant = r; } From b1271ac7fb9eccb74c68916c7da1b2ef0d7bee8b Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 12 Dec 2022 11:52:45 +0100 Subject: [PATCH 28/44] Check for missed boolean propagations --- src/math/polysat/solver.cpp | 28 +++++++++++++++++++++++++++- src/math/polysat/solver.h | 3 ++- 2 files changed, 29 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 366156989..d1b46b4d2 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -205,6 +205,7 @@ namespace polysat { if (!is_conflict()) linear_propagate(); SASSERT(wlist_invariant()); + SASSERT(bool_watch_invariant()); SASSERT(assignment_invariant()); } @@ -217,6 +218,7 @@ namespace polysat { signed_constraint c = lit2cnstr(lit); activate_constraint(c); auto& wlist = m_bvars.watch(~lit); + LOG("wlist[" << ~lit << "]: " << wlist); unsigned i = 0, j = 0, sz = wlist.size(); for (; i < sz && !is_conflict(); ++i) if (!propagate(lit, *wlist[i])) @@ -1364,7 +1366,7 @@ namespace polysat { /** * Check that two variables of each constraint are watched. */ - bool solver::wlist_invariant() { + bool solver::wlist_invariant() const { #if 0 for (pvar v = 0; v < m_value.size(); ++v) { std::stringstream s; @@ -1378,6 +1380,7 @@ namespace polysat { for (unsigned i = m_qhead; i < m_search.size(); ++i) if (m_search[i].is_boolean()) skip.insert(m_search[i].lit().var()); + SASSERT(is_conflict() || skip.empty()); // after propagation we either finished the queue or we are in a conflict for (auto c : m_constraints) { if (skip.contains(c->bvar())) continue; @@ -1403,6 +1406,29 @@ namespace polysat { return true; } + bool solver::bool_watch_invariant() const { + if (is_conflict()) // propagation may be unfinished if a conflict was discovered + return true; + // Check for missed boolean propagations: no clause should have exactly one unassigned literal, unless it is already true. + for (auto const& cls : m_constraints.clauses()) { + for (auto const& clref : cls) { + clause const& cl = *clref; + bool const is_true = any_of(cl, [&](auto lit) { return m_bvars.is_true(lit); }); + if (is_true) + continue; + size_t const undefs = count_if(cl, [&](auto lit) { return !m_bvars.is_assigned(lit); }); + if (undefs == 1) { + LOG("Missed boolean propagation of clause: " << cl); + for (sat::literal lit : cl) { + LOG(" " << lit_pp(*this, lit)); + } + } + SASSERT(undefs != 1); + } + } + return true; + } + pdd solver::subst(pdd const& p) const { return assignment().apply_to(p); } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index a550f35c0..9b1dba28e 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -303,7 +303,8 @@ namespace polysat { bool invariant(); static bool invariant(signed_constraints const& cs); - bool wlist_invariant(); + bool wlist_invariant() const; + bool bool_watch_invariant() const; bool assignment_invariant(); bool verify_sat(); From 1eb8eb560b9cce66778e902fc7d2f9312844fb80 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 12 Dec 2022 13:37:28 +0100 Subject: [PATCH 29/44] test_ineq2 --- src/test/polysat.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index c1808d9a4..d646a49b7 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -712,7 +712,7 @@ namespace polysat { * n*q1 = a - b 3*1 == 3 - 0 * n*q2 + r2 = c*a - c*b 3*0 + 1 == 11*3 - 11*0 (= 33 = 1 mod 32) * n > r2 > 0 3 > 1 > 0 - * It is actually satisfiable. + * It is actually satisfiable, e.g.: { {n, 3}, {q1, 1}, {a, 3}, {b, 0}, {c, 11}, {q2, 0}, {r2, 1} } (not a unique solution) */ static void test_ineq2() { scoped_solver s(__func__); @@ -728,7 +728,7 @@ namespace polysat { s.add_ult(r2, n); s.add_diseq(r2); s.check(); - s.expect_sat({ {n, 3}, {q1, 1}, {a, 3}, {b, 0}, {c, 11}, {q2, 0}, {r2, 1} }); + s.expect_sat(); } /** @@ -1644,12 +1644,12 @@ void tst_polysat() { #if 1 // Enable this block to run a single unit test with detailed output. collect_test_records = false; test_max_conflicts = 50; - test_polysat::test_parity4(); -// test_polysat::test_parity1(); + // test_polysat::test_parity1(); // test_polysat::test_parity1b(); // test_polysat::test_parity2(); // test_polysat::test_parity3(); - // test_polysat::test_ineq2(); + // test_polysat::test_parity4(); + test_polysat::test_ineq2(); return; #endif From 759d8f2a94447143a593e4a808249c607aadf519 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 12 Dec 2022 13:50:15 +0100 Subject: [PATCH 30/44] Fix watching of boolean literals --- src/math/polysat/constraint_manager.cpp | 110 ++++++++++++++++++------ src/math/polysat/constraint_manager.h | 1 + 2 files changed, 85 insertions(+), 26 deletions(-) diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp index fefc113ee..fb32347c9 100644 --- a/src/math/polysat/constraint_manager.cpp +++ b/src/math/polysat/constraint_manager.cpp @@ -85,42 +85,100 @@ namespace polysat { } } - // find literals that are not propagated to false - // if clause is unsat then assign arbitrary - // solver handles unsat clauses by creating a conflict. - // solver also can propagate, but need to check that it does indeed. + /** + * Move literals to be watched to the front of the clause. + */ + void constraint_manager::normalize_watch(clause& cl) { + SASSERT(cl.size() > 1); + + // A literal may be watched if there is no unwatched literal at higher level, + // where true and unassigned literals are considered at infinite level. + // We prefer true literals to unassigned literals. + auto get_watch_level = [&](sat::literal lit) -> unsigned { + switch (s.m_bvars.value(lit)) { + case l_false: + return s.m_bvars.level(lit); + case l_true: + return UINT_MAX; + case l_undef: + return UINT_MAX - 1; + } + UNREACHABLE(); + return 0; + }; + + unsigned lvl0 = get_watch_level(cl[0]); + unsigned lvl1 = get_watch_level(cl[1]); + if (lvl0 < lvl1) { + std::swap(lvl0, lvl1); + std::swap(cl[0], cl[1]); + } + SASSERT(lvl0 >= lvl1); + for (unsigned i = 2; i < cl.size(); ++i) { + sat::literal const lit = cl[i]; + unsigned const lvl = get_watch_level(lit); + if (lvl > lvl0) { + cl[i] = cl[1]; + cl[1] = cl[0]; + lvl1 = lvl0; + cl[0] = lit; + lvl0 = lvl; + } + else if (lvl > lvl1) { + cl[i] = cl[1]; + cl[1] = lit; + lvl1 = lvl; + } + SASSERT_EQ(lvl0, get_watch_level(cl[0])); + SASSERT_EQ(lvl1, get_watch_level(cl[1])); + SASSERT(lvl0 >= lvl1 && lvl1 >= get_watch_level(cl[i])); + } + SASSERT(all_of(cl, [&](auto lit) { return get_watch_level(lit) <= get_watch_level(cl[0]); })); + SASSERT(std::all_of(cl.begin() + 1, cl.end(), [&](auto lit) { return get_watch_level(lit) <= get_watch_level(cl[1]); })); + } + void constraint_manager::watch(clause& cl, bool value_propagate) { if (cl.empty()) return; - bool first = true; - for (unsigned i = 0; i < cl.size(); ++i) { - if (s.m_bvars.is_false(cl[i])) - continue; - signed_constraint sc = s.lit2cnstr(cl[i]); - if (value_propagate && sc.is_currently_false(s)) { - if (s.m_bvars.is_true(cl[i])) { - s.set_conflict(sc); - return; + if (value_propagate) { +#if 0 // this should be already done with insert_eval when constructing the clause (maybe not for non-redundant clauses?) + for (sat::literal lit : cl) { + if (s.m_bvars.is_false(lit)) + continue; + signed_constraint sc = s.lit2cnstr(lit); + if (sc.is_currently_false(s)) { + if (s.m_bvars.is_true(lit)) { + s.set_conflict(sc); + return; + } + s.assign_eval(~lit); } - s.assign_eval(~cl[i]); - continue; } - - s.m_bvars.watch(cl[i]).push_back(&cl); - std::swap(cl[!first], cl[i]); - if (!first) - return; - first = false; +#endif } - if (first) - s.m_bvars.watch(cl[0]).push_back(&cl); - if (cl.size() > 1) - s.m_bvars.watch(cl[1]).push_back(&cl); + if (cl.size() == 1) { + if (s.m_bvars.is_false(cl[0])) + s.set_conflict(cl); + else if (!s.m_bvars.is_assigned(cl[0])) + s.assign_propagate(cl[0], cl); + return; + } + + normalize_watch(cl); + + s.m_bvars.watch(cl[0]).push_back(&cl); + s.m_bvars.watch(cl[1]).push_back(&cl); + if (s.m_bvars.is_true(cl[0])) return; - if (first) + SASSERT(!s.m_bvars.is_true(cl[1])); + if (!s.m_bvars.is_false(cl[1])) { + SASSERT(!s.m_bvars.is_assigned(cl[0]) && !s.m_bvars.is_assigned(cl[1])); + return; + } + if (s.m_bvars.is_false(cl[0])) s.set_conflict(cl); else s.assign_propagate(cl[0], cl); diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h index 9871c5c6c..1d6065f41 100644 --- a/src/math/polysat/constraint_manager.h +++ b/src/math/polysat/constraint_manager.h @@ -74,6 +74,7 @@ namespace polysat { void gc_constraints(); void gc_clauses(); + void normalize_watch(clause& cl); void watch(clause& cl, bool value_propagate); void unwatch(clause& cl); From 587e77648af6c5ef2327b0b31b54486d846e7ece Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 12 Dec 2022 13:57:30 +0100 Subject: [PATCH 31/44] Keep value_propagate for now --- src/math/polysat/constraint_manager.cpp | 3 ++- src/math/polysat/umul_ovfl_constraint.cpp | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp index fb32347c9..7e9d93257 100644 --- a/src/math/polysat/constraint_manager.cpp +++ b/src/math/polysat/constraint_manager.cpp @@ -142,7 +142,8 @@ namespace polysat { return; if (value_propagate) { -#if 0 // this should be already done with insert_eval when constructing the clause (maybe not for non-redundant clauses?) +#if 1 // this should be already done with insert_eval when constructing the clause (maybe not for non-redundant clauses?) + // (this loop also masks the mistake of calling clause_builder::insert instead of clause_builder::insert_eval) for (sat::literal lit : cl) { if (s.m_bvars.is_false(lit)) continue; diff --git a/src/math/polysat/umul_ovfl_constraint.cpp b/src/math/polysat/umul_ovfl_constraint.cpp index 69c497f6b..ea7d28904 100644 --- a/src/math/polysat/umul_ovfl_constraint.cpp +++ b/src/math/polysat/umul_ovfl_constraint.cpp @@ -120,8 +120,8 @@ namespace polysat { SASSERT(bound * p.val() > max); SASSERT((bound - 1) * p.val() <= max); clause_builder cb(s); - cb.insert(~sc); - cb.insert(~premise); + cb.insert_eval(~sc); + cb.insert_eval(~premise); cb.insert(conseq); clause_ref just = cb.build(); SASSERT(just); From 917e1b6a4c33beed3417a882936db6950620a018 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 12 Dec 2022 14:46:38 +0100 Subject: [PATCH 32/44] When adding clauses, prioritize bool-propagation over evaluation See test_band1 and clause: v2 == v0 & v1 --> v2 <= 0 --- src/math/polysat/conflict.cpp | 3 +++ src/math/polysat/constraint_manager.cpp | 28 +++++++++++++++++++++++-- 2 files changed, 29 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index e03ace554..101d821d6 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -185,6 +185,7 @@ namespace polysat { } void conflict::init(signed_constraint c) { + LOG("Conflict: constraint " << lit_pp(s, c)); SASSERT(empty()); m_level = s.m_level; m_narrow_queue.push_back(c.blit()); // if the conflict is only due to a missed propagation of c @@ -217,6 +218,7 @@ namespace polysat { } void conflict::init(clause const& cl) { + LOG("Conflict: clause " << cl); SASSERT(empty()); m_level = s.m_level; for (auto lit : cl) { @@ -229,6 +231,7 @@ namespace polysat { } void conflict::init(pvar v, bool by_viable_fallback) { + LOG("Conflict: viable v" << v); SASSERT(empty()); m_level = s.m_level; if (by_viable_fallback) { diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp index 7e9d93257..9ec04ef60 100644 --- a/src/math/polysat/constraint_manager.cpp +++ b/src/math/polysat/constraint_manager.cpp @@ -142,8 +142,32 @@ namespace polysat { return; if (value_propagate) { -#if 1 // this should be already done with insert_eval when constructing the clause (maybe not for non-redundant clauses?) - // (this loop also masks the mistake of calling clause_builder::insert instead of clause_builder::insert_eval) +#if 1 + // First, try to bool-propagate. + // Otherwise, we might get a clause-conflict and a missed propagation after resolving the conflict. + // With this, we will get a constraint-conflict instead. + // TODO: maybe it makes sense to choose bool vs. eval depending on which has the lower level? + sat::literal undef_lit = sat::null_literal; + for (sat::literal lit : cl) { + if (s.m_bvars.is_false(lit)) + continue; + if (s.m_bvars.is_true(lit)) { + undef_lit = sat::null_literal; + break; + } + SASSERT(!s.m_bvars.is_assigned(lit)); + if (undef_lit == sat::null_literal) + undef_lit = lit; + else { + undef_lit = sat::null_literal; + break; + } + } + if (undef_lit != sat::null_literal) + s.assign_propagate(undef_lit, cl); + + // this should be already done with insert_eval when constructing the clause (maybe not for non-redundant clauses?) + // (this loop also masks the mistake of calling clause_builder::insert instead of clause_builder::insert_eval) for (sat::literal lit : cl) { if (s.m_bvars.is_false(lit)) continue; From 9f1f949d9dbb5eb6643644d7ff28faa35ed44722 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 12 Dec 2022 14:51:04 +0100 Subject: [PATCH 33/44] tests --- src/test/polysat.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index d646a49b7..4e2a32440 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -1243,7 +1243,7 @@ namespace polysat { // x*y <= b & a <= x & !Omega(x*y) => a*y <= b static void test_ineq_non_axiom4(unsigned bw, unsigned i) { auto const bound = rational::power_of_two(bw - 1); - scoped_solver s(std::string(__func__) + " perm=" + std::to_string(i)); + scoped_solver s(concat(__func__, " bw=", bw, " perm=", i)); LOG("permutation: " << i); auto x = s.var(s.add_var(bw)); auto y = s.var(s.add_var(bw)); @@ -1648,8 +1648,10 @@ void tst_polysat() { // test_polysat::test_parity1b(); // test_polysat::test_parity2(); // test_polysat::test_parity3(); - // test_polysat::test_parity4(); - test_polysat::test_ineq2(); + test_polysat::test_parity4(); + // test_polysat::test_ineq2(); + // test_polysat::test_ineq_non_axiom4(32, 3); // stuck in viable refinement loop + // test_polysat::test_band1(); return; #endif @@ -1669,6 +1671,7 @@ void tst_polysat() { RUN(test_polysat::test_parity1b()); RUN(test_polysat::test_parity2()); RUN(test_polysat::test_parity3()); + RUN(test_polysat::test_parity4()); RUN(test_polysat::test_clause_simplify1()); From eda65344537cb3da0d58bf98f91e1705385bb5eb Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 12 Dec 2022 16:41:18 +0100 Subject: [PATCH 34/44] more readable intervals --- src/math/polysat/solver.cpp | 7 +------ src/math/polysat/solver.h | 3 ++- src/math/polysat/viable.cpp | 2 +- 3 files changed, 4 insertions(+), 8 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index d1b46b4d2..b7fe62a27 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -1335,12 +1335,7 @@ namespace polysat { } std::ostream& num_pp::display(std::ostream& out) const { - rational const& p = rational::power_of_two(s.size(var)); - if (val > mod(-val, p)) - out << -mod(-val, p); - else - out << val; - return out; + return out << dd::val_pp(s.var2pdd(var), val, require_parens); } void solver::collect_statistics(statistics& st) const { diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 9b1dba28e..7ebc273a8 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -542,8 +542,9 @@ namespace polysat { solver const& s; pvar var; rational const& val; + bool require_parens; public: - num_pp(solver const& s, pvar var, rational const& val): s(s), var(var), val(val) {} + num_pp(solver const& s, pvar var, rational const& val, bool require_parens = false): s(s), var(var), val(val), require_parens(require_parens) {} std::ostream& display(std::ostream& out) const; }; diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 56ff926d7..e1c1f17b2 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -376,7 +376,7 @@ namespace polysat { lo = val - lambda_l; increase_hi(hi); } - LOG("forbidden interval v" << v << " " << val << " " << e->coeff << " * " << e->interval << " [" << lo << ", " << hi << "["); + LOG("forbidden interval v" << v << " " << num_pp(s, v, val) << " " << num_pp(s, v, e->coeff, true) << " * " << e->interval << " [" << num_pp(s, v, lo) << ", " << num_pp(s, v, hi) << "["); SASSERT(hi <= mod_value); bool full = (lo == 0 && hi == mod_value); if (hi == mod_value) From 4a2379c23dfc93e91ca7c58dbe75812709bb62d5 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 12 Dec 2022 17:48:23 +0100 Subject: [PATCH 35/44] Add unit test for refinement loop in bench6 --- src/test/polysat.cpp | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 4e2a32440..d6930d4dc 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -1510,6 +1510,17 @@ namespace polysat { s.expect_sat({{a, 5}}); } + static void test_bench6_viable() { + scoped_solver s(__func__); + rational coeff("12737129816104781496592808350955669863859698313220462044340334240870444260393"); + auto a = s.var(s.add_var(256)); + auto b = s.var(s.add_var(256)); + s.add_eq(4 * b - coeff * a); + s.add_eq(b - 1); + // s.add_eq(a - 100); + s.check(); + } + }; // class test_polysat @@ -1648,10 +1659,11 @@ void tst_polysat() { // test_polysat::test_parity1b(); // test_polysat::test_parity2(); // test_polysat::test_parity3(); - test_polysat::test_parity4(); + // test_polysat::test_parity4(); // test_polysat::test_ineq2(); // test_polysat::test_ineq_non_axiom4(32, 3); // stuck in viable refinement loop // test_polysat::test_band1(); + test_polysat::test_bench6_viable(); return; #endif From 479e0e58eac9db7686c1f40b82eb515ee4833b44 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 12 Dec 2022 18:18:24 +0100 Subject: [PATCH 36/44] Better intervals for equations --- src/math/polysat/forbidden_intervals.cpp | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 960e55170..01b4eec8f 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -180,7 +180,7 @@ namespace polysat { SASSERT(b1.is_val()); SASSERT(b2.is_val()); - // a*v <= 0, a odd + // a*v + b <= 0, a odd if (match_zero(c, a1, b1, e1, a2, b2, e2, fi)) return true; // a*v + b > 0, a odd @@ -385,6 +385,9 @@ namespace polysat { * a*v <= 0, a odd * forbidden interval for v is [1,0[ * + * a*v + b <= 0, a odd + * forbidden interval for v is [n+1,n[ where n = -b * a^-1 + * * TODO: extend to * 2^k*a*v <= 0, a odd * (using periodic intervals?) @@ -395,12 +398,15 @@ namespace polysat { rational const & a2, pdd const& b2, pdd const& e2, fi_record& fi) { _last_function = __func__; - if (c.is_positive() && a1.is_odd() && b1.is_zero() && a2.is_zero() && b2.is_zero()) { + if (c.is_positive() && a1.is_odd() && a2.is_zero() && b2.is_zero()) { auto& m = e1.manager(); - rational lo_val(1); - auto lo = m.one(); - rational hi_val(0); - auto hi = m.zero(); + rational const& mod_value = m.two_to_N(); + rational a1_inv; + VERIFY(a1.mult_inverse(m.power_of_2(), a1_inv)); + rational hi_val = mod(-b1.val() * a1_inv, mod_value); + pdd hi = -e1 * a1_inv; + rational lo_val = mod(hi_val + 1, mod_value); + pdd lo = hi + 1; fi.coeff = 1; fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); if (b1 != e1) From a5f12e9d573a8a03de547e319d8ad43ea2a1b293 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Dec 2022 19:40:19 -0800 Subject: [PATCH 37/44] add parity constraint for disequality Signed-off-by: Nikolaj Bjorner --- src/math/polysat/conflict.cpp | 2 +- src/math/polysat/saturation.cpp | 43 ++++++++++++++++++++++++++++++++- src/math/polysat/saturation.h | 3 +++ 3 files changed, 46 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 101d821d6..51fd38f89 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -298,7 +298,7 @@ namespace polysat { void conflict::insert_vars(signed_constraint c) { for (pvar v : c->vars()) - if (s.is_assigned(v)) + if (s.is_assigned(v)) m_vars.insert(v); } diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 40ecdb547..8d6d7229a 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -35,7 +35,10 @@ namespace polysat { void saturation::perform(pvar v, conflict& core) { for (auto c : core) if (perform(v, c, core)) { - IF_VERBOSE(0, verbose_stream() << m_rule << " v" << v << " " << c << "\n"); + IF_VERBOSE(0, auto const& cl = core.lemmas().back(); + verbose_stream() << m_rule << " v" << v << " "; + for (auto lit : *cl) verbose_stream() << s.lit2cnstr(lit) << " "; + verbose_stream() << "\n"); return; } } @@ -50,6 +53,8 @@ namespace polysat { return true; if (try_parity(v, core, i)) return true; + if (try_parity_diseq(v, core, i)) + return true; if (try_factor_equality(v, core, i)) return true; if (try_ugt_x(v, core, i)) @@ -251,6 +256,16 @@ namespace polysat { return y.is_val() && y.val() == 0 && i.rhs() == y && i.lhs() == a * s.var(x) + b; } + bool saturation::is_AxB_diseq_0(pvar x, inequality const& i, pdd& a, pdd& b, pdd& y) { + if (!i.is_strict()) + return false; + y = i.lhs(); + rational y_val; + if (!s.try_eval(y, y_val) || y_val != 0) + return false; + return i.rhs().degree(x) == 1 && (i.rhs().factor(x, 1, a, b), true); + } + /** * Match [coeff*x] coeff*x*Y where x is a variable */ @@ -755,6 +770,32 @@ namespace polysat { return false; } + /** + * 2^{K-1}*x*y != 0 => odd(x) & odd(y) + * 2^k*x != 0 => parity(x) < K - k + * 2^k*x*y != 0 => parity(x) + parity(y) < K - k + */ + bool saturation::try_parity_diseq(pvar x, conflict& core, inequality const& axb_l_y) { + set_rule("[x] 2^k*x*y != 0 => parity(x) + parity(y) < K - k"); + auto& m = s.var2pdd(x); + unsigned N = m.power_of_2(); + pdd y = m.zero(); + pdd a = y, b = y, X = y; + if (!is_AxB_diseq_0(x, axb_l_y, a, b, y)) + return false; + if (!is_forced_eq(b, 0)) + return false; + auto coeff = a.leading_coefficient(); + if (coeff.is_odd()) + return false; + SASSERT(coeff != 0); + unsigned k = coeff.trailing_zeros(); + m_lemma.reset(); + m_lemma.insert_eval(~s.eq(y)); + m_lemma.insert_eval(~s.eq(b)); + return propagate(core, axb_l_y, ~s.parity(X, N - k)); + } + /** * a*x = 0 => a = 0 or even(x) * a*x = 0 => a = 0 or x = 0 or even(a) diff --git a/src/math/polysat/saturation.h b/src/math/polysat/saturation.h index ec53b89bc..267581517 100644 --- a/src/math/polysat/saturation.h +++ b/src/math/polysat/saturation.h @@ -47,6 +47,7 @@ namespace polysat { bool try_ugt_z(pvar z, conflict& core, inequality const& x_l_z0, inequality const& yz_l_xz, pdd const& y, pdd const& x); bool try_parity(pvar x, conflict& core, inequality const& axb_l_y); + bool try_parity_diseq(pvar x, conflict& core, inequality const& axb_l_y); bool try_mul_bounds(pvar x, conflict& core, inequality const& axb_l_y); bool try_factor_equality(pvar x, conflict& core, inequality const& a_l_b); bool try_mul_eq_1(pvar x, conflict& core, inequality const& axb_l_y); @@ -87,6 +88,8 @@ namespace polysat { bool is_AxB_eq_0(pvar x, inequality const& c, pdd& a, pdd& b, pdd& y); bool verify_AxB_eq_0(pvar x, inequality const& c, pdd const& a, pdd const& b, pdd const& y); + // c := Ax + B != Y, val(Y) = 0 + bool is_AxB_diseq_0(pvar x, inequality const& c, pdd& a, pdd& b, pdd& y); // c := Y*X ~ z*X bool is_YX_l_zX(pvar z, inequality const& c, pdd& x, pdd& y); From 6c7f5564968c704ad41f1baa0a16a13870e5abcd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Dec 2022 20:11:01 -0800 Subject: [PATCH 38/44] activate non-overflow bounds Signed-off-by: Nikolaj Bjorner --- src/math/polysat/umul_ovfl_constraint.cpp | 13 +++++++++++++ src/math/polysat/umul_ovfl_constraint.h | 1 + 2 files changed, 14 insertions(+) diff --git a/src/math/polysat/umul_ovfl_constraint.cpp b/src/math/polysat/umul_ovfl_constraint.cpp index ea7d28904..345541377 100644 --- a/src/math/polysat/umul_ovfl_constraint.cpp +++ b/src/math/polysat/umul_ovfl_constraint.cpp @@ -80,6 +80,9 @@ namespace polysat { if (is_always_true(is_positive, p1, q1)) return; + if (first) + activate(s, is_positive); + if (try_viable(s, is_positive, p(), q(), p1, q1)) return; @@ -91,6 +94,16 @@ namespace polysat { } + void umul_ovfl_constraint::activate(solver& s, bool is_positive) { + // TODO - remove to enable + return; + if (!is_positive) { + signed_constraint sc(this, is_positive); + s.add_clause(~sc, s.eq(p()), s.eq(q()), s.ule(p(), p()*q()), false); + s.add_clause(~sc, s.eq(p()), s.eq(q()), s.ule(q(), p()*q()), false); + } + } + /** * if p constant, q, propagate inequality */ diff --git a/src/math/polysat/umul_ovfl_constraint.h b/src/math/polysat/umul_ovfl_constraint.h index 1f2961f87..1595f0bd6 100644 --- a/src/math/polysat/umul_ovfl_constraint.h +++ b/src/math/polysat/umul_ovfl_constraint.h @@ -30,6 +30,7 @@ namespace polysat { static lbool eval(pdd const& p, pdd const& q); bool narrow_bound(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q); bool try_viable(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q); + void activate(solver& s, bool is_positive); public: ~umul_ovfl_constraint() override {} From 6f1e4283bb02713af227523eb25d7b5481968e2f Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 13 Dec 2022 11:42:52 +0100 Subject: [PATCH 39/44] Merge forbidden intervals for positive and negative equations --- src/math/polysat/forbidden_intervals.cpp | 61 +++++++----------------- src/math/polysat/forbidden_intervals.h | 5 -- 2 files changed, 16 insertions(+), 50 deletions(-) diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 01b4eec8f..33082f3b6 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -181,11 +181,10 @@ namespace polysat { SASSERT(b2.is_val()); // a*v + b <= 0, a odd + // a*v + b > 0, a odd if (match_zero(c, a1, b1, e1, a2, b2, e2, fi)) return true; - // a*v + b > 0, a odd - if (match_non_zero_linear(c, a1, b1, e1, a2, b2, e2, fi)) - return true; + if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi)) return true; if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi)) @@ -390,7 +389,7 @@ namespace polysat { * * TODO: extend to * 2^k*a*v <= 0, a odd - * (using periodic intervals?) + * (using intervals for the lower bits of v) */ bool forbidden_intervals::match_zero( signed_constraint const& c, @@ -398,52 +397,24 @@ namespace polysat { rational const & a2, pdd const& b2, pdd const& e2, fi_record& fi) { _last_function = __func__; - if (c.is_positive() && a1.is_odd() && a2.is_zero() && b2.is_zero()) { + if (a1.is_odd() && a2.is_zero() && b2.is_zero()) { auto& m = e1.manager(); rational const& mod_value = m.two_to_N(); rational a1_inv; VERIFY(a1.mult_inverse(m.power_of_2(), a1_inv)); - rational hi_val = mod(-b1.val() * a1_inv, mod_value); - pdd hi = -e1 * a1_inv; - rational lo_val = mod(hi_val + 1, mod_value); - pdd lo = hi + 1; - fi.coeff = 1; - fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); - if (b1 != e1) - fi.side_cond.push_back(s.eq(b1, e1)); - if (b2 != e2) - fi.side_cond.push_back(s.eq(b2, e2)); - return true; - } - return false; - } - /** - * a*v + b > 0, a odd - * - * TODO: extend to - * 2^k*a*v + b > 0, a odd - * (using periodic intervals?) - */ - bool forbidden_intervals::match_non_zero_linear( - signed_constraint const& c, - rational const & a1, pdd const& b1, pdd const& e1, - rational const & a2, pdd const& b2, pdd const& e2, - fi_record& fi) { - _last_function = __func__; - if (c.is_negative() && a1.is_odd() && a2.is_zero() && b2.is_zero()) { - // a*v + b > 0 - // <=> a*v + b != 0 - // <=> v + a^-1 * b != 0 - // <=> v != - a^-1 * b - auto& m = e1.manager(); - rational const& mod_value = m.two_to_N(); - rational a1_inv; - VERIFY(a1.mult_inverse(m.power_of_2(), a1_inv)); - rational lo_val(mod(-b1.val() * a1_inv, mod_value)); - auto lo = -e1 * a1_inv; - rational hi_val(mod(lo_val + 1, mod_value)); - auto hi = lo + 1; + // interval for a*v + b > 0 is [n,n+1[ where n = -b * a^-1 + rational lo_val = mod(-b1.val() * a1_inv, mod_value); + pdd lo = -e1 * a1_inv; + rational hi_val = mod(lo_val + 1, mod_value); + pdd hi = lo + 1; + + // interval for a*v + b <= 0 is the complement + if (c.is_positive()) { + std::swap(lo_val, hi_val); + std::swap(lo, hi); + } + fi.coeff = 1; fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); if (b1 != e1) diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index afe3130bf..9d5a6b393 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -73,11 +73,6 @@ namespace polysat { rational const & a2, pdd const& b2, pdd const& e2, fi_record& fi); - bool match_non_zero_linear(signed_constraint const& c, - rational const & a1, pdd const& b1, pdd const& e1, - rational const & a2, pdd const& b2, pdd const& e2, - fi_record& fi); - bool match_non_zero(signed_constraint const& c, rational const & a1, pdd const& b1, pdd const& e1, fi_record& fi); From a3c7a869cd72ca98fc16197edc1fd6bb19dba850 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 13 Dec 2022 11:47:21 +0100 Subject: [PATCH 40/44] bool_watch_invariant --- src/math/polysat/solver.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index b7fe62a27..96fbeeb5a 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -1404,7 +1404,9 @@ namespace polysat { bool solver::bool_watch_invariant() const { if (is_conflict()) // propagation may be unfinished if a conflict was discovered return true; - // Check for missed boolean propagations: no clause should have exactly one unassigned literal, unless it is already true. + // Check for missed boolean propagations: + // - no clause should have exactly one unassigned literal, unless it is already true. + // - no clause should be false for (auto const& cls : m_constraints.clauses()) { for (auto const& clref : cls) { clause const& cl = *clref; @@ -1419,6 +1421,8 @@ namespace polysat { } } SASSERT(undefs != 1); + bool const is_false = all_of(cl, [&](auto lit) { return m_bvars.is_false(lit); }); + SASSERT(!is_false); } } return true; From 519ebd8a8bd8bf9f7ef356d6e3179bc2bb36170c Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 13 Dec 2022 11:49:54 +0100 Subject: [PATCH 41/44] log and note --- src/math/polysat/solver.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 96fbeeb5a..def600bad 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -533,13 +533,15 @@ namespace polysat { using T = std::decay_t; if constexpr (std::is_same_v) { sat::literal lit = arg; - m_search.push_boolean(arg); + m_search.push_boolean(lit); m_trail.push_back(trail_instr_t::assign_bool_i); + LOG("Replay: " << lit); } else if constexpr (std::is_same_v) { pvar v = arg; m_search.push_assignment(v, m_value[v]); m_trail.push_back(trail_instr_t::assign_i); + LOG("Replay: " << assignment_pp(*this, v, m_value[v])); // TODO: are the viable sets propagated properly? // when substituting polynomials, it will now take into account the replayed variables, which may itself depend on previous propagations. // will we get into trouble with cyclic dependencies? @@ -553,6 +555,12 @@ namespace polysat { // then we get an assignment up to that dependency level. // each literal can only depend on entries with lower dependency level // (that is the invariant that propagations are justified by a prefix of the search stack.) + // Actually, cyclic dependencies probably don't happen: + // - viable restrictions only occur when all-but-one variable is set (or some vars are irrelevant... those might introduce additional fake dependencies) + // - we only replay propagations... so all new variable assignments are propagations (that depend on earlier decisions) + // - but now the replayed constraints may evaluate to true already and thus not give the forbidden intervals from before anymore... + // so maybe we miss some dependencies this way? a variable was propagated because of a constraint, but after replay the constraint evaluates to true and thus does not add an interval anymore. + // TODO: work out example to explain and test this } else static_assert(always_false::value, "non-exhaustive visitor"); @@ -1101,7 +1109,7 @@ namespace polysat { void solver::backjump(unsigned new_level) { SASSERT(new_level >= base_level()); if (m_level != new_level) { - LOG_H3("Backjumping to level " << new_level << " from level " << m_level); + LOG_H3("Backjumping to level " << new_level << " from level " << m_level << " (base_level: " << base_level() << ")"); pop_levels(m_level - new_level); } } From 434e794790b95c019693f5e77ab9f2c5cdae691e Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 13 Dec 2022 12:00:38 +0100 Subject: [PATCH 42/44] test --- src/test/polysat.cpp | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index d6930d4dc..b81c66352 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -678,10 +678,12 @@ namespace polysat { s.expect_unsat(); } - static void test_parity4() { - scoped_solver s(__func__); - auto x = s.var(s.add_var(8)); - auto y = s.var(s.add_var(8)); + // x*y + 2 == 0 + // parity(y) >= 4 || parity(y) >= 8 + static void test_parity4(unsigned bw = 8) { + scoped_solver s(concat(__func__, " bw=", bw)); + pdd x = s.var(s.add_var(bw)); + pdd y = s.var(s.add_var(bw)); s.add_eq(x * y + 2); s.add_clause({ s.parity(y, 4), s.parity(y, 8) }, false); s.check(); @@ -1659,11 +1661,13 @@ void tst_polysat() { // test_polysat::test_parity1b(); // test_polysat::test_parity2(); // test_polysat::test_parity3(); - // test_polysat::test_parity4(); + test_polysat::test_parity4(); + test_polysat::test_parity4(256); // test_polysat::test_ineq2(); // test_polysat::test_ineq_non_axiom4(32, 3); // stuck in viable refinement loop + // test_polysat::test_ineq_non_axiom4(32, 4); // stuck in viable refinement loop // test_polysat::test_band1(); - test_polysat::test_bench6_viable(); + // test_polysat::test_bench6_viable(); return; #endif @@ -1742,6 +1746,7 @@ void tst_polysat() { RUN(test_polysat::test_fi_nonzero()); RUN(test_polysat::test_fi_nonmax()); RUN(test_polysat::test_fi_disequal_mild()); + RUN(test_polysat::test_bench6_viable()); RUN(test_polysat::test_ineq_axiom1()); RUN(test_polysat::test_ineq_axiom2()); From 7e7cea54f4ff06e474f926e06a536e0a128de327 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 13 Dec 2022 15:02:45 +0100 Subject: [PATCH 43/44] Intervals from equality constraints: remove superfluous side constraints --- src/math/polysat/forbidden_intervals.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 33082f3b6..2a49b33f2 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -417,10 +417,6 @@ namespace polysat { fi.coeff = 1; fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); - if (b1 != e1) - fi.side_cond.push_back(s.eq(b1, e1)); - if (b2 != e2) - fi.side_cond.push_back(s.eq(b2, e2)); return true; } return false; From 1bc4313333c6155822e091d265aef88189fdd04d Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 13 Dec 2022 15:26:22 +0100 Subject: [PATCH 44/44] Fix unsoundness in previous commit --- src/math/polysat/forbidden_intervals.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 2a49b33f2..8e8131651 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -417,6 +417,9 @@ namespace polysat { fi.coeff = 1; fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); + // RHS == 0 is a precondition because we can only multiply with a^-1 in equations, not inequalities + if (b2 != e2) + fi.side_cond.push_back(s.eq(b2, e2)); return true; } return false;