diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp index 8d121fe3f..9ee26227b 100644 --- a/src/math/polysat/boolean.cpp +++ b/src/math/polysat/boolean.cpp @@ -11,6 +11,7 @@ Author: --*/ #include "math/polysat/boolean.h" +#include "math/polysat/clause.h" #include "math/polysat/log.h" namespace polysat { @@ -69,10 +70,10 @@ namespace polysat { std::ostream& bool_var_manager::display(std::ostream& out) const { for (sat::bool_var v = 0; v < size(); ++v) { - sat::literal lit{v}; + sat::literal lit(v); if (value(lit) == l_true) out << " " << lit; - if (value(lit) == l_false) + else if (value(lit) == l_false) out << " " << ~lit; } return out; diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp index 65de89a05..3f2ed6abd 100644 --- a/src/math/polysat/conflict_core.cpp +++ b/src/math/polysat/conflict_core.cpp @@ -103,7 +103,7 @@ namespace polysat { } void conflict_core::insert(signed_constraint c) { - LOG("inserting: " << c); + LOG("inserting: " << c << " " << c.is_always_true() << " " << c->is_marked() << " " << c->has_bvar()); // Skip trivial constraints // (e.g., constant ones such as "4 > 1"... only true ones should appear, otherwise the lemma would be a tautology) if (c.is_always_true()) @@ -164,6 +164,7 @@ namespace polysat { remove_literal(sat::literal(var)); if (core_has_neg) remove_literal(~sat::literal(var)); + unset_bmark(var); for (sat::literal lit : cl) if (lit.var() != var) diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index 0a6a59567..fc86f1449 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -78,17 +78,16 @@ namespace polysat { signed_constraint c = find_replacement(c2, v, core); if (!c) continue; - - if (!c->contains_var(v)) { - 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; - } - else + if (c->contains_var(v)) 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; } return l_false; } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 0966ae8cc..e291b6a69 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -508,12 +508,12 @@ namespace polysat { } /** Conflict resolution case where boolean literal 'lit' is on top of the stack */ - void solver::resolve_bool(sat::literal lit) { - LOG_H3("resolve_bool: " << lit); + void solver::resolve_bool(sat::literal lit) { sat::bool_var const var = lit.var(); SASSERT(m_bvars.is_propagation(var)); // NOTE: boolean resolution should work normally even in bailout mode. clause* other = m_bvars.reason(var); + LOG_H3("resolve_bool: " << lit << " " << *other); m_conflict.resolve(m_constraints, var, *other); } @@ -543,12 +543,11 @@ namespace polysat { SASSERT(lemma->size() > 0); lemma->set_justified_var(v); add_lemma(lemma); - sat::literal lit = decide_bool(*lemma); - SASSERT(lit != sat::null_literal); + decide_bool(*lemma); } // Guess a literal from the given clause; returns the guessed constraint - sat::literal solver::decide_bool(clause& lemma) { + void solver::decide_bool(clause& lemma) { LOG_H3("Guessing literal in lemma: " << lemma); IF_LOGGING(m_viable.log()); LOG("Boolean assignment: " << m_bvars); @@ -574,20 +573,21 @@ namespace polysat { } } LOG_V("num_choices: " << num_choices); + if (choice == sat::null_literal) { + // This case may happen when all undefined literals are false under the current variable assignment. + // TODO: The question is whether such lemmas should be generated? Check test_monot() for such a case. + for (auto lit : lemma) + set_conflict(~m_constraints.lookup(lit)); + return; + } signed_constraint c = m_constraints.lookup(choice); push_cjust(lemma.justified_var(), c); - if (num_choices == 0) { - // This case may happen when all undefined literals are false under the current variable assignment. - // TODO: The question is whether such lemmas should be generated? Check test_monot() for such a case. - // set_conflict(lemma); - NOT_IMPLEMENTED_YET(); - } else if (num_choices == 1) + if (num_choices == 1) propagate_bool(choice, &lemma); else decide_bool(choice, lemma); - return choice; } /** @@ -603,7 +603,7 @@ namespace polysat { m_conflict.reset(); backjump(m_justification[v].level() - 1); - + // The justification for this restriction is the guessed constraint from the lemma. // cjust[v] will be updated accordingly by decide_bool. m_viable.add_non_viable(v, val); @@ -805,15 +805,23 @@ namespace polysat { std::ostream& solver::display(std::ostream& out) const { out << "Assignment:\n"; - for (auto [v, val] : assignment()) { - auto j = m_justification[v]; - out << "\t" << assignment_pp(*this, v, val) << " @" << j.level(); - if (j.is_propagation()) - out << " " << m_cjust[v]; - out << "\n"; - // out << m_viable[v] << "\n"; + for (auto item : m_search) { + if (item.is_assignment()) { + pvar v = item.var(); + auto j = m_justification[v]; + out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level(); + if (j.is_propagation()) + out << " " << m_cjust[v]; + out << "\n"; + } + else { + sat::bool_var v = item.lit().var(); + out << "\t" << item.lit() << " @" << m_bvars.level(v); + if (m_bvars.reason(v)) + out << " " << *m_bvars.reason(v); + out << "\n"; + } } - out << "Boolean assignment:\n\t" << m_bvars << "\n"; out << "Constraints:\n"; for (auto c : m_constraints) out << "\t" << *c << "\n"; diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 799ac25ec..f20fa5067 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -153,7 +153,7 @@ namespace polysat { void assign_bool(unsigned level, sat::literal lit, clause* reason, clause* lemma); void activate_constraint(signed_constraint c); void deactivate_constraint(signed_constraint c); - sat::literal decide_bool(clause& lemma); + void decide_bool(clause& lemma); void decide_bool(sat::literal lit, clause& lemma); void propagate_bool(sat::literal lit, clause* reason); void propagate_bool_at(unsigned level, sat::literal lit, clause* reason);