diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 77bb1b680..0f5dc26ae 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -58,7 +58,8 @@ def init_project_def():
     add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model')
     add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model', 'solver_assertions',
                     'substitution', 'grobner', 'simplex', 'proofs', 'pattern', 'parser_util', 'fpa', 'lp'])
-    add_lib('sat_smt', ['sat', 'euf', 'smt', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern', 'qe_lite'], 'sat/smt')
+    add_lib('polysat', ['util', 'dd'], 'sat/smt/polysat'),
+    add_lib('sat_smt', ['sat', 'euf', 'smt', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'polysat', 'normal_forms', 'lp', 'pattern', 'qe_lite'], 'sat/smt')
     add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic')
     add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')    
     add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv')
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index a12571f35..13fd58db8 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -73,6 +73,7 @@ add_subdirectory(parsers/smt2)
 add_subdirectory(solver/assertions)
 add_subdirectory(ast/pattern)
 add_subdirectory(math/lp)
+add_subdirectory(sat/smt/polysat)
 add_subdirectory(sat/smt)
 add_subdirectory(sat/tactic)
 add_subdirectory(nlsat/tactic)
diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt
index 24c34a0a4..182d01249 100644
--- a/src/sat/smt/CMakeLists.txt
+++ b/src/sat/smt/CMakeLists.txt
@@ -35,16 +35,9 @@ 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_fi.cpp
     polysat_model.cpp
     polysat_solver.cpp
-    polysat_ule.cpp
-    polysat_umul_ovfl.cpp
-    polysat_viable.cpp
     q_clause.cpp
     q_ematch.cpp
     q_eval.cpp
diff --git a/src/sat/smt/polysat/CMakeLists.txt b/src/sat/smt/polysat/CMakeLists.txt
new file mode 100644
index 000000000..0011e0ee5
--- /dev/null
+++ b/src/sat/smt/polysat/CMakeLists.txt
@@ -0,0 +1,15 @@
+z3_add_component(polysat
+  SOURCES
+    polysat_assignment.cpp
+    polysat_constraints.cpp
+    polysat_core.cpp
+    polysat_fi.cpp
+    polysat_ule.cpp
+    polysat_umul_ovfl.cpp
+    polysat_viable.cpp
+  COMPONENT_DEPENDENCIES
+    util
+    dd
+    smt_params
+)
+
diff --git a/src/sat/smt/polysat_assignment.cpp b/src/sat/smt/polysat/polysat_assignment.cpp
similarity index 97%
rename from src/sat/smt/polysat_assignment.cpp
rename to src/sat/smt/polysat/polysat_assignment.cpp
index a985188fa..aedf6d409 100644
--- a/src/sat/smt/polysat_assignment.cpp
+++ b/src/sat/smt/polysat/polysat_assignment.cpp
@@ -12,8 +12,8 @@ Author:
 
 --*/
 
-#include "sat/smt/polysat_assignment.h"
-#include "sat/smt/polysat_core.h"
+#include "sat/smt/polysat/polysat_assignment.h"
+#include "sat/smt/polysat/polysat_core.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat_assignment.h b/src/sat/smt/polysat/polysat_assignment.h
similarity index 98%
rename from src/sat/smt/polysat_assignment.h
rename to src/sat/smt/polysat/polysat_assignment.h
index daff03dd5..befaad0b7 100644
--- a/src/sat/smt/polysat_assignment.h
+++ b/src/sat/smt/polysat/polysat_assignment.h
@@ -13,7 +13,7 @@ Author:
 --*/
 #pragma once
 #include "util/scoped_ptr_vector.h"
-#include "sat/smt/polysat_types.h"
+#include "sat/smt/polysat/polysat_types.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat_constraints.cpp b/src/sat/smt/polysat/polysat_constraints.cpp
similarity index 85%
rename from src/sat/smt/polysat_constraints.cpp
rename to src/sat/smt/polysat/polysat_constraints.cpp
index b588019dc..99da7b0db 100644
--- a/src/sat/smt/polysat_constraints.cpp
+++ b/src/sat/smt/polysat/polysat_constraints.cpp
@@ -12,11 +12,10 @@ Author:
 
 --*/
 
-#include "sat/smt/polysat_core.h"
-#include "sat/smt/polysat_solver.h"
-#include "sat/smt/polysat_constraints.h"
-#include "sat/smt/polysat_ule.h"
-#include "sat/smt/polysat_umul_ovfl.h"
+#include "sat/smt/polysat/polysat_core.h"
+#include "sat/smt/polysat/polysat_constraints.h"
+#include "sat/smt/polysat/polysat_ule.h"
+#include "sat/smt/polysat/polysat_umul_ovfl.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat_constraints.h b/src/sat/smt/polysat/polysat_constraints.h
similarity index 99%
rename from src/sat/smt/polysat_constraints.h
rename to src/sat/smt/polysat/polysat_constraints.h
index b62fbba21..687b3d91a 100644
--- a/src/sat/smt/polysat_constraints.h
+++ b/src/sat/smt/polysat/polysat_constraints.h
@@ -15,7 +15,7 @@ Author:
 
 #pragma once 
 #include "util/trail.h"
-#include "sat/smt/polysat_types.h"
+#include "sat/smt/polysat/polysat_types.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat_core.cpp b/src/sat/smt/polysat/polysat_core.cpp
similarity index 92%
rename from src/sat/smt/polysat_core.cpp
rename to src/sat/smt/polysat/polysat_core.cpp
index be4bb0cf0..07eeaa0c1 100644
--- a/src/sat/smt/polysat_core.cpp
+++ b/src/sat/smt/polysat/polysat_core.cpp
@@ -29,8 +29,7 @@ polysat::core
 --*/
 
 #include "params/bv_rewriter_params.hpp"
-#include "sat/smt/polysat_solver.h"
-#include "sat/smt/euf_solver.h"
+#include "sat/smt/polysat/polysat_core.h"
 
 namespace polysat {
 
@@ -79,10 +78,10 @@ namespace polysat {
         }
     };
 
-    core::core(solver& s) :
+    core::core(solver_interface& s) :
         s(s),         
         m_viable(*this),
-        m_constraints(s.get_trail_stack()),
+        m_constraints(s.trail()),
         m_assignment(*this),
         m_var_queue(m_activity)
     {}
@@ -109,7 +108,7 @@ namespace polysat {
         m_justification.push_back(null_dependency);
         m_watch.push_back({});
         m_var_queue.mk_var_eh(v);
-        s.ctx.push(mk_add_var(*this));
+        s.trail().push(mk_add_var(*this));
         return v;
     }
 
@@ -134,7 +133,7 @@ namespace polysat {
             add_watch(idx, vars[0]);
         if (vars.size() > 1)
             add_watch(idx, vars[1]);
-        s.ctx.push(mk_add_watch(*this));
+        s.trail().push(mk_add_watch(*this));
         return idx;
     }
 
@@ -146,7 +145,7 @@ namespace polysat {
         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));
+        s.trail().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();
@@ -169,11 +168,11 @@ namespace polysat {
     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)
+        s.trail().push(value_trail(m_qhead));
+        for (; m_qhead < m_prop_queue.size() && !s.inconsistent(); ++m_qhead)
             propagate_assignment(m_prop_queue[m_qhead]);        
-        s.ctx.push(value_trail(m_vqhead));
-        for (; m_vqhead < m_prop_queue.size() && !s.ctx.inconsistent(); ++m_vqhead) 
+        s.trail().push(value_trail(m_vqhead));
+        for (; m_vqhead < m_prop_queue.size() && !s.inconsistent(); ++m_vqhead) 
             propagate_value(m_prop_queue[m_vqhead]);        
         return true;
     }
