v2 of polysat

src/sat/sat_solver.cpp

@@ -2429,9 +2429,8 @@ namespace sat {
         m_conflicts_since_restart++;
         m_conflicts_since_gc++;
         m_stats.m_conflict++;
-        if (m_step_size > m_config.m_step_size_min) {
-            m_step_size -= m_config.m_step_size_dec;
-        }
+        if (m_step_size > m_config.m_step_size_min)
+            m_step_size -= m_config.m_step_size_dec;        
 
         bool unique_max;
         m_conflict_lvl = get_max_lvl(m_not_l, m_conflict, unique_max);        

src/sat/smt/CMakeLists.txt

@@ -33,6 +33,12 @@ z3_add_component(sat_smt
     pb_internalize.cpp
     pb_pb.cpp
     pb_solver.cpp
+    polysat_assignment.cpp
+    polysat_constraints.cpp
+    polysat_core.cpp
+    polysat_internalize.cpp
+    polysat_model.cpp
+    polysat_solver.cpp
     q_clause.cpp
     q_ematch.cpp
     q_eval.cpp

src/sat/smt/euf_solver.cpp

@@ -209,6 +209,15 @@ namespace euf {
         s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx));
     }
 
+    lbool solver::resolve_conflict() {
+        for (auto* s : m_solvers) {
+            lbool r = s->resolve_conflict();
+            if (r != l_undef)
+                return r;
+        }
+        return l_undef;
+    }
+
     /**
     Retrieve set of literals r that imply r.
     Since the set of literals are retrieved modulo multiple theories in a single implication

src/sat/smt/euf_solver.h

@@ -363,6 +363,7 @@ namespace euf {
         bool propagate(enode* a, enode* b, th_explain* p) { return propagate(a, b, p->to_index()); }
         size_t* to_justification(sat::literal l) { return to_ptr(l); }
         void set_conflict(th_explain* p) { set_conflict(p->to_index()); }
+        bool inconsistent() const { return s().inconsistent() || m_egraph.inconsistent(); }
 
         bool set_root(literal l, literal r) override;
         void flush_roots() override;
@@ -378,6 +379,7 @@ namespace euf {
         bool get_case_split(bool_var& var, lbool& phase) override;
         void asserted(literal l) override;
         sat::check_result check() override;
+        lbool resolve_conflict() override;
         void push() override;
         void pop(unsigned n) override;
         void user_push() override;

src/sat/smt/polysat_assignment.cpp

@@ -0,0 +1,119 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat substitution and assignment
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-06
+
+--*/
+
+#include "sat/smt/polysat_assignment.h"
+#include "sat/smt/polysat_core.h"
+
+namespace polysat {
+
+    substitution::substitution(pdd p)
+        : m_subst(std::move(p)) { }
+
+    substitution::substitution(dd::pdd_manager& m)
+        : m_subst(m.one()) { }
+
+    substitution substitution::add(pvar var, rational const& value) const {
+        return {m_subst.subst_add(var, value)};
+    }
+
+    pdd substitution::apply_to(pdd const& p) const {
+        return p.subst_val(m_subst);
+    }
+
+    bool substitution::contains(pvar var) const {
+        rational out_value;
+        return value(var, out_value);
+    }
+
+    bool substitution::value(pvar var, rational& out_value) const {
+        return m_subst.subst_get(var, out_value);
+    }
+
+    assignment::assignment(core& s)
+        : m_core(s) { }
+
+
+    assignment assignment::clone() const {
+        assignment a(s());
+        a.m_pairs = m_pairs;
+        a.m_subst.reserve(m_subst.size());
+        for (unsigned i = m_subst.size(); i-- > 0; )
+            if (m_subst[i])
+                a.m_subst.set(i, alloc(substitution, *m_subst[i]));
+        a.m_subst_trail = m_subst_trail;
+        return a;
+    }
+
+    bool assignment::contains(pvar var) const {
+        return subst(s().size(var)).contains(var);
+    }
+
+    bool assignment::value(pvar var, rational& out_value) const {
+        return subst(s().size(var)).value(var, out_value);
+    }
+
+    substitution& assignment::subst(unsigned sz) {
+        return const_cast<substitution&>(std::as_const(*this).subst(sz));
+    }
+
+    substitution const& assignment::subst(unsigned sz) const {
+        m_subst.reserve(sz + 1);
+        if (!m_subst[sz])
+            m_subst.set(sz, alloc(substitution, s().sz2pdd(sz)));
+        return *m_subst[sz];
+    }
+
+    void assignment::push(pvar var, rational const& value) {
+        SASSERT(all_of(m_pairs, [var](assignment_item_t const& item) { return item.first != var; }));
+        m_pairs.push_back({var, value});
+        unsigned const sz = s().size(var);
+        substitution& sub = subst(sz);
+        m_subst_trail.push_back(sub);
+        sub = sub.add(var, value);
+        SASSERT_EQ(sub, *m_subst[sz]);
+    }
+
+    void assignment::pop() {
+        substitution& sub = m_subst_trail.back();
+        unsigned sz = sub.bit_width();
+        SASSERT_EQ(sz, s().size(m_pairs.back().first));
+        *m_subst[sz] = sub;
+        m_subst_trail.pop_back();
+        m_pairs.pop_back();
+    }
+
+    pdd assignment::apply_to(pdd const& p) const {
+        unsigned const sz = p.power_of_2();
+        return subst(sz).apply_to(p);
+    }
+
+    std::ostream& substitution::display(std::ostream& out) const {
+        char const* delim = "";
+        pdd p = m_subst;
+        while (!p.is_val()) {
+            SASSERT(p.lo().is_val());
+            out << delim << "v" << p.var() << " := " << p.lo();
+            delim = " ";
+            p = p.hi();
+        }
+        return out;
+    }
+
+    std::ostream& assignment::display(std::ostream& out) const {
+        char const* delim = "";
+        for (auto const& [var, value] : m_pairs) 
+            out << delim << var << " == " << value, delim = " ";	  
+        return out;
+    }
+}

src/sat/smt/polysat_assignment.h

@@ -0,0 +1,120 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat substitution and assignment
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-06
+
+--*/
+#pragma once
+#include "util/scoped_ptr_vector.h"
+#include "sat/smt/polysat_types.h"
+
+namespace polysat {
+
+    class core;
+
+    using assignment_item_t = std::pair<pvar, rational>;
+
+    class substitution_iterator {
+        pdd m_current;
+        substitution_iterator(pdd current) : m_current(std::move(current)) {}
+        friend class substitution;
+
+    public:
+        using value_type = assignment_item_t;
+        using difference_type = std::ptrdiff_t;
+        using pointer = value_type const*;
+        using reference = value_type const&;
+        using iterator_category = std::input_iterator_tag;
+
+        substitution_iterator& operator++() {
+            SASSERT(!m_current.is_val());
+            m_current = m_current.hi();
+            return *this;
+        }
+
+        value_type operator*() const {
+            SASSERT(!m_current.is_val());
+            return { m_current.var(), m_current.lo().val() };
+        }
+
+        bool operator==(substitution_iterator const& other) const { return m_current == other.m_current; }
+        bool operator!=(substitution_iterator const& other) const { return !operator==(other); }
+    };
+
+    /** Substitution for a single bit width. */
+    class substitution {
+        pdd m_subst;
+
+        substitution(pdd p);
+
+    public:
+        substitution(dd::pdd_manager& m);
+        [[nodiscard]] substitution add(pvar var, rational const& value) const;
+        [[nodiscard]] pdd apply_to(pdd const& p) const;
+
+        [[nodiscard]] bool contains(pvar var) const;
+        [[nodiscard]] bool value(pvar var, rational& out_value) const;
+
+        [[nodiscard]] bool empty() const { return m_subst.is_one(); }
+
+        pdd const& to_pdd() const { return m_subst; }
+        unsigned bit_width() const { return to_pdd().power_of_2(); }
+
+        bool operator==(substitution const& other) const { return &m_subst.manager() == &other.m_subst.manager() && m_subst == other.m_subst; }
+        bool operator!=(substitution const& other) const { return !operator==(other); }
+
+        std::ostream& display(std::ostream& out) const;
+
+        using const_iterator = substitution_iterator;
+        const_iterator begin() const { return {m_subst}; }
+        const_iterator end() const { return {m_subst.manager().one()}; }
+    };
+
+    /** Full variable assignment, may include variables of varying bit widths. */
+    class assignment {
+        core& m_core;
+        vector<assignment_item_t>               m_pairs;
+        mutable scoped_ptr_vector<substitution> m_subst;
+        vector<substitution>                    m_subst_trail;
+
+        substitution& subst(unsigned sz);
+        core& s() const { return m_core; }
+    public:
+        assignment(core& s);
+        // prevent implicit copy, use clone() if you do need a copy
+        assignment(assignment const&) = delete;
+        assignment& operator=(assignment const&) = delete;
+        assignment(assignment&&) = default;
+        assignment& operator=(assignment&&) = default;
+        assignment clone() const;
+
+        void push(pvar var, rational const& value);
+        void pop();
+
+        pdd apply_to(pdd const& p) const;
+
+        bool contains(pvar var) const;
+        bool value(pvar var, rational& out_value) const;
+        rational value(pvar var) const { rational val; VERIFY(value(var, val)); return val; }
+        bool empty() const { return pairs().empty(); }
+        substitution const& subst(unsigned sz) const;
+        vector<assignment_item_t> const& pairs() const { return m_pairs; }
+        using const_iterator = decltype(m_pairs)::const_iterator;
+        const_iterator begin() const { return pairs().begin(); }
+        const_iterator end() const { return pairs().end(); }
+
+        std::ostream& display(std::ostream& out) const;
+    };
+
+    inline std::ostream& operator<<(std::ostream& out, substitution const& sub) { return sub.display(out); }
+
+    inline std::ostream& operator<<(std::ostream& out, assignment const& a) { return a.display(out); }
+}
+

