diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 984abaef5..9bbab7ea5 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -46,4 +46,32 @@ namespace polysat { return ule(lvl, bvar, static_cast(!sign), b, a, d); } + bool constraint::propagate(solver& s, pvar v) { + LOG_H3("Propagate " << s.m_vars[v] << " in " << *this); + SASSERT(!vars().empty()); + unsigned idx = 0; + if (vars()[idx] != v) + idx = 1; + SASSERT(v == vars()[idx]); + // find other watch variable. + for (unsigned i = vars().size(); i-- > 2; ) { + unsigned other_v = vars()[i]; + if (!s.is_assigned(other_v)) { + s.add_watch(*this, other_v); + std::swap(vars()[idx], vars()[i]); + return true; + } + } + // at most one variable remains unassigned. + unsigned other_v = vars()[idx]; + propagate_core(s, v, other_v); + return false; + } + + void constraint::propagate_core(solver& s, pvar v, pvar other_v) { + (void)v; + (void)other_v; + narrow(s); + } + } diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 86c15ae87..4ded5036a 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -48,7 +48,8 @@ namespace polysat { bool is_sle() const { return m_kind == ckind_t::sle_t; } ckind_t kind() const { return m_kind; } virtual std::ostream& display(std::ostream& out) const = 0; - virtual bool propagate(solver& s, pvar v) = 0; + bool propagate(solver& s, pvar v); + virtual void propagate_core(solver& s, pvar v, pvar other_v); virtual constraint* resolve(solver& s, pvar v) = 0; virtual bool is_always_false() = 0; virtual bool is_currently_false(solver& s) = 0; @@ -66,6 +67,8 @@ namespace polysat { bool is_positive() const { return m_status == l_true; } bool is_negative() const { return m_status == l_false; } bool is_undef() const { return m_status == l_undef; } + + /** Precondition: all variables other than v are assigned. */ virtual bool forbidden_interval(solver& s, pvar v, eval_interval& i, constraint*& neg_condition) { return false; } }; @@ -75,6 +78,10 @@ namespace polysat { scoped_ptr_vector m_literals; public: clause() {} + clause(scoped_ptr&& c) { + SASSERT(c); + m_literals.push_back(c.detach()); + } clause(scoped_ptr_vector&& literals): m_literals(std::move(literals)) { SASSERT(std::all_of(m_literals.begin(), m_literals.end(), [](constraint* c) { return c != nullptr; })); SASSERT(empty() || std::all_of(m_literals.begin(), m_literals.end(), [this](constraint* c) { return c->level() == level(); })); diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp index e971c1a56..b09cbd182 100644 --- a/src/math/polysat/eq_constraint.cpp +++ b/src/math/polysat/eq_constraint.cpp @@ -22,26 +22,6 @@ namespace polysat { return out << p() << (sign() == pos_t ? " == 0" : " != 0") << " [" << m_status << "]"; } - bool eq_constraint::propagate(solver& s, pvar v) { - LOG_H3("Propagate " << s.m_vars[v] << " in " << *this); - SASSERT(!vars().empty()); - unsigned idx = 0; - if (vars()[idx] != v) - idx = 1; - SASSERT(v == vars()[idx]); - // find other watch variable. - for (unsigned i = vars().size(); i-- > 2; ) { - if (!s.is_assigned(vars()[i])) { - std::swap(vars()[idx], vars()[i]); - return true; - } - } - // at most one variable remains unassigned. - - narrow(s); - return false; - } - constraint* eq_constraint::resolve(solver& s, pvar v) { if (is_positive()) return eq_resolve(s, v); @@ -52,10 +32,50 @@ namespace polysat { } void eq_constraint::narrow(solver& s) { - if (is_positive()) - eq_narrow(s); - if (is_negative()) - diseq_narrow(s); + SASSERT(!is_undef()); + LOG("Assignment: " << s.m_search); + auto q = p().subst_val(s.m_search); + LOG("Substituted: " << p() << " := " << q); + if (q.is_zero()) { + if (is_positive()) + return; + if (is_negative()) { + LOG("Conflict (zero under current assignment)"); + s.set_conflict(*this); + return; + } + } + if (q.is_never_zero()) { + if (is_positive()) { + LOG("Conflict (never zero under current assignment)"); + s.set_conflict(*this); + return; + } + if (is_negative()) + return; + } + + if (q.is_unilinear()) { + // a*x + b == 0 + pvar v = q.var(); + rational a = q.hi().val(); + rational b = q.lo().val(); + bddv const& x = s.var2bits(v).var(); + bddv lhs = a * x + b; + rational zero = rational::zero(); + bdd xs = is_positive() ? (lhs == zero) : (lhs != zero); + s.push_cjust(v, this); + s.intersect_viable(v, xs); + + rational val; + if (s.find_viable(v, val) == dd::find_t::singleton) { + s.propagate(v, val, *this); + } + + return; + } + + // TODO: what other constraints can be extracted cheaply? } bool eq_constraint::is_always_false() { @@ -87,6 +107,7 @@ namespace polysat { return false; } + /** * Equality constraints */ @@ -112,39 +133,6 @@ namespace polysat { return nullptr; } - void eq_constraint::eq_narrow(solver& s) { - LOG("Assignment: " << s.m_search); - auto q = p().subst_val(s.m_search); - LOG("Substituted: " << p() << " := " << q); - if (q.is_zero()) - return; - if (q.is_never_zero()) { - LOG("Conflict (never zero under current assignment)"); - s.set_conflict(*this); - return; - } - - if (q.is_unilinear()) { - // a*x + b == 0 - pvar v = q.var(); - rational a = q.hi().val(); - rational b = q.lo().val(); - bddv const& x = s.var2bits(v).var(); - bdd xs = (a * x + b == rational(0)); - s.push_cjust(v, this); - s.intersect_viable(v, xs); - - rational val; - if (s.find_viable(v, val) == dd::find_t::singleton) { - s.propagate(v, val, *this); - } - - return; - } - - // TODO: what other constraints can be extracted cheaply? - } - /** * Disequality constraints @@ -155,8 +143,67 @@ namespace polysat { return nullptr; } - void eq_constraint::diseq_narrow(solver& s) { - NOT_IMPLEMENTED_YET(); + + + /// Compute forbidden interval for equality constraint by considering it as p <=u 0 (or p >u 0 for disequality) + bool eq_constraint::forbidden_interval(solver& s, pvar v, eval_interval& i, constraint*& neg_condition) + { + SASSERT(!is_undef()); + + // Current only works when degree(v) is at most one + unsigned const deg = p().degree(v); + if (deg > 1) + return false; + + if (deg == 0) { + UNREACHABLE(); // this case is not useful for conflict resolution (but it could be handled in principle) + // i is empty or full, condition would be this constraint itself? + return true; + } + + unsigned const sz = s.size(v); + dd::pdd_manager& m = s.sz2pdd(sz); + + pdd p1 = m.zero(); + pdd e1 = m.zero(); + p().factor(v, 1, p1, e1); + + pdd e2 = m.zero(); + + // Currently only works if coefficient is a power of two + if (!p1.is_val()) + return false; + rational a1 = p1.val(); + // TODO: to express the interval for coefficient 2^i symbolically, we need right-shift/upper-bits-extract in the language. + // So currently we can only do it if the coefficient is 1. + if (!a1.is_zero() && !a1.is_one()) + return false; + /* + unsigned j1 = 0; + if (!a1.is_zero() && !a1.is_power_of_two(j1)) + return false; + */ + + // Concrete values of evaluable terms + auto e1s = e1.subst_val(s.m_search); + auto e2s = m.zero(); + SASSERT(e1s.is_val()); + SASSERT(e2s.is_val()); + + // e1 + t <= 0, with t = 2^j1*y + // condition for empty/full: 0 == -1, never satisfied, so we always have a proper interval! + SASSERT(!a1.is_zero()); + pdd lo = 1 - e1; + rational lo_val = (1 - e1s).val(); + pdd hi = -e1; + rational hi_val = (-e1s).val(); + if (is_negative()) { + swap(lo, hi); + lo_val.swap(hi_val); + } + i = eval_interval::proper(lo, lo_val, hi, hi_val); + neg_condition = nullptr; + return true; } } diff --git a/src/math/polysat/eq_constraint.h b/src/math/polysat/eq_constraint.h index 5951a4b88..d8b622a75 100644 --- a/src/math/polysat/eq_constraint.h +++ b/src/math/polysat/eq_constraint.h @@ -27,18 +27,16 @@ namespace polysat { ~eq_constraint() override {} pdd const & p() const { return m_poly; } std::ostream& display(std::ostream& out) const override; - bool propagate(solver& s, pvar v) override; constraint* resolve(solver& s, pvar v) override; bool is_always_false() override; bool is_currently_false(solver& s) override; bool is_currently_true(solver& s) override; void narrow(solver& s) override; + bool forbidden_interval(solver& s, pvar v, eval_interval& i, constraint*& neg_condition) override; private: constraint* eq_resolve(solver& s, pvar v); - void eq_narrow(solver& s); constraint* diseq_resolve(solver& s, pvar v); - void diseq_narrow(solver& s); }; } diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 949e8fa26..e2acfbe10 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -20,7 +20,7 @@ namespace polysat { struct fi_record { eval_interval interval; - scoped_ptr cond; // could be multiple constraints later + scoped_ptr neg_cond; // could be multiple constraints later constraint* src; }; @@ -72,15 +72,12 @@ namespace polysat { for (constraint* c : conflict) { LOG("constraint: " << *c); eval_interval interval = eval_interval::full(); - constraint* cond = nullptr; // TODO: change to scoped_ptr - if (c->forbidden_interval(s, v, interval, cond)) { + constraint* neg_cond = nullptr; // TODO: change to scoped_ptr + if (c->forbidden_interval(s, v, interval, neg_cond)) { LOG("~> interval: " << interval); - if (cond) - LOG(" cond: " << *cond); - else - LOG(" cond: "); + LOG(" neg_cond: " << show_deref(neg_cond)); if (interval.is_currently_empty()) { - dealloc(cond); + dealloc(neg_cond); continue; } if (interval.is_full()) @@ -92,19 +89,20 @@ namespace polysat { longest_i = records.size(); } } - records.push_back({std::move(interval), cond, c}); + records.push_back({std::move(interval), neg_cond, c}); if (has_full) break; } } + LOG("has_full: " << std::boolalpha << has_full); if (has_full) { - auto const& full_record = records.back(); + // We have a single interval covering the whole domain + // => the side conditions of that interval are enough to produce a conflict + auto& full_record = records.back(); SASSERT(full_record.interval.is_full()); - LOG("has_full: " << std::boolalpha << has_full); - // TODO: use full interval to explain - NOT_IMPLEMENTED_YET(); - return false; + out_lemma = std::move(full_record.neg_cond); + return true; } if (records.empty()) @@ -153,9 +151,9 @@ namespace polysat { literals.push_back(c); // Side conditions // TODO: check whether the condition is subsumed by c? maybe at the end do a "lemma reduction" step, to try and reduce branching? - scoped_ptr& cond = records[i].cond; - if (cond) - literals.push_back(cond.detach()); + scoped_ptr& neg_cond = records[i].neg_cond; + if (neg_cond) + literals.push_back(neg_cond.detach()); } out_lemma = std::move(literals); diff --git a/src/math/polysat/log.h b/src/math/polysat/log.h index 6653ebfc7..27de02d8a 100644 --- a/src/math/polysat/log.h +++ b/src/math/polysat/log.h @@ -18,6 +18,7 @@ #include #include #include +#include "math/polysat/log_helper.h" class polysat_log_indent { diff --git a/src/math/polysat/log_helper.h b/src/math/polysat/log_helper.h new file mode 100644 index 000000000..dd316fdde --- /dev/null +++ b/src/math/polysat/log_helper.h @@ -0,0 +1,44 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + Logging support + +Abstract: + + Utilities for logging. + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#pragma once + +#include +#include "util/util.h" + +template +struct show_deref_t { + T* ptr; +}; + +template +std::ostream& operator<<(std::ostream& os, show_deref_t s) { + if (s.ptr) + return os << *s.ptr; + else + return os << ""; +} + +template +show_deref_t show_deref(T* ptr) { + return show_deref_t{ptr}; +} + +template +show_deref_t show_deref(scoped_ptr const& ptr) { + return show_deref_t{ptr.get()}; +} diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 789382298..d2f1b9050 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -50,7 +50,6 @@ namespace polysat { void solver::add_non_viable(pvar v, rational const& val) { LOG("pvar " << v << " /= " << val); - TRACE("polysat", tout << "v" << v << " /= " << val << "\n";); SASSERT(is_viable(v, val)); auto const& bits = var2bits(v); intersect_viable(v, bits.var() != val); @@ -120,6 +119,7 @@ namespace polysat { else if (!can_decide()) { LOG_H2("SAT"); return l_true; } else decide(); } + LOG_H2("UNDEF (resource limit)"); return l_undef; } @@ -194,6 +194,21 @@ namespace polysat { } bool_var solver::new_sle(pdd const& p, pdd const& q, unsigned dep, csign_t sign) { + // To do signed comparison of bitvectors, flip the msb and do unsigned comparison: + // + // x <=s y <=> x + 2^(w-1) <=u y + 2^(w-1) + // + // Example for bit width 3: + // 111 -1 + // 110 -2 + // 101 -3 + // 100 -4 + // 011 3 + // 010 2 + // 001 1 + // 000 0 + // + // Argument: flipping the msb swaps the negative and non-negative blocks auto shift = rational::power_of_two(p.power_of_2() - 1); return new_ule(p + shift, q + shift, dep, sign); } @@ -219,7 +234,11 @@ namespace polysat { LOG("WARN: there is no constraint for bool_var " << v); return; } + if (is_conflict()) + return; + SASSERT(c->is_undef()); c->assign_eh(is_true); + LOG("Activate constraint: " << *c); add_watch(*c); m_assign_eh_history.push_back(v); m_trail.push_back(trail_instr_t::assign_eh_i); @@ -235,6 +254,7 @@ namespace polysat { push_qhead(); while (can_propagate()) propagate(m_search[m_qhead++].first); + SASSERT(wlist_invariant()); } void solver::propagate(pvar v) { @@ -250,6 +270,7 @@ namespace polysat { } void solver::propagate(pvar v, rational const& val, constraint& c) { + LOG("Propagation: pvar " << v << " := " << val << ", due to " << c); if (is_viable(v, val)) { m_free_vars.del_var_eh(v); assign_core(v, val, justification::propagation(m_level)); @@ -326,10 +347,15 @@ namespace polysat { void solver::add_watch(constraint& c) { auto const& vars = c.vars(); - if (vars.size() > 0) - m_watch[vars[0]].push_back(&c); - if (vars.size() > 1) - m_watch[vars[1]].push_back(&c); + if (vars.size() > 0) + add_watch(c, vars[0]); + if (vars.size() > 1) + add_watch(c, vars[1]); + } + + void solver::add_watch(constraint &c, pvar v) { + LOG("watching v" << v << " of constraint " << c); + m_watch[v].push_back(&c); } void solver::erase_watch(constraint& c) { @@ -366,10 +392,14 @@ namespace polysat { switch (find_viable(v, val)) { case dd::find_t::empty: LOG("Conflict: no value for pvar " << v); + // NOTE: all such cases should be discovered elsewhere (e.g., during propagation/narrowing) + // (fail here in debug mode so we notice if we miss some) + DEBUG_CODE( UNREACHABLE(); ); set_conflict(v); break; case dd::find_t::singleton: LOG("Propagation: pvar " << v << " := " << val << " (due to unique value)"); + // NOTE: this case may happen legitimately if all other possibilities were excluded by brute force search assign_core(v, val, justification::propagation(m_level)); break; case dd::find_t::multiple: @@ -387,6 +417,7 @@ namespace polysat { ++m_stats.m_num_propagations; LOG("pvar " << v << " := " << val << " by " << j); SASSERT(is_viable(v, val)); + SASSERT(std::all_of(m_search.begin(), m_search.end(), [v](auto p) { return p.first != v; })); m_value[v] = val; m_search.push_back(std::make_pair(v, val)); m_trail.push_back(trail_instr_t::assign_i); @@ -451,12 +482,22 @@ namespace polysat { LOG_H2("Conflict due to empty viable set for pvar " << conflict_var); clause new_lemma; if (forbidden_intervals::explain(*this, m_conflict, conflict_var, new_lemma)) { - LOG_H3("Learning disjunctive lemma"); + LOG_H3("Lemma from forbidden intervals (size: " << new_lemma.size() << ")"); + for (constraint* c : new_lemma) + LOG("Literal: " << *c); SASSERT(new_lemma.size() > 0); if (new_lemma.size() == 1) { lemma = new_lemma.detach()[0]; - // TODO: continue normally? - } else { + SASSERT(lemma); + lemma->assign_eh(true); + reset_marks(); + for (auto v : lemma->vars()) + set_mark(v); + m_conflict.reset(); + m_conflict.push_back(lemma.get()); + // continue normally + } + else { SASSERT(m_disjunctive_lemma.empty()); reset_marks(); for (constraint* c : new_lemma) { @@ -568,13 +609,16 @@ namespace polysat { void solver::learn_lemma(pvar v, constraint* c) { if (!c) return; + LOG("Learning: " << *c); SASSERT(m_conflict_level <= m_justification[v].level()); push_cjust(v, c); add_lemma(c); } /** - * variable v was assigned by a decision at position i in the search stack. + * Revert a decision that caused a conflict. + * Variable v was assigned by a decision at position i in the search stack. + * * TODO: we could resolve constraints in cjust[v] against each other to * obtain stronger propagation. Example: * (x + 1)*P = 0 and (x + 1)*Q = 0, where gcd(P,Q) = 1, then we have x + 1 = 0. @@ -584,23 +628,31 @@ namespace polysat { */ void solver::revert_decision(pvar v) { rational val = m_value[v]; + LOG_H3("Reverting decision: pvar " << v << " -> " << val); SASSERT(m_justification[v].is_decision()); bdd viable = m_viable[v]; constraints just(m_cjust[v]); backjump(m_justification[v].level()-1); - for (unsigned i = m_cjust[v].size(); i < just.size(); ++i) - push_cjust(v, just[i]); - for (constraint* c : m_conflict) { - push_cjust(v, c); - c->narrow(*this); - } - m_conflict.reset(); + // Since decision "v -> val" caused a conflict, we may keep all + // viability restrictions on v and additionally exclude val. push_viable(v); m_viable[v] = viable; add_non_viable(v, val); - m_free_vars.del_var_eh(v); + for (unsigned i = m_cjust[v].size(); i < just.size(); ++i) + push_cjust(v, just[i]); + for (constraint* c : m_conflict) { + // Add the conflict as justification for the exclusion of 'val' + push_cjust(v, c); + // NOTE: in general, narrow may change the conflict. + // But since we just backjumped, narrowing should not result in an additional conflict. + c->narrow(*this); + } + m_conflict.reset(); narrow(v); - decide(v); + if (m_justification[v].is_unassigned()) { + m_free_vars.del_var_eh(v); + decide(v); + } } void solver::backjump(unsigned new_level) { @@ -616,10 +668,13 @@ namespace polysat { constraint* solver::resolve(pvar v) { SASSERT(!m_cjust[v].empty()); SASSERT(m_justification[v].is_propagation()); + LOG("resolve pvar " << v); if (m_cjust[v].size() != 1) return nullptr; constraint* d = m_cjust[v].back(); - return d->resolve(*this, v); + constraint* res = d->resolve(*this, v); + LOG("resolved: " << show_deref(res)); + return res; } /** @@ -633,6 +688,7 @@ namespace polysat { if (!c) return; LOG("Lemma: " << *c); + SASSERT(!c->is_undef()); SASSERT(!get_bv2c(c->bvar())); insert_bv2c(c->bvar(), c); add_watch(*c); @@ -666,6 +722,7 @@ namespace polysat { unsigned base_level = m_base_levels[m_base_levels.size() - num_scopes]; LOG("Pop " << num_scopes << " user scopes; lowest popped level = " << base_level << "; current level = " << m_level); pop_levels(m_level - base_level + 1); + m_conflict.reset(); // TODO: maybe keep conflict if level of all constraints is lower than base_level? } bool solver::at_base_level() const { @@ -712,6 +769,29 @@ namespace polysat { return true; } + /** + * Check that two variables of each constraint are watched. + */ + bool solver::wlist_invariant() { + constraints cs; + cs.append(m_constraints.size(), m_constraints.data()); + cs.append(m_redundant.size(), m_redundant.data()); + for (auto* c : cs) { + unsigned num_watches = 0; + for (auto const& wlist : m_watch) { + unsigned n = std::count(wlist.begin(), wlist.end(), c); + VERIFY(n <= 1); // no duplicates in the watchlist + num_watches += n; + } + switch (c->vars().size()) { + case 0: VERIFY(num_watches == 0); break; + case 1: VERIFY(num_watches == 1); break; + default: VERIFY(num_watches == 2); break; + } + } + return true; + } + } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 85c3d6f09..21bfcf5ad 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -38,6 +38,7 @@ namespace polysat { stats() { reset(); } }; + friend class constraint; friend class eq_constraint; friend class var_constraint; friend class ule_constraint; @@ -187,6 +188,7 @@ namespace polysat { void erase_watch(pvar v, constraint& c); void erase_watch(constraint& c); void add_watch(constraint& c); + void add_watch(constraint& c, pvar v); void set_conflict(constraint& c); void set_conflict(pvar v); @@ -225,6 +227,7 @@ namespace polysat { bool invariant(); bool invariant(scoped_ptr_vector const& cs); + bool wlist_invariant(); public: diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index b7a32ec59..0d560c761 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -22,30 +22,12 @@ namespace polysat { return out << m_lhs << (sign() == pos_t ? " <=u " : " >u ") << m_rhs << " [" << m_status << "]"; } - bool ule_constraint::propagate(solver& s, pvar v) { - LOG_H3("Propagate " << s.m_vars[v] << " in " << *this); - SASSERT(!vars().empty()); - unsigned idx = 0; - if (vars()[idx] != v) - idx = 1; - SASSERT(v == vars()[idx]); - // find other watch variable. - for (unsigned i = vars().size(); i-- > 2; ) { - if (!s.is_assigned(vars()[i])) { - std::swap(vars()[idx], vars()[i]); - return true; - } - } - - narrow(s); - return false; - } - constraint* ule_constraint::resolve(solver& s, pvar v) { return nullptr; } void ule_constraint::narrow(solver& s) { + SASSERT(!is_undef()); LOG("Assignment: " << s.m_search); auto p = lhs().subst_val(s.m_search); LOG("Substituted LHS: " << lhs() << " := " << p); @@ -136,9 +118,6 @@ namespace polysat { return p.is_val() && q.is_val() && p.val() > q.val(); } - /** - * Precondition: all variables other than v are assigned. - */ bool ule_constraint::forbidden_interval(solver& s, pvar v, eval_interval& i, constraint*& neg_condition) { SASSERT(!is_undef()); diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h index 9bf51b1cc..7df4ea53b 100644 --- a/src/math/polysat/ule_constraint.h +++ b/src/math/polysat/ule_constraint.h @@ -32,7 +32,6 @@ namespace polysat { pdd const& lhs() const { return m_lhs; } pdd const& rhs() const { return m_rhs; } std::ostream& display(std::ostream& out) const override; - bool propagate(solver& s, pvar v) override; constraint* resolve(solver& s, pvar v) override; bool is_always_false(pdd const& lhs, pdd const& rhs); bool is_always_false() override; diff --git a/src/math/polysat/var_constraint.cpp b/src/math/polysat/var_constraint.cpp index aae02f408..2c788f553 100644 --- a/src/math/polysat/var_constraint.cpp +++ b/src/math/polysat/var_constraint.cpp @@ -21,11 +21,6 @@ namespace polysat { return out << "v" << m_var << ": " << m_viable << "\n"; } - bool var_constraint::propagate(solver& s, pvar v) { - UNREACHABLE(); - return false; - } - constraint* var_constraint::resolve(solver& s, pvar v) { UNREACHABLE(); return nullptr; diff --git a/src/math/polysat/var_constraint.h b/src/math/polysat/var_constraint.h index 700bc209a..9d2a0380e 100644 --- a/src/math/polysat/var_constraint.h +++ b/src/math/polysat/var_constraint.h @@ -33,7 +33,6 @@ namespace polysat { constraint(lvl, bvar, sign, dep, ckind_t::bit_t), m_var(v), m_viable(b) {} ~var_constraint() override {} std::ostream& display(std::ostream& out) const override; - bool propagate(solver& s, pvar v) override; constraint* resolve(solver& s, pvar v) override; void narrow(solver& s) override; bool is_always_false() override; diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 6a152e9c5..f29e13d5b 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -63,6 +63,21 @@ namespace polysat { s.check(); } + /// Has constraints which must be inserted into other watchlist to discover UNSAT + static void test_wlist() { + scoped_solver s; + auto a = s.var(s.add_var(3)); + auto b = s.var(s.add_var(3)); + auto c = s.var(s.add_var(3)); + auto d = s.var(s.add_var(3)); + s.add_eq(d + c + b + a + 1); + s.add_eq(d + c + b + a); + s.add_eq(d + c + b); + s.add_eq(d + c); + s.add_eq(d); + s.check(); + } + /** * most basic linear equation solving. @@ -143,6 +158,23 @@ namespace polysat { s.check(); } + /** + * unsat + * - learns 3*x + 1 == 0 by polynomial resolution + * - this forces x == 5, which means the first constraint is unsatisfiable by parity. + */ + static void test_p3() { + scoped_solver s; + auto x = s.var(s.add_var(4)); + auto y = s.var(s.add_var(4)); + auto z = s.var(s.add_var(4)); + s.add_eq(x*x*y + 3*y + 7); + s.add_eq(2*y + z + 8); + s.add_eq(3*x + 4*y*z + 2*z*z + 1); + s.check(); + } + + // Unique solution: u = 5 static void test_ineq_basic1() { scoped_solver s; @@ -376,15 +408,23 @@ namespace polysat { void tst_polysat() { polysat::test_add_conflicts(); + polysat::test_wlist(); polysat::test_l1(); polysat::test_l2(); polysat::test_l3(); polysat::test_l4(); polysat::test_l5(); -#if 0 - // worry about this later polysat::test_p1(); polysat::test_p2(); + polysat::test_p3(); + polysat::test_ineq_basic1(); + polysat::test_ineq_basic2(); + polysat::test_ineq_basic3(); + polysat::test_ineq_basic4(); + polysat::test_ineq_basic5(); + polysat::test_ineq_basic6(); +#if 0 + // worry about this later polysat::test_ineq1(); polysat::test_ineq2(); #endif diff --git a/src/util/scoped_ptr_vector.h b/src/util/scoped_ptr_vector.h index 701815bee..32cd67a68 100644 --- a/src/util/scoped_ptr_vector.h +++ b/src/util/scoped_ptr_vector.h @@ -87,6 +87,8 @@ public: return tmp; } + T* const* data() const { return m_vector.data(); } + using const_iterator = typename ptr_vector::const_iterator; const_iterator begin() const { return m_vector.begin(); } const_iterator end() const { return m_vector.end(); }