From 9614e428a672efdc09363265a08acd24df56fda3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Mar 2023 08:41:22 -0700 Subject: [PATCH] wip: enabling reinit approach Signed-off-by: Nikolaj Bjorner --- src/math/polysat/constraint_manager.cpp | 1 + src/math/polysat/op_constraint.cpp | 8 ++- src/math/polysat/saturation.cpp | 6 +-- src/math/polysat/simplify_clause.cpp | 3 ++ src/math/polysat/solver.cpp | 67 +++++++++++++------------ src/math/polysat/solver.h | 2 + 6 files changed, 47 insertions(+), 40 deletions(-) diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp index 8085b9cb1..8adcac7ca 100644 --- a/src/math/polysat/constraint_manager.cpp +++ b/src/math/polysat/constraint_manager.cpp @@ -74,6 +74,7 @@ namespace polysat { register_clause(cl); watch(*cl); cl->set_active(); + s.push_reinit_stack(*cl); } // Release constraints at the given level and above. diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index 5f2cae8f5..9f24b6a0b 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -131,10 +131,8 @@ namespace polysat { if (first) activate(s); - if (clause_ref lemma = produce_lemma(s, s.get_assignment())) { + if (clause_ref lemma = produce_lemma(s, s.get_assignment())) s.add_clause(*lemma); - s.push_reinit_stack(*lemma); - } if (!s.is_conflict() && is_currently_false(s, is_positive)) s.set_conflict(signed_constraint(this, is_positive)); @@ -552,8 +550,8 @@ namespace polysat { pdd prod = p() * r(); rational prodv = (pv * rv).val(); - if (prodv != rational::power_of_two(parity_pv)) - verbose_stream() << prodv << " " << rational::power_of_two(parity_pv) << " " << parity_pv << " " << pv << " " << rv << "\n"; +// if (prodv != rational::power_of_two(parity_pv)) +// verbose_stream() << prodv << " " << rational::power_of_two(parity_pv) << " " << parity_pv << " " << pv << " " << rv << "\n"; unsigned lower = 0, upper = m.power_of_2(); // binary search for the parity (otw. we would have justifications like "parity_at_most(k) && parity_at_least(k)" for at most "k" widths while (lower + 1 < upper) { diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 32084fd98..8b4260fcc 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -1275,7 +1275,7 @@ namespace polysat { m_lemma.reset(); m_lemma.insert(~c); if (propagate(x, core, a_l_b, s.eq(i.lhs() - i.rhs()))) { - verbose_stream() << "infer equality " << s.eq(i.lhs() - i.rhs()) << "\n"; + IF_VERBOSE(1, verbose_stream() << "infer equality " << s.eq(i.lhs() - i.rhs()) << "\n"); return true; } } @@ -1865,7 +1865,7 @@ namespace polysat { // IF_VERBOSE(0, verbose_stream() << "min-max: x := v" << x << " [" << x_min << "," << x_max << "] y := v" << y << " [" << y_min << ", " << y_max << "] y0 " << y0 << "\n"); if (!update_bounds_for_xs(x_sp2, x_max, y_min, y_max, y0, a1, b1, c1, d1, a2, b2, c2, d2, M, a_l_b)) return false; - IF_VERBOSE(0, verbose_stream() << "min-max: x := v" << x << " [" << x_min << "," << x_max << "] y := v" << y << " [" << y_min << ", " << y_max << "] y0 " << y0 << "\n"); + IF_VERBOSE(1, verbose_stream() << "min-max: x := v" << x << " [" << x_min << "," << x_max << "] y := v" << y << " [" << y_min << ", " << y_max << "] y0 " << y0 << "\n"); SASSERT(y_min <= y0 && y0 <= y_max); VERIFY(y_min <= y0 && y0 <= y_max); @@ -1917,7 +1917,7 @@ namespace polysat { if (k == N) return false; if (rational::power_of_two(k) > p_val) { - verbose_stream() << k << " " << p_val << " " << a_l_b << "\n"; + // verbose_stream() << k << " " << p_val << " " << a_l_b << "\n"; m_lemma.reset(); for (auto const& c : at_least_k) m_lemma.insert_eval(~c); diff --git a/src/math/polysat/simplify_clause.cpp b/src/math/polysat/simplify_clause.cpp index d8a86cae7..159e8a2ae 100644 --- a/src/math/polysat/simplify_clause.cpp +++ b/src/math/polysat/simplify_clause.cpp @@ -560,6 +560,9 @@ namespace polysat { return args->hash(); } }; + + if (!s.inc()) + return false; ptr_vector info_list; map, pdd_info*, optional_pdd_hash, default_eq>> info_table; diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index f3f424bd5..c69f761d1 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -334,22 +334,12 @@ namespace polysat { } - // TODO - // pop_levels is called from pop and backjump - // backjump invoked a few places. - // the logic for propagating clauses after a pop or backjump - // is different. pop_levels inserts into repropagate - // pop_levels should end with a call to reinit_clauses where - // old_sz is the current trail head for clauses created within the scope. - // - // pop-levels can also update the scope of variables created below the pop level. - // the scope of variables would be set to the new level for clauses surviving a pop. void solver::reinit_clauses(unsigned old_sz) { unsigned sz = m_clauses_to_reinit.size(); SASSERT(old_sz <= sz); unsigned j = old_sz; - for (unsigned i = old_sz; i < sz; i++) { + for (unsigned i = old_sz; i < sz; ++i) { clause& c = *m_clauses_to_reinit[i]; SASSERT(c.on_reinit_stack()); bool reinit = false; @@ -364,17 +354,42 @@ namespace polysat { // Each Boolean has a "scope". The scope is initialized to the scope where // the Boolean is created. - if (reinit && !at_base_level()) + if (reinit) // clause propagated literal, must keep it in the reinit stack. m_clauses_to_reinit[j++] = &c; - else if (has_variables_to_reinit(c) && !at_base_level()) + else if (has_variables_to_reinit(c) && false) m_clauses_to_reinit[j++] = &c; else c.set_on_reinit_stack(false); + for (auto lit : c) + m_literals_to_reinit.push_back(lit); } m_clauses_to_reinit.shrink(j); + for (auto lit : m_literals_to_reinit) + reinit_literal(lit); + m_literals_to_reinit.reset(); } + void solver::reinit_literal(sat::literal lit) { + // check for missed lower evaluations + if (m_bvars.is_undef(lit)) { + switch (lit2cnstr(lit).eval(*this)) { + case l_true: + assign_eval(lit); + break; + case l_false: + assign_eval(~lit); + break; + default: + break; + } + } + // put the interval back into viable if we lost it + if (m_bvars.is_assigned(lit)) { + signed_constraint sc = m_bvars.is_true(lit) ? lit2cnstr(lit) : ~lit2cnstr(lit); + sc.narrow(*this, false); + } + } bool solver::can_repropagate() { return !m_repropagate_lits.empty() && !is_conflict(); @@ -405,24 +420,8 @@ namespace polysat { LOG("Repropagate lit " << lit); // check for missed lower boolean propagations repropagate(lit); - // check for missed lower evaluations - if (m_bvars.is_undef(lit)) { - switch (lit2cnstr(lit).eval(*this)) { - case l_true: - assign_eval(lit); - break; - case l_false: - assign_eval(~lit); - break; - default: - break; - } - } - // put the interval back into viable if we lost it - if (m_bvars.is_assigned(lit)) { - signed_constraint sc = m_bvars.is_true(lit) ? lit2cnstr(lit) : ~lit2cnstr(lit); - sc.narrow(*this, false); - } + + reinit_literal(lit); } } @@ -790,7 +789,9 @@ namespace polysat { // Unit clauses are not stored in watch lists and must be re-propagated separately. m_repropagate_units.push_back(reason); } - else if (!ENABLE_REINIT_STACK) + else if (ENABLE_REINIT_STACK) + m_literals_to_reinit.push_back(lit); + else m_repropagate_lits.push_back(lit); m_bvars.unassign(lit); m_search.pop(); @@ -1139,6 +1140,7 @@ namespace polysat { appraise_lemma(lemmas.back()); } if (!best_lemma) { + display(verbose_stream()); verbose_stream() << "conflict: " << m_conflict << "\n"; verbose_stream() << "no lemma\n"; for (clause* cl: lemmas) { @@ -1146,6 +1148,7 @@ namespace polysat { for (sat::literal lit : *cl) verbose_stream() << " " << lit_pp(*this, lit) << "\n"; } + } SASSERT(best_score < lemma_score::max()); VERIFY(best_lemma); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index b265504d0..da81b824e 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -352,10 +352,12 @@ namespace polysat { // clause reinitialization ptr_vector m_clauses_to_reinit; + sat::literal_vector m_literals_to_reinit; unsigned_vector m_reinit_heads; unsigned m_reinit_head = 0; void reinit_clauses(unsigned old_sz); bool has_variables_to_reinit(clause const& c) const; + void reinit_literal(sat::literal lit); bool inc() { return m_lim.inc(); }