src/sat/smt/polysat_constraints.cpp

@@ -0,0 +1,25 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat constraints
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-06
+
+--*/
+#include "sat/smt/polysat_core.h"
+#include "sat/smt/polysat_solver.h"
+#include "sat/smt/polysat_constraints.h"
+
+namespace polysat {
+
+    signed_constraint constraints::ule(pdd const& p, pdd const& q) {
+        auto* c = alloc(ule_constraint, p, q);
+        m_trail.push(new_obj_trail(c));
+        return signed_constraint(ckind_t::ule_t, c);
+    }
+}

src/sat/smt/polysat_constraints.h

@@ -0,0 +1,128 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat constraints
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-06
+
+--*/
+
+
+#pragma once 
+#include "sat/smt/polysat_types.h"
+
+namespace polysat {
+
+    class core;
+
+    using pdd = dd::pdd;
+    using pvar = unsigned;
+
+    enum ckind_t { ule_t, umul_ovfl_t, smul_fl_t, op_t };
+
+    class constraint {
+        unsigned_vector     m_vars;
+    public:
+        virtual ~constraint() {}
+        unsigned_vector& vars() { return m_vars; }
+        unsigned_vector const& vars() const { return m_vars; }
+        unsigned var(unsigned idx) const { return m_vars[idx]; }
+        bool contains_var(pvar v) const { return m_vars.contains(v); }
+    };
+
+    class ule_constraint : public constraint {
+        pdd m_lhs, m_rhs;
+    public:
+        ule_constraint(pdd const& lhs, pdd const& rhs) : m_lhs(lhs), m_rhs(rhs) {}
+    };
+
+    class signed_constraint {
+        bool m_sign = false;
+        ckind_t m_op = ule_t;
+        constraint* m_constraint = nullptr;
+    public:
+        signed_constraint() {}
+        signed_constraint(ckind_t c, constraint* p) : m_op(c), m_constraint(p) {}
+        signed_constraint operator~() const { signed_constraint r(*this); r.m_sign = !r.m_sign; return r; }
+        bool sign() const { return m_sign; }
+        unsigned_vector& vars() { return m_constraint->vars(); }
+        unsigned_vector const& vars() const { return m_constraint->vars(); }
+        unsigned var(unsigned idx) const { return m_constraint->var(idx); }
+        bool contains_var(pvar v) const { return m_constraint->contains_var(v); }
+        bool is_ule() const { return m_op == ule_t; }
+        ule_constraint& to_ule() { return *reinterpret_cast<ule_constraint*>(m_constraint); }
+        bool is_eq(pvar& v, rational& val) { throw default_exception("nyi"); }
+    };
+
+    using dependent_constraint = std::pair<signed_constraint, stacked_dependency*>;
+
+    class constraints {
+        trail_stack& m_trail;
+    public:
+        constraints(trail_stack& c) : m_trail(c) {}
+
+        signed_constraint eq(pdd const& p) { return ule(p, p.manager().mk_val(0)); }
+        signed_constraint eq(pdd const& p, rational const& v) { return eq(p - p.manager().mk_val(v)); }
+        signed_constraint ule(pdd const& p, pdd const& q);
+        signed_constraint sle(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
+        signed_constraint ult(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
+        signed_constraint slt(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
+        signed_constraint umul_ovfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
+        signed_constraint smul_ovfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
+        signed_constraint smul_udfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
+        signed_constraint bit(pdd const& p, unsigned i) { throw default_exception("nyi"); }
+
+        signed_constraint diseq(pdd const& p) { return ~eq(p); }
+        signed_constraint diseq(pdd const& p, pdd const& q) { return diseq(p - q); }
+        signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); }
+        signed_constraint diseq(pdd const& p, int             q) { return diseq(p, rational(q)); }
+        signed_constraint diseq(pdd const& p, unsigned        q) { return diseq(p, rational(q)); }
+
+        signed_constraint ule(pdd const& p, rational const& q) { return ule(p, p.manager().mk_val(q)); }
+        signed_constraint ule(rational const& p, pdd const& q) { return ule(q.manager().mk_val(p), q); }
+        signed_constraint ule(pdd const& p, int             q) { return ule(p, rational(q)); }
+        signed_constraint ule(pdd const& p, unsigned        q) { return ule(p, rational(q)); }
+        signed_constraint ule(int             p, pdd const& q) { return ule(rational(p), q); }
+        signed_constraint ule(unsigned        p, pdd const& q) { return ule(rational(p), q); }
+
+        signed_constraint uge(pdd const& p, pdd const& q) { return ule(q, p); }
+        signed_constraint uge(pdd const& p, rational const& q) { return ule(q, p); }
+
+        signed_constraint ult(pdd const& p, rational const& q) { return ult(p, p.manager().mk_val(q)); }
+        signed_constraint ult(rational const& p, pdd const& q) { return ult(q.manager().mk_val(p), q); }
+        signed_constraint ult(int             p, pdd const& q) { return ult(rational(p), q); }
+        signed_constraint ult(unsigned        p, pdd const& q) { return ult(rational(p), q); }
+        signed_constraint ult(pdd const& p, int q) { return ult(p, rational(q)); }
+        signed_constraint ult(pdd const& p, unsigned q) { return ult(p, rational(q)); }
+
+        signed_constraint slt(pdd const& p, rational const& q) { return slt(p, p.manager().mk_val(q)); }
+        signed_constraint slt(rational const& p, pdd const& q) { return slt(q.manager().mk_val(p), q); }
+        signed_constraint slt(pdd const& p, int             q) { return slt(p, rational(q)); }
+        signed_constraint slt(pdd const& p, unsigned        q) { return slt(p, rational(q)); }
+        signed_constraint slt(int             p, pdd const& q) { return slt(rational(p), q); }
+        signed_constraint slt(unsigned        p, pdd const& q) { return slt(rational(p), q); }
+
+
+        signed_constraint sgt(pdd const& p, pdd const& q) { return slt(q, p); }
+        signed_constraint sgt(pdd const& p, int        q) { return slt(q, p); }
+        signed_constraint sgt(pdd const& p, unsigned   q) { return slt(q, p); }
+        signed_constraint sgt(int        p, pdd const& q) { return slt(q, p); }
+        signed_constraint sgt(unsigned   p, pdd const& q) { return slt(q, p); }
+
+        signed_constraint umul_ovfl(pdd const& p, rational const& q) { return umul_ovfl(p, p.manager().mk_val(q)); }
+        signed_constraint umul_ovfl(rational const& p, pdd const& q) { return umul_ovfl(q.manager().mk_val(p), q); }
+        signed_constraint umul_ovfl(pdd const& p, int             q) { return umul_ovfl(p, rational(q)); }
+        signed_constraint umul_ovfl(pdd const& p, unsigned        q) { return umul_ovfl(p, rational(q)); }
+        signed_constraint umul_ovfl(int             p, pdd const& q) { return umul_ovfl(rational(p), q); }
+        signed_constraint umul_ovfl(unsigned        p, pdd const& q) { return umul_ovfl(rational(p), q); }
+
+
+        //signed_constraint even(pdd const& p) { return parity_at_least(p, 1); }
+        //signed_constraint odd(pdd const& p) { return ~even(p); }
+    };
+}

src/sat/smt/polysat_core.cpp

@@ -0,0 +1,276 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    polysat_core.cpp
+
+Abstract:
+
+    PolySAT core functionality
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-01-26
+    Jakob Rath 2021-04-06
+
+Notes:
+
+polysat::solver
+- adds assignments
+- calls propagation and check
+
+polysat::core
+- propagates literals 
+- crates case splits by value assignment (equalities)
+- detects conflicts based on Literal assignmets
+- adds lemmas based on projections
+
+--*/
+
+#include "params/bv_rewriter_params.hpp"
+#include "sat/smt/polysat_solver.h"
+#include "sat/smt/euf_solver.h"
+
+namespace polysat {
+
+    class core::mk_assign_var : public trail {
+        pvar m_var;
+        core& c;
+    public:
+        mk_assign_var(pvar v, core& c) : m_var(v), c(c) {}
+        void undo() {
+            c.m_justification[m_var] = nullptr;
+            c.m_assignment.pop();
+        }
+    };
+
+    class core::mk_dqueue_var : public trail {
+        pvar m_var;
+        core& c;
+    public:
+        mk_dqueue_var(pvar v, core& c) : m_var(v), c(c) {}
+        void undo() {
+            c.m_var_queue.unassign_var_eh(m_var);
+        }
+    };
+
+    class core::mk_add_var : public trail {
+        core& c;
+    public:
+        mk_add_var(core& c) : c(c) {}
+        void undo() override {
+            c.del_var();
+        }
+    };
+
+    class core::mk_add_watch : public trail {
+        core& c;
+        unsigned m_idx;
+    public:
+        mk_add_watch(core& c, unsigned idx) : c(c), m_idx(idx) {}
+        void undo() override {
+            auto& sc = c.m_prop_queue[m_idx].first;
+            auto& vars = sc.vars();
+            if (vars.size() > 0)
+                c.m_watch[vars[0]].pop_back();
+            if (vars.size() > 1)
+                c.m_watch[vars[1]].pop_back();
+        }
+    };
+
+    core::core(solver& s) :
+        s(s),         
+        m_viable(*this),
+        m_constraints(s.get_trail_stack()),
+        m_assignment(*this),
+        m_dep(s.get_region()),
+        m_var_queue(m_activity)
+    {}
+
+    pdd core::value(rational const& v, unsigned sz) {
+        return sz2pdd(sz).mk_val(v);
+    }
+
+    dd::pdd_manager& core::sz2pdd(unsigned sz) const {
+        m_pdd.reserve(sz + 1);
+        if (!m_pdd[sz])
+            m_pdd.set(sz, alloc(dd::pdd_manager, 1000, dd::pdd_manager::semantics::mod2N_e, sz));
+        return *m_pdd[sz];
+    }
+
+    dd::pdd_manager& core::var2pdd(pvar v) const {
+        return sz2pdd(size(v));
+    }
+
+    pvar core::add_var(unsigned sz) { 
+        unsigned v = m_vars.size();
+        m_vars.push_back(sz2pdd(sz).mk_var(v));
+        m_activity.push_back({ sz, 0 });
+        m_justification.push_back(nullptr);
+        m_watch.push_back({});
+        m_var_queue.mk_var_eh(v);
+        s.ctx.push(mk_add_var(*this));
+        return v;
+    }
+
+    void core::del_var() {
+        unsigned v = m_vars.size() - 1;
+        m_vars.pop_back();
+        m_activity.pop_back();
+        m_justification.pop_back();
+        m_watch.pop_back();
+        m_var_queue.del_var_eh(v);
+    }
+
+    // case split on unassigned variables until all are assigned values.
+    // create equality literal for unassigned variable.
+    // return new_eq if there is a new literal.
+    
+    sat::check_result core::check() { 
+        if (m_var_queue.empty())
+            return sat::check_result::CR_DONE;
+        m_var = m_var_queue.next_var();       
+        s.ctx.push(mk_dqueue_var(m_var, *this));
+        switch (m_viable.find_viable(m_var, m_value)) {
+        case find_t::empty:
+            m_unsat_core = m_viable.explain();
+            propagate_unsat_core();
+            return sat::check_result::CR_CONTINUE;
+        case find_t::singleton:
+            s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain());
+            return sat::check_result::CR_CONTINUE;
+        case find_t::multiple:  
+            return sat::check_result::CR_CONTINUE;
+        case find_t::resource_out:
+            return sat::check_result::CR_GIVEUP;
+        }
+        UNREACHABLE();
+        return sat::check_result::CR_GIVEUP;
+    }
+
+    // First propagate Boolean assignment, then propagate value assignment
+    bool core::propagate() { 
+        if (m_qhead == m_prop_queue.size() && m_vqhead == m_prop_queue.size())
+            return false;
+        s.ctx.push(value_trail(m_qhead));
+        for (; m_qhead < m_prop_queue.size() && !s.ctx.inconsistent(); ++m_qhead)
+            propagate_constraint(m_qhead, m_prop_queue[m_qhead]);        
+        s.ctx.push(value_trail(m_vqhead));
+        for (; m_vqhead < m_prop_queue.size() && !s.ctx.inconsistent(); ++m_vqhead) 
+            propagate_value(m_vqhead, m_prop_queue[m_vqhead]);        
+        return true;
+    }
+
+    void core::propagate_constraint(unsigned idx, dependent_constraint& dc) { 
+        auto [sc, dep] = dc;
+        if (sc.is_eq(m_var, m_value)) {
+            propagate_assignment(m_var, m_value, dep);
+            return;
+        }
+        add_watch(idx, sc);
+    }
+
+    void core::add_watch(unsigned idx, signed_constraint& sc) {        
+        auto& vars = sc.vars();
+        unsigned i = 0, j = 0, sz = vars.size();
+        for (; i < sz && j < 2; ++i)
+            if (!is_assigned(vars[i]))
+                std::swap(vars[i], vars[j++]);
+        if (vars.size() > 0)
+            add_watch(idx, vars[0]);
+        if (vars.size() > 1)
+            add_watch(idx, vars[1]);
+        s.ctx.push(mk_add_watch(*this, idx));
+    }
+
+    void core::add_watch(unsigned idx, unsigned var) {
+        m_watch[var].push_back(idx);
+    }
+
+    void core::propagate_assignment(pvar v, rational const& value, stacked_dependency* dep) {
+        if (is_assigned(v))
+            return;
+        if (m_var_queue.contains(v)) {
+            m_var_queue.del_var_eh(v);
+            s.ctx.push(mk_dqueue_var(v, *this));
+        }
+        m_values[v] = value;
+        m_justification[v] = dep;   
+        m_assignment.push(v , value);
+        s.ctx.push(mk_assign_var(v, *this));
+
+        // update the watch lists for pvars
+        // remove constraints from m_watch[v] that have more than 2 free variables.
+        // for entries where there is only one free variable left add to viable set 
+        unsigned j = 0;
+        for (auto idx : m_watch[v]) {
+            auto [sc, dep] = m_prop_queue[idx];
+            auto& vars = sc.vars();
+            if (vars[0] != v)
+                std::swap(vars[0], vars[1]);
+            SASSERT(vars[0] == v);
+            bool swapped = false;
+            for (unsigned i = vars.size(); i-- > 2; ) {
+                if (!is_assigned(vars[i])) {
+                    add_watch(idx, vars[i]);
+                    std::swap(vars[i], vars[0]);
+                    swapped = true;
+                    break;
+                }
+            }
+            if (!swapped) {
+                m_watch[v][j++] = idx;
+            }
+
+            // constraint is unitary, add to viable set 
+            if (vars.size() >= 2 && is_assigned(vars[0]) && !is_assigned(vars[1])) {
+                // m_viable.add_unitary(vars[1], idx);
+            }
+        }
+        m_watch[v].shrink(j);
+    }
+
+    void core::propagate_value(unsigned idx, dependent_constraint const& dc) {
+        auto [sc, dep] = dc;
+        // check if sc evaluates to false
+        switch (eval(sc)) {
+        case l_true:
+            return;
+        case l_false:
+            m_unsat_core = explain_eval(dc);
+            propagate_unsat_core();
+            return;
+        default:
+            break;
+        }
+        // if sc is v == value, then check the watch list for v if they evaluate to false.
+        if (sc.is_eq(m_var, m_value)) {
+            for (auto idx : m_watch[m_var]) {
+                auto [sc, dep] = m_prop_queue[idx];
+                if (eval(sc) == l_false) {
+                    m_unsat_core = explain_eval({ sc, dep });
+                    propagate_unsat_core();
+                    return;
+                }
+            }
+        }
+
+        throw default_exception("nyi"); 
+    }
+
+    bool core::propagate_unsat_core() { 
+        // default is to use unsat core:
+        s.set_conflict(m_unsat_core);
+        // if core is based on viable, use s.set_lemma();
+        throw default_exception("nyi"); 
+    }
+
+    void core::assign_eh(signed_constraint const& sc, dependency const& dep) { 
+        m_prop_queue.push_back({ sc, m_dep.mk_leaf(dep) });
+        s.ctx.push(push_back_vector(m_prop_queue));
+    }
+
+
+
+}