@@ -202,12 +201,12 @@ namespace polysat {
             return;
         if (m_var_queue.contains(v)) {
             m_var_queue.del_var_eh(v);
-            s.ctx.push(mk_dqueue_var(v, *this));
+            s.trail().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));
+        s.trail().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.
@@ -289,7 +288,7 @@ namespace polysat {
 
     void core::assign_eh(unsigned index, bool sign, dependency const& dep) { 
         m_prop_queue.push_back({ index, sign, dep });
-        s.ctx.push(push_back_vector(m_prop_queue));
+        s.trail().push(push_back_vector(m_prop_queue));
     }
 
     dependency_vector core::explain_eval(signed_constraint const& sc) { 
@@ -309,7 +308,7 @@ namespace polysat {
     }
 
     trail_stack& core::trail() {
-        return s.get_trail_stack();
+        return s.trail();
     }
 
 }
diff --git a/src/sat/smt/polysat_core.h b/src/sat/smt/polysat/polysat_core.h
similarity index 94%
rename from src/sat/smt/polysat_core.h
rename to src/sat/smt/polysat/polysat_core.h
index b7c9f9eb8..bb21ee641 100644
--- a/src/sat/smt/polysat_core.h
+++ b/src/sat/smt/polysat/polysat_core.h
@@ -20,15 +20,15 @@ Author:
 #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"
+#include "sat/smt/polysat/polysat_types.h"
+#include "sat/smt/polysat/polysat_constraints.h"
+#include "sat/smt/polysat/polysat_viable.h"
+#include "sat/smt/polysat/polysat_assignment.h"
 
 namespace polysat {
 
     class core;
-    class solver;
+    class solver_interface;
 
     class core {
         class mk_add_var;
@@ -45,7 +45,7 @@ namespace polysat {
             signed_constraint sc;
             dependency d;
         };
-        solver& s;
+        solver_interface& s;
         viable m_viable;
         constraints m_constraints;
         assignment m_assignment;
@@ -87,7 +87,7 @@ namespace polysat {
         dependency_vector explain_eval(signed_constraint const& sc);
 
     public:
-        core(solver& s);
+        core(solver_interface& s);
 
         sat::check_result check();
 
diff --git a/src/sat/smt/polysat_fi.cpp b/src/sat/smt/polysat/polysat_fi.cpp
similarity index 98%
rename from src/sat/smt/polysat_fi.cpp
rename to src/sat/smt/polysat/polysat_fi.cpp
index 349243ed8..e54fb5cea 100644
--- a/src/sat/smt/polysat_fi.cpp
+++ b/src/sat/smt/polysat/polysat_fi.cpp
@@ -13,11 +13,11 @@ Author:
     Nikolaj Bjorner (nbjorner) 2021-03-19
 
 --*/
-#include "sat/smt/polysat_fi.h"
-#include "sat/smt/polysat_interval.h"
-#include "sat/smt/polysat_umul_ovfl.h"
-#include "sat/smt/polysat_ule.h"
-#include "sat/smt/polysat_core.h"
+#include "sat/smt/polysat/polysat_fi.h"
+#include "sat/smt/polysat/polysat_interval.h"
+#include "sat/smt/polysat/polysat_umul_ovfl.h"
+#include "sat/smt/polysat/polysat_ule.h"
+#include "sat/smt/polysat/polysat_core.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat_fi.h b/src/sat/smt/polysat/polysat_fi.h
similarity index 96%
rename from src/sat/smt/polysat_fi.h
rename to src/sat/smt/polysat/polysat_fi.h
index 7782deb4a..e1f876c3c 100644
--- a/src/sat/smt/polysat_fi.h
+++ b/src/sat/smt/polysat/polysat_fi.h
@@ -14,9 +14,9 @@ Author:
 
 --*/
 #pragma once
-#include "sat/smt/polysat_types.h"
-#include "sat/smt/polysat_interval.h"
-#include "sat/smt/polysat_constraints.h"
+#include "sat/smt/polysat/polysat_types.h"
+#include "sat/smt/polysat/polysat_interval.h"
+#include "sat/smt/polysat/polysat_constraints.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat/polysat_interval.h b/src/sat/smt/polysat/polysat_interval.h
new file mode 100644
index 000000000..0299f83b3
--- /dev/null
+++ b/src/sat/smt/polysat/polysat_interval.h
@@ -0,0 +1,224 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat intervals
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+#pragma once
+#include "sat/smt/polysat/polysat_types.h"
+#include <optional>
+
+namespace polysat {
+
+    struct pdd_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 {
+        std::optional<pdd_bounds> m_bounds = std::nullopt;
+
+        interval() = default;
+        interval(pdd const& lo, pdd const& hi): 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}; }
+
+        interval(interval const&) = default;
+        interval(interval&&) = default;
+        interval& operator=(interval const& other) {
+            m_bounds = std::nullopt;  // clear pdds first to allow changing pdd_manager (probably should change the PDD assignment operator; but for now I want to be able to detect manager confusions)
+            m_bounds = other.m_bounds;
+            return *this;
+        }
+        interval& operator=(interval&& other) {
+            m_bounds = std::nullopt;  // clear pdds first to allow changing pdd_manager
+            m_bounds = std::move(other.m_bounds);
+            return *this;
+        }
+        ~interval() = default;
+
+        bool is_full() const { return !m_bounds; }
+        bool is_proper() const { return !!m_bounds; }
+        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() << "[";
+    }
+
+    // distance from a to b, wrapping around at mod_value.
+    // basically mod(b - a, mod_value), but distance(0, mod_value, mod_value) = mod_value.
+    inline rational distance(rational const& a, rational const& b, rational const& mod_value) {
+        SASSERT(mod_value.is_power_of_two());
+        SASSERT(0 <= a && a < mod_value);
+        SASSERT(0 <= b && b <= mod_value);
+        rational x = b - a;
+        if (x.is_neg())
+            x += mod_value;
+        return x;
+    }
+
+    class r_interval {
+        rational m_lo;
+        rational m_hi;
+
+        r_interval(rational lo, rational hi)
+            : m_lo(std::move(lo)), m_hi(std::move(hi))
+        {}
+
+    public:
+
+        static r_interval empty() {
+            return {rational::zero(), rational::zero()};
+        }
+
+        static r_interval full() {
+            return {rational(-1), rational::zero()};
+        }
+
+        static r_interval proper(rational lo, rational hi) {
+            SASSERT(0 <= lo);
+            SASSERT(0 <= hi);
+            return {std::move(lo), std::move(hi)};
+        }
+
+        bool is_full() const { return m_lo.is_neg(); }
+        bool is_proper() const { return !is_full(); }
+        bool is_empty() const { return is_proper() && lo() == hi(); }
+        rational const& lo() const { SASSERT(is_proper()); return m_lo; }
+        rational const& hi() const { SASSERT(is_proper()); return m_hi; }
+
+        // this one also supports representing full intervals as [lo;mod_value[
+        static rational len(rational const& lo, rational const& hi, rational const& mod_value) {
+            SASSERT(mod_value.is_power_of_two());
+            SASSERT(0 <= lo && lo < mod_value);
+            SASSERT(0 <= hi && hi <= mod_value);
+            SASSERT(hi != mod_value || lo == 0);  // hi == mod_value only allowed when lo == 0
+            rational len = hi - lo;
+            if (len.is_neg())
+                len += mod_value;
+            return len;
+        }
+
+        rational len(rational const& mod_value) const {
+            SASSERT(is_proper());
+            return len(lo(), hi(), mod_value);
+        }
+
+        // deals only with proper intervals
+        // but works with full intervals represented as [0;mod_value[  -- maybe we should just change representation of full intervals to this always
+        static bool contains(rational const& lo, rational const& hi, rational const& val) {
+            if (lo <= hi)
+                return lo <= val && val < hi;
+            else
+                return val < hi || val >= lo;
+        }
+
+        bool contains(rational const& val) const {
+            if (is_full())
+                return true;
+            else
+                return contains(lo(), hi(), val);
+        }
+
+    };
+
+    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) {
+            SASSERT(0 <= lo_val && lo_val <= lo.manager().max_value());
+            SASSERT(0 <= hi_val && hi_val <= hi.manager().max_value());
+            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(), lo().manager().two_to_N());
+        }
+
+        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();
+        }
+
+        bool currently_contains(eval_interval const& other) const {
+            if (is_full())
+                return true;
+            if (other.is_full())
+                return false;
+            // lo <= lo' <= hi' <= hi'
+            if (lo_val() <= other.lo_val() && other.lo_val() <= other.hi_val() && other.hi_val() <= hi_val())
+                return true;
+            if (lo_val() <= hi_val())
+                return false;
+            // hi < lo <= lo' <= hi'
+            if (lo_val() <= other.lo_val() && other.lo_val() <= other.hi_val())
+                return true;
+            // lo' <= hi' <= hi < lo
+            if (other.lo_val() <= other.hi_val() && other.hi_val() <= hi_val())
+                return true;
+            // hi' <= hi < lo <= lo'
+            if (other.hi_val() <= hi_val() && lo_val() <= other.lo_val())
+                return true;
+            return false;
+        }
+
+    };  // class eval_interval
+
+    inline std::ostream& operator<<(std::ostream& os, eval_interval const& i) {
+        if (i.is_full())
+            return os << "full";
+        else {
+            auto& m = i.hi().manager();
+            return os << i.symbolic() << " := [" << m.normalize(i.lo_val()) << ";" << m.normalize(i.hi_val()) << "[";
+        }
+    }
+
+}
diff --git a/src/sat/smt/polysat/polysat_types.h b/src/sat/smt/polysat/polysat_types.h
new file mode 100644
index 000000000..e77e755bf
--- /dev/null
+++ b/src/sat/smt/polysat/polysat_types.h
@@ -0,0 +1,67 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-06
+
+--*/
+#pragma once
+
+#include <variant>
+#include "math/dd/dd_pdd.h"
+#include "util/trail.h"
+#include "util/sat_literal.h"
+
+namespace polysat {
+
+    using pdd = dd::pdd;
+    using pvar = unsigned;
+    using theory_var = unsigned;
+
+    using pvar_vector = unsigned_vector;
+    inline const pvar null_var = UINT_MAX;
+
+
+
+    class dependency {
+        std::variant<sat::literal, std::pair<theory_var, theory_var>> m_data;
+        unsigned m_level;
+    public:
+        dependency(sat::literal lit, unsigned level) : m_data(lit), m_level(level) {}
+        dependency(theory_var v1, theory_var v2, unsigned level) : m_data(std::make_pair(v1, v2)), m_level(level) {} 
+        bool is_null() const { return is_literal() && *std::get_if<sat::literal>(&m_data) == sat::null_literal; }
+        bool is_literal() const { return std::holds_alternative<sat::literal>(m_data); }
+        sat::literal literal() const { SASSERT(is_literal()); return *std::get_if<sat::literal>(&m_data); }
+        std::pair<theory_var, theory_var> eq() const { SASSERT(!is_literal()); return *std::get_if<std::pair<theory_var, theory_var>>(&m_data); }
+        unsigned level() const { return m_level; }
+    };
+
+    inline const dependency null_dependency = dependency(sat::null_literal, UINT_MAX);
+
+    inline std::ostream& operator<<(std::ostream& out, dependency d) {
+        if (d.is_null())
+            return out << "null";
+        else if (d.is_literal())
+            return out << d.literal() << "@" << d.level();
+        else
+            return out << "v" << d.eq().first << " == v" << d.eq().second << "@" << d.level();
+    }
+
+    using dependency_vector = vector<dependency>;
+
+    class signed_constraint;
+
+    class solver_interface {
+    public:
+        virtual void add_eq_literal(pvar v, rational const& val) = 0;
+        virtual void set_conflict(dependency_vector const& core) = 0;
+        virtual void set_lemma(vector<signed_constraint> const& lemma, unsigned level, dependency_vector const& core) = 0;
+        virtual dependency propagate(signed_constraint sc, dependency_vector const& deps) = 0;
+        virtual void propagate(dependency const& d, bool sign, dependency_vector const& deps) = 0;
+        virtual trail_stack& trail() = 0;
+        virtual bool inconsistent() const = 0;
+    };
+
+}
diff --git a/src/sat/smt/polysat_ule.cpp b/src/sat/smt/polysat/polysat_ule.cpp
similarity index 99%
rename from src/sat/smt/polysat_ule.cpp
rename to src/sat/smt/polysat/polysat_ule.cpp
index 08448b34d..0fb01bcae 100644
--- a/src/sat/smt/polysat_ule.cpp
+++ b/src/sat/smt/polysat/polysat_ule.cpp
@@ -70,8 +70,8 @@ Useful lemmas:
 
 --*/
 
