From c7da31a67d736299f781a93b06a22603c4acb272 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Dec 2021 10:24:42 -0800 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/math/polysat/conflict.cpp | 2 +- src/math/polysat/constraint.h | 1 + src/math/polysat/forbidden_intervals.cpp | 28 +++++----- src/math/polysat/forbidden_intervals.h | 2 +- src/math/polysat/solver.cpp | 3 +- src/math/polysat/viable.cpp | 69 +++++++++++++++--------- src/math/polysat/viable.h | 15 +++--- 7 files changed, 74 insertions(+), 46 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 730581f41..06735cec4 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -243,13 +243,13 @@ namespace polysat { for (unsigned v : m_vars) { if (!is_pmarked(v)) continue; - s.inc_activity(v); auto eq = s.eq(s.var(v), s.get_value(v)); cm().ensure_bvar(eq.get()); if (eq.bvalue(s) == l_undef) s.assign_eval(s.get_level(v), eq.blit()); lemma.push(~eq); } + s.decay_activity(); return lemma; } diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 71c0c7243..3e73b1792 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -284,6 +284,7 @@ namespace polysat { eval_interval interval; vector side_cond; signed_constraint src; + rational coeff; struct less { bool operator()(fi_record const& a, fi_record const& b) const { diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 12dcf9a43..a71b7ccf6 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -27,11 +27,9 @@ namespace polysat { * \returns True iff a forbidden interval exists and the output parameters were set. */ - bool forbidden_intervals::get_interval(signed_constraint const& c, pvar v, rational & coeff, eval_interval& out_interval, vector& out_side_cond) { + bool forbidden_intervals::get_interval(signed_constraint const& c, pvar v, fi_record& fi) { if (!c->is_ule()) return false; - - coeff = 1; struct backtrack { bool released = false; @@ -44,24 +42,30 @@ namespace polysat { } }; - backtrack _backtrack(out_side_cond); + backtrack _backtrack(fi.side_cond); - auto [ok1, a1, e1, b1] = linear_decompose(v, c->to_ule().lhs(), out_side_cond); - auto [ok2, a2, e2, b2] = linear_decompose(v, c->to_ule().rhs(), out_side_cond); + fi.coeff = 1; + fi.src = c; + + auto [ok1, a1, e1, b1] = linear_decompose(v, c->to_ule().lhs(), fi.side_cond); + auto [ok2, a2, e2, b2] = linear_decompose(v, c->to_ule().rhs(), fi.side_cond); if (!ok1 || !ok2 || (a1.is_zero() && a2.is_zero())) return false; + SASSERT(b1.is_val()); + SASSERT(b2.is_val()); + + // TBD: use fi.coeff = -1 to tell caller to treat it as a diseq_lin. + // record a1, a2, b1, b2 for fast access and add side conditions on b1, b2? if (a1 != a2 && !a1.is_zero() && !a2.is_zero()) return false; - SASSERT(b1.is_val()); - SASSERT(b2.is_val()); - + _backtrack.released = true; - if (match_linear1(c, a1, b1, e1, a2, b2, e2, coeff, out_interval, out_side_cond)) + if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi.coeff, fi.interval, fi.side_cond)) return true; - if (match_linear2(c, a1, b1, e1, a2, b2, e2, coeff, out_interval, out_side_cond)) + if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi.coeff, fi.interval, fi.side_cond)) return true; - if (match_linear3(c, a1, b1, e1, a2, b2, e2, coeff, out_interval, out_side_cond)) + if (match_linear3(c, a1, b1, e1, a2, b2, e2, fi.coeff, fi.interval, fi.side_cond)) return true; _backtrack.released = false; diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index dd5fbb178..99ceb7f92 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -47,6 +47,6 @@ namespace polysat { public: forbidden_intervals(solver& s) :s(s) {} - bool get_interval(signed_constraint const& c, pvar v, rational & coeff, eval_interval& out_interval, vector& side_cond); + bool get_interval(signed_constraint const& c, pvar v, fi_record& fi); }; } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index a00d009cd..11a90ae05 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -444,7 +444,7 @@ namespace polysat { LOG("end-try-eliminate v"); } - + search_iterator search_it(m_search); while (search_it.next()) { LOG("search state: " << m_search); @@ -458,6 +458,7 @@ namespace polysat { m_search.pop_asssignment(); continue; } + inc_activity(v); justification& j = m_justification[v]; if (j.level() > base_level() && !m_conflict.resolve_value(v) && j.is_decision()) { revert_decision(v); diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index ecba7b963..aca599b05 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -34,31 +34,39 @@ namespace polysat { dealloc(e); } - viable::entry* viable::alloc_entry() { - rational coeff(1); + viable::entry* viable::alloc_entry() { if (m_alloc.empty()) - return alloc(entry, coeff); + return alloc(entry); auto* e = m_alloc.back(); e->side_cond.reset(); - e->coeff = coeff; + e->coeff = 1; m_alloc.pop_back(); return e; } void viable::pop_viable() { - auto& [v, is_unit, e] = m_trail.back(); - auto& vec = is_unit ? m_units[v] : m_non_units[v]; - e->remove_from(vec, e); + auto& [v, k, e] = m_trail.back(); + switch (k) { + case entry_kind::unit_e: + e->remove_from(m_units[v], e); + break; + case entry_kind::equal_e: + e->remove_from(m_equal_lin[v], e); + break; + default: + e->remove_from(m_diseq_lin[v], e); + break; + } m_alloc.push_back(e); m_trail.pop_back(); } void viable::push_viable() { - auto& [v, is_unit, e] = m_trail.back(); + auto& [v, k, e] = m_trail.back(); SASSERT(e->prev() != e || !m_units[v]); SASSERT(e->prev() != e || e->next() == e); - SASSERT(is_unit); - (void)is_unit; + SASSERT(k == entry_kind::unit_e); + (void)k; if (e->prev() != e) { e->prev()->insert_after(e); if (e->interval.lo_val() < e->next()->interval.lo_val()) @@ -72,25 +80,35 @@ namespace polysat { bool viable::intersect(pvar v, signed_constraint const& c) { auto& fi = s.m_forbidden_intervals; entry* ne = alloc_entry(); - if (!fi.get_interval(c, v, ne->coeff, ne->interval, ne->side_cond) || ne->interval.is_currently_empty()) { + if (!fi.get_interval(c, v, *ne)) { + m_alloc.push_back(ne); + return false; + } + else if (ne->interval.is_currently_empty()) { m_alloc.push_back(ne); return false; } else if (ne->coeff == 1) { - ne->src = c; return intersect(v, ne); } - else { - ne->src = c; - m_trail.push_back({ v, false, ne }); - s.m_trail.push_back(trail_instr_t::viable_add_i); - ne->init(ne); - if (!m_non_units[v]) - m_non_units[v] = ne; - else - ne->insert_after(m_non_units[v]); + else if (ne->coeff == -1) { + insert(ne, v, m_diseq_lin, entry_kind::diseq_e); return true; } + else { + insert(ne, v, m_equal_lin, entry_kind::equal_e); + return true; + } + } + + void viable::insert(entry* e, pvar v, ptr_vector& entries, entry_kind k) { + m_trail.push_back({ v, k, e }); + s.m_trail.push_back(trail_instr_t::viable_add_i); + e->init(e); + if (!entries[v]) + entries[v] = e; + else + e->insert_after(entries[v]); } bool viable::intersect(pvar v, entry* ne) { @@ -106,14 +124,14 @@ namespace polysat { } auto create_entry = [&]() { - m_trail.push_back({ v, true, ne }); + m_trail.push_back({ v, entry_kind::unit_e, ne }); s.m_trail.push_back(trail_instr_t::viable_add_i); ne->init(ne); return ne; }; auto remove_entry = [&](entry* e) { - m_trail.push_back({ v, true, e }); + m_trail.push_back({ v, entry_kind::unit_e, e }); s.m_trail.push_back(trail_instr_t::viable_rem_i); e->remove_from(m_units[v], e); }; @@ -170,7 +188,7 @@ namespace polysat { * and division with coeff are valid. Is there a more relaxed scheme? */ bool viable::refine_viable(pvar v, rational const& val) { - auto* e = m_non_units[v]; + auto* e = m_equal_lin[v]; if (!e) return true; entry* first = e; @@ -222,6 +240,7 @@ namespace polysat { entry* ne = alloc_entry(); ne->src = e->src; ne->side_cond = e->side_cond; + // TODO: have forbidden_interval.cpp add these side conditions for non-unit equalities and diseq_lin? ne->side_cond.push_back(s.eq(e->interval.hi(), e->interval.hi_val())); ne->side_cond.push_back(s.eq(e->interval.lo(), e->interval.lo_val())); ne->coeff = 1; @@ -474,7 +493,7 @@ namespace polysat { std::ostream& viable::display(std::ostream& out, pvar v) const { display(out, v, m_units[v]); - display(out, v, m_non_units[v]); + display(out, v, m_equal_lin[v]); return out; } diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index 2822f5806..d2470c04c 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -32,14 +32,15 @@ namespace polysat { solver& s; struct entry : public dll_base, public fi_record { - rational coeff; - entry(rational const& m) : fi_record({ eval_interval::full(), {}, {} }), coeff(m) {} + entry() : fi_record({ eval_interval::full(), {}, {}, rational::one()}) {} }; + enum class entry_kind { unit_e, equal_e, diseq_e }; ptr_vector m_alloc; ptr_vector m_units; // set of viable values based on unit multipliers - ptr_vector m_non_units; // entries that have non-unit multipliers - svector> m_trail; // undo stack + ptr_vector m_equal_lin; // entries that have non-unit multipliers, but are equal + ptr_vector m_diseq_lin; // entries that have distinct non-zero multipliers + svector> m_trail; // undo stack bool well_formed(entry* e); @@ -51,15 +52,17 @@ namespace polysat { std::ostream& display(std::ostream& out, pvar v, entry* e) const; + void insert(entry* e, pvar v, ptr_vector& entries, entry_kind k); + public: viable(solver& s); ~viable(); // declare and remove var - void push(unsigned) { m_units.push_back(nullptr); m_non_units.push_back(nullptr); } + void push(unsigned) { m_units.push_back(nullptr); m_equal_lin.push_back(nullptr); } - void pop() { m_units.pop_back(); m_non_units.pop_back(); } + void pop() { m_units.pop_back(); m_equal_lin.pop_back(); } void pop_viable();