src/sat/smt/polysat_core.h

@@ -0,0 +1,128 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    polysat_core.h
+
+Abstract:
+
+    Core solver for polysat
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-30
+    Jakob Rath 2021-04-06
+
+--*/
+#pragma once
+
+#include "util/dependency.h"
+#include "math/dd/dd_pdd.h"
+#include "sat/smt/sat_th.h"
+#include "sat/smt/polysat_types.h"
+#include "sat/smt/polysat_constraints.h"
+#include "sat/smt/polysat_viable.h"
+#include "sat/smt/polysat_assignment.h"
+
+namespace polysat {
+
+    class core;
+    class solver;
+
+    class core {
+        class mk_add_var;
+        class mk_dqueue_var;
+        class mk_assign_var;
+        class mk_add_watch;
+        typedef svector<std::pair<unsigned, unsigned>> activity;
+        friend class viable;
+        friend class constraints;
+        friend class assignment;
+
+        solver& s;
+        viable m_viable;
+        constraints m_constraints;
+        assignment m_assignment;
+        unsigned m_qhead = 0, m_vqhead = 0;
+        svector<dependent_constraint> m_prop_queue;
+        stacked_dependency_manager<dependency>     m_dep;
+        mutable scoped_ptr_vector<dd::pdd_manager> m_pdd;
+        dependency_vector m_unsat_core;
+
+
+        // attributes associated with variables
+        vector<pdd>            m_vars;                       // for each variable a pdd
+        vector<rational>       m_values;                     // current value of assigned variable
+        ptr_vector<stacked_dependency>     m_justification;  // justification for assignment
+        activity                m_activity;                  // activity of variables
+        var_queue<activity>     m_var_queue;                 // priority queue of variables to assign
+        vector<unsigned_vector> m_watch;                     // watch lists for variables for constraints on m_prop_queue where they occur
+
+        vector<pdd>             m_subst;            // substitution, one for each size.
+
+        // values to split on
+        rational    m_value;
+        pvar        m_var = 0;
+
+        dd::pdd_manager& sz2pdd(unsigned sz) const;
+        dd::pdd_manager& var2pdd(pvar v) const;
+        unsigned size(pvar v) const { return var2pdd(v).power_of_2(); }
+        void del_var();
+
+        bool is_assigned(pvar v) { return nullptr != m_justification[v]; }
+        void propagate_constraint(unsigned idx, dependent_constraint& dc);
+        void propagate_value(unsigned idx, dependent_constraint const& dc);
+        void propagate_assignment(pvar v, rational const& value, stacked_dependency* dep);
+        bool propagate_unsat_core();
+
+        void add_watch(unsigned idx, signed_constraint& sc);
+        void add_watch(unsigned idx, unsigned var);
+
+        lbool eval(signed_constraint sc) { throw default_exception("nyi"); }
+        dependency_vector explain_eval(dependent_constraint const& dc) { throw default_exception("nyi"); }
+
+    public:
+        core(solver& s);
+
+        sat::check_result check();
+
+        bool propagate();
+        void assign_eh(signed_constraint const& sc, dependency const& dep);
+
+        expr_ref constraint2expr(signed_constraint const& sc) const { throw default_exception("nyi"); }
+
+        pdd value(rational const& v, unsigned sz);
+
+        signed_constraint eq(pdd const& p) { return m_constraints.eq(p); }
+        signed_constraint eq(pdd const& p, pdd const& q) { return m_constraints.eq(p - q); }
+        signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); }
+        signed_constraint sle(pdd const& p, pdd const& q) { return m_constraints.sle(p, q); }
+        signed_constraint umul_ovfl(pdd const& p, pdd const& q) { return m_constraints.umul_ovfl(p, q); }
+        signed_constraint smul_ovfl(pdd const& p, pdd const& q) { return m_constraints.smul_ovfl(p, q); }
+        signed_constraint smul_udfl(pdd const& p, pdd const& q) { return m_constraints.smul_udfl(p, q); }
+        signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
+
+
+        pdd lshr(pdd a, pdd b) { throw default_exception("nyi"); }
+        pdd ashr(pdd a, pdd b) { throw default_exception("nyi"); }
+        pdd shl(pdd a, pdd b) { throw default_exception("nyi"); }
+        pdd band(pdd a, pdd b) { throw default_exception("nyi"); }
+        pdd bxor(pdd a, pdd b) { throw default_exception("nyi"); }
+        pdd bor(pdd a, pdd b) { throw default_exception("nyi"); }
+        pdd bnand(pdd a, pdd b) { throw default_exception("nyi"); }
+        pdd bxnor(pdd a, pdd b) { throw default_exception("nyi"); }
+        pdd bnor(pdd a, pdd b) { throw default_exception("nyi"); }
+        pdd bnot(pdd a) { throw default_exception("nyi"); }
+        std::pair<pdd, pdd> quot_rem(pdd const& n, pdd const& d) { throw default_exception("nyi"); }
+        pdd zero_ext(pdd a, unsigned sz) { throw default_exception("nyi"); }
+        pdd sign_ext(pdd a, unsigned sz) { throw default_exception("nyi"); }
+        pdd extract(pdd src, unsigned hi, unsigned lo) { throw default_exception("nyi"); }
+        pdd concat(unsigned n, pdd const* args) { throw default_exception("nyi"); }
+        pvar add_var(unsigned sz);
+        pdd var(pvar p) { return m_vars[p]; }
+
+        std::ostream& display(std::ostream& out) const { throw default_exception("nyi"); }
+    };
+
+}