-#include "sat/smt/polysat_constraints.h"
-#include "sat/smt/polysat_ule.h"
+#include "sat/smt/polysat/polysat_constraints.h"
+#include "sat/smt/polysat/polysat_ule.h"
 
 #define LOG(_msg_) verbose_stream() << _msg_ << "\n"
 
diff --git a/src/sat/smt/polysat_ule.h b/src/sat/smt/polysat/polysat_ule.h
similarity index 94%
rename from src/sat/smt/polysat_ule.h
rename to src/sat/smt/polysat/polysat_ule.h
index 12efe506a..e21ed1029 100644
--- a/src/sat/smt/polysat_ule.h
+++ b/src/sat/smt/polysat/polysat_ule.h
@@ -12,9 +12,8 @@ Author:
 
 --*/
 #pragma once
-#include "sat/smt/polysat_ule.h"
-#include "sat/smt/polysat_assignment.h"
-#include "sat/smt/polysat_constraints.h"
+#include "sat/smt/polysat/polysat_assignment.h"
+#include "sat/smt/polysat/polysat_constraints.h"
 
 
 namespace polysat {
diff --git a/src/sat/smt/polysat_umul_ovfl.cpp b/src/sat/smt/polysat/polysat_umul_ovfl.cpp
similarity index 92%
rename from src/sat/smt/polysat_umul_ovfl.cpp
rename to src/sat/smt/polysat/polysat_umul_ovfl.cpp
index 5c448bc0a..dfe400603 100644
--- a/src/sat/smt/polysat_umul_ovfl.cpp
+++ b/src/sat/smt/polysat/polysat_umul_ovfl.cpp
@@ -10,9 +10,9 @@ Author:
     Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09
 
 --*/
-#include "sat/smt/polysat_constraints.h"
-#include "sat/smt/polysat_assignment.h"
-#include "sat/smt/polysat_umul_ovfl.h"
+#include "sat/smt/polysat/polysat_constraints.h"
+#include "sat/smt/polysat/polysat_assignment.h"
+#include "sat/smt/polysat/polysat_umul_ovfl.h"
 
 
 namespace polysat {
diff --git a/src/sat/smt/polysat_umul_ovfl.h b/src/sat/smt/polysat/polysat_umul_ovfl.h
similarity index 95%
rename from src/sat/smt/polysat_umul_ovfl.h
rename to src/sat/smt/polysat/polysat_umul_ovfl.h
index 502ed4bbf..41972ef59 100644
--- a/src/sat/smt/polysat_umul_ovfl.h
+++ b/src/sat/smt/polysat/polysat_umul_ovfl.h
@@ -11,7 +11,7 @@ Author:
 
 --*/
 #pragma once
-#include "sat/smt/polysat_constraints.h"
+#include "sat/smt/polysat/polysat_constraints.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat_viable.cpp b/src/sat/smt/polysat/polysat_viable.cpp
similarity index 99%
rename from src/sat/smt/polysat_viable.cpp
rename to src/sat/smt/polysat/polysat_viable.cpp
index d68822563..a11a02b91 100644
--- a/src/sat/smt/polysat_viable.cpp
+++ b/src/sat/smt/polysat/polysat_viable.cpp
@@ -18,8 +18,8 @@ Notes:
 
 #include "util/debug.h"
 #include "util/log.h"
-#include "sat/smt/polysat_viable.h"
-#include "sat/smt/polysat_core.h"
+#include "sat/smt/polysat/polysat_viable.h"
+#include "sat/smt/polysat/polysat_core.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat_viable.h b/src/sat/smt/polysat/polysat_viable.h
similarity index 97%
rename from src/sat/smt/polysat_viable.h
rename to src/sat/smt/polysat/polysat_viable.h
index f1c826d10..79fcfa76e 100644
--- a/src/sat/smt/polysat_viable.h
+++ b/src/sat/smt/polysat/polysat_viable.h
@@ -21,8 +21,8 @@ Author:
 #include "util/map.h"
 #include "util/small_object_allocator.h"
 
-#include "sat/smt/polysat_types.h"
-#include "sat/smt/polysat_fi.h"
+#include "sat/smt/polysat/polysat_types.h"
+#include "sat/smt/polysat/polysat_fi.h"
 
 namespace polysat {
 
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index 3e01ff391..9e57b8cae 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -27,8 +27,8 @@ The result of polysat::core::check is one of:
 #include "ast/euf/euf_bv_plugin.h"
 #include "sat/smt/polysat_solver.h"
 #include "sat/smt/euf_solver.h"
-#include "sat/smt/polysat_ule.h"
-#include "sat/smt/polysat_umul_ovfl.h"
+#include "sat/smt/polysat/polysat_ule.h"
+#include "sat/smt/polysat/polysat_umul_ovfl.h"
 
 
 namespace polysat {
@@ -82,7 +82,7 @@ namespace polysat {
                 core.push_back(d.literal());
             }
             else {
-                auto const [v1, v2] = m_var_eqs[d.index()];
+                auto const [v1, v2] = d.eq();
                 euf::enode* const n1 = var2enode(v1);
                 euf::enode* const n2 = var2enode(v2);
                 VERIFY(n1->get_root() == n2->get_root());
@@ -151,7 +151,7 @@ namespace polysat {
         auto sc = m_core.eq(p, q);        
         m_var_eqs.setx(m_var_eqs_head, {v1, v2}, {v1, v2});
         ctx.push(value_trail<unsigned>(m_var_eqs_head));    
-        auto d = dependency(m_var_eqs_head, s().scope_lvl());
+        auto d = dependency(v1, v2, s().scope_lvl());
         unsigned index = m_core.register_constraint(sc, d);
         m_core.assign_eh(index, false, d); 
         m_var_eqs_head++;
@@ -192,7 +192,7 @@ namespace polysat {
             ctx.propagate(lit, ex);
         }
         else if (sign) {  
-            auto const [v1, v2] = m_var_eqs[d.index()];
+            auto const [v1, v2] = d.eq();
             // equalities are always asserted so a negative propagation is a conflict.
             auto n1 = var2enode(v1);
             auto n2 = var2enode(v2);
@@ -202,6 +202,14 @@ namespace polysat {
         }
     }
 
+    bool solver::inconsistent() const {
+        return s().inconsistent();
+    }
+
+    trail_stack& solver::trail() {
+        return ctx.get_trail_stack();
+    }
+
     void solver::add_lemma(vector<signed_constraint> const& lemma) {
         sat::literal_vector lits;
         for (auto sc : lemma)
diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h
index 76923f88f..8489619da 100644
--- a/src/sat/smt/polysat_solver.h
+++ b/src/sat/smt/polysat_solver.h
@@ -18,7 +18,7 @@ Author:
 
 #include "sat/smt/sat_th.h"
 #include "math/dd/dd_pdd.h"
-#include "sat/smt/polysat_core.h"
+#include "sat/smt/polysat/polysat_core.h"
 
 namespace euf {
     class solver;
@@ -27,7 +27,7 @@ namespace euf {
 namespace polysat {
 
 
-    class solver : public euf::th_euf_solver {
+    class solver : public euf::th_euf_solver, public solver_interface {
         typedef euf::theory_var theory_var;
         typedef euf::theory_id theory_id;
         typedef sat::literal literal;
@@ -53,8 +53,6 @@ namespace polysat {
             expr* get_hint(euf::solver& s) const override { return nullptr; }
         };
 
-        friend class core;
-
         bv_util                  bv;
         arith_util               m_autil;
         stats                    m_stats;
@@ -128,12 +126,14 @@ namespace polysat {
         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);
-        dependency propagate(signed_constraint sc, dependency_vector const& deps);
-        void propagate(dependency const& d, bool sign, dependency_vector const& deps);
-        
+        void add_eq_literal(pvar v, rational const& val) override;
+        void set_conflict(dependency_vector const& core) override;
+        void set_lemma(vector<signed_constraint> const& lemma, unsigned level, dependency_vector const& core) override;
+        dependency propagate(signed_constraint sc, dependency_vector const& deps) override;
+        void propagate(dependency const& d, bool sign, dependency_vector const& deps) override;
+        trail_stack& trail() override;
+        bool inconsistent() const override;
+
         void add_lemma(vector<signed_constraint> const& lemma);
 
         std::pair<sat::literal_vector, euf::enode_pair_vector> explain_deps(dependency_vector const& deps);
diff --git a/src/sat/smt/polysat_types.h b/src/sat/smt/polysat_types.h
deleted file mode 100644
index c8c8324d7..000000000
--- a/src/sat/smt/polysat_types.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/*++
-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"
-
-namespace polysat {
-
-    using pdd = dd::pdd;
-    using pvar = unsigned;
-
-    using pvar_vector = unsigned_vector;
-    inline const pvar null_var = UINT_MAX;
-
-
-    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_null() const { return m_level == UINT_MAX; }
-        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; }
-    };
-
-    inline const dependency null_dependency = dependency(0, UINT_MAX);
-
-    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>;
-
-}