From 3447d80310719b598e7208fb6d92291d80a78b94 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Sep 2021 12:26:45 -0700 Subject: [PATCH] fix todo on enforcing premises Signed-off-by: Nikolaj Bjorner --- src/math/polysat/conflict.cpp | 52 +++++++++++++---------------- src/math/polysat/conflict.h | 4 +-- src/math/polysat/explain.cpp | 61 ++++++++++++++++++++++------------- src/math/polysat/explain.h | 2 +- 4 files changed, 64 insertions(+), 55 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index c6ad149a9..be4ea6d9d 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -146,22 +146,35 @@ namespace polysat { m_constraints.push_back(c); } - void conflict::insert(signed_constraint c, vector premises) { + void conflict::insert(signed_constraint c, vector const& premises) { insert(c); - m_saturation_premises.insert(c, std::move(premises)); // TODO: map doesn't have move-insertion, so this still copies the vector. + // 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()); + clause_ref lemma = c_lemma.build(); + cm().store(lemma.get(), s); + if (s.m_bvars.value(c.blit()) == l_undef) + s.assign_bool(s.level(*lemma), c.blit(), lemma.get(), nullptr); } void conflict::remove(signed_constraint c) { + SASSERT(!c->has_bvar() || std::count(m_constraints.begin(), m_constraints.end(), c) == 0); unset_mark(c); - if (c->has_bvar()) { - SASSERT(std::count(m_constraints.begin(), m_constraints.end(), c) == 0); - remove_literal(c.blit()); - } + if (c->has_bvar()) + remove_literal(c.blit()); else m_constraints.erase(c); } - void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector c_new_premises) { + void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector const& c_new_premises) { remove(c_old); insert(c_new, c_new_premises); } @@ -185,10 +198,8 @@ namespace polysat { SASSERT(!contains_literal(~lit)); SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0); - remove_literal(lit); - - unset_mark(m.lookup(lit)); - + remove_literal(lit); + unset_mark(m.lookup(lit)); for (sat::literal lit2 : cl) if (lit2 != lit) insert(m.lookup(~lit2)); @@ -205,25 +216,6 @@ namespace polysat { insert(c); } LOG_H3("keeping: " << c); - // NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c? - auto it = m_saturation_premises.find_iterator(c); - if (it == m_saturation_premises.end()) - return; - auto& premises = it->m_value; - clause_builder c_lemma(s); - for (auto premise : premises) { - LOG_H3("premise: " << premise); - keep(premise); - SASSERT(premise->has_bvar()); - SASSERT(premise.is_currently_true(s) || premise.bvalue(s) == l_true); - // otherwise the propagation doesn't make sense - c_lemma.push(~premise.blit()); - } - c_lemma.push(c.blit()); - clause_ref lemma = c_lemma.build(); - cm().store(lemma.get(), s); - if (s.m_bvars.value(c.blit()) == l_undef) - s.assign_bool(s.level(*lemma), c.blit(), lemma.get(), nullptr); } clause_builder conflict::build_lemma() { diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index 3dd6b9bfc..655fa185e 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -86,9 +86,9 @@ namespace polysat { void set(clause const& cl); void insert(signed_constraint c); - void insert(signed_constraint c, vector premises); + void insert(signed_constraint c, vector const& premises); void remove(signed_constraint c); - void replace(signed_constraint c_old, signed_constraint c_new, vector c_new_premises); + void replace(signed_constraint c_old, signed_constraint c_new, vector const& c_new_premises); void keep(signed_constraint c); diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index 901a8635b..8f10c014a 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -46,48 +46,65 @@ namespace polysat { // c2 ... constraint that is currently false // Try to replace it with a new false constraint (derived from superposition with a true constraint) - signed_constraint ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict& core) { + lbool ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict& core) { + vector premises; for (auto c1 : core) { if (!is_positive_equality_over(v, c1)) continue; if (!c1.is_currently_true(s())) continue; - signed_constraint c = resolve1(v, c1, c2); if (!c) continue; - vector premises; - premises.push_back(c1); - premises.push_back(c2); - core.replace(c2, c, std::move(premises)); - return c; + if (!c->has_bvar()) + s().m_constraints.ensure_bvar(c.get()); + + switch (c.bvalue(s())) { + case l_false: + // new conflict state based on propagation and theory conflict + core.reset(); + core.insert(c1); + core.insert(c2); + core.insert(~c); + return l_true; + case l_undef: + // Ensure that c is assigned and justified + 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())); + break; + default: + break; + } + + // NOTE: more variables than just 'v' might have been removed here (see polysat::test_p3). + // c alone (+ variables) is now enough to represent the conflict. + core.reset(); + core.set(c); + return c->contains_var(v) ? l_undef : l_true; } - return {}; + return l_false; } // TODO(later): check superposition into disequality again (see notes) // true = done, false = abort, undef = continue + // TODO: can try multiple replacements at once; then the c2 loop needs to be done only once... (requires some reorganization for storing the premises) lbool ex_polynomial_superposition::try_explain1(pvar v, conflict& core) { for (auto c2 : core) { if (!is_positive_equality_over(v, c2)) continue; if (!c2.is_currently_false(s())) continue; - - // TODO: can try multiple replacements at once; then the c2 loop needs to be done only once... (requires some reorganization for storing the premises) - signed_constraint c = find_replacement(c2, v, core); - if (!c) - continue; - if (c->contains_var(v)) + switch (find_replacement(c2, v, core)) { + case l_undef: return l_undef; - if (!c->has_bvar() || l_undef == c.bvalue(s())) - core.keep(c); // adds propagation of c to the search stack - - // NOTE: more variables than just 'v' might have been removed here (see polysat::test_p3). - // c alone (+ variables) is now enough to represent the conflict. - core.reset(); - core.set(c); - return l_true; + case l_true: + return l_true; + case l_false: + continue; + } } return l_false; } diff --git a/src/math/polysat/explain.h b/src/math/polysat/explain.h index fa61b55f4..47fc20ee0 100644 --- a/src/math/polysat/explain.h +++ b/src/math/polysat/explain.h @@ -36,7 +36,7 @@ namespace polysat { private: bool is_positive_equality_over(pvar v, signed_constraint const& c); signed_constraint resolve1(pvar v, signed_constraint c1, signed_constraint c2); - signed_constraint find_replacement(signed_constraint c2, pvar v, conflict& core); + lbool find_replacement(signed_constraint c2, pvar v, conflict& core); void reduce_by(pvar v, conflict& core); bool reduce_by(pvar, signed_constraint c, conflict& core); lbool try_explain1(pvar v, conflict& core);