src/sat/smt/polysat_internalize.cpp

@@ -0,0 +1,343 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    polysat_model.cpp
+
+Abstract:
+
+    PolySAT model generation
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-01-26
+
+--*/
+
+#include "params/bv_rewriter_params.hpp"
+#include "sat/smt/polysat_solver.h"
+#include "sat/smt/euf_solver.h"
+
+namespace polysat {
+
+    euf::theory_var solver::mk_var(euf::enode* n) {
+        return euf::th_euf_solver::mk_var(n);
+    }
+
+    sat::literal solver::internalize(expr* e, bool sign, bool root) {
+        force_push();
+        SASSERT(m.is_bool(e));
+        if (!visit_rec(m, e, sign, root))
+            return sat::null_literal;
+        sat::literal lit = expr2literal(e);
+        if (sign)
+            lit.neg();
+        return lit;
+    }
+
+    void solver::internalize(expr* e) {
+        force_push();
+        visit_rec(m, e, false, false);
+    }
+
+    bool solver::visit(expr* e) {      
+        force_push();
+        if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
+            ctx.internalize(e);
+            return true;
+        }
+        m_stack.push_back(sat::eframe(e));
+        return false;
+    }
+
+    bool solver::visited(expr* e) {
+        euf::enode* n = expr2enode(e);
+        return n && n->is_attached_to(get_id());        
+    }
+
+    bool solver::post_visit(expr* e, bool sign, bool root) {
+        euf::enode* n = expr2enode(e);
+        app* a = to_app(e);
+
+        if (visited(e))
+            return true;
+
+        SASSERT(!n || !n->is_attached_to(get_id()));
+        if (!n)
+            n = mk_enode(e, false);
+
+        SASSERT(!n->is_attached_to(get_id()));
+        mk_var(n);
+        SASSERT(n->is_attached_to(get_id()));
+        internalize_polysat(a);
+        return true;
+    }
+  
+    void solver::internalize_polysat(app* a) {
+
+#define if_unary(F) if (a->get_num_args() == 1) { internalize_unary(a, [&](pdd const& p) { return F(p); }); break; }
+
+        switch (a->get_decl_kind()) {
+        case OP_BMUL:             internalize_binary(a, [&](pdd const& p, pdd const& q) { return p * q; }); break;
+        case OP_BADD:             internalize_binary(a, [&](pdd const& p, pdd const& q) { return p + q; }); break;
+        case OP_BSUB:             internalize_binary(a, [&](pdd const& p, pdd const& q) { return p - q; }); break;
+        case OP_BLSHR:            internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.lshr(p, q); }); break;
+        case OP_BSHL:             internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.shl(p, q); }); break;
+        case OP_BAND:             internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.band(p, q); }); break;
+        case OP_BOR:              internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bor(p, q); }); break;
+        case OP_BXOR:             internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bxor(p, q); }); break;
+        case OP_BNAND:            if_unary(m_core.bnot); internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bnand(p, q); }); break;
+        case OP_BNOR:             if_unary(m_core.bnot); internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bnor(p, q); }); break;
+        case OP_BXNOR:            if_unary(m_core.bnot); internalize_binary(a, [&](pdd const& p, pdd const& q) { return m_core.bxnor(p, q); }); break;
+        case OP_BNOT:             internalize_unary(a, [&](pdd const& p) { return m_core.bnot(p); }); break;
+        case OP_BNEG:             internalize_unary(a, [&](pdd const& p) { return -p; }); break;
+        case OP_MKBV:             internalize_mkbv(a); break;
+        case OP_BV_NUM:           internalize_num(a); break;
+        case OP_ULEQ:             internalize_le<false, false, false>(a); break;
+        case OP_SLEQ:             internalize_le<true,  false, false>(a); break;
+        case OP_UGEQ:             internalize_le<false, true,  false>(a); break;
+        case OP_SGEQ:             internalize_le<true,  true,  false>(a); break;
+        case OP_ULT:              internalize_le<false, true,  true>(a); break;
+        case OP_SLT:              internalize_le<true,  true,  true>(a); break;
+        case OP_UGT:              internalize_le<false, false, true>(a); break;
+        case OP_SGT:              internalize_le<true,  false, true>(a); break;
+
+        case OP_BUMUL_NO_OVFL:    internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.umul_ovfl(p, q); }); break;
+        case OP_BSMUL_NO_OVFL:    internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.smul_ovfl(p, q); }); break;
+        case OP_BSMUL_NO_UDFL:    internalize_binaryc(a, [&](pdd const& p, pdd const& q) { return m_core.smul_udfl(p, q); }); break;
+
+        case OP_BUMUL_OVFL:
+        case OP_BSMUL_OVFL:
+        case OP_BSDIV_OVFL:
+        case OP_BNEG_OVFL:
+        case OP_BUADD_OVFL:
+        case OP_BSADD_OVFL:
+        case OP_BUSUB_OVFL:
+        case OP_BSSUB_OVFL:
+            // handled by bv_rewriter for now
+            UNREACHABLE();
+            break;
+
+        case OP_BUDIV_I:          internalize_div_rem_i(a, true); break;
+        case OP_BUREM_I:          internalize_div_rem_i(a, false); break;
+
+        case OP_BUDIV:            internalize_div_rem(a, true); break;
+        case OP_BUREM:            internalize_div_rem(a, false); break;
+        case OP_BSDIV0:           UNREACHABLE(); break;
+        case OP_BUDIV0:           UNREACHABLE(); break;
+        case OP_BSREM0:           UNREACHABLE(); break;
+        case OP_BUREM0:           UNREACHABLE(); break;
+        case OP_BSMOD0:           UNREACHABLE(); break;
+
+        case OP_EXTRACT:          internalize_extract(a); break;
+        case OP_CONCAT:           internalize_concat(a); break;
+        case OP_ZERO_EXT:         internalize_par_unary(a, [&](pdd const& p, unsigned sz) { return m_core.zero_ext(p, sz); }); break;
+        case OP_SIGN_EXT:         internalize_par_unary(a, [&](pdd const& p, unsigned sz) { return m_core.sign_ext(p, sz); }); break;
+
+            // polysat::solver should also support at least:
+        case OP_BREDAND: // x == 2^K - 1        unary, return single bit, 1 if all input bits are set.
+        case OP_BREDOR:  // x > 0               unary, return single bit, 1 if at least one input bit is set.
+        case OP_BCOMP:   // x == y              binary, return single bit, 1 if the arguments are equal.
+        case OP_BSDIV:            
+        case OP_BSREM:            
+        case OP_BSMOD:     
+        case OP_BSDIV_I:            
+        case OP_BSREM_I:                        
+        case OP_BSMOD_I:
+        case OP_BASHR:
+            IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n");
+            NOT_IMPLEMENTED_YET();
+            return;
+        default:
+            IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n");
+            NOT_IMPLEMENTED_YET();
+            return;
+        }
+#undef if_unary
+    }
+
+    class solver::mk_atom_trail : public trail {
+        solver& th;
+        sat::bool_var m_var;
+    public:
+        mk_atom_trail(sat::bool_var v, solver& th) : th(th), m_var(v) {}
+        void undo() override {
+            solver::atom* a = th.get_bv2a(m_var);
+            a->~atom();
+            th.erase_bv2a(m_var);
+        }
+    };
+
+    solver::atom* solver::mk_atom(sat::bool_var bv) {
+        atom* a = get_bv2a(bv);
+        if (a)
+            return a;
+        a = new (get_region()) atom(bv);
+        insert_bv2a(bv, a);
+        ctx.push(mk_atom_trail(bv, *this));
+        return a;
+    }
+
+    void solver::internalize_binaryc(app* e, std::function<polysat::signed_constraint(pdd, pdd)> const& fn) {
+        auto p = expr2pdd(e->get_arg(0));
+        auto q = expr2pdd(e->get_arg(1));
+        auto sc = ~fn(p, q);
+        sat::literal lit = expr2literal(e);
+        mk_atom(lit.var())->m_sc = sc;
+    }
+
+    void solver::internalize_div_rem_i(app* e, bool is_div) {
+        auto p = expr2pdd(e->get_arg(0));
+        auto q = expr2pdd(e->get_arg(1));
+        auto [quot, rem] = m_core.quot_rem(p, q);
+        internalize_set(e, is_div ? quot : rem);        
+    }
+
+    void solver::internalize_div_rem(app* e, bool is_div) {
+        bv_rewriter_params p(s().params());
+        if (p.hi_div0()) {
+            internalize_div_rem_i(e, is_div);
+            return;
+        }
+        expr* arg1 = e->get_arg(0);
+        expr* arg2 = e->get_arg(1);
+        unsigned sz = bv.get_bv_size(e);
+        expr_ref zero(bv.mk_numeral(0, sz), m);
+        sat::literal eqZ = eq_internalize(arg2, zero);
+        sat::literal eqU = eq_internalize(e, is_div ? bv.mk_bv_udiv0(arg1) : bv.mk_bv_urem0(arg1));
+        sat::literal eqI = eq_internalize(e, is_div ? bv.mk_bv_udiv_i(arg1, arg2) : bv.mk_bv_urem_i(arg1, arg2));
+        add_clause(~eqZ, eqU);
+        add_clause(eqZ, eqI);
+        ctx.add_aux(~eqZ, eqU);
+        ctx.add_aux(eqZ, eqI);        
+    }
+
+    void solver::internalize_num(app* a) {
+        rational val;
+        unsigned sz = 0;
+        VERIFY(bv.is_numeral(a, val, sz));        
+        auto p = m_core.value(val, sz);
+        internalize_set(a, p);
+    }
+
+    // TODO - test that internalize works with recursive call on bit2bool
+    void solver::internalize_mkbv(app* a) {
+        unsigned i = 0;
+        for (expr* arg : *a) {
+            expr_ref b2b(m);
+            b2b = bv.mk_bit2bool(a, i);            
+            sat::literal bit_i = ctx.internalize(b2b, false, false);
+            sat::literal lit = expr2literal(arg);
+            add_equiv(lit, bit_i);
+#if 0
+            ctx.add_aux_equiv(lit, bit_i);
+#endif
+            ++i;
+        }
+    }
+
+    void solver::internalize_extract(app* e) {
+        unsigned const hi = bv.get_extract_high(e);
+        unsigned const lo = bv.get_extract_low(e);
+        auto const src = expr2pdd(e->get_arg(0));
+        auto const p = m_core.extract(src, hi, lo);
+        SASSERT_EQ(p.power_of_2(), hi - lo + 1);
+        internalize_set(e, p);
+    }
+
+    void solver::internalize_concat(app* e) {
+        SASSERT(bv.is_concat(e));
+        vector<pdd> args;
+        for (expr* arg : *e)
+            args.push_back(expr2pdd(arg));
+        auto const p = m_core.concat(args.size(), args.data());
+        internalize_set(e, p);
+    }
+
+    void solver::internalize_par_unary(app* e, std::function<pdd(pdd,unsigned)> const& fn) {
+        pdd const p = expr2pdd(e->get_arg(0));
+        unsigned const par = e->get_parameter(0).get_int();
+        internalize_set(e, fn(p, par));
+    }
+
+    void solver::internalize_binary(app* e, std::function<pdd(pdd, pdd)> const& fn) {
+        SASSERT(e->get_num_args() >= 1);
+        auto p = expr2pdd(e->get_arg(0));
+        for (unsigned i = 1; i < e->get_num_args(); ++i) 
+            p = fn(p, expr2pdd(e->get_arg(i)));
+        internalize_set(e, p);
+    }
+
+    void solver::internalize_unary(app* e, std::function<pdd(pdd)> const& fn) {
+        SASSERT(e->get_num_args() == 1);
+        auto p = expr2pdd(e->get_arg(0));
+        internalize_set(e, fn(p));
+    }
+
+    template<bool Signed, bool Rev, bool Negated>
+    void solver::internalize_le(app* e) {
+        auto p = expr2pdd(e->get_arg(0));
+        auto q = expr2pdd(e->get_arg(1));
+        if (Rev)
+            std::swap(p, q);
+        auto sc = Signed ? m_core.sle(p, q) : m_core.ule(p, q);
+        if (Negated)
+            sc = ~sc;
+        
+        sat::literal lit = expr2literal(e);
+        atom* a = mk_atom(lit.var());
+        a->m_sc = sc;
+    }
+
+    void solver::internalize_bit2bool(atom* a, expr* e, unsigned idx) {
+        pdd p = expr2pdd(e);
+        a->m_sc = m_core.bit(p, idx);
+    }
+
+    dd::pdd solver::expr2pdd(expr* e) {
+        return var2pdd(get_th_var(e));
+    }
+
+    dd::pdd solver::var2pdd(euf::theory_var v) {
+        if (!m_var2pdd_valid.get(v, false)) {
+            unsigned bv_size = get_bv_size(v);
+            pvar pv = m_core.add_var(bv_size);
+            m_pddvar2var.setx(pv, v, UINT_MAX);
+            pdd p = m_core.var(pv);
+            internalize_set(v, p);
+            return p;
+        }
+        return m_var2pdd[v];
+    }
+
+    void solver::apply_sort_cnstr(euf::enode* n, sort* s) {
+        if (!bv.is_bv(n->get_expr()))
+            return;
+        theory_var v = n->get_th_var(get_id());
+        if (v == euf::null_theory_var) 
+            v = mk_var(n);
+        var2pdd(v);
+    }
+
+    void solver::internalize_set(expr* e, pdd const& p) {
+        internalize_set(get_th_var(e), p);
+    }
+
+    void solver::internalize_set(euf::theory_var v, pdd const& p) {
+        SASSERT_EQ(get_bv_size(v), p.power_of_2());
+        m_var2pdd.reserve(get_num_vars(), p);
+        m_var2pdd_valid.reserve(get_num_vars(), false);
+        ctx.push(set_bitvector_trail(m_var2pdd_valid, v));
+#if 0
+        m_var2pdd[v].reset(p.manager());
+#endif
+        m_var2pdd[v] = p;
+    }
+
+    void solver::eq_internalized(euf::enode* n) {
+        SASSERT(m.is_eq(n->get_expr()));
+    }
+
+
+}

