From 579275a17d0c523bd78f3bf3d8e3a0ce8a24654d Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 3 Feb 2023 16:25:07 +0100 Subject: [PATCH] cleanup --- src/math/polysat/conflict.cpp | 29 +++++------------------ src/math/polysat/conflict.h | 11 +++------ src/math/polysat/saturation.cpp | 7 +++--- src/math/polysat/solver.cpp | 3 +-- src/math/polysat/solver.h | 1 - src/math/polysat/variable_elimination.cpp | 4 ++-- 6 files changed, 16 insertions(+), 39 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 60f6da8e6..8298b16ff 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -70,7 +70,7 @@ namespace polysat { void infer_lemmas_for_value(pvar v, conflict& core) { (void)m_poly_sup.perform(v, core); - (void)m_saturation.perform(v, core); + m_saturation.perform(v, core); } void infer_lemmas_for_value(pvar v, signed_constraint const& c, conflict& core) { @@ -267,10 +267,9 @@ namespace polysat { void conflict::insert(signed_constraint c) { if (contains(c)) return; - if (c.is_always_true()) - return; LOG("Inserting " << lit_pp(s, c)); SASSERT_EQ(c.bvalue(s), l_true); + SASSERT(!c.is_always_true()); // such constraints would be removed earlier SASSERT(!c.is_always_false()); // if we added c, the core would be a tautology SASSERT(!c->vars().empty()); m_literals.insert(c.blit().index()); @@ -283,19 +282,6 @@ namespace polysat { } } - void conflict::insert_eval(signed_constraint c) { - switch (c.bvalue(s)) { - case l_undef: - s.assign_eval(c.blit()); - break; - case l_true: - break; - case l_false: - break; - } - insert(c); - } - void conflict::insert_vars(signed_constraint c) { for (pvar v : c->vars()) if (s.is_assigned(v)) @@ -307,16 +293,14 @@ namespace polysat { } void conflict::add_lemma(char const* name, signed_constraint const* cs, size_t cs_len) { - clause_builder cb(s); + clause_builder cb(s, name); for (size_t i = 0; i < cs_len; ++i) cb.insert_eval(cs[i]); - add_lemma(name, cb.build()); + add_lemma(cb.build()); } - void conflict::add_lemma(char const* name, clause_ref lemma) { - if (!name) - name = ""; - LOG_H3("Lemma " << name << ": " << show_deref(lemma)); + void conflict::add_lemma(clause_ref lemma) { + LOG_H3("Lemma: " << ": " << show_deref(lemma)); VERIFY(lemma); for (auto lit : *lemma) @@ -325,7 +309,6 @@ namespace polysat { s.m_simplify_clause.apply(*lemma); lemma->set_redundant(true); - lemma->set_name(name); for (sat::literal lit : *lemma) { LOG(lit_pp(s, lit)); // NOTE: it can happen that the literal's bvalue is l_true at this point. diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index 7c0990310..bec8fa75d 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -145,29 +145,24 @@ namespace polysat { /** * Insert constraint c into conflict state. - * - * Skips trivial constraints: - * - e.g., constant constraints such as "4 > 1" */ void insert(signed_constraint c); /** Insert assigned variables of c */ void insert_vars(signed_constraint c); - /** Evaluate constraint under assignment and insert it into conflict state. */ - void insert_eval(signed_constraint c); - /** Add a lemma to the conflict, to be added after conflict resolution */ void add_lemma(char const* name, std::initializer_list cs); void add_lemma(char const* name, signed_constraint const* cs, size_t cs_len); - void add_lemma(char const* name, clause_ref lemma); + void add_lemma(clause_ref lemma); + void add_lemma(char const* name, clause_ref lemma) { lemma->set_name(name); add_lemma(lemma); } // remove /** Re-add a lemma to the conflict that we were unable to add after the previous conflict. */ void restore_lemma(clause_ref lemma); /** Remove c from core */ void remove(signed_constraint c); - void remove_var(pvar v); + /** * Remove all constraints and variables from the conflict state. * Use this during conflict resolution if the core needs to be replaced. diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index ad48ae706..5cdc397dc 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -216,8 +216,8 @@ namespace polysat { SASSERT(all_of(m_lemma, [this](sat::literal lit) { return is_forced_false(s.lit2cnstr(lit)); })); m_lemma.insert(c); - core.add_lemma(m_rule, m_lemma.build()); - verbose_stream() << "Lemma\n"; + m_lemma.set_name(m_rule); + core.add_lemma(m_lemma.build()); log_lemma(v, core); return true; } @@ -247,7 +247,8 @@ namespace polysat { return false; m_lemma.insert_eval(c); - core.add_lemma(m_rule, m_lemma.build()); + m_lemma.set_name(m_rule); + core.add_lemma(m_lemma.build()); log_lemma(v, core); return true; } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 95d09e8a3..3717f1427 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -1056,10 +1056,9 @@ namespace polysat { void solver::assign_eval(sat::literal lit) { signed_constraint const c = lit2cnstr(lit); LOG_V(10, "Evaluate: " << lit_pp(*this, lit)); - // assertion is false if (!c.is_currently_true(*this)) IF_VERBOSE(0, verbose_stream() << c << " is not currently true\n"); SASSERT(c.is_currently_true(*this)); - VERIFY(c.is_currently_true(*this)); + VERIFY_EQ(c.eval(*this), l_true); unsigned level = 0; // NOTE: constraint may be evaluated even if some variables are still unassigned (e.g., 0*x doesn't depend on x). for (auto v : c->vars()) diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 0868bc0dc..1c85e3bd7 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -287,7 +287,6 @@ namespace polysat { void rescale_activity(); void report_unsat(); - void learn_lemma(clause& lemma); void backjump(unsigned new_level); void add_clause(clause_ref clause); diff --git a/src/math/polysat/variable_elimination.cpp b/src/math/polysat/variable_elimination.cpp index 0eb68043b..9cf5fbe8b 100644 --- a/src/math/polysat/variable_elimination.cpp +++ b/src/math/polysat/variable_elimination.cpp @@ -421,7 +421,7 @@ namespace polysat { LOG("p1: " << p1); LOG("p2: " << p2); - clause_builder cb(s); + clause_builder cb(s, "variable elimination"); if (evaluated) { for (auto [w, wv] : sub) @@ -434,7 +434,7 @@ namespace polysat { cb.insert(c_new); ref c = cb.build(); if (c) // Can we get tautologies this way? - core.add_lemma("variable elimination", c); + core.add_lemma(c); } }