From f83705bf9fd95d16f6f03d8d4ee40e0b117ea013 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 29 Apr 2021 19:12:54 +0200 Subject: [PATCH] Polysat: first pass at forbidden intervals (not yet fully integrated into solver) (#5227) * Add interval class * Take dependency as const reference * Compute forbidden intervals for ule-constraints * Add class for evaluated interval * We need the evaluated bounds as well * Don't add constraint to cjust multiple times (hack, to be improved later) * typo * More interval helpers * Add constraint::ult factory function * Fix forbidden interval condition * Add solver::has_viable * Add conflict explanation using forbidden intervals (not yet fully integrated into solver) --- src/math/dd/dd_pdd.h | 3 + src/math/polysat/CMakeLists.txt | 1 + src/math/polysat/constraint.cpp | 11 +- src/math/polysat/constraint.h | 11 +- src/math/polysat/eq_constraint.h | 2 +- src/math/polysat/fixplex_def.h | 2 +- src/math/polysat/forbidden_intervals.cpp | 163 +++++++++++++++++++++++ src/math/polysat/forbidden_intervals.h | 29 ++++ src/math/polysat/interval.h | 107 +++++++++++++++ src/math/polysat/solver.cpp | 29 +++- src/math/polysat/solver.h | 10 +- src/math/polysat/ule_constraint.cpp | 140 +++++++++++++++++++ src/math/polysat/ule_constraint.h | 4 +- src/math/polysat/var_constraint.h | 2 +- 14 files changed, 501 insertions(+), 13 deletions(-) create mode 100644 src/math/polysat/forbidden_intervals.cpp create mode 100644 src/math/polysat/forbidden_intervals.h create mode 100644 src/math/polysat/interval.h diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 224e567d9..e5024e0c2 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -430,6 +430,7 @@ namespace dd { unsigned max_pow2_divisor() const { return m.max_pow2_divisor(root); } unsigned_vector const& free_vars() const { return m.free_vars(*this); } + void swap(pdd& other) { std::swap(root, other.root); } pdd_iterator begin() const; pdd_iterator end() const; @@ -457,6 +458,8 @@ namespace dd { inline pdd& operator-=(pdd & p, pdd const& q) { p = p - q; return p; } inline pdd& operator+=(pdd & p, pdd const& q) { p = p + q; return p; } + inline void swap(pdd& p, pdd& q) { p.swap(q); } + std::ostream& operator<<(std::ostream& out, pdd const& b); struct pdd_monomial { diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index e678bcc32..9e3a45798 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -4,6 +4,7 @@ z3_add_component(polysat eq_constraint.cpp ule_constraint.cpp var_constraint.cpp + forbidden_intervals.cpp justification.cpp log.cpp solver.cpp diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 35db88e10..984abaef5 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -29,16 +29,21 @@ namespace polysat { return *dynamic_cast(this); } - constraint* constraint::eq(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref& d) { + constraint* constraint::eq(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref const& d) { return alloc(eq_constraint, lvl, bvar, sign, p, d); } - constraint* constraint::viable(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const& b, p_dependency_ref& d) { + constraint* constraint::viable(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const& b, p_dependency_ref const& d) { return alloc(var_constraint, lvl, bvar, sign, v, b, d); } - constraint* constraint::ule(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref& d) { + constraint* constraint::ule(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { return alloc(ule_constraint, lvl, bvar, sign, a, b, d); } + constraint* constraint::ult(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) { + // a < b <=> !(b <= a) + return ule(lvl, bvar, static_cast(!sign), b, a, d); + } + } diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 788b2edc0..8b7f1e6a0 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -13,6 +13,7 @@ Author: --*/ #pragma once #include "math/polysat/types.h" +#include "math/polysat/interval.h" namespace polysat { @@ -34,12 +35,13 @@ namespace polysat { bool_var m_bool_var; csign_t m_sign; ///< sign/polarity lbool m_status = l_undef; ///< current constraint status, computed from value of m_bool_var and m_sign - constraint(unsigned lvl, bool_var bvar, csign_t sign, p_dependency_ref& dep, ckind_t k): + constraint(unsigned lvl, bool_var bvar, csign_t sign, p_dependency_ref const& dep, ckind_t k): m_level(lvl), m_kind(k), m_dep(dep), m_bool_var(bvar), m_sign(sign) {} public: - static constraint* eq(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref& d); - static constraint* viable(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const& b, p_dependency_ref& d); - static constraint* ule(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref& d); + static constraint* eq(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref const& d); + static constraint* viable(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const& b, p_dependency_ref const& d); + static constraint* ule(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); + static constraint* ult(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d); virtual ~constraint() {} bool is_eq() const { return m_kind == ckind_t::eq_t; } bool is_ule() const { return m_kind == ckind_t::ule_t; } @@ -63,6 +65,7 @@ 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; } + virtual bool forbidden_interval(solver& s, pvar v, eval_interval& i, constraint*& neg_condition) { return false; } }; inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); } diff --git a/src/math/polysat/eq_constraint.h b/src/math/polysat/eq_constraint.h index c20f0e35b..5951a4b88 100644 --- a/src/math/polysat/eq_constraint.h +++ b/src/math/polysat/eq_constraint.h @@ -20,7 +20,7 @@ namespace polysat { class eq_constraint : public constraint { pdd m_poly; public: - eq_constraint(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref& dep): + eq_constraint(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref const& dep): constraint(lvl, bvar, sign, dep, ckind_t::eq_t), m_poly(p) { m_vars.append(p.free_vars()); } diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h index 7196f74c7..ba262d859 100644 --- a/src/math/polysat/fixplex_def.h +++ b/src/math/polysat/fixplex_def.h @@ -246,7 +246,7 @@ namespace polysat { numeral b = m.inv(a_ij >> (tz1 - tz2)); M.mul(r_i, a); M.add(r_i, b, r_k); - unsigned x_k = m_row[rk].m_base; + unsigned x_k = m_rows[rk].m_base; // TBD: redo according to slides // TBD: std::swap(m_row2base[ri], m_row2base[rk]); diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp new file mode 100644 index 000000000..7b16dabef --- /dev/null +++ b/src/math/polysat/forbidden_intervals.cpp @@ -0,0 +1,163 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + Conflict explanation using forbidden intervals as described in + "Solving bitvectors with MCSAT: explanations from bits and pieces" + by S. Graham-Lengrand, D. Jovanovic, B. Dutertre. + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#include "math/polysat/forbidden_intervals.h" +#include "math/polysat/log.h" + +namespace polysat { + + struct fi_record { + eval_interval interval; + scoped_ptr cond; // could be multiple constraints later + constraint* src; + }; + + /** + * Find a sequence of intervals that covers all of Z_modulus. + * + * \returns true iff such a covering exists + * \param longest_i: the longest interval (as index into 'records') + * \param out_seq: will contain the covering (as list of indices into 'records') + */ + static bool find_covering_sequence(vector const& records, unsigned longest_i, rational modulus, unsigned_vector& out_seq) { + rational baseline = records[longest_i].interval.hi_val(); + while (!records[longest_i].interval.currently_contains(baseline)) { + rational best_extent = rational::zero(); + unsigned furthest_i = UINT_MAX; + for (unsigned i = records.size(); i-- > 0; ) { + auto const& interval = records[i].interval; + if (interval.currently_contains(baseline)) { + rational extent = mod(interval.hi_val() - baseline, modulus); + if (extent > best_extent) { + best_extent = extent; + furthest_i = i; + } + } + } + if (furthest_i == UINT_MAX) { + // There's a hole we can't cover. + // This can happen if a constraint didn't produce an interval + // (but not necessarily, values may be covered by multiple constraints) + return false; + } + SASSERT(best_extent > 0); + out_seq.push_back(furthest_i); + baseline = records[furthest_i].interval.hi_val(); + } + SASSERT(out_seq.size() > 0); + if (!records[out_seq[0]].interval.currently_contains(baseline)) + out_seq.push_back(longest_i); + return true; + } + + bool forbidden_intervals::explain(solver& s, ptr_vector const& conflict, pvar v, scoped_ptr_vector& out_lemma) { + + // Extract forbidden intervals from conflicting constraints + vector records; + bool has_full = false; + rational longest_len; + unsigned longest_i = UINT_MAX; + 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)) { + LOG("~> interval: " << interval); + if (cond) + LOG(" cond: " << *cond); + else + LOG(" cond: "); + if (interval.is_currently_empty()) { + dealloc(cond); + continue; + } + if (interval.is_full()) + has_full = true; + else { + auto const len = interval.current_len(); + if (len > longest_len) { + longest_len = len; + longest_i = records.size(); + } + } + records.push_back({std::move(interval), cond, c}); + if (has_full) + break; + } + } + + if (has_full) { + auto const& 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; + } + + if (records.empty()) + return false; + + SASSERT(longest_i != UINT_MAX); + LOG("longest: i=" << longest_i << "; " << records[longest_i].interval); + + rational const modulus = rational::power_of_two(s.size(v)); + + // Select a sequence of covering intervals + unsigned_vector seq; + if (!find_covering_sequence(records, longest_i, modulus, seq)) { + return false; + } + LOG("seq: " << seq); + + p_dependency* d = nullptr; + unsigned lemma_lvl = 0; + for (unsigned i : seq) { + constraint* c = records[i].src; + d = s.m_dm.mk_join(d, c->dep()); + lemma_lvl = std::max(lemma_lvl, c->level()); + } + p_dependency_ref lemma_dep(d, s.m_dm); + + // Create lemma + // Idea: + // - If the side conditions hold, and + // - the upper bound of each interval is contained in the next interval, + // then the forbidden intervals cover the whole domain and we have a conflict. + // We learn the negation of this conjunction. + for (unsigned seq_i = seq.size(); seq_i-- > 0; ) { + unsigned const i = seq[seq_i]; + unsigned const next_i = seq[(seq_i+1) % seq.size()]; + // Build constraint: upper bound of each interval is not contained in the next interval, + // using the equivalence: t \in [l;h[ <=> t-l < h-l + auto const& hi = records[i].interval.hi(); + auto const& next_lo = records[next_i].interval.lo(); + auto const& next_hi = records[next_i].interval.hi(); + auto const& lhs = hi - next_lo; + auto const& rhs = next_hi - next_lo; + constraint* c = constraint::ult(lemma_lvl, s.m_next_bvar++, neg_t, lhs, rhs, lemma_dep); + LOG("constraint: " << *c); + out_lemma.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) + out_lemma.push_back(cond.detach()); + } + + return true; + } + +} diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h new file mode 100644 index 000000000..34ee37bbf --- /dev/null +++ b/src/math/polysat/forbidden_intervals.h @@ -0,0 +1,29 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + Conflict explanation using forbidden intervals as described in + "Solving bitvectors with MCSAT: explanations from bits and pieces" + by S. Graham-Lengrand, D. Jovanovic, B. Dutertre. + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#pragma once +#include "math/polysat/constraint.h" +#include "math/polysat/interval.h" +#include "math/polysat/solver.h" + +namespace polysat { + + class forbidden_intervals { + + public: + static bool explain(solver& s, ptr_vector const& conflict, pvar v, scoped_ptr_vector& out_lemma); + + }; +} diff --git a/src/math/polysat/interval.h b/src/math/polysat/interval.h new file mode 100644 index 000000000..f03bd1f38 --- /dev/null +++ b/src/math/polysat/interval.h @@ -0,0 +1,107 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat intervals + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#pragma once +#include "math/polysat/types.h" +#include "util/optional.h" + +namespace polysat { + + enum class ikind_t { full, proper }; + + struct bounds { + pdd lo; ///< lower bound, inclusive + pdd hi; ///< upper bound, exclusive + }; + + /** + * An interval is either [lo; hi[ (excl. upper bound) or the full domain Z_{2^w}. + * If lo > hi, the interval wraps around, i.e., represents the union of [lo; 2^w[ and [0; hi[. + * Membership test t \in [lo; hi[ is equivalent to t - lo < hi - lo. + */ + class interval { + ikind_t m_kind; + optional m_bounds; + + interval(): m_kind(ikind_t::full) {} + interval(pdd const& lo, pdd const& hi): + m_kind(ikind_t::proper), m_bounds({lo, hi}) {} + public: + static interval empty(dd::pdd_manager& m) { return proper(m.zero(), m.zero()); } + static interval full() { return {}; } + static interval proper(pdd const& lo, pdd const& hi) { return {lo, hi}; } + + bool is_full() const { return m_kind == ikind_t::full; } + bool is_proper() const { return m_kind == ikind_t::proper; } + bool is_always_empty() const { return is_proper() && lo() == hi(); } + pdd const& lo() const { SASSERT(is_proper()); return m_bounds->lo; } + pdd const& hi() const { SASSERT(is_proper()); return m_bounds->hi; } + }; + + inline std::ostream& operator<<(std::ostream& os, interval const& i) { + if (i.is_full()) + return os << "full"; + else + return os << "[" << i.lo() << " ; " << i.hi() << "["; + } + + class eval_interval { + interval m_symbolic; + rational m_concrete_lo; + rational m_concrete_hi; + + eval_interval(interval&& i, rational const& lo_val, rational const& hi_val): + m_symbolic(std::move(i)), m_concrete_lo(lo_val), m_concrete_hi(hi_val) {} + public: + static eval_interval empty(dd::pdd_manager &m) { + return {interval::empty(m), rational::zero(), rational::zero()}; + } + static eval_interval full() { + return {interval::full(), rational::zero(), rational::zero()}; + } + static eval_interval proper(pdd const &lo, rational const &lo_val, pdd const &hi, rational const &hi_val) { + return {interval::proper(lo, hi), lo_val, hi_val}; + } + + bool is_full() const { return m_symbolic.is_full(); } + bool is_proper() const { return m_symbolic.is_proper(); } + bool is_always_empty() const { return m_symbolic.is_always_empty(); } + bool is_currently_empty() const { return is_proper() && lo_val() == hi_val(); } + interval const& symbolic() const { return m_symbolic; } + pdd const& lo() const { return m_symbolic.lo(); } + pdd const& hi() const { return m_symbolic.hi(); } + rational const& lo_val() const { SASSERT(is_proper()); return m_concrete_lo; } + rational const& hi_val() const { SASSERT(is_proper()); return m_concrete_hi; } + rational current_len() const { + SASSERT(is_proper()); + return mod(hi_val() - lo_val(), rational::power_of_two(lo().power_of_2())); + } + bool currently_contains(rational const& val) const { + if (is_full()) + return true; + else if (lo_val() <= hi_val()) + return lo_val() <= val && val < hi_val(); + else + return val < hi_val() || val >= lo_val(); + } + }; + + inline std::ostream& operator<<(std::ostream& os, eval_interval const& i) { + if (i.is_full()) + return os << "full"; + else + return os << i.symbolic() << " := [" << i.lo_val() << ";" << i.hi_val() << "["; + } + + +} diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 1dc55eeae..bba748fb7 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -19,6 +19,7 @@ Author: #include "math/polysat/solver.h" #include "math/polysat/log.h" #include "math/polysat/fixplex_def.h" +#include "math/polysat/forbidden_intervals.h" namespace polysat { @@ -40,6 +41,10 @@ namespace polysat { return *bits; } + bool solver::has_viable(pvar v) { + return !m_viable[v].is_false(); + } + bool solver::is_viable(pvar v, rational const& val) { return var2bits(v).contains(m_viable[v], val); } @@ -421,17 +426,39 @@ namespace polysat { return; } + pvar conflict_var = null_var; scoped_ptr lemma; reset_marks(); for (constraint* c : m_conflict) - for (auto v : c->vars()) + for (auto v : c->vars()) { set_mark(v); + if (!has_viable(v)) { + SASSERT(conflict_var == null_var || conflict_var == v); // at most one variable can be empty + conflict_var = v; + } + } + + if (conflict_var != null_var) { + LOG_H2("Conflict due to empty viable set for pvar " << conflict_var); + scoped_ptr_vector disjunctive_lemma; + if (forbidden_intervals::explain(*this, m_conflict, conflict_var, disjunctive_lemma)) { + LOG_H3("Learning disjunctive lemma"); // << disjunctive_lemma); + SASSERT(disjunctive_lemma.size() > 0); + if (disjunctive_lemma.size() == 1) { + // TODO: continue normally? + } else { + // TODO: solver needs to return l_undef and allow external handling of disjunctive lemma + } + } + } for (unsigned i = m_search.size(); i-- > 0; ) { pvar v = m_search[i].first; + LOG_H2("Working on pvar " << v); if (!is_marked(v)) continue; justification& j = m_justification[v]; + LOG("Justification: " << j); if (j.level() <= base_level()) { report_unsat(); return; diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 0e5a1f200..ef14e6cc8 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -42,6 +42,7 @@ namespace polysat { friend class eq_constraint; friend class var_constraint; friend class ule_constraint; + friend class forbidden_intervals; typedef ptr_vector constraints; @@ -113,12 +114,20 @@ namespace polysat { } void push_cjust(pvar v, constraint* c) { + if (m_cjust[v].contains(c)) // TODO: better check (flag on constraint?) + return; m_cjust[v].push_back(c); m_trail.push_back(trail_instr_t::just_i); m_cjust_trail.push_back(v); } unsigned size(pvar v) const { return m_size[v]; } + + /** + * Check whether variable v has any viable values left according to m_viable. + */ + bool has_viable(pvar v); + /** * check if value is viable according to m_viable. */ @@ -139,7 +148,6 @@ namespace polysat { */ void add_viable_dep(pvar v, p_dependency* dep); - /** * Find a next viable value for variable. */ diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index a1bcb72c9..f1373acb3 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -136,4 +136,144 @@ 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()); + + // Current only works when degree(v) is at most one on both sides + unsigned const deg1 = lhs().degree(v); + unsigned const deg2 = rhs().degree(v); + if (deg1 > 1 || deg2 > 1) + return false; + + if (deg1 == 0 && deg2 == 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(); + if (deg1 == 0) + e1 = lhs(); + else + lhs().factor(v, 1, p1, e1); + + pdd p2 = m.zero(); + pdd e2 = m.zero(); + if (deg2 == 0) + e2 = rhs(); + else + rhs().factor(v, 1, p2, e2); + + // Interval extraction only works if v-coefficients are the same + if (deg1 != 0 && deg2 != 0 && p1 != p2) + return false; + + // Currently only works if coefficient is a power of two + if (!p1.is_val()) + return false; + if (!p2.is_val()) + return false; + rational a1 = p1.val(); + rational a2 = p2.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; + if (!a2.is_zero() && !a2.is_one()) + return false; + /* + unsigned j1 = 0; + unsigned j2 = 0; + if (!a1.is_zero() && !a1.is_power_of_two(j1)) + return false; + if (!a2.is_zero() && !a2.is_power_of_two(j2)) + return false; + */ + + // Concrete values of evaluable terms + auto e1s = e1.subst_val(s.m_search); + auto e2s = e2.subst_val(s.m_search); + SASSERT(e1s.is_val()); + SASSERT(e2s.is_val()); + + bool is_trivial; + pdd condition_body = m.zero(); + pdd lo = m.zero(); + rational lo_val = rational::zero(); + pdd hi = m.zero(); + rational hi_val = rational::zero(); + + if (a2.is_zero()) { + SASSERT(!a1.is_zero()); + // e1 + t <= e2, with t = 2^j1*y + // condition for empty/full: e2 == -1 + is_trivial = (e2s + 1).is_zero(); + condition_body = e2 + 1; + if (!is_trivial) { + lo = e2 - e1 + 1; + lo_val = (e2s - e1s + 1).val(); + hi = -e1; + hi_val = (-e1s).val(); + } + } + else if (a1.is_zero()) { + SASSERT(!a2.is_zero()); + // e1 <= e2 + t, with t = 2^j2*y + // condition for empty/full: e1 == 0 + is_trivial = e1s.is_zero(); + condition_body = e1; + if (!is_trivial) { + lo = -e2; + lo_val = (-e2s).val(); + hi = e1 - e2; + hi_val = (e1s - e2s).val(); + } + } + else { + SASSERT(!a1.is_zero()); + SASSERT(!a2.is_zero()); + // e1 + t <= e2 + t, with t = 2^j1*y = 2^j2*y + // condition for empty/full: e1 == e2 + is_trivial = e1s.val() == e2s.val(); + condition_body = e1 - e2; + if (!is_trivial) { + lo = -e2; + lo_val = (-e2s).val(); + hi = -e1; + hi_val = (-e1s).val(); + } + } + + if (condition_body.is_val()) { + // Condition is trivial; no need to create a constraint for that. + SASSERT(is_trivial == condition_body.is_zero()); + neg_condition = nullptr; + } + else + neg_condition = constraint::eq(level(), s.m_next_bvar++, is_trivial ? neg_t : pos_t, condition_body, m_dep); + + if (is_trivial) { + if (is_positive()) + i = eval_interval::empty(m); + else + i = eval_interval::full(); + } else { + if (is_negative()) { + swap(lo, hi); + lo_val.swap(hi_val); + } + i = eval_interval::proper(lo, lo_val, hi, hi_val); + } + + return true; + } + } diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h index cc7cdd45c..9bf51b1cc 100644 --- a/src/math/polysat/ule_constraint.h +++ b/src/math/polysat/ule_constraint.h @@ -21,7 +21,7 @@ namespace polysat { pdd m_lhs; pdd m_rhs; public: - ule_constraint(unsigned lvl, bool_var bvar, csign_t sign, pdd const& l, pdd const& r, p_dependency_ref& dep): + ule_constraint(unsigned lvl, bool_var bvar, csign_t sign, pdd const& l, pdd const& r, p_dependency_ref const& dep): constraint(lvl, bvar, sign, dep, ckind_t::ule_t), m_lhs(l), m_rhs(r) { m_vars.append(l.free_vars()); for (auto v : r.free_vars()) @@ -39,6 +39,8 @@ namespace polysat { 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; }; } diff --git a/src/math/polysat/var_constraint.h b/src/math/polysat/var_constraint.h index 9490fdd1f..700bc209a 100644 --- a/src/math/polysat/var_constraint.h +++ b/src/math/polysat/var_constraint.h @@ -29,7 +29,7 @@ namespace polysat { pvar m_var; bdd m_viable; public: - var_constraint(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const & b, p_dependency_ref& dep): + var_constraint(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const & b, p_dependency_ref const& dep): 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;