src/sat/smt/polysat_model.cpp

@@ -0,0 +1,58 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    polysat_model.cpp
+
+Abstract:
+
+    PolySAT model generation
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-01-26
+
+--*/
+
+#include "params/bv_rewriter_params.hpp"
+#include "sat/smt/polysat_solver.h"
+#include "sat/smt/euf_solver.h"
+
+namespace polysat {
+
+
+    void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
+#if 0
+        auto p = expr2pdd(n->get_expr());
+        rational val;
+        VERIFY(m_polysat.try_eval(p, val));
+        values[n->get_root_id()] = bv.mk_numeral(val, get_bv_size(n));    
+#endif
+    }   
+
+
+    bool solver::check_model(sat::model const& m) const {
+        return false;
+    }
+
+    void solver::finalize_model(model& mdl) {
+
+    }
+
+    std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const {
+        return out;
+    }
+
+    std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
+        return out;
+    }
+
+    std::ostream& solver::display(std::ostream& out) const {
+        m_core.display(out);
+        for (unsigned v = 0; v < get_num_vars(); ++v)
+            if (m_var2pdd_valid.get(v, false))
+                out << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n";
+        return out;
+    }
+}

src/sat/smt/polysat_solver.cpp

@@ -0,0 +1,191 @@
+/*---
+Copyright (c 2022 Microsoft Corporation
+
+Module Name:
+
+    polysat_internalize.cpp
+
+Abstract:
+
+    PolySAT interface to bit-vector
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-01-26
+
+Notes:
+The solver adds literals to polysat::core, calls propagation and check
+The result of polysat::core::check is one of:
+- is_sat: the model is complete
+- is_unsat: there is a Boolean conflict. The SAT solver backtracks and resolves the conflict.
+- new_eq: the solver adds a new equality literal to the SAT solver.
+- new_lemma: there is a conflict, but it is resolved by backjumping and adding a lemma to the SAT solver.
+- giveup: Polysat was unable to determine satisfiability.
+
+--*/
+
+#include "ast/euf/euf_bv_plugin.h"
+#include "sat/smt/polysat_solver.h"
+#include "sat/smt/euf_solver.h"
+
+
+namespace polysat {
+
+    solver::solver(euf::solver& ctx, theory_id id):
+        euf::th_euf_solver(ctx, symbol("bv"), id),
+        bv(ctx.get_manager()),
+        m_autil(ctx.get_manager()),
+        m_core(*this),
+        m_lemma(ctx.get_manager())
+    {
+        ctx.get_egraph().add_plugin(alloc(euf::bv_plugin, ctx.get_egraph()));
+    }
+
+    unsigned solver::get_bv_size(euf::enode* n) {
+        return bv.get_bv_size(n->get_expr());
+    }
+
+    unsigned solver::get_bv_size(theory_var v) {
+        return bv.get_bv_size(var2expr(v));        
+    }
+
+    bool solver::unit_propagate() {
+        return m_core.propagate();
+    }
+
+    sat::check_result solver::check() {
+        return m_core.check();
+    }
+
+    void solver::asserted(literal l) {
+        atom* a = get_bv2a(l.var());
+        TRACE("bv", tout << "asserted: " << l << "\n";);
+        if (!a)
+            return;
+        force_push();
+        auto sc = a->m_sc;
+        if (l.sign())
+            sc = ~sc;
+        m_core.assign_eh(sc, dependency(l, s().lvl(l)));
+    }
+
+    void solver::set_conflict(dependency_vector const& core) {
+        auto [lits, eqs] = explain_deps(core);
+        auto ex = euf::th_explain::conflict(*this, lits, eqs, nullptr);
+        ctx.set_conflict(ex);
+    }
+
+    std::pair<sat::literal_vector, euf::enode_pair_vector> solver::explain_deps(dependency_vector const& deps) {
+        sat::literal_vector core;
+        euf::enode_pair_vector eqs;
+        for (auto d : deps) {
+            if (d.is_literal()) {
+                core.push_back(d.literal());
+            }
+            else {
+                auto const [v1, v2] = m_var_eqs[d.index()];
+                euf::enode* const n1 = var2enode(v1);
+                euf::enode* const n2 = var2enode(v2);
+                VERIFY(n1->get_root() == n2->get_root());
+                eqs.push_back(euf::enode_pair(n1, n2));
+            }
+        }
+        DEBUG_CODE({
+            for (auto lit : core)
+                VERIFY(s().value(lit) == l_true);
+            for (auto const& [n1, n2] : eqs)
+                VERIFY(n1->get_root() == n2->get_root());
+            });
+        IF_VERBOSE(10,
+            for (auto lit : core)
+                verbose_stream() << "    " << lit << ":  " << mk_ismt2_pp(literal2expr(lit), m) << "\n";
+            for (auto const& [n1, n2] : eqs)
+                verbose_stream() << "    " << ctx.bpp(n1) << "  ==  " << ctx.bpp(n2) << "\n";);
+
+        return { core, eqs };
+    }
+
+    void solver::set_lemma(vector<signed_constraint> const& lemma, unsigned level, dependency_vector const& core) {
+        auto [lits, eqs] = explain_deps(core);
+        auto ex = euf::th_explain::conflict(*this, lits, eqs, nullptr);
+        ctx.push(value_trail<bool>(m_has_lemma));
+        m_has_lemma = true;
+        m_lemma_level = level;
+        m_lemma.reset();
+        for (auto sc : lemma)
+            m_lemma.push_back(m_core.constraint2expr(sc));
+        ctx.set_conflict(ex);
+    }
+
+    // If an MCSat lemma is added, then backjump based on the lemma level and 
+    // add the lemma to the solver with potentially fresh literals.
+    // return l_false to signal sat::solver that backjumping has been taken care of internally.
+    lbool solver::resolve_conflict() {
+        if (!m_has_lemma)
+            return l_undef;
+
+        unsigned num_scopes = s().scope_lvl() - m_lemma_level;
+
+        // s().pop_reinit(num_scopes);
+
+        sat::literal_vector lits;
+        for (auto* e : m_lemma)
+            lits.push_back(ctx.mk_literal(e));
+        s().add_clause(lits.size(), lits.data(), sat::status::th(true, get_id(), nullptr));
+        return l_false;
+    }
+
+    // Create an equality literal that represents the value assignment
+    // Prefer case split to true.
+    // The equality gets added in a callback using asserted().
+    void solver::add_eq_literal(pvar pvar, rational const& val) {
+        auto v = m_pddvar2var[pvar];
+        auto n = var2enode(v);
+        auto eq = eq_internalize(n->get_expr(), bv.mk_numeral(val, get_bv_size(v)));
+        s().set_phase(eq);
+    }
+
+    void solver::new_eq_eh(euf::th_eq const& eq) {
+        auto v1 = eq.v1(), v2 = eq.v2();
+        pdd p = var2pdd(v1);
+        pdd q = var2pdd(v2);
+        auto sc = m_core.eq(p, q);        
+        m_var_eqs.setx(m_var_eqs_head, std::make_pair(v1, v2), std::make_pair(v1, v2));
+        ctx.push(value_trail<unsigned>(m_var_eqs_head));        
+        m_core.assign_eh(sc, dependency(m_var_eqs_head, s().scope_lvl())); 
+        m_var_eqs_head++;
+    }
+
+    void solver::new_diseq_eh(euf::th_eq const& ne) {
+        euf::theory_var v1 = ne.v1(), v2 = ne.v2();
+        pdd p = var2pdd(v1);
+        pdd q = var2pdd(v2);
+        auto sc = ~m_core.eq(p, q);
+        sat::literal neq = ~expr2literal(ne.eq());
+        TRACE("bv", tout << neq << " := " << s().value(neq) << " @" << s().scope_lvl() << "\n");
+        m_core.assign_eh(sc, dependency(neq, s().lvl(neq)));
+    }
+
+    // Core uses the propagate callback to add unit propagations to the trail.
+    // The polysat::solver takes care of translating signed constraints into expressions, which translate into literals.
+    // Everything goes over expressions/literals. polysat::core is not responsible for replaying expressions. 
+    void solver::propagate(signed_constraint sc, dependency_vector const& deps) {
+        sat::literal lit = ctx.mk_literal(m_core.constraint2expr(sc));
+        auto [core, eqs] = explain_deps(deps);
+        auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr);
+        ctx.propagate(lit, ex);
+    }
+
+    void solver::add_lemma(vector<signed_constraint> const& lemma) {
+        sat::literal_vector lits;
+        for (auto sc : lemma)
+            lits.push_back(ctx.mk_literal(m_core.constraint2expr(sc)));
+        s().add_clause(lits.size(), lits.data(), sat::status::th(true, get_id(), nullptr));
+    }
+
+    void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) {
+        auto& jst = euf::th_explain::from_index(idx);
+        ctx.get_th_antecedents(l, jst, r, probing);
+    }
+
+}

