From c82bbaad7d68d89740d5f86994377804cbbc25b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Sep 2021 13:29:36 -0700 Subject: [PATCH] update todos, working on assignment minimization --- src/math/polysat/conflict.cpp | 29 ++++++++---------------- src/math/polysat/conflict.h | 2 -- src/math/polysat/constraint.cpp | 8 +++++++ src/math/polysat/constraint.h | 11 +++++----- src/math/polysat/explain.cpp | 34 ++++++++++++++--------------- src/math/polysat/explain.h | 6 ++--- src/math/polysat/ule_constraint.cpp | 12 +++++----- src/math/polysat/ule_constraint.h | 4 ++-- 8 files changed, 51 insertions(+), 55 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index be4ea6d9d..ee2ffb937 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -12,21 +12,12 @@ Author: Notes: - TODO: constraints containing v could be tracked incrementally when constraints are added/removed using an index. - TODO: try a final core reduction step or other core minimization TODO: If we have e.g. 4x+y=2 and y=0, then we have a conflict no matter the value of x, so we should drop x=? from the core. (works currently if x is unassigned; for other cases we would need extra info from constraint::is_currently_false) - - TODO: build_lemma: note that we may have added too many variables: e.g., y disappears in x*y if x=0 - TODO: keep is buggy. The assert - SASSERT(premise.is_currently_true(s()) || premise.bvalue(s()) == l_true); - does not necessarily hold. A saturation premise could be inserted that is a resolvent that evaluates to false - and therefore not a current Boolean literal on the search stack. - TODO: revert(pvar v) is too weak. It should apply saturation rules currently only available for propagated values. @@ -46,9 +37,7 @@ Notes: namespace polysat { conflict::conflict(solver& s):s(s) { - ex_engines.push_back(alloc(ex_polynomial_superposition)); - for (auto* engine : ex_engines) - engine->set_solver(s); + ex_engines.push_back(alloc(ex_polynomial_superposition, s)); ve_engines.push_back(alloc(ve_reduction)); inf_engines.push_back(alloc(inf_saturate)); for (auto* engine : inf_engines) @@ -77,7 +66,6 @@ namespace polysat { m_literals.reset(); m_vars.reset(); m_conflict_var = null_var; - m_saturation_premises.reset(); m_bailout = false; SASSERT(empty()); } @@ -146,16 +134,17 @@ namespace polysat { m_constraints.push_back(c); } + + // NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c? + // Ensure that c is assigned and justified void conflict::insert(signed_constraint c, vector const& premises) { insert(c); - // NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c? clause_builder c_lemma(s); for (auto premise : premises) { LOG_H3("premise: " << premise); keep(premise); SASSERT(premise->has_bvar()); SASSERT(premise.bvalue(s) == l_true); - // otherwise the propagation doesn't make sense c_lemma.push(~premise.blit()); } c_lemma.push(c.blit()); @@ -210,12 +199,12 @@ namespace polysat { * insert it (and recursively, its premises) into \Gamma */ void conflict::keep(signed_constraint c) { - if (!c->has_bvar()) { - remove(c); - cm().ensure_bvar(c.get()); - insert(c); - } + if (c->has_bvar()) + return; LOG_H3("keeping: " << c); + remove(c); + cm().ensure_bvar(c.get()); + insert(c); } clause_builder conflict::build_lemma() { diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index 655fa185e..d656e929e 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -58,8 +58,6 @@ namespace polysat { scoped_ptr_vector ve_engines; scoped_ptr_vector inf_engines; - // ptr_addr_map> m_saturation_premises; - map, obj_hash, default_eq> m_saturation_premises; public: conflict(solver& s); ~conflict(); diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 04ef30172..5329eed14 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -121,6 +121,14 @@ namespace polysat { return {lookup(lit.var()), lit}; } + bool signed_constraint::is_currently_false(solver& s) const { + return get()->is_currently_false(s.assignment(), is_positive()); + } + + bool signed_constraint::is_currently_true(solver& s) const { + return get()->is_currently_true(s.assignment(), is_positive()); + } + /** Look up constraint among stored constraints. */ constraint* constraint_manager::dedup(constraint* c1) { constraint* c2 = nullptr; diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 207d6741c..c2569c965 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -16,6 +16,7 @@ Author: #include "math/polysat/clause.h" #include "math/polysat/types.h" #include "math/polysat/interval.h" +#include "math/polysat/search_state.h" namespace polysat { @@ -161,8 +162,8 @@ namespace polysat { bool propagate(solver& s, bool is_positive, pvar v); virtual void propagate_core(solver& s, bool is_positive, pvar v, pvar other_v); virtual bool is_always_false(bool is_positive) const = 0; - virtual bool is_currently_false(solver& s, bool is_positive) const = 0; - virtual bool is_currently_true(solver& s, bool is_positive) const = 0; + virtual bool is_currently_false(assignment_t const& a, bool is_positive) const = 0; + virtual bool is_currently_true(assignment_t const& a, bool is_positive) const = 0; virtual void narrow(solver& s, bool is_positive) = 0; virtual inequality as_inequality(bool is_positive) const = 0; @@ -220,9 +221,9 @@ namespace polysat { bool propagate(solver& s, pvar v) { return get()->propagate(s, is_positive(), v); } void propagate_core(solver& s, pvar v, pvar other_v) { get()->propagate_core(s, is_positive(), v, other_v); } bool is_always_false() const { return get()->is_always_false(is_positive()); } - bool is_always_true() const { return get()->is_always_false(is_negative()); } - bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); } - bool is_currently_true(solver& s) const { return get()->is_currently_true(s, is_positive()); } + bool is_always_true() const { return get()->is_always_false(is_negative()); } + bool is_currently_false(solver& s) const; + bool is_currently_true(solver& s) const; lbool bvalue(solver& s) const; unsigned level(solver& s) const { return get()->level(s); } void narrow(solver& s) { get()->narrow(s, is_positive()); } diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index 8f10c014a..47b08fa52 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -19,8 +19,8 @@ namespace polysat { signed_constraint ex_polynomial_superposition::resolve1(pvar v, signed_constraint c1, signed_constraint c2) { // c1 is true, c2 is false - SASSERT(c1.is_currently_true(s())); - SASSERT(c2.is_currently_false(s())); + SASSERT(c1.is_currently_true(s)); + SASSERT(c2.is_currently_false(s)); LOG_H3("Resolving upon v" << v); LOG("c1: " << c1); LOG("c2: " << c2); @@ -33,9 +33,9 @@ namespace polysat { // (this condition might be too strict, but we use it for now to prevent looping) if (b.degree(v) <= r.degree(v)) return {}; - signed_constraint c = s().eq(r); - LOG("resolved: " << c << " currently false? " << c.is_currently_false(s())); - if (!c.is_currently_false(s())) + signed_constraint c = s.eq(r); + LOG("resolved: " << c << " currently false? " << c.is_currently_false(s)); + if (!c.is_currently_false(s)) return {}; return c; } @@ -51,15 +51,15 @@ namespace polysat { for (auto c1 : core) { if (!is_positive_equality_over(v, c1)) continue; - if (!c1.is_currently_true(s())) + if (!c1.is_currently_true(s)) continue; signed_constraint c = resolve1(v, c1, c2); if (!c) continue; if (!c->has_bvar()) - s().m_constraints.ensure_bvar(c.get()); + s.m_constraints.ensure_bvar(c.get()); - switch (c.bvalue(s())) { + switch (c.bvalue(s)) { case l_false: // new conflict state based on propagation and theory conflict core.reset(); @@ -72,8 +72,8 @@ namespace polysat { premises.push_back(c1); premises.push_back(c2); core.replace(c2, c, premises); - SASSERT(l_true == c.bvalue(s())); - SASSERT(c.is_currently_false(s())); + SASSERT(l_true == c.bvalue(s)); + SASSERT(c.is_currently_false(s)); break; default: break; @@ -95,7 +95,7 @@ namespace polysat { for (auto c2 : core) { if (!is_positive_equality_over(v, c2)) continue; - if (!c2.is_currently_false(s())) + if (!c2.is_currently_false(s)) continue; switch (find_replacement(c2, v, core)) { case l_undef: @@ -115,7 +115,7 @@ namespace polysat { while (progress) { progress = false; for (auto c : core) { - if (is_positive_equality_over(v, c) && c.is_currently_true(s()) && reduce_by(v, c, core)) { + if (is_positive_equality_over(v, c) && c.is_currently_true(s) && reduce_by(v, c, core)) { progress = true; break; } @@ -130,7 +130,7 @@ namespace polysat { continue; if (is_positive_equality_over(v, c)) continue; - if (!c.is_currently_false(s())) + if (!c.is_currently_false(s)) continue; if (c->is_ule()) { auto lhs = c->to_ule().lhs(); @@ -139,14 +139,14 @@ namespace polysat { auto b = rhs.reduce(v, p); if (a == lhs && b == rhs) continue; - auto c2 = s().ule(a, b); + auto c2 = s.ule(a, b); if (!c.is_positive()) c2 = ~c2; - SASSERT(c2.is_currently_false(s())); - if (!c2->has_bvar() || l_undef == c2.bvalue(s())) + SASSERT(c2.is_currently_false(s)); + if (!c2->has_bvar() || l_undef == c2.bvalue(s)) core.keep(c2); // adds propagation of c to the search stack core.reset(); - if (c2.bvalue(s()) == l_false) { + if (c2.bvalue(s) == l_false) { core.insert(eq); core.insert(c); core.insert(~c2); diff --git a/src/math/polysat/explain.h b/src/math/polysat/explain.h index 47fc20ee0..1ed08a9dd 100644 --- a/src/math/polysat/explain.h +++ b/src/math/polysat/explain.h @@ -23,11 +23,10 @@ namespace polysat { class explainer { friend class conflict; - solver* m_solver = nullptr; - void set_solver(solver& s) { m_solver = &s; } protected: - solver& s() { return *m_solver; } + solver& s; public: + explainer(solver& s) :s(s) {} virtual ~explainer() {} virtual bool try_explain(pvar v, /* vector const& cjust_v, */ conflict& core) = 0; }; @@ -41,6 +40,7 @@ namespace polysat { bool reduce_by(pvar, signed_constraint c, conflict& core); lbool try_explain1(pvar v, conflict& core); public: + ex_polynomial_superposition(solver& s) : explainer(s) {} bool try_explain(pvar v, conflict& core) override; }; diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index e9c981427..04beb697a 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -204,15 +204,15 @@ namespace polysat { return is_always_false(is_positive, lhs(), rhs()); } - bool ule_constraint::is_currently_false(solver& s, bool is_positive) const { - auto p = lhs().subst_val(s.assignment()); - auto q = rhs().subst_val(s.assignment()); + bool ule_constraint::is_currently_false(assignment_t const& a, bool is_positive) const { + auto p = lhs().subst_val(a); + auto q = rhs().subst_val(a); return is_always_false(is_positive, p, q); } - bool ule_constraint::is_currently_true(solver& s, bool is_positive) const { - auto p = lhs().subst_val(s.assignment()); - auto q = rhs().subst_val(s.assignment()); + bool ule_constraint::is_currently_true(assignment_t const& a, bool is_positive) const { + auto p = lhs().subst_val(a); + auto q = rhs().subst_val(a); if (is_positive) { if (p.is_zero()) return true; diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h index f5e732d54..fd29d7f33 100644 --- a/src/math/polysat/ule_constraint.h +++ b/src/math/polysat/ule_constraint.h @@ -34,8 +34,8 @@ namespace polysat { std::ostream& display(std::ostream& out) const override; bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) const; bool is_always_false(bool is_positive) const override; - bool is_currently_false(solver& s, bool is_positive) const override; - bool is_currently_true(solver& s, bool is_positive) const override; + bool is_currently_false(assignment_t const& a, bool is_positive) const override; + bool is_currently_true(assignment_t const& a, bool is_positive) const override; void narrow(solver& s, bool is_positive) override; inequality as_inequality(bool is_positive) const override; unsigned hash() const override;