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

@@ -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 {

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

src/math/polysat/constraint.cpp

@@ -29,16 +29,21 @@ namespace polysat {
         return *dynamic_cast<eq_constraint const*>(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<csign_t>(!sign), b, a, d);
+    }
+
 }

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); }

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());
         }

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]);

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<constraint> 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<fi_record> 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<constraint> const& conflict, pvar v, scoped_ptr_vector<constraint>& out_lemma) {
+
+        // Extract forbidden intervals from conflicting constraints
+        vector<fi_record> 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: <null>");
+                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<constraint>& cond = records[i].cond;
+            if (cond)
+                out_lemma.push_back(cond.detach());
+        }
+
+        return true;
+    }
+
+}

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<constraint> const& conflict, pvar v, scoped_ptr_vector<constraint>& out_lemma);
+
+    };
+}

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<bounds> 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() << "[";
+    }
+
+
+}

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<constraint> 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<constraint> 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;

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<constraint> 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.
          */

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;
+    }
+
 }

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;
     };
 
 }

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;