src/sat/smt/polysat_solver.h

@@ -0,0 +1,187 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    polysat_solver.h
+
+Abstract:
+
+    Theory plugin for bit-vectors
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-30
+
+--*/
+#pragma once
+
+#include "sat/smt/sat_th.h"
+#include "math/dd/dd_pdd.h"
+#include "sat/smt/polysat_core.h"
+
+namespace euf {
+    class solver;
+}
+
+namespace polysat {
+
+
+    class solver : public euf::th_euf_solver {
+        typedef euf::theory_var theory_var;
+        typedef euf::theory_id theory_id;
+        typedef sat::literal literal;
+        typedef sat::bool_var bool_var;
+        typedef sat::literal_vector literal_vector;
+        using pdd = dd::pdd;
+
+        struct stats {
+            void reset() { memset(this, 0, sizeof(stats)); }
+            stats() { reset(); }
+        };
+
+        struct atom {
+            bool_var                m_bv;
+            signed_constraint       m_sc;
+            atom(bool_var b) :m_bv(b) {}
+            ~atom() { }
+        };
+
+        class polysat_proof : public euf::th_proof_hint {
+        public:
+            ~polysat_proof() override {}
+            expr* get_hint(euf::solver& s) const override { return nullptr; }
+        };
+
+        friend class core;
+
+        bv_util                  bv;
+        arith_util               m_autil;
+        stats                    m_stats;
+        core                     m_core;
+        polysat_proof            m_proof;
+
+        vector<pdd>              m_var2pdd;                   // theory_var 2 pdd
+        bool_vector              m_var2pdd_valid;             // valid flag
+        unsigned_vector          m_pddvar2var;                // pvar -> theory_var
+        ptr_vector<atom>         m_bool_var2atom;             // bool_var -> atom
+
+        svector<std::pair<euf::theory_var, euf::theory_var>> m_var_eqs;
+        unsigned                 m_var_eqs_head = 0;
+
+        bool m_has_lemma = false;
+        unsigned m_lemma_level = 0;
+        expr_ref_vector m_lemma;
+
+        // internalize
+        bool visit(expr* e) override;
+        bool visited(expr* e) override;
+        bool post_visit(expr* e, bool sign, bool root) override;
+        unsigned get_bv_size(euf::enode* n);
+        unsigned get_bv_size(theory_var v);
+        theory_var get_var(euf::enode* n);
+        void fixed_var_eh(theory_var v);
+        bool is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) override { return false; }
+        bool is_bv(theory_var v) const { return bv.is_bv(var2expr(v)); }
+        void register_true_false_bit(theory_var v, unsigned i);
+        void add_bit(theory_var v, sat::literal lit);
+        void eq_internalized(sat::bool_var b1, sat::bool_var b2, unsigned idx, theory_var v1, theory_var v2, sat::literal eq, euf::enode* n);
+
+        void insert_bv2a(bool_var bv, atom* a) { m_bool_var2atom.setx(bv, a, nullptr); }
+        void erase_bv2a(bool_var bv) { m_bool_var2atom[bv] = nullptr; }
+        atom* get_bv2a(bool_var bv) const { return m_bool_var2atom.get(bv, nullptr); }
+        class mk_atom_trail;
+        atom* mk_atom(sat::bool_var bv);
+        void set_bit_eh(theory_var v, literal l, unsigned idx);
+        void init_bits(expr* e, expr_ref_vector const & bits);
+        void mk_bits(theory_var v);
+        void add_def(sat::literal def, sat::literal l);
+        void internalize_unary(app* e, std::function<pdd(pdd)> const& fn);
+        void internalize_binary(app* e, std::function<pdd(pdd, pdd)> const& fn);
+        void internalize_binaryc(app* e, std::function<signed_constraint(pdd, pdd)> const& fn);
+        void internalize_par_unary(app* e, std::function<pdd(pdd,unsigned)> const& fn);
+        void internalize_novfl(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref&)>& fn);
+        void internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& un);
+        void internalize_num(app * n);       
+        void internalize_concat(app * n);        
+        void internalize_bv2int(app* n);
+        void internalize_int2bv(app* n);
+        void internalize_mkbv(app* n);
+        void internalize_xor3(app* n);
+        void internalize_carry(app* n);
+        void internalize_sub(app* n);
+        void internalize_extract(app* n);
+        void internalize_repeat(app* n);
+        void internalize_bit2bool(app* n);
+        void internalize_udiv_i(app* n);
+        template<bool Signed, bool Reverse, bool Negated>
+        void internalize_le(app* n);
+        void internalize_div_rem_i(app* e, bool is_div);
+        void internalize_div_rem(app* e, bool is_div);
+        void internalize_polysat(app* a);
+        void assert_bv2int_axiom(app * n);
+        void assert_int2bv_axiom(app* n);
+        void internalize_bit2bool(atom* a, expr* e, unsigned idx);
+
+        pdd expr2pdd(expr* e);
+        pdd var2pdd(euf::theory_var v);
+        void internalize_set(expr* e, pdd const& p);
+        void internalize_set(euf::theory_var v, pdd const& p);
+
+        // callbacks from core
+        void add_eq_literal(pvar v, rational const& val);
+        void set_conflict(dependency_vector const& core);
+        void set_lemma(vector<signed_constraint> const& lemma, unsigned level, dependency_vector const& core);
+        void propagate(signed_constraint sc, dependency_vector const& deps);
+        void add_lemma(vector<signed_constraint> const& lemma);
+
+        std::pair<sat::literal_vector, euf::enode_pair_vector> explain_deps(dependency_vector const& deps);
+	       
+    public:
+        solver(euf::solver& ctx, theory_id id);
+        void set_lookahead(sat::lookahead* s) override { }
+        void init_search() override {}
+        double get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const override { return 0; }
+        bool is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) override { return false; }
+        bool is_external(bool_var v) override { return false; }
+        void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r, bool probing) override;
+        void asserted(literal l) override;
+        sat::check_result check() override;
+        void simplify() override {}
+        void clauses_modifed() override {}
+        lbool get_phase(bool_var v) override { return l_undef; }
+        std::ostream& display(std::ostream& out) const override;
+        std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
+        std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
+        void collect_statistics(statistics& st) const override {}
+        euf::th_solver* clone(euf::solver& ctx) override { throw default_exception("nyi"); }
+        extension* copy(sat::solver* s) override { throw default_exception("nyi"); }
+        void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override {}
+        void gc() override {}
+        void pop_reinit() override {}
+        lbool resolve_conflict() override;
+        bool validate() override { return true; }
+        void init_use_list(sat::ext_use_list& ul) override {}
+        bool is_blocked(literal l, sat::ext_constraint_idx) override { return false; }
+        bool check_model(sat::model const& m) const override;
+        void finalize_model(model& mdl) override;
+
+        void new_eq_eh(euf::th_eq const& eq) override;
+        void new_diseq_eh(euf::th_eq const& ne) override;
+        bool use_diseqs() const override { return true; }
+        bool unit_propagate() override;
+
+        void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
+
+        bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
+                        std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override { return false; }
+
+        bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override { return false; }
+        sat::literal internalize(expr* e, bool sign, bool root) override;
+        void internalize(expr* e) override;
+        void eq_internalized(euf::enode* n) override;
+        euf::theory_var mk_var(euf::enode* n) override;
+        void apply_sort_cnstr(euf::enode * n, sort * s) override;
+    };
+
+}

