diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index 14f1a4ac6..786d4ad65 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -2,6 +2,7 @@ z3_add_component(polysat SOURCES boolean.cpp clause_builder.cpp + conflict_core.cpp constraint.cpp eq_constraint.cpp explain.cpp diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp new file mode 100644 index 000000000..7306e381f --- /dev/null +++ b/src/math/polysat/conflict_core.cpp @@ -0,0 +1,28 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat conflict + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ + +#include "math/polysat/conflict_core.h" +#include "math/polysat/solver.h" +#include "math/polysat/log.h" +#include "math/polysat/log_helper.h" + +namespace polysat { + + std::ostream& conflict_core::display(std::ostream& out) const { + out << "TODO: display conflict_core"; + // depending on sign: A /\ B /\ C or ¬A \/ ¬B \/ ¬C + return out; + } + +} diff --git a/src/math/polysat/conflict_core.h b/src/math/polysat/conflict_core.h new file mode 100644 index 000000000..c44723e78 --- /dev/null +++ b/src/math/polysat/conflict_core.h @@ -0,0 +1,66 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat conflict + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#pragma once +#include "math/polysat/constraint.h" + +namespace polysat { + + /// Represents a conflict as core (~negation of clause). + /// + /// TODO: can probably move some clause_builder functionality into this class. + class conflict_core { + // constraint_ref_vector m_constraints; + vector m_constraints; + bool m_needs_model = true; ///< True iff the conflict depends on the current variable assignment. (If so, additional constraints must be added to the final learned clause.) + + public: + vector const& constraints() const { + return m_constraints; + } + + bool empty() const { + return m_constraints.empty(); + } + + void reset() { + m_constraints.reset(); + m_needs_model = true; + } + + // for bailing out with a conflict at the base level + void set(std::nullptr_t) { + SASSERT(empty()); + m_constraints.push_back({}); + m_needs_model = false; + } + + // void set( + + // TODO: set core from conflicting units + // TODO: set clause + + // TODO: use iterator instead (this method is needed for marking so duplicates don't necessarily have to be skipped) + unsigned_vector vars(constraint_manager const& cm) const { + unsigned_vector vars; + for (auto const& c : m_constraints) + vars.append(c->vars()); + return vars; + } + + std::ostream& display(std::ostream& out) const; + }; + + inline std::ostream& operator<<(std::ostream& out, conflict_core const& c) { return c.display(out); } + +} diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index da9f12928..ebb86ff4c 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -151,8 +151,9 @@ namespace polysat { std::ostream& constraint::display_extra(std::ostream& out) const { out << " @" << level() << " (b" << bvar() << ")"; - if (is_undef()) - out << " [inactive]"; + if (is_positive()) out << " [pos]"; + if (is_negative()) out << " [neg]"; + if (is_undef()) out << " [inactive]"; return out; } diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 6ae437671..bbdf5e595 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -166,7 +166,8 @@ namespace polysat { sat::literal blit() const { SASSERT(!is_undef()); return m_status == l_true ? sat::literal(m_bvar) : ~sat::literal(m_bvar); } void assign(bool is_true) { - SASSERT(m_status == l_undef /* || m_status == to_lbool(is_true) */); + SASSERT(m_status == l_undef || m_status == to_lbool(is_true)); + // SASSERT(m_status == l_undef /* || m_status == to_lbool(is_true) */); m_status = to_lbool(is_true); // SASSERT(m_manager->m_bvars.value(bvar()) == l_undef || m_manager->m_bvars.value(bvar()) == m_status); // TODO: is this always true? maybe we sometimes want to check the opposite phase temporarily. } @@ -176,7 +177,7 @@ namespace polysat { bool is_negative() const { return m_status == l_false; } clause* unit_clause() const { return m_unit_clause; } - void set_unit_clause(clause* cl) { SASSERT(cl); SASSERT(!m_unit_clause); m_unit_clause = cl; } + void set_unit_clause(clause* cl) { SASSERT(cl); SASSERT(!m_unit_clause || m_unit_clause == cl); m_unit_clause = cl; } p_dependency* unit_dep() const; /** Precondition: all variables other than v are assigned. @@ -351,6 +352,7 @@ namespace polysat { constraint* m_constraint; bool m_should_unassign = false; public: + /// c must live longer than tmp_assign. tmp_assign(constraint* c, sat::literal lit): m_constraint(c) { SASSERT(c); @@ -362,8 +364,6 @@ namespace polysat { else SASSERT_EQ(c->blit(), lit); } - // NSB review: assumes life-time of c extends use in tmp_assign. - tmp_assign(constraint_ref const& c, sat::literal lit): tmp_assign(c.get(), lit) {} void revert() { if (m_should_unassign) { m_constraint->unassign(); diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index 7626aa179..681bb7461 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -41,6 +41,30 @@ namespace polysat { for (auto* c : confl.clauses()) m_conflict.push_back(c); + // Collect unit constraints + // + // TODO: the distinction between units and unit clauses is a bit awkward; maybe it should be removed. + // We could then also remove the hybrid container 'constraints_and_clauses' by a clause_ref_vector + SASSERT(m_conflict_units.empty()); + for (constraint* c : m_conflict.units()) + // if (c->is_eq()) + m_conflict_units.push_back(c); + for (auto clause : m_conflict.clauses()) { + if (clause->size() == 1) { + sat::literal lit = (*clause)[0]; + constraint* c = m_solver.m_constraints.lookup(lit.var()); + LOG("unit clause: " << show_deref(c)); + // Morally, a derived unit clause is always asserted at the base level. + // (Even if we don't want to keep this one around. But maybe we should? Do we want to reconstruct proofs?) + c->set_unit_clause(clause); + c->assign(!lit.sign()); + // this clause is really a unit. + // if (c->is_eq()) { + m_conflict_units.push_back(c); + // } + } + } + // TODO: we should share work done for examining constraints between different resolution methods clause_ref lemma; if (!lemma) lemma = by_polynomial_superposition(); @@ -57,9 +81,9 @@ namespace polysat { } // All constraints in the lemma must be false in the conflict state for (auto lit : lemma->literals()) { - if (m_solver.m_bvars.value(lit.var()) == l_false) + if (m_solver.m_bvars.value(lit) == l_false) continue; - SASSERT(m_solver.m_bvars.value(lit.var()) != l_true); + SASSERT(m_solver.m_bvars.value(lit) != l_true); constraint* c = m_solver.m_constraints.lookup(lit.var()); SASSERT(c); tmp_assign _t(c, lit); @@ -90,6 +114,8 @@ namespace polysat { */ clause_ref conflict_explainer::by_polynomial_superposition() { LOG_H3("units-size: " << m_conflict.units().size() << " conflict-clauses " << m_conflict.clauses().size()); + +#if 0 constraint* c1 = nullptr, *c2 = nullptr; if (m_conflict.units().size() == 2 && m_conflict.clauses().size() == 0) { @@ -99,23 +125,26 @@ namespace polysat { else { // other combinations? -#if 0 +#if 1 // A clause can also be a unit. // Even if a clause is not a unit, we could still resolve a propagation // into some literal in the current conflict clause. // Selecting resolvents should not be specific to superposition. - // for (auto clause : m_conflict.clauses()) { + LOG("clause " << *clause << " size " << clause->size()); if (clause->size() == 1) { sat::literal lit = (*clause)[0]; - if (lit.sign()) - continue; + // if (lit.sign()) + // continue; constraint* c = m_solver.m_constraints.lookup(lit.var()); - c->assign(true); + // Morally, a derived unit clause is always asserted at the base level. + // (Even if we don't want to keep this one around. But maybe we should? Do we want to reconstruct proofs?) + c->set_unit_clause(clause); + c->assign(!lit.sign()); // this clause is really a unit. LOG("unit clause: " << *c); - if (c->is_eq() && c->is_positive()) { + if (c->is_eq()) { // && c->is_positive()) { c1 = c; break; } @@ -134,6 +163,8 @@ namespace polysat { } if (!c1 || !c2 || c1 == c2) return nullptr; + LOG("c1: " << show_deref(c1)); + LOG("c2: " << show_deref(c2)); if (c1->is_eq() && c2->is_eq() && c1->is_positive() && c2->is_positive()) { pdd a = c1->to_eq().p(); pdd b = c2->to_eq().p(); @@ -147,6 +178,72 @@ namespace polysat { clause.push_new_constraint(m_solver.m_constraints.eq(lvl, r)); return clause.build(); } + if (c1->is_eq() && c2->is_eq() && c1->is_negative() && c2->is_positive()) { + pdd a = c1->to_eq().p(); + pdd b = c2->to_eq().p(); + pdd r = a; + // TODO: only holds if the factor for 'a' is non-zero + if (!a.resolve(m_var, b, r)) + return nullptr; + unsigned const lvl = std::max(c1->level(), c2->level()); + clause_builder clause(m_solver); + clause.push_literal(~c1->blit()); + clause.push_literal(~c2->blit()); + clause.push_new_constraint(~m_solver.m_constraints.eq(lvl, r)); + SASSERT(false); // TODO "breakpoint" for debugging + return clause.build(); + } + +#else + for (constraint* c1 : m_conflict_units) { + if (!c1->is_eq()) + continue; + for (constraint* c2 : m_conflict_units) { // TODO: can start iteration at index(c1)+1 + if (c1 == c2) + continue; + if (!c2->is_eq()) + continue; + if (c1->is_negative() && c2->is_negative()) + continue; + LOG("c1: " << show_deref(c1)); + LOG("c2: " << show_deref(c2)); + if (c1->is_positive() && c2->is_negative()) { + std::swap(c1, c2); + } + pdd a = c1->to_eq().p(); + pdd b = c2->to_eq().p(); + pdd r = a; + unsigned const lvl = std::max(c1->level(), c2->level()); + if (c1->is_positive() && c2->is_positive()) { + if (!a.resolve(m_var, b, r) && !b.resolve(m_var, a, r)) + continue; + clause_builder clause(m_solver); + clause.push_literal(~c1->blit()); + clause.push_literal(~c2->blit()); + clause.push_new_constraint(m_solver.m_constraints.eq(lvl, r)); + auto cl = clause.build(); + LOG("r: " << show_deref(cl->new_constraints()[0])); + LOG("result: " << show_deref(cl)); + // SASSERT(false); // NOTE: this is a simple "breakpoint" for debugging + return cl; + } + if (c1->is_negative() && c2->is_positive()) { + // TODO: only holds if the factor for 'a' is non-zero + if (!a.resolve(m_var, b, r)) + continue; + clause_builder clause(m_solver); + clause.push_literal(~c1->blit()); + clause.push_literal(~c2->blit()); + clause.push_new_constraint(~m_solver.m_constraints.eq(lvl, r)); + auto cl = clause.build(); + LOG("r: " << show_deref(cl->new_constraints()[0])); + LOG("result: " << show_deref(cl)); + // SASSERT(false); // NOTE: this is a simple "breakpoint" for debugging + return cl; + } + } + } +#endif return nullptr; } diff --git a/src/math/polysat/explain.h b/src/math/polysat/explain.h index 062fbe2d6..daac9fef7 100644 --- a/src/math/polysat/explain.h +++ b/src/math/polysat/explain.h @@ -24,6 +24,7 @@ namespace polysat { class conflict_explainer { solver& m_solver; constraints_and_clauses m_conflict; + ptr_vector m_conflict_units; pvar m_var = null_var; ptr_vector m_cjust_v; diff --git a/src/math/polysat/log.cpp b/src/math/polysat/log.cpp index ae2902147..70ebb1a8d 100644 --- a/src/math/polysat/log.cpp +++ b/src/math/polysat/log.cpp @@ -25,9 +25,7 @@ Other: #if POLYSAT_LOGGING_ENABLED -static LogLevel -get_max_log_level(std::string const& fn, std::string const& pretty_fn) -{ +static LogLevel get_max_log_level(std::string const& fn, std::string const& pretty_fn) { (void)fn; (void)pretty_fn; @@ -46,16 +44,12 @@ get_max_log_level(std::string const& fn, std::string const& pretty_fn) } /// Filter log messages -bool -polysat_should_log(LogLevel msg_level, std::string fn, std::string pretty_fn) -{ +bool polysat_should_log(LogLevel msg_level, std::string fn, std::string pretty_fn) { LogLevel max_log_level = get_max_log_level(fn, pretty_fn); return msg_level <= max_log_level; } -static char const* -level_color(LogLevel msg_level) -{ +static char const* level_color(LogLevel msg_level) { switch (msg_level) { case LogLevel::Heading1: return ""; // red @@ -70,9 +64,7 @@ level_color(LogLevel msg_level) int polysat_log_indent_level = 0; -std::pair -polysat_log(LogLevel msg_level, std::string fn, std::string /* pretty_fn */) -{ +std::pair polysat_log(LogLevel msg_level, std::string fn, std::string /* pretty_fn */) { std::ostream& os = std::cerr; size_t width = 20; @@ -87,25 +79,23 @@ polysat_log(LogLevel msg_level, std::string fn, std::string /* pretty_fn */) dwMode |= ENABLE_VIRTUAL_TERMINAL_PROCESSING; ok = ok && SetConsoleMode(hOut, dwMode); #else - int const fd = _fileno(stderr); + int const fd = fileno(stderr); if (color && !isatty(fd)) { color = nullptr; } #endif - if (color) { os << color; } + if (color) + os << color; os << "[" << fn << "] " << std::string(padding, ' '); os << std::string(polysat_log_indent_level, ' '); return {os, (bool)color}; } -polysat_log_indent::polysat_log_indent(int amount) - : m_amount{amount} -{ +polysat_log_indent::polysat_log_indent(int amount): m_amount{amount} { polysat_log_indent_level += m_amount; } -polysat_log_indent::~polysat_log_indent() -{ +polysat_log_indent::~polysat_log_indent() { polysat_log_indent_level -= m_amount; } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index db11bf379..0633ecd9d 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -522,6 +522,7 @@ namespace polysat { LOG("Lemma: " << show_deref(lemma)); clause_ref new_lemma = resolve(v); LOG("New Lemma: " << show_deref(new_lemma)); + // SASSERT(new_lemma); // TODO: only for debugging, to have a breakpoint on resolution failure if (!new_lemma) { backtrack(i, lemma); return; @@ -672,7 +673,7 @@ namespace polysat { } } while (i-- > 0); - add_lemma_clause(lemma); // TODO: handle units correctly + add_lemma(lemma); // TODO: this lemma is stored but otherwise "lost" because it will not be activated / not added to any watch data structures report_unsat(); } @@ -692,44 +693,27 @@ namespace polysat { m_dm.linearize(conflict_dep, deps); } - /** - * The polynomial p encodes an equality that the decision was infeasible. - * The effect of this function is that the assignment to v is undone and replaced - * by a new decision or unit propagation or conflict. - * We add 'p == 0' as a lemma. The lemma depends on the dependencies used - * to derive p, and the level of the lemma is the maximal level of the dependencies. - */ void solver::learn_lemma(pvar v, clause_ref lemma) { if (!lemma) return; LOG("Learning: " << show_deref(lemma)); + SASSERT(lemma->size() > 0); SASSERT(m_conflict_level <= m_justification[v].level()); - if (lemma->size() == 1) { - constraint_ref c; - if (lemma->new_constraints().size() > 0) { - SASSERT_EQ(lemma->new_constraints().size(), 1); - c = lemma->new_constraints()[0]; - } - else { - c = m_constraints.lookup(lemma->literals()[0].var()); - } - SASSERT_EQ(lemma->literals()[0].var(), c->bvar()); - SASSERT(c); - add_lemma_unit(c); - push_cjust(v, c.get()); - activate_constraint_base(c.get(), !lemma->literals()[0].sign()); + clause* cl = lemma.get(); + add_lemma(std::move(lemma)); + if (cl->size() == 1) { + sat::literal lit = cl->literals()[0]; + constraint* c = m_constraints.lookup(lit.var()); + c->set_unit_clause(cl); + push_cjust(v, c); + activate_constraint_base(c, !lit.sign()); + } + else { + sat::literal lit = decide_bool(*cl); + SASSERT(lit != sat::null_literal); + constraint* c = m_constraints.lookup(lit.var()); + push_cjust(v, c); } - else - learn_lemma_clause(v, std::move(lemma)); - } - - void solver::learn_lemma_clause(pvar v, clause_ref lemma) { - SASSERT(lemma); - sat::literal lit = decide_bool(*lemma); - SASSERT(lit != sat::null_literal); - constraint* c = m_constraints.lookup(lit.var()); - push_cjust(v, c); - add_lemma_clause(std::move(lemma)); } // Guess a literal from the given clause; returns the guessed constraint @@ -750,7 +734,6 @@ namespace polysat { return !c->is_currently_false(*this); }; - // constraint *choice = nullptr; sat::literal choice = sat::null_literal; unsigned num_choices = 0; // TODO: should probably cache this? @@ -789,12 +772,7 @@ namespace polysat { rational val = m_value[v]; LOG_H3("Reverting decision: pvar " << v << " := " << val); SASSERT(m_justification[v].is_decision()); - constraints just(m_cjust[v]); backjump(m_justification[v].level()-1); - // Since decision "v -> val" caused a conflict, we may keep all - // viability restrictions on v and additionally exclude val. - // TODO: viability restrictions on 'v' must have happened before decision on 'v'. Do we really need to save/restore m_viable here? - SASSERT(m_cjust[v] == just); // check this with assertion m_viable.add_non_viable(v, val); @@ -815,7 +793,8 @@ namespace polysat { // and then may lead to an assertion failure through this call to narrow. // TODO: what to do with "unassigned" constraints at this point? (we probably should have resolved those away, even in the 'backtrack' case.) // NOTE: they are constraints from clauses that were added to cjust… how to deal with that? should we add the whole clause to cjust? - if (!c->is_undef()) // TODO: this check to be removed once this is fixed properly. + SASSERT(!c->is_undef()); + // if (!c->is_undef()) // TODO: this check to be removed once this is fixed properly. c->narrow(*this); if (is_conflict()) { LOG_H1("Conflict during revert_decision/narrow!"); @@ -902,7 +881,7 @@ namespace polysat { m_conflict.reset(); clause* reason_cl = reason.get(); - add_lemma_clause(std::move(reason)); + add_lemma(std::move(reason)); propagate_bool(~lit, reason_cl); if (is_conflict()) { LOG_H1("Conflict during revert_bool_decision/propagate_bool!"); @@ -924,7 +903,7 @@ namespace polysat { if (reason->literals().size() == 1) { SASSERT(reason->literals()[0] == lit); constraint* c = m_constraints.lookup(lit.var()); - m_redundant.push_back(c); + // m_redundant.push_back(c); activate_constraint_base(c, !lit.sign()); } else @@ -949,6 +928,7 @@ namespace polysat { /// Used for external unit constraints and unit consequences. void solver::activate_constraint_base(constraint* c, bool is_true) { SASSERT(c); + LOG("\n" << *this); // c must be in m_original or m_redundant so it can be deactivated properly when popping the base level SASSERT_EQ(std::count(m_original.begin(), m_original.end(), c) + std::count(m_redundant.begin(), m_redundant.end(), c), 1); sat::literal lit(c->bvar(), !is_true); @@ -1016,30 +996,22 @@ namespace polysat { } // Add lemma to storage but do not activate it - void solver::add_lemma_unit(constraint_ref lemma) { + void solver::add_lemma(clause_ref lemma) { if (!lemma) return; LOG("Lemma: " << show_deref(lemma)); - constraint* c = m_constraints.store(std::move(lemma)); - insert_constraint(m_redundant, c); - // TODO: create unit clause - } - - // Add lemma to storage but do not activate it - void solver::add_lemma_clause(clause_ref lemma) { - if (!lemma) - return; - // TODO: check for unit clauses! - LOG("Lemma: " << show_deref(lemma)); - if (lemma->size() < 2) { - LOG_H1("TODO: this should be treated as unit constraint and asserted at the base level!"); - } - // SASSERT(lemma->size() > 1); + SASSERT(lemma->size() > 0); clause* cl = m_constraints.store(std::move(lemma)); m_redundant_clauses.push_back(cl); + if (cl->size() == 1) { + constraint* c = m_constraints.lookup(cl->literals()[0].var()); + insert_constraint(m_redundant, c); + } } void solver::insert_constraint(ptr_vector& cs, constraint* c) { + SASSERT(c); + LOG_V("INSERTING: " << *c); cs.push_back(c); for (unsigned i = cs.size() - 1; i-- > 0; ) { auto* c1 = cs[i + 1]; @@ -1082,17 +1054,17 @@ namespace polysat { return m_base_levels.empty() ? 0 : m_base_levels.back(); } - bool solver::active_at_base_level(sat::bool_var bvar) const { - // NOTE: this active_at_base_level is actually not what we want!!! - // first of all, it might not really be a base level: could be a non-base level between previous base levels. - // in that case, how do we determine the right dependencies??? - // secondly, we are interested in "unit clauses", not as much whether we assigned something on the base level... - // TODO: however, propagating stuff at the base level... need to be careful with dependencies there... might need to turn all base-level propagations into unit clauses... - VERIFY(false); - // bool res = m_bvars.is_assigned(bvar) && m_bvars.level(bvar) <= base_level(); - // SASSERT_EQ(res, !!m_constraints.lookup(bvar)->unit_clause()); - // return res; - } + // bool solver::active_at_base_level(sat::bool_var bvar) const { + // // NOTE: this active_at_base_level is actually not what we want!!! + // // first of all, it might not really be a base level: could be a non-base level between previous base levels. + // // in that case, how do we determine the right dependencies??? + // // secondly, we are interested in "unit clauses", not as much whether we assigned something on the base level... + // // TODO: however, propagating stuff at the base level... need to be careful with dependencies there... might need to turn all base-level propagations into unit clauses... + // VERIFY(false); + // // bool res = m_bvars.is_assigned(bvar) && m_bvars.level(bvar) <= base_level(); + // // SASSERT_EQ(res, !!m_constraints.lookup(bvar)->unit_clause()); + // // return res; + // } bool solver::try_eval(pdd const& p, rational& out_value) const { pdd r = p.subst_val(assignment()); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index fc66e5507..2b806b5e3 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -126,7 +126,8 @@ namespace polysat { void push_cjust(pvar v, constraint* c) { if (m_cjust[v].contains(c)) // TODO: better check (flag on constraint?) return; - LOG_V("cjust[v" << v << "] += " << *c); + LOG_V("cjust[v" << v << "] += " << show_deref(c)); + SASSERT(c); m_cjust[v].push_back(c); m_trail.push_back(trail_instr_t::just_i); m_cjust_trail.push_back(v); @@ -206,9 +207,6 @@ namespace polysat { bool is_conflict() const { return !m_conflict.empty(); } bool at_base_level() const; unsigned base_level() const; - bool active_at_base_level(sat::bool_var bvar) const; - bool active_at_base_level(sat::literal lit) const { return active_at_base_level(lit.var()); } - bool active_at_base_level(constraint& c) const { return active_at_base_level(c.bvar()); } void resolve_conflict(); void backtrack(unsigned i, clause_ref lemma); @@ -216,10 +214,8 @@ namespace polysat { void revert_decision(pvar v, clause_ref reason); void revert_bool_decision(sat::literal lit, clause_ref reason); void learn_lemma(pvar v, clause_ref lemma); - void learn_lemma_clause(pvar v, clause_ref lemma); void backjump(unsigned new_level); - void add_lemma_unit(constraint_ref lemma); - void add_lemma_clause(clause_ref lemma); + void add_lemma(clause_ref lemma); constraint_literal mk_eq(pdd const& p); constraint_literal mk_diseq(pdd const& p); diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 8201f7b87..1e6d14991 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -265,11 +265,8 @@ namespace polysat { if (is_viable(v, x)) xs.push_back(x); - LOG("Viable for pvar " << v << ": " << xs); + LOG("Viable for v" << v << ": " << xs); } - else { - LOG("Viable for pvar " << v << ": "); - } } #endif diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index b84db711b..9145e498f 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -43,6 +43,7 @@ namespace polysat { public: scoped_solver(std::string name): solver(lim), m_name(name) { + std::cout << "\n\n\n" << std::string(78, '#') << "\n"; std::cout << "\nSTART: " << m_name << "\n"; } @@ -355,7 +356,7 @@ namespace polysat { * We do overflow checks by doubling the base bitwidth here. */ static void test_monot(unsigned base_bw = 5) { - scoped_solver s(__func__); + scoped_solver s(std::string{__func__} + "(" + std::to_string(base_bw) + ")"); auto max_int_const = rational::power_of_two(base_bw) - 1; @@ -589,7 +590,7 @@ namespace polysat { * y*z >= 2^32 */ static void test_monot_bounds(unsigned base_bw = 32) { - scoped_solver s(__func__); + scoped_solver s(std::string{__func__} + "(" + std::to_string(base_bw) + ")"); unsigned bw = 2 * base_bw; auto y = s.var(s.add_var(bw)); auto z = s.var(s.add_var(bw)); @@ -709,6 +710,41 @@ namespace polysat { } + /** + * x*x <= z + * (x+1)*(x+1) <= z + * y == x+1 + * ¬(y*y <= z) + * + * The original version had signed comparisons but that doesn't matter for the UNSAT result. + * UNSAT can be seen easily by substituting the equality. + */ + static void test_subst(unsigned bw = 32) { + scoped_solver s(__func__); + auto x = s.var(s.add_var(bw)); + auto y = s.var(s.add_var(bw)); + auto z = s.var(s.add_var(bw)); + s.add_ule(x * x, z); // optional + s.add_ule((x + 1) * (x + 1), z); + s.add_eq(x + 1 - y); + s.add_ult(z, y*y); + s.check(); + s.expect_unsat(); + } + + static void test_subst_signed(unsigned bw = 32) { + scoped_solver s(__func__); + auto x = s.var(s.add_var(bw)); + auto y = s.var(s.add_var(bw)); + auto z = s.var(s.add_var(bw)); + s.add_sle(x * x, z); // optional + s.add_sle((x + 1) * (x + 1), z); + s.add_eq(x + 1 - y); + s.add_slt(z, y*y); + s.check(); + s.expect_unsat(); + } + // Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases // NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later) @@ -833,8 +869,9 @@ namespace polysat { void tst_polysat() { + polysat::test_subst(); // polysat::test_monot_bounds(8); - polysat::test_monot_bounds_simple(8); + // polysat::test_monot_bounds_simple(8); return; polysat::test_add_conflicts();