src/sat/smt/polysat_substitution.h

@@ -0,0 +1,212 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat substitution
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-06
+
+--*/
+#pragma once
+#include "sat/smt/polysat_types.h"
+
+namespace polysat {
+
+    using assignment_item_t = std::pair<pvar, rational>;
+
+    class substitution_iterator {
+        pdd m_current;
+        substitution_iterator(pdd current) : m_current(std::move(current)) {}
+        friend class substitution;
+
+    public:
+        using value_type = assignment_item_t;
+        using difference_type = std::ptrdiff_t;
+        using pointer = value_type const*;
+        using reference = value_type const&;
+        using iterator_category = std::input_iterator_tag;
+
+        substitution_iterator& operator++() {
+            SASSERT(!m_current.is_val());
+            m_current = m_current.hi();
+            return *this;
+        }
+
+        value_type operator*() const {
+            SASSERT(!m_current.is_val());
+            return { m_current.var(), m_current.lo().val() };
+        }
+
+        bool operator==(substitution_iterator const& other) const { return m_current == other.m_current; }
+        bool operator!=(substitution_iterator const& other) const { return !operator==(other); }
+    };
+
+    /** Substitution for a single bit width. */
+    class substitution {
+        pdd m_subst;
+
+        substitution(pdd p);
+
+    public:
+        substitution(dd::pdd_manager& m);
+        [[nodiscard]] substitution add(pvar var, rational const& value) const;
+        [[nodiscard]] pdd apply_to(pdd const& p) const;
+
+        [[nodiscard]] bool contains(pvar var) const;
+        [[nodiscard]] bool value(pvar var, rational& out_value) const;
+
+        [[nodiscard]] bool empty() const { return m_subst.is_one(); }
+
+        pdd const& to_pdd() const { return m_subst; }
+        unsigned bit_width() const { return to_pdd().power_of_2(); }
+
+        bool operator==(substitution const& other) const { return &m_subst.manager() == &other.m_subst.manager() && m_subst == other.m_subst; }
+        bool operator!=(substitution const& other) const { return !operator==(other); }
+
+        std::ostream& display(std::ostream& out) const;
+
+        using const_iterator = substitution_iterator;
+        const_iterator begin() const { return {m_subst}; }
+        const_iterator end() const { return {m_subst.manager().one()}; }
+    };
+
+    /** Full variable assignment, may include variables of varying bit widths. */
+    class assignment {
+        vector<assignment_item_t>               m_pairs;
+        mutable scoped_ptr_vector<substitution> m_subst;
+        vector<substitution>                    m_subst_trail;
+
+        substitution& subst(unsigned sz);
+        solver& s() const { return *m_solver; }
+    public:
+        assignment(solver& s);
+        // prevent implicit copy, use clone() if you do need a copy
+        assignment(assignment const&) = delete;
+        assignment& operator=(assignment const&) = delete;
+        assignment(assignment&&) = default;
+        assignment& operator=(assignment&&) = default;
+        assignment clone() const;
+
+        void push(pvar var, rational const& value);
+        void pop();
+
+        pdd apply_to(pdd const& p) const;
+
+        bool contains(pvar var) const;
+        bool value(pvar var, rational& out_value) const;
+        rational value(pvar var) const { rational val; VERIFY(value(var, val)); return val; }
+        bool empty() const { return pairs().empty(); }
+        substitution const& subst(unsigned sz) const;
+        vector<assignment_item_t> const& pairs() const { return m_pairs; }
+        using const_iterator = decltype(m_pairs)::const_iterator;
+        const_iterator begin() const { return pairs().begin(); }
+        const_iterator end() const { return pairs().end(); }
+
+        std::ostream& display(std::ostream& out) const;
+    };
+
+    inline std::ostream& operator<<(std::ostream& out, substitution const& sub) { return sub.display(out); }
+
+    inline std::ostream& operator<<(std::ostream& out, assignment const& a) { return a.display(out); }
+}
+
+namespace polysat {
+
+    enum class search_item_k
+    {
+        assignment,
+        boolean,
+    };
+
+    class search_item {
+        search_item_k m_kind;
+        union {
+            pvar m_var;
+            sat::literal m_lit;
+        };
+        bool m_resolved = false; // when marked as resolved it is no longer valid to reduce the conflict state
+
+        search_item(pvar var): m_kind(search_item_k::assignment), m_var(var) {}
+        search_item(sat::literal lit): m_kind(search_item_k::boolean), m_lit(lit) {}
+    public:
+        static search_item assignment(pvar var) { return search_item(var); }
+        static search_item boolean(sat::literal lit) { return search_item(lit); }
+        bool is_assignment() const { return m_kind == search_item_k::assignment; }
+        bool is_boolean() const { return m_kind == search_item_k::boolean; }
+        bool is_resolved() const { return m_resolved; }
+        search_item_k kind() const { return m_kind; }
+        pvar var() const { SASSERT(is_assignment()); return m_var; }
+        sat::literal lit() const { SASSERT(is_boolean()); return m_lit; }
+        void set_resolved() { m_resolved = true; }
+    };
+
+    class search_state {
+        solver&             s;
+
+        vector<search_item> m_items;
+        assignment          m_assignment;
+
+        // store index into m_items
+        unsigned_vector     m_pvar_to_idx;
+        unsigned_vector     m_bool_to_idx;
+
+        bool value(pvar v, rational& r) const;
+
+    public:
+        search_state(solver& s): s(s), m_assignment(s) {}
+        unsigned size() const { return m_items.size(); }
+        search_item const& back() const { return m_items.back(); }
+        search_item const& operator[](unsigned i) const { return m_items[i]; }
+
+        assignment const& get_assignment() const { return m_assignment; }
+        substitution const& subst(unsigned sz) const { return m_assignment.subst(sz); }
+
+        // TODO: implement the following method if we actually need the assignments without resolved items already during conflict resolution
+        //       (no separate trail needed, just a second m_subst and an index into the trail, I think)
+        //       (update on set_resolved? might be one iteration too early, looking at the old solver::resolve_conflict loop)
+        substitution const& unresolved_assignment(unsigned sz) const;
+
+        void push_assignment(pvar v, rational const& r);
+        void push_boolean(sat::literal lit);
+        void pop();
+
+        unsigned get_pvar_index(pvar v) const;
+        unsigned get_bool_index(sat::bool_var var) const;
+        unsigned get_bool_index(sat::literal lit) const { return get_bool_index(lit.var()); }
+
+        void set_resolved(unsigned i) { m_items[i].set_resolved(); }
+
+        using const_iterator = decltype(m_items)::const_iterator;
+        const_iterator begin() const { return m_items.begin(); }
+        const_iterator end() const { return m_items.end(); }
+
+        std::ostream& display(std::ostream& out) const;
+        std::ostream& display(search_item const& item, std::ostream& out) const;
+        std::ostream& display_verbose(std::ostream& out) const;
+        std::ostream& display_verbose(search_item const& item, std::ostream& out) const;
+    };
+
+    struct search_state_pp {
+        search_state const& s;
+        bool verbose;
+        search_state_pp(search_state const& s, bool verbose = false) : s(s), verbose(verbose) {}
+    };
+
+    struct search_item_pp {
+        search_state const& s;
+        search_item const& i;
+        bool verbose;
+        search_item_pp(search_state const& s, search_item const& i, bool verbose = false) : s(s), i(i), verbose(verbose) {}
+    };
+
+    inline std::ostream& operator<<(std::ostream& out, search_state const& s) { return s.display(out); }
+
+    inline std::ostream& operator<<(std::ostream& out, search_state_pp const& p) { return p.verbose ? p.s.display_verbose(out) : p.s.display(out); }
+
+    inline std::ostream& operator<<(std::ostream& out, search_item_pp const& p) { return p.verbose ? p.s.display_verbose(p.i, out) : p.s.display(p.i, out); }
+
+}

src/sat/smt/polysat_types.h

@@ -0,0 +1,45 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-06
+
+--*/
+#pragma once
+
+#include "math/dd/dd_pdd.h"
+#include "util/sat_literal.h"
+#include "util/dependency.h"
+
+namespace polysat {
+
+    using pdd = dd::pdd;
+    using pvar = unsigned;
+
+
+    class dependency {
+        unsigned m_index;
+        unsigned m_level;
+    public:
+        dependency(sat::literal lit, unsigned level) : m_index(2 * lit.index()), m_level(level) {}
+        dependency(unsigned var_idx, unsigned level) : m_index(1 + 2 * var_idx), m_level(level) {} 
+        bool is_literal() const { return m_index % 2 == 0; }
+        sat::literal literal() const { SASSERT(is_literal());  return sat::to_literal(m_index / 2); }
+        unsigned index() const { SASSERT(!is_literal()); return (m_index - 1) / 2; }
+        unsigned level() const { return m_level; }
+    };
+
+    using stacked_dependency = stacked_dependency_manager<dependency>::dependency;
+
+    inline std::ostream& operator<<(std::ostream& out, dependency d) {
+        if (d.is_literal())
+            return out << d.literal() << "@" << d.level();
+        else
+            return out << "v" << d.index() << "@" << d.level();
+    }
+
+    using dependency_vector = vector<dependency>;
+
+}

src/sat/smt/polysat_viable.h

@@ -0,0 +1,55 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    maintain viable domains
+    It uses the interval extraction functions from forbidden intervals.
+    An empty viable set corresponds directly to a conflict that does not rely on
+    the non-viable variable.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-06
+
+--*/
+#pragma once
+
+#include "util/rational.h"
+#include "sat/smt/polysat_types.h"
+
+namespace polysat {
+
+    enum class find_t {
+        empty,
+        singleton,
+        multiple,
+        resource_out,
+    };
+
+    class core;
+
+    class viable {
+        core& c;
+    public:
+        viable(core& c) : c(c) {}
+
+	    /**
+         * Find a next viable value for variable.
+         */
+        find_t find_viable(pvar v, rational& out_val) { throw default_exception("nyi"); }
+
+        /*
+        * Explain why the current variable is not viable or signleton.
+        */
+        dependency_vector explain() { throw default_exception("nyi"); }
+
+        /*
+        * Register constraint at index 'idx' as unitary in v.
+        */
+        void add_unitary(pvar v, unsigned idx) { throw default_exception("nyi"); }
+
+    };
+
+}

src/util/var_queue.h

@@ -68,6 +68,8 @@ public:
     void reset() {
         m_queue.reset();
     }
+
+    bool contains(var v) const { return m_queue.contains(v); }
     
     bool empty() const { return m_queue.empty(); }