diff --git a/src/params/sat_params.pyg b/src/params/sat_params.pyg
index d45b4c0bf..2c76b89c4 100644
--- a/src/params/sat_params.pyg
+++ b/src/params/sat_params.pyg
@@ -75,15 +75,6 @@ def_module_params('sat',
 	                      ('anf', BOOL, False, 'enable ANF based simplification in-processing'),
 	                      ('anf.delay', UINT, 2, 'delay ANF simplification by in-processing round'),
                           ('anf.exlin', BOOL, False, 'enable extended linear simplification'), 
-		                  ('cut', BOOL, False, 'enable AIG based simplification in-processing'),
-	                      ('cut.delay', UINT, 2, 'delay cut simplification by in-processing round'),
-                          ('cut.aig',   BOOL, False, 'extract aigs (and ites) from cluases for cut simplification'),
-                          ('cut.lut',   BOOL, False, 'extract luts from clauses for cut simplification'),
-                          ('cut.xor',   BOOL, False, 'extract xors from clauses for cut simplification'),
-                          ('cut.npn3',  BOOL, False, 'extract 3 input functions from clauses for cut simplification'),
-                          ('cut.dont_cares', BOOL, True, 'integrate dont cares with cuts'),
-                          ('cut.redundancies', BOOL, True, 'integrate redundancy checking of cuts'),
-                          ('cut.force', BOOL, False, 'force redoing cut-enumeration until a fixed-point'),
                           ('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),
                           # - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth.
                           #          So if the value is 10, at most 1024 cubes will be generated of length 10.
diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt
index 9d1d8dd7e..e85513e49 100644
--- a/src/sat/CMakeLists.txt
+++ b/src/sat/CMakeLists.txt
@@ -1,7 +1,6 @@
 z3_add_component(sat
   SOURCES
     dimacs.cpp
-    sat_aig_cuts.cpp
     sat_aig_finder.cpp
     sat_anf_simplifier.cpp
     sat_asymm_branch.cpp
@@ -12,8 +11,6 @@ z3_add_component(sat
     sat_clause_use_list.cpp
     sat_cleaner.cpp
     sat_config.cpp
-    sat_cut_simplifier.cpp
-    sat_cutset.cpp
     sat_ddfw_wrapper.cpp    
     sat_drat.cpp
     sat_elim_eqs.cpp
@@ -21,7 +18,6 @@ z3_add_component(sat
     sat_integrity_checker.cpp
     sat_local_search.cpp
     sat_lookahead.cpp
-    sat_lut_finder.cpp
     sat_model_converter.cpp
     sat_mus.cpp
     sat_npn3_finder.cpp
diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp
deleted file mode 100644
index 8fd98bc9e..000000000
--- a/src/sat/sat_aig_cuts.cpp
+++ /dev/null
@@ -1,886 +0,0 @@
-/*++
-  Copyright (c) 2020 Microsoft Corporation
-
-  Module Name:
-
-   sat_aig_cuts.cpp
-
-  Abstract:
-   
-    Perform cut-set enumeration to identify equivalences.
-
-  Author:
-
-    Nikolaj Bjorner 2020-01-02
-
-  --*/
-
-#include "util/trace.h"
-#include "sat/sat_aig_cuts.h"
-#include "sat/sat_solver.h"
-#include "sat/sat_lut_finder.h"
-
-namespace sat {
-        
-    aig_cuts::aig_cuts() {
-        m_cut_set1.init(m_region, m_config.m_max_cutset_size + 1, UINT_MAX);
-        m_cut_set2.init(m_region, m_config.m_max_cutset_size + 1, UINT_MAX);
-        m_empty_cuts.init(m_region, m_config.m_max_cutset_size + 1, UINT_MAX);
-        m_num_cut_calls = 0;
-        m_num_cuts = 0;
-    }
-
-    vector<cut_set> const& aig_cuts::operator()() {
-        if (m_config.m_full) flush_roots();
-        unsigned_vector node_ids = filter_valid_nodes();
-        TRACE(cut_simplifier, display(tout););
-        augment(node_ids);
-        TRACE(cut_simplifier, display(tout););
-        ++m_num_cut_calls;
-        return m_cuts;
-    }
-
-    void aig_cuts::augment(unsigned_vector const& ids) {
-        for (unsigned id : ids) {
-            if (m_aig[id].empty()) {
-                continue;
-            }
-            IF_VERBOSE(20, m_cuts[id].display(verbose_stream() << "augment " << id << "\nbefore\n"));
-            for (node const& n : m_aig[id]) {
-                augment(id, n);
-            }
-
-#if 0
-            // augment cuts directly       
-            m_cut_save.reset();
-            cut_set& cs = m_cuts[id];
-            for (cut const& c : cs) {
-                if (c.size() > 1) m_cut_save.push_back(c);
-            }
-            for (cut const& c : m_cut_save) {
-                lut lut(*this, c);
-                augment_lut(id, lut, cs);
-            }
-#endif
-            IF_VERBOSE(20, m_cuts[id].display(verbose_stream() << "after\n"));            
-        }
-    }
-
-    void aig_cuts::augment(unsigned id, node const& n) {
-        unsigned nc = n.size();
-        m_insertions = 0;
-        cut_set& cs = m_cuts[id];
-        if (!is_touched(id, n)) {
-            // no-op
-        }
-        else if (n.is_var()) {
-            SASSERT(!n.sign());
-        }
-        else if (n.is_lut()) {
-            lut lut(*this, n);
-            augment_lut(id, lut, cs);
-        }
-        else if (n.is_ite()) {
-            augment_ite(id, n, cs);
-        }
-        else if (nc == 0) { 
-            augment_aig0(id, n, cs);
-        }
-        else if (nc == 1) {
-            augment_aig1(id, n, cs);
-        }
-        else if (nc == 2) {
-            augment_aig2(id, n, cs);
-        }
-        else if (nc <= cut::max_cut_size()) {
-            augment_aigN(id, n, cs);
-        }
-        if (m_insertions > 0) {
-            touch(id);
-        }
-    }
-
-    bool aig_cuts::insert_cut(unsigned v, cut const& c, cut_set& cs) {
-        if (!cs.insert(m_on_cut_add, m_on_cut_del, c)) {
-            return true;
-        }
-        m_num_cuts++;
-        if (++m_insertions > max_cutset_size(v)) {
-            return false;
-        }
-        while (cs.size() >= max_cutset_size(v)) {
-            // never evict the first entry, it is used for the starting point
-            unsigned idx = 1 + (m_rand() % (cs.size() - 1));
-            evict(cs, idx);
-        }
-        return true;
-    }
-
-    void aig_cuts::augment_lut(unsigned v, lut const& n, cut_set& cs) {
-        IF_VERBOSE(4, n.display(verbose_stream() << "augment_lut " << v << " ") << "\n");
-        literal l1 = n.child(0);
-        VERIFY(&cs != &lit2cuts(l1));
-        for (auto const& a : lit2cuts(l1)) {
-            m_tables[0] = &a;
-            m_lits[0] = l1;
-            cut b(a);
-            augment_lut_rec(v, n, b, 1, cs);                        
-        }
-    }
-
-    void aig_cuts::augment_lut_rec(unsigned v, lut const& n, cut& a, unsigned idx, cut_set& cs) {
-        if (idx < n.size()) {
-            literal lit = n.child(idx); 
-            VERIFY(&cs != &lit2cuts(lit));
-            for (auto const& b : lit2cuts(lit)) {
-                cut ab;
-                if (!ab.merge(a, b)) continue;
-                m_tables[idx] = &b;
-                m_lits[idx] = lit;
-                augment_lut_rec(v, n, ab, idx + 1, cs);                
-            }
-            return;
-        }
-        for (unsigned i = n.size(); i-- > 0; ) { 
-            m_luts[i] = m_tables[i]->shift_table(a);            
-        }
-        uint64_t r = 0;
-        SASSERT(a.size() <= 6);
-        SASSERT(n.size() <= 6);
-        for (unsigned j = (1u << a.size()); j-- > 0; ) {
-            unsigned w = 0;
-            // when computing the output at position j, 
-            // the i'th bit to index into n.lut() is 
-            // based on the j'th output bit in lut[i]
-            // m_lits[i].sign() tracks if output bit is negated
-            for (unsigned i = n.size(); i-- > 0; ) {
-                w |= (((m_luts[i] >> j) ^ (uint64_t)m_lits[i].sign()) & 1u) << i;
-            }
-            r |= ((n.table() >> w) & 1u) << j;
-        } 
-        a.set_table(r);
-        IF_VERBOSE(8,
-            verbose_stream() << "lut: " << v << " - " << a << "\n";
-            for (unsigned i = 0; i < n.size(); ++i) {
-                verbose_stream() << m_lits[i] << ": " << *m_tables[i] << "\n";
-            });
-        insert_cut(v, a, cs);
-    }  
-
-    void aig_cuts::augment_ite(unsigned v, node const& n, cut_set& cs) {
-        IF_VERBOSE(4, display(verbose_stream() << "augment_ite " << v << " ", n) << "\n");
-        literal l1 = child(n, 0);
-        literal l2 = child(n, 1);
-        literal l3 = child(n, 2);
-        VERIFY(&cs != &lit2cuts(l1)); 
-        VERIFY(&cs != &lit2cuts(l2));  
-        VERIFY(&cs != &lit2cuts(l3));  
-        for (auto const& a : lit2cuts(l1)) {
-            for (auto const& b : lit2cuts(l2)) {
-                cut ab;
-                if (!ab.merge(a, b)) continue;                
-                for (auto const& c : lit2cuts(l3)) {
-                    cut abc;
-                    if (!abc.merge(ab, c)) continue;                    
-                    uint64_t t1 = a.shift_table(abc);
-                    uint64_t t2 = b.shift_table(abc);
-                    uint64_t t3 = c.shift_table(abc);
-                    if (l1.sign()) t1 = ~t1;
-                    if (l2.sign()) t2 = ~t2;
-                    if (l3.sign()) t3 = ~t3;
-                    abc.set_table((t1 & t2) | ((~t1) & t3));
-                    if (n.sign()) abc.negate();
-                    if (!insert_cut(v, abc, cs)) return;
-                } 
-            }
-        }
-    }
-
-    void aig_cuts::augment_aig0(unsigned v, node const& n, cut_set& cs) {
-        IF_VERBOSE(4, display(verbose_stream() << "augment_unit " << v << " ", n) << "\n");
-        SASSERT(n.is_and() && n.size() == 0);
-        reset(cs);
-        cut c;
-        c.set_table(n.sign() ? 0x0 : 0x1);
-        push_back(cs, c);
-    }
-
-    void aig_cuts::augment_aig1(unsigned v, node const& n, cut_set& cs) {
-        IF_VERBOSE(4, display(verbose_stream() << "augment_aig1 " << v << " ", n) << "\n");
-        SASSERT(n.is_and());
-        literal lit = child(n, 0);
-        VERIFY(&cs != &lit2cuts(lit));
-        for (auto const& a : lit2cuts(lit)) {
-            cut c(a);
-            if (n.sign()) c.negate();
-            if (!insert_cut(v, c, cs)) return;             
-        }
-    }
-
-    void aig_cuts::augment_aig2(unsigned v, node const& n, cut_set& cs) {
-        IF_VERBOSE(4, display(verbose_stream() << "augment_aig2 " << v << " ", n) << "\n");
-        SASSERT(n.is_and() || n.is_xor());
-        literal l1 = child(n, 0);
-        literal l2 = child(n, 1);
-        VERIFY(&cs != &lit2cuts(l1));
-        VERIFY(&cs != &lit2cuts(l2));
-        for (auto const& a : lit2cuts(l1)) {
-            for (auto const& b : lit2cuts(l2)) {
-                cut c;            
-                if (!c.merge(a, b)) continue;                
-                uint64_t t1 = a.shift_table(c);
-                uint64_t t2 = b.shift_table(c);
-                if (l1.sign()) t1 = ~t1;
-                if (l2.sign()) t2 = ~t2;
-                uint64_t t3 = n.is_and() ? (t1 & t2) : (t1 ^ t2);
-                c.set_table(t3);
-                if (n.sign()) c.negate();
-                // validate_aig2(a, b, v, n, c); 
-                if (!insert_cut(v, c, cs)) return;                
-            }
-        }
-    }
-
-    void aig_cuts::augment_aigN(unsigned v, node const& n, cut_set& cs) {
-        IF_VERBOSE(4, display(verbose_stream() << "augment_aigN " << v << " ", n) << "\n");
-        m_cut_set1.reset(m_on_cut_del);
-        SASSERT(n.is_and() || n.is_xor());
-        literal lit = child(n, 0);
-        for (auto const& a : lit2cuts(lit)) {
-            cut b(a);
-            if (lit.sign()) {
-                b.negate();
-            }            
-            m_cut_set1.push_back(m_on_cut_add, b);
-        }
-        for (unsigned i = 1; i < n.size(); ++i) {
-            m_cut_set2.reset(m_on_cut_del);
-            lit = child(n, i);
-            m_insertions = 0;
-            for (auto const& a : m_cut_set1) {
-                for (auto const& b : lit2cuts(lit)) {
-                    cut c;
-                    if (!c.merge(a, b)) continue;
-                    uint64_t t1 = a.shift_table(c);
-                    uint64_t t2 = b.shift_table(c);
-                    if (lit.sign()) t2 = ~t2;
-                    uint64_t t3 = n.is_and() ? (t1 & t2) : (t1 ^ t2);
-                    c.set_table(t3);
-                    if (i + 1 == n.size() && n.sign()) c.negate();
-                    if (!insert_cut(UINT_MAX, c, m_cut_set2)) goto next_child;                    
-                }
-            }
-        next_child:
-            m_cut_set1.swap(m_cut_set2);
-        }
-        m_insertions = 0;
-        for (auto & cut : m_cut_set1) {
-            // validate_aigN(v, n, cut);
-            if (!insert_cut(v, cut, cs)) {
-                break;
-            }
-        }        
-    }
-
-    bool aig_cuts::is_touched(bool_var v, node const& n) {
-        for (unsigned i = 0; i < n.size(); ++i) {
-            literal lit = m_literals[n.offset() + i];
-            if (is_touched(lit)) {
-                return true;
-            }
-        }
-        return is_touched(v);
-    }
-
-    void aig_cuts::reserve(unsigned v) {
-        m_aig.reserve(v + 1);
-        m_cuts.reserve(v + 1);
-        m_max_cutset_size.reserve(v + 1, m_config.m_max_cutset_size);
-        m_last_touched.reserve(v + 1, 0);
-    }
-
-    void aig_cuts::add_var(unsigned v) {
-        reserve(v);
-        if (m_aig[v].empty()) {
-            m_aig[v].push_back(node(v));
-            init_cut_set(v);
-            touch(v);
-        }
-    }
-
-    void aig_cuts::add_node(bool_var v, node const& n) {
-        for (unsigned i = 0; i < n.size(); ++i) {
-            reserve(m_literals[i].var());
-            if (m_aig[m_literals[i].var()].empty()) {
-                add_var(m_literals[i].var());
-            }
-        }
-        if (m_aig[v].empty() || n.is_const()) {
-            m_aig[v].reset();
-            m_aig[v].push_back(n); 
-            on_node_add(v, n);            
-            init_cut_set(v);
-            if (n.is_const()) {
-                augment_aig0(v, n, m_cuts[v]);
-            }
-            touch(v);
-            IF_VERBOSE(12, display(verbose_stream() << "add " << v << " == ", n) << "\n");            
-        }
-        else if (m_aig[v][0].is_const() || !insert_aux(v, n)) {
-            m_literals.shrink(m_literals.size() - n.size());
-            TRACE(cut_simplifier, tout << "duplicate\n";);
-        }
-        SASSERT(!m_aig[v].empty());
-    }
-
-    void aig_cuts::add_node(bool_var v, uint64_t lut, unsigned sz, bool_var const* args) {
-        TRACE(cut_simplifier, tout << v << " == " << cut::table2string(sz, lut) << " " << bool_var_vector(sz, args) << "\n";);
-        reserve(v);
-        unsigned offset = m_literals.size();
-        node n(lut, sz, offset);
-        for (unsigned i = 0; i < sz; ++i) {
-            reserve(args[i]);
-            m_literals.push_back(literal(args[i], false));
-        }
-        add_node(v, n);
-    }
-
-    void aig_cuts::add_node(literal head, bool_op op, unsigned sz, literal const* args) {
-        TRACE(cut_simplifier, tout << head << " == " << op << " " << literal_vector(sz, args) << "\n";);
-        unsigned v = head.var();
-        reserve(v);
-        unsigned offset = m_literals.size();
-        node n(head.sign(), op, sz, offset);
-        m_literals.append(sz, args);
-        for (unsigned i = 0; i < sz; ++i) reserve(args[i].var());
-        if (op == and_op || op == xor_op) {
-            std::sort(m_literals.data() + offset, m_literals.data() + offset + sz);
-        }
-        add_node(v, n);
-    }
-
-    void aig_cuts::add_cut(bool_var v, uint64_t lut, bool_var_vector const& args) {
-        // args can be assumed to be sorted
-        DEBUG_CODE(for (unsigned i = 0; i + 1 < args.size(); ++i) VERIFY(args[i] < args[i+1]););
-        add_var(v);
-        for (bool_var w : args) add_var(w); 
-        cut c;
-        for (bool_var w : args) VERIFY(c.add(w));
-        c.set_table(lut);
-        insert_cut(v, c, m_cuts[v]);
-    }
-
-
-    void aig_cuts::set_root(bool_var v, literal r) {
-        IF_VERBOSE(10, verbose_stream() << "set-root " << v << " -> " << r << "\n");
-        m_roots.push_back(std::make_pair(v, r));
-    }
-
-    void aig_cuts::flush_roots() {
-        if (m_roots.empty()) return;
-        to_root to_root;
-        for (unsigned i = m_roots.size(); i-- > 0; ) {
-            bool_var v = m_roots[i].first;
-            literal  r = m_roots[i].second;
-            reserve(v);
-            reserve(r.var());
-            literal rr = to_root[r.var()];
-            to_root[v] = r.sign() ? ~rr : rr;
-        }
-        for (unsigned i = 0; i < m_aig.size(); ++i) {
-            // invalidate nodes that have been rooted
-            if (to_root[i] != literal(i, false)) {
-                m_aig[i].reset();
-                reset(m_cuts[i]);
-            }
-            else {
-                unsigned j = 0;
-                for (node & n : m_aig[i]) {
-                    if (flush_roots(i, to_root, n)) {
-                        m_aig[i][j++] = n;
-                    }
-                }
-                m_aig[i].shrink(j);
-            }
-        }
-        for (cut_set& cs : m_cuts) {
-            flush_roots(to_root, cs);
-        }
-        m_roots.reset();
-        TRACE(cut_simplifier, display(tout););
-    }
-
-    bool aig_cuts::flush_roots(bool_var var, to_root const& to_root, node& n) {
-        bool changed = false;
-        for (unsigned i = 0; i < n.size(); ++i) {
-            literal& lit = m_literals[n.offset() + i];
-            literal r = to_root[lit.var()];
-            if (r != lit) {
-                changed = true;
-                lit = lit.sign() ? ~r : r;
-            }
-            if (lit.var() == var) {
-                return false;
-            }
-        }
-        if (changed && (n.is_and() || n.is_xor())) {
-            std::sort(m_literals.data() + n.offset(), m_literals.data() + n.offset() + n.size());
-        }
-        return true;
-    }
-
-    void aig_cuts::flush_roots(to_root const& to_root, cut_set& cs) {
-        for (unsigned j = 0; j < cs.size(); ++j) {
-            for (unsigned v : cs[j]) {
-                if (to_root[v] != literal(v, false)) {
-                    evict(cs, j--);
-                    break;
-                }
-            }
-        }
-    }
-
-    lbool aig_cuts::get_value(bool_var v) const {
-        return (m_aig[v].size() == 1 && m_aig[v][0].is_const()) ? 
-            (m_aig[v][0].sign() ? l_false : l_true) : 
-            l_undef;
-    }
-
-    void aig_cuts::init_cut_set(unsigned id) {
-        SASSERT(m_aig[id].size() == 1);
-        SASSERT(m_aig[id][0].is_valid());
-        auto& cut_set = m_cuts[id];
-        reset(cut_set);
-        cut_set.init(m_region, m_config.m_max_cutset_size + 1, id);
-        push_back(cut_set, cut(id));
-    }
-
-    bool aig_cuts::eq(node const& a, node const& b) {
-        if (a.is_valid() != b.is_valid()) return false;
-        if (!a.is_valid()) return true;
-        if (a.op() != b.op() || a.sign() != b.sign() || a.size() != b.size()) 
-            return false;
-        for (unsigned i = a.size(); i-- > 0; ) {
-            if (m_literals[a.offset() + i] != m_literals[b.offset() + i]) 
-                return false;
-        }
-        return true;
-    }
-
-    bool aig_cuts::similar(node const& a, node const& b) {
-        bool sim = true;
-        sim = a.is_lut() && !b.is_lut() && a.size() == b.size();
-        for (unsigned i = a.size(); sim && i-- > 0; ) {
-            sim = m_literals[a.offset() + i].var() == m_literals[b.offset() + i].var();
-        }
-        return sim;
-    }
-
-    bool aig_cuts::insert_aux(unsigned v, node const& n) {
-        if (!m_config.m_full) return false;
-        unsigned num_gt = 0, num_eq = 0;
-        for (node const& n2 : m_aig[v]) {
-            if (eq(n, n2) || similar(n, n2)) return false;
-            else if (n.size() < n2.size()) num_gt++;
-            else if (n.size() == n2.size()) num_eq++;
-        }
-        if (m_aig[v].size() < m_config.m_max_aux) {
-            on_node_add(v, n);
-            m_aig[v].push_back(n);
-            touch(v);
-            return true;
-        }
-        if (num_gt > 0) {
-            unsigned idx = rand() % num_gt;
-            for (node const& n2 : m_aig[v]) {
-                if (n.size() < n2.size()) {
-                    if (idx == 0) {
-                        on_node_del(v, m_aig[v][idx]);
-                        on_node_add(v, n);
-                        m_aig[v][idx] = n;
-                        touch(v);
-                        return true;
-                    }
-                    --idx;
-                }
-            }
-        }
-        if (num_eq > 0) {
-            unsigned idx = rand() % num_eq;
-            for (node const& n2 : m_aig[v]) {
-                if (n.size() == n2.size()) {
-                    if (idx == 0) {
-                        on_node_del(v, m_aig[v][idx]);
-                        on_node_add(v, n);
-                        m_aig[v][idx] = n;
-                        touch(v);
-                        return true;
-                    }
-                    --idx;
-                }
-            }
-        }
-        return false;
-    }
-
-    unsigned_vector aig_cuts::filter_valid_nodes() const {
-        unsigned id = 0;
-        unsigned_vector result;
-        for (auto& v : m_aig) {
-            if (!v.empty()) result.push_back(id);
-            ++id;
-        }
-        return result;
-    }
-
-    cut_val aig_cuts::eval(node const& n, cut_eval const& env) const {
-        uint64_t result = 0;
-        switch (n.op()) {
-        case var_op:
-            UNREACHABLE();
-            break;
-        case and_op:
-            result = ~0ull;
-            for (unsigned i = 0; i < n.size(); ++i) {
-                literal u = m_literals[n.offset() + i];
-                uint64_t uv = u.sign() ? env[u.var()].m_f : env[u.var()].m_t;
-                result &= uv;
-            }
-            break;
-        case xor_op: 
-            result = 0ull;
-            for (unsigned i = 0; i < n.size(); ++i) {
-                literal u = m_literals[n.offset() + i];
-                uint64_t uv = u.sign() ? env[u.var()].m_f : env[u.var()].m_t;
-                result ^= uv;
-            }
-            break;
-        case ite_op: {
-            literal u = m_literals[n.offset() + 0]; 
-            literal v = m_literals[n.offset() + 1]; 
-            literal w = m_literals[n.offset() + 2]; 
-            uint64_t uv = u.sign() ? env[u.var()].m_f : env[u.var()].m_t;
-            uint64_t vv = v.sign() ? env[v.var()].m_f : env[v.var()].m_t;
-            uint64_t wv = w.sign() ? env[w.var()].m_f : env[w.var()].m_t;
-            result = (uv & vv) | ((~uv) & wv);
-            break;
-        }
-        default:
-            UNREACHABLE();
-        }
-        if (n.sign()) result = ~result;
-        return cut_val(result, ~result);
-    }
-    
-    cut_eval aig_cuts::simulate(unsigned num_rounds) {
-        cut_eval result;
-        for (unsigned i = 0; i < m_cuts.size(); ++i) {
-            uint64_t r = 
-                (uint64_t)m_rand() + ((uint64_t)m_rand() << 16ull) + 
-                ((uint64_t)m_rand() << 32ull) + ((uint64_t)m_rand() << 48ull);
-            result.push_back(cut_val(r, ~r));
-        }
-        for (unsigned i = 0; i < num_rounds; ++i) {
-            for (unsigned j = 0; j < m_cuts.size(); ++j) {
-                cut_set const& cs = m_cuts[j];
-                if (cs.size() <= 1) {
-                    if (!m_aig[j].empty() && !m_aig[j][0].is_var()) {
-                        result[j] = eval(m_aig[j][0], result);
-                    }
-                }
-                else if (cs.size() > 1) {
-                    cut const& c = cs[1 + (m_rand() % (cs.size() - 1))];
-                    result[j] = c.eval(result);
-                }
-            }
-        }
-        return result;
-    }
-
-
-    void aig_cuts::on_node_add(unsigned v, node const& n) {
-        if (m_on_clause_add) {
-            node2def(m_on_clause_add, n, literal(v, false));
-        }
-    }
-
-    void aig_cuts::on_node_del(unsigned v, node const& n) {
-        if (m_on_clause_del) {
-            node2def(m_on_clause_del, n, literal(v, false));        
-        }
-    }
-
-    void aig_cuts::set_on_clause_add(on_clause_t& on_clause_add) {
-        m_on_clause_add = on_clause_add;
-        std::function<void(unsigned v, cut const& c)> _on_cut_add = 
-            [this](unsigned v, cut const& c) { cut2def(m_on_clause_add, c, literal(v, false)); };
-        m_on_cut_add = _on_cut_add;
-    }
-
-    void aig_cuts::set_on_clause_del(on_clause_t& on_clause_del) {
-        m_on_clause_del = on_clause_del;
-        std::function<void(unsigned v, cut const& c)> _on_cut_del = 
-            [this](unsigned v, cut const& c) { cut2def(m_on_clause_del, c, literal(v, false)); };
-        m_on_cut_del = _on_cut_del;
-    }
-
-    /**
-     * Encode the cut (variables and truth-table) in a set of clauses.
-     * r is the result.
-     */
-
-    void aig_cuts::cut2def(on_clause_t& on_clause, cut const& c, literal r) {
-        IF_VERBOSE(10, verbose_stream() << "cut2def: " << r << " == " << c << "\n");
-        VERIFY(r != null_literal);
-        unsigned sz = c.size();
-        unsigned num_assigns = 1 << sz;
-        for (unsigned i = 0; i < num_assigns; ++i) {
-            m_clause.reset();
-            for (unsigned j = 0; j < sz; ++j) {
-                literal lit(c[j], 0 != (i & (1ull << j)));
-                m_clause.push_back(lit);                
-            }
-            literal rr = r;
-            if (0 == (c.table() & (1ull << i))) rr.neg();
-            m_clause.push_back(rr);
-            on_clause(m_clause);
-        }
-    }
-
-    void aig_cuts::node2def(on_clause_t& on_clause, node const& n, literal r) {
-        IF_VERBOSE(10, display(verbose_stream() << "node2def " << r << " == ", n) << "\n");
-        SASSERT(on_clause);
-        literal c, t, e;
-        if (n.sign()) r.neg();
-        m_clause.reset();
-        unsigned num_comb = 0;
-        switch (n.op()) {
-        case var_op:
-            return;
-        case and_op:
-            for (unsigned i = 0; i < n.size(); ++i) {
-                m_clause.push_back(~r);
-                m_clause.push_back(m_literals[n.offset() + i]);
-                on_clause(m_clause);
-                m_clause.reset();
-            }
-            for (unsigned i = 0; i < n.size(); ++i) {
-                m_clause.push_back(~m_literals[n.offset()+i]);
-            }
-            m_clause.push_back(r);
-            on_clause(m_clause);
-            return;
-        case ite_op:
-            // r & c => t, r & ~c => e
-            // ~r & c => ~t, ~r & ~c => ~e
-            SASSERT(n.size() == 3);
-            c = m_literals[n.offset()+0];
-            t = m_literals[n.offset()+1];
-            e = m_literals[n.offset()+2];
-            m_clause.push_back(~r, ~c, t);
-            on_clause(m_clause);
-            m_clause.reset();
-            m_clause.push_back(~r, c, e);
-            on_clause(m_clause);
-            m_clause.reset();
-            m_clause.push_back(r, ~c, ~t);
-            on_clause(m_clause);
-            m_clause.reset();
-            m_clause.push_back(r, c, ~e);
-            on_clause(m_clause);
-            return;
-        case xor_op: 
-            // r = a ^ b ^ c
-            // <=>
-            // ~r ^ a ^ b ^ c = 1
-            if (n.size() > 10) {
-                throw default_exception("cannot handle large xors");
-            }
-            num_comb = (1 << n.size());
-            for (unsigned i = 0; i < num_comb; ++i) {
-                bool parity = n.size() % 2 == 1;
-                m_clause.reset();
-                for (unsigned j = 0; j < n.size(); ++j) {
-                    literal lit = m_literals[n.offset() + j];
-                    if (0 == (i & (1 << j))) {
-                        lit.neg();
-                    }
-                    else {
-                        parity ^= true;
-                    }
-                    m_clause.push_back(lit);
-                }
-                m_clause.push_back(parity ? r : ~r);
-                TRACE(cut_simplifier, tout << "validate: " << m_clause << "\n";);
-                on_clause(m_clause);
-            }
-            return;
-        case lut_op: 
-            // r = LUT(v0, v1, v2)
-            num_comb = (1 << n.size());
-            for (unsigned i = 0; i < num_comb; ++i) {
-                m_clause.reset();
-                for (unsigned j = 0; j < n.size(); ++j) {
-                    literal lit = m_literals[n.offset() + j];
-                    if (0 != (i & (1 << j))) lit.neg();
-                    m_clause.push_back(lit);
-                }
-                m_clause.push_back(0 == (n.lut() & (1ull << i)) ? ~r : r);
-                TRACE(cut_simplifier, tout << n.lut() << " " <<  m_clause << "\n";);
-                on_clause(m_clause);
-            }
-            return;
-        default:
-            UNREACHABLE();
-            break;
-        }
-    }
-
-    /**
-     * compile the truth table from c into clauses that define ~v.
-     * compile definitions for nodes until all inputs have been covered.
-     * Assume only the first definition for a node is used for all cuts.
-     */
-    void aig_cuts::cut2clauses(on_clause_t& on_clause, unsigned v, cut const& c) {
-        bool_vector visited(m_aig.size(), false);
-        for (unsigned u : c) visited[u] = true;
-        unsigned_vector todo;
-        todo.push_back(v);
-
-        while (!todo.empty()) {
-            unsigned u = todo.back();
-            todo.pop_back();
-            if (visited[u]) {
-                continue;
-            }
-            visited[u] = true;
-            node const& n = m_aig[u][0];
-            node2def(on_clause, n, literal(u, false));
-            for (unsigned i = 0; i < n.size(); ++i) {
-                todo.push_back(m_literals[n.offset()+i].var());
-            }
-        }        
-        cut2def(on_clause, c, literal(v, true));
-    }
-
-    /**
-     * simplify a set of cuts by removing don't cares.
-     */
-    void aig_cuts::simplify() {        
-        uint64_t masks[7];
-        for (unsigned i = 0; i <= 6; ++i) {
-            masks[i] = cut::effect_mask(i);
-        }
-        unsigned dont_cares = 0;
-        for (cut_set & cs : m_cuts) {
-            for (cut const& c : cs) {
-                uint64_t t = c.table();
-                for (unsigned i = 0; i < std::min(6u, c.size()); ++i) {
-                    uint64_t diff = masks[i] & (t ^ (t >> (1ull << i)));
-                    if (diff == 0ull) {
-                        cut d(c);
-                        d.remove_elem(i);
-                        cs.insert(m_on_cut_add, m_on_cut_del, d);
-                        cs.evict(m_on_cut_del, c);
-                        ++dont_cares;
-                        break;
-                    }
-                }
-            }
-        }
-        IF_VERBOSE(2, verbose_stream() << "#don't cares " << dont_cares << "\n");
-    }
-
-    struct aig_cuts::validator {
-        aig_cuts& t;
-        params_ref p;
-        reslimit lim;
-        solver s;
-        unsigned_vector vars;
-        bool_vector   is_var;
-
-        validator(aig_cuts& t):t(t),s(p, lim) {
-            p.set_bool("cut_simplifier", false);
-            s.updt_params(p);
-        }
-
-        void on_clause(literal_vector const& clause) {
-            IF_VERBOSE(20, verbose_stream() << clause << "\n");
-            for (literal lit : clause) {
-                while (lit.var() >= s.num_vars()) s.mk_var();
-                is_var.reserve(lit.var() + 1, false);
-                if (!is_var[lit.var()]) { vars.push_back(lit.var()); is_var[lit.var()] = true; }
-            }
-            s.mk_clause(clause);            
-        }
-        
-        void check() {
-            lbool r = s.check();
-            IF_VERBOSE(10, verbose_stream() << "check: " << r << "\n");
-            if (r == l_true) {
-                IF_VERBOSE(0,
-                    std::sort(vars.begin(), vars.end());
-                    s.display(verbose_stream());
-                    for (auto v : vars) verbose_stream() << v << " := " << s.get_model()[v] << "\n";
-                );
-                UNREACHABLE();
-            }
-        }
-    };
-
-    void aig_cuts::validate_aig2(cut const& a, cut const& b, unsigned v, node const& n, cut const& c) {
-        validator val(*this);
-        on_clause_t on_clause = [&](literal_vector const& clause) { val.on_clause(clause); };
-        cut2def(on_clause, a, literal(child(n, 0).var(), false));
-        cut2def(on_clause, b, literal(child(n, 1).var(), false));
-        cut2def(on_clause, c, literal(v, false));
-        node2def(on_clause, n, literal(v, true));
-        val.check();
-    } 
-
-    void aig_cuts::validate_aigN(unsigned v, node const& n, cut const& c) {
-        IF_VERBOSE(10, verbose_stream() << "validate_aigN " << v << " == " << c << "\n");
-        validator val(*this);
-        on_clause_t on_clause = [&](literal_vector const& clause) { val.on_clause(clause); };
-        for (unsigned i = 0; i < n.size(); ++i) {
-            unsigned w = m_literals[n.offset() + i].var();
-            for (cut const& d : m_cuts[w]) {
-                cut2def(on_clause, d, literal(w, false));
-            }
-        }
-        cut2def(on_clause, c, literal(v, false));
-        node2def(on_clause, n, literal(v, true));
-        val.check();
-    }  
-
-    std::ostream& aig_cuts::display(std::ostream& out) const {
-        auto ids = filter_valid_nodes();
-        for (auto id : ids) {
-            out << id << " == ";
-            bool first = true;
-            for (auto const& n : m_aig[id]) {
-                if (first) first = false; else out << "   ";
-                display(out, n) << "\n";
-            }
-            m_cuts[id].display(out);
-        }
-        return out;
-    }
-
-    std::ostream& aig_cuts::display(std::ostream& out, node const& n) const {
-        out << (n.sign() ? "! " : "  ");
-        switch (n.op()) {
-        case var_op: out << "var "; break;
-        case and_op: out << "& "; break;
-        case xor_op: out << "^ "; break;
-        case ite_op: out << "? "; break;
-        default: break;
-        }
-        for (unsigned i = 0; i < n.size(); ++i) {
-            out << m_literals[n.offset() + i] << " ";
-        }
-        return out;
-    }
-
-}
-
diff --git a/src/sat/sat_aig_cuts.h b/src/sat/sat_aig_cuts.h
deleted file mode 100644
index 9e60ce9ec..000000000
--- a/src/sat/sat_aig_cuts.h
+++ /dev/null
@@ -1,238 +0,0 @@
-/*++
-  Copyright (c) 2020 Microsoft Corporation
-
-  Module Name:
-
-   sat_aig_cuts.h
-
-  Abstract:
-   
-    Extract AIG definitions from clauses.
-    Perform cut-set enumeration to identify equivalences.
-
-    AIG extraction is incremental.
-    It can be called repeatedly.
-    Initially, a main aig node is inserted 
-    (from initial clauses or the input 
-    clausification in goal2sat).
-    Then, auxiliary AIG nodes can be inserted
-    by walking the current set of main and learned 
-    clauses. AIG nodes with fewer arguments are preferred.
-    
-    
-
-  Author:
-
-    Nikolaj Bjorner 2020-01-02
-
-  --*/
-
-#pragma once
-
-#include "sat/sat_cutset.h"
-#include "sat/sat_types.h"
-
-namespace sat {
-
-    enum bool_op {
-        var_op,
-        and_op,
-        ite_op,
-        xor_op,
-        lut_op,
-        no_op
-    };
-
-    inline std::ostream& operator<<(std::ostream& out, bool_op op) {
-        switch (op) {
-        case var_op: return out << "v";
-        case and_op: return out << "&";
-        case ite_op: return out << "?";
-        case xor_op: return out << "^";
-        case lut_op: return out << "#";
-        default: return out << "";
-        }
-    }
-
-    class aig_cuts {
-    public:
-        typedef std::function<void(literal_vector const&)> on_clause_t;
-
-        struct config {
-            unsigned m_max_cutset_size;
-            unsigned m_max_aux;
-            unsigned m_max_insertions;
-            bool     m_full;
-        config(): m_max_cutset_size(20), m_max_aux(5), m_max_insertions(20), m_full(true) {}
-        };
-    private:
-
-        // encodes one of var, and, !and, xor, !xor, ite, !ite.
-        class node {
-            bool     m_sign{ false };
-            bool_op  m_op{ no_op };
-            uint64_t m_lut{ 0 };
-            unsigned m_size{ 0 };
-            unsigned m_offset{ 0 };
-        public:
-            node(): 
-                m_sign(false), m_op(no_op), m_size(UINT_MAX), m_offset(UINT_MAX) {}
-            explicit node(unsigned v) : 
-                m_sign(false), m_op(var_op), m_size(0), m_offset(v) {}
-            explicit node(bool sign, bool_op op, unsigned nc, unsigned o) : 
-                m_sign(sign), m_op(op), m_size(nc), m_offset(o) {}
-            explicit node(uint64_t lut, unsigned nc, unsigned o):
-                m_sign(false), m_op(lut_op), m_lut(lut), m_size(nc), m_offset(o) {}
-            bool is_valid() const { return m_offset != UINT_MAX; }
-            bool_op op() const { return m_op; }
-            bool is_var() const { return m_op == var_op; }
-            bool is_and() const { return m_op == and_op; }
-            bool is_xor() const { return m_op == xor_op; }
-            bool is_ite() const { return m_op == ite_op; }
-            bool is_lut() const { return m_op == lut_op; }
-            bool is_const() const { return is_and() && size() == 0; }
-            unsigned var() const { SASSERT(is_var()); return m_offset; }
-            bool sign() const { return m_sign; }
-            unsigned size() const { return m_size; }
-            unsigned offset() const { return m_offset; }
-            uint64_t lut() const { return m_lut; }
-        };
-        random_gen            m_rand;
-        config                m_config;
-        vector<svector<node>> m_aig;    
-        literal_vector        m_literals;
-        region                m_region;
-        cut_set               m_cut_set1, m_cut_set2, m_empty_cuts;
-        vector<cut_set>       m_cuts;
-        unsigned_vector       m_max_cutset_size;
-        unsigned_vector       m_last_touched;
-        unsigned              m_num_cut_calls;
-        unsigned              m_num_cuts;
-        svector<std::pair<bool_var, literal>> m_roots;
-        unsigned              m_insertions;
-        on_clause_t           m_on_clause_add, m_on_clause_del;
-        cut_set::on_update_t  m_on_cut_add, m_on_cut_del;
-        literal_vector        m_clause;
-        cut const*            m_tables[6];
-        uint64_t              m_luts[6];
-        literal               m_lits[6];
-
-        class to_root {
-            literal_vector m_to_root;
-            void reserve(bool_var v) {
-                while (v >= m_to_root.size()) {
-                    m_to_root.push_back(literal(m_to_root.size(), false));
-                }
-            }
-        public:
-            literal operator[](bool_var v) const { 
-                return (v < m_to_root.size()) ? m_to_root[v] : literal(v, false); 
-            }
-            literal& operator[](bool_var v) { 
-                reserve(v);
-                return m_to_root[v];
-            }
-        };
-
-        class lut {
-            aig_cuts& a;
-            node const* n;
-            cut const* c;
-        public:
-            lut(aig_cuts& a, node const& n) : a(a), n(&n), c(nullptr) {}
-            lut(aig_cuts& a, cut const& c) : a(a), n(nullptr), c(&c) {}
-            unsigned size() const { return n ? n->size() : c->size(); }
-            literal child(unsigned idx) const { return n ? a.child(*n, idx) : a.child(*c, idx); }
-            uint64_t table() const { return n ? n->lut() : c->table(); }
-            std::ostream& display(std::ostream& out) const { return n ? a.display(out, *n) : out << *c; }
-        };
-
-        bool is_touched(bool_var v, node const& n);
-        bool is_touched(literal lit) const { return is_touched(lit.var()); }
-        bool is_touched(bool_var v) const { return v < m_last_touched.size() && m_last_touched[v] + m_aig.size() >= m_num_cut_calls * m_aig.size(); }
-        void reserve(unsigned v);
-        bool insert_aux(unsigned v, node const& n);
-        void init_cut_set(unsigned id);
-
-        bool eq(node const& a, node const& b);
-        bool similar(node const& a, node const& b);
-
-        unsigned_vector filter_valid_nodes() const;
-        void augment(unsigned_vector const& ids);
-        void augment(unsigned id, node const& n);
-        void augment_ite(unsigned v,  node const& n, cut_set& cs);
-        void augment_aig0(unsigned v, node const& n, cut_set& cs);
-        void augment_aig1(unsigned v, node const& n, cut_set& cs);
-        void augment_aig2(unsigned v, node const& n, cut_set& cs);
-        void augment_aigN(unsigned v, node const& n, cut_set& cs);
-
-
-        void augment_lut(unsigned v,  lut const& n, cut_set& cs);        
-        void augment_lut_rec(unsigned v, lut const& n, cut& a, unsigned idx, cut_set& cs);
-
-        cut_set const& lit2cuts(literal lit) const { return lit.var() < m_cuts.size() ? m_cuts[lit.var()] : m_empty_cuts; }
-
-        bool insert_cut(unsigned v, cut const& c, cut_set& cs);
-
-        void flush_roots();
-        bool flush_roots(bool_var var, to_root const& to_root, node& n);
-        void flush_roots(to_root const& to_root, cut_set& cs);
-
-        cut_val eval(node const& n, cut_eval const& env) const;
-        lbool get_value(bool_var v) const;
-
-        std::ostream& display(std::ostream& out, node const& n) const;
-
-        literal child(node const& n, unsigned idx) const { SASSERT(!n.is_var()); SASSERT(idx < n.size()); return m_literals[n.offset() + idx]; }
-        literal child(cut const& n, unsigned idx) const { SASSERT(idx < n.size()); return literal(n[idx], false); }
-
-        void on_node_add(unsigned v, node const& n);
-        void on_node_del(unsigned v, node const& n);
-
-        void evict(cut_set& cs, unsigned idx) { cs.evict(m_on_cut_del, idx); }
-        void reset(cut_set& cs) { cs.reset(m_on_cut_del); }
-        void push_back(cut_set& cs, cut const& c) { cs.push_back(m_on_cut_add, c); }
-        void shrink(cut_set& cs, unsigned j) { cs.shrink(m_on_cut_del, j); }
-
-        void cut2clauses(on_clause_t& on_clause, unsigned v, cut const& c);
-        void node2def(on_clause_t& on_clause, node const& n, literal r);
-
-        struct validator;
-        void validate_cut(unsigned v, cut const& c);
-        void validate_aig2(cut const& a, cut const& b, unsigned v, node const& n, cut const& c);
-        void validate_aigN(unsigned v, node const& n, cut const& c); 
-
-        void add_node(bool_var v, node const& n);
-    public:
-
-        aig_cuts();
-        void add_var(unsigned v);
-        void add_node(literal head, bool_op op, unsigned sz, literal const* args);
-        void add_node(bool_var head, uint64_t lut, unsigned sz, bool_var const* args);
-        void add_cut(bool_var v, uint64_t lut, bool_var_vector const& args);
-        void set_root(bool_var v, literal r);
-
-        void set_on_clause_add(on_clause_t& on_clause_add);
-        void set_on_clause_del(on_clause_t& on_clause_del);
-
-        void inc_max_cutset_size(unsigned v) { m_max_cutset_size.reserve(v + 1, 0);  m_max_cutset_size[v] += 10; touch(v); }
-        unsigned max_cutset_size(unsigned v) const { return v == UINT_MAX ? m_config.m_max_cutset_size : m_max_cutset_size[v]; }
-
-        vector<cut_set> const & operator()();
-        unsigned num_cuts() const { return m_num_cuts; }
-
-        void cut2def(on_clause_t& on_clause, cut const& c, literal r);
-
-        void touch(bool_var v) { m_last_touched.reserve(v + 1, false);  m_last_touched[v] = v + m_num_cut_calls * m_aig.size(); }
-
-        cut_eval simulate(unsigned num_rounds);
-
-        void simplify();
-
-        std::ostream& display(std::ostream& out) const;
-
-    };
-
-}
-
-
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 338ea8692..3dfb67f2a 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -109,15 +109,6 @@ namespace sat {
         m_anf_simplify      = p.anf();
         m_anf_delay         = p.anf_delay();
         m_anf_exlin         = p.anf_exlin();
-        m_cut_simplify      = p.cut();
-        m_cut_delay         = p.cut_delay();
-        m_cut_aig           = p.cut_aig();
-        m_cut_lut           = p.cut_lut();
-        m_cut_xor           = p.cut_xor();
-        m_cut_npn3          = p.cut_npn3();
-        m_cut_dont_cares    = p.cut_dont_cares();
-        m_cut_redundancies  = p.cut_redundancies();
-        m_cut_force         = p.cut_force();
         m_lookahead_simplify = p.lookahead_simplify();
         m_lookahead_double = p.lookahead_double();
         m_lookahead_simplify_bca = p.lookahead_simplify_bca();
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index d032e64a1..83241fe88 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -119,15 +119,6 @@ namespace sat {
         bool               m_local_search;
         local_search_mode  m_local_search_mode;
         bool               m_local_search_dbg_flips;
-        bool               m_cut_simplify;
-        unsigned           m_cut_delay;
-        bool               m_cut_aig;
-        bool               m_cut_lut;
-        bool               m_cut_xor;
-        bool               m_cut_npn3;
-        bool               m_cut_dont_cares;
-        bool               m_cut_redundancies;
-        bool               m_cut_force;
         bool               m_anf_simplify;
         unsigned           m_anf_delay;
         bool               m_anf_exlin;
diff --git a/src/sat/sat_cut_simplifier.cpp b/src/sat/sat_cut_simplifier.cpp
deleted file mode 100644
index 0125a7af1..000000000
--- a/src/sat/sat_cut_simplifier.cpp
+++ /dev/null
@@ -1,755 +0,0 @@
-/*++
-  Copyright (c) 2020 Microsoft Corporation
-
-  Module Name:
-
-   sat_cut_simplifier.cpp
-
-  Abstract:
-   
-    extract AIG definitions from clauses
-    Perform cut-set enumeration to identify equivalences.
-
-  Author:
-
-    Nikolaj Bjorner 2020-01-02
-
-  --*/
-
-#include "sat/sat_cut_simplifier.h"
-#include "sat/sat_xor_finder.h"
-#include "sat/sat_lut_finder.h"
-#include "sat/sat_npn3_finder.h"
-#include "sat/sat_elim_eqs.h"
-
-namespace sat {
-    
-    struct cut_simplifier::report {
-        cut_simplifier& s;
-        stopwatch       m_watch;
-        unsigned        m_num_eqs, m_num_units, m_num_cuts, m_num_learned_implies;
-        
-        report(cut_simplifier& s): s(s) { 
-            m_watch.start(); 
-            m_num_eqs   = s.m_stats.m_num_eqs;
-            m_num_units = s.m_stats.m_num_units;
-            m_num_cuts  = s.m_stats.m_num_cuts;
-            m_num_learned_implies = s.m_stats.m_num_learned_implies;
-        }
-        ~report() {
-            unsigned ne = s.m_stats.m_num_eqs   - m_num_eqs;
-            unsigned nu = s.m_stats.m_num_units - m_num_units;
-            unsigned nc = s.m_stats.m_num_cuts  - m_num_cuts;
-            unsigned ni = s.m_stats.m_num_learned_implies - m_num_learned_implies;
-            IF_VERBOSE(2, 
-                       verbose_stream() << "(sat.cut-simplifier";
-                       if (nu > 0) verbose_stream() << " :num-units " << nu;
-                       if (ne > 0) verbose_stream() << " :num-eqs "   << ne;
-                       if (ni > 0) verbose_stream() << " :num-bin " << ni;
-                       if (nc > 0) verbose_stream() << " :num-cuts "  << nc;                       
-                       verbose_stream() << " :mb " << mem_stat() << m_watch << ")\n");
-        }
-    };
-
-    struct cut_simplifier::validator {
-        solver& _s;
-        params_ref p;
-        literal_vector m_assumptions;
-
-        validator(solver& _s, params_ref const& p): _s(_s), p(p) {
-        }
-
-        void validate(unsigned n, literal const* clause) {
-            validate(literal_vector(n, clause));
-        }
-
-        void validate(literal_vector const& clause) {
-            if (clause.size() == 2 && clause[0] == ~clause[1]) return;
-            solver s(p, _s.rlimit());
-            s.copy(_s, false);
-            IF_VERBOSE(10, verbose_stream() << "validate: " << clause << "\n");
-            m_assumptions.reset();
-            for (literal lit : clause) m_assumptions.push_back(~lit);           
-            lbool r = s.check(clause.size(), m_assumptions.data());
-            if (r != l_false) {
-                IF_VERBOSE(0, 
-                           verbose_stream() << "not validated: " << clause << "\n";
-                           s.display(verbose_stream()););
-                UNREACHABLE();
-            }
-        }
-    };
-
-    void cut_simplifier::ensure_validator() {
-        if (!m_validator) {
-            params_ref p;
-            p.set_bool("aig", false);
-            p.set_bool("drat.check_unsat", false);
-            p.set_sym("drat.file", symbol());
-            p.set_uint("max_conflicts", 10000);
-            m_validator = alloc(validator, s, p);
-        }
-    }
-
-    cut_simplifier::cut_simplifier(solver& _s):
-        s(_s), 
-        m_trail_size(0),
-        m_validator(nullptr) {  
-        if (s.get_config().m_drat) {
-            std::function<void(literal_vector const& clause)> _on_add = 
-                [this](literal_vector const& clause) { s.m_drat.add(clause); };
-            std::function<void(literal_vector const& clause)> _on_del = 
-                [this](literal_vector const& clause) { s.m_drat.del(clause); };
-            m_aig_cuts.set_on_clause_add(_on_add);
-            m_aig_cuts.set_on_clause_del(_on_del);
-        }
-        else if (m_config.m_validate_cuts) {
-            ensure_validator();
-            std::function<void(literal_vector const& clause)> _on_add = 
-                [this](literal_vector const& clause) { 
-                m_validator->validate(clause); 
-            };
-            m_aig_cuts.set_on_clause_add(_on_add);
-        }
-    }
-
-    cut_simplifier::~cut_simplifier() {
-        dealloc(m_validator);
-    }
-
-    void cut_simplifier::add_and(literal head, unsigned sz, literal const* lits) {
-        m_aig_cuts.add_node(head, and_op, sz, lits);
-        for (unsigned i = 0; i < sz; ++i) VERIFY(head.var() != lits[i].var());
-        m_stats.m_num_ands++;
-    }
-
-    //      head == l1 or l2 or l3 
-    // <=> 
-    //     ~head == ~l1 and ~l2 and ~l3
-    void cut_simplifier::add_or(literal head, unsigned sz, literal const* lits) {
-        m_lits.reset();
-        m_lits.append(sz, lits);
-        for (unsigned i = 0; i < sz; ++i) m_lits[i].neg();
-        m_aig_cuts.add_node(~head, and_op, sz, m_lits.data());
-        m_stats.m_num_ands++;
-    }
-
-    void cut_simplifier::add_xor(literal head, unsigned sz, literal const* lits) {
-        m_aig_cuts.add_node(head, xor_op, sz, lits);
-        m_stats.m_num_xors++;
-    }
-
-    void cut_simplifier::add_ite(literal head, literal c, literal t, literal e) {
-        literal lits[3] = { c, t, e };
-        m_aig_cuts.add_node(head, ite_op, 3, lits);
-        m_stats.m_num_ites++;
-    }
-
-    void cut_simplifier::add_iff(literal head, literal l1, literal l2) {
-        literal lits[2] = { l1, ~l2 };
-        m_aig_cuts.add_node(head, xor_op, 2, lits);
-        m_stats.m_num_xors++;
-    }
-
-    void cut_simplifier::set_root(bool_var v, literal r) {
-        m_aig_cuts.set_root(v, r);
-    }
-
-    void cut_simplifier::operator()() {
-
-        bool force = s.m_config.m_cut_force;
-        report _report(*this);
-        TRACE(cut_simplifier, s.display(tout););
-        unsigned n = 0, i = 0;
-        ++m_stats.m_num_calls;
-        do {
-            n = m_stats.m_num_eqs + m_stats.m_num_units;
-            clauses2aig();
-            aig2clauses();
-            ++i;
-        }
-        while (((force && i < 5) || i*i < m_stats.m_num_calls) && n < m_stats.m_num_eqs + m_stats.m_num_units);
-    }
-
-    /**
-       \brief extract AIG definitions from clauses
-       Ensure that they are sorted and variables have unique definitions.
-     */
-    void cut_simplifier::clauses2aig() {
-
-        for (; m_config.m_enable_units && m_trail_size < s.init_trail_size(); ++m_trail_size) {
-            literal lit = s.trail_literal(m_trail_size);
-            m_aig_cuts.add_node(lit, and_op, 0, nullptr);
-        }
-
-        clause_vector clauses(s.clauses());
-        if (m_config.m_learned2aig) clauses.append(s.learned());
-               
-        std::function<void (literal head, literal_vector const& ands)> on_and = 
-            [&,this](literal head, literal_vector const& ands) {
-            m_aig_cuts.add_node(head, and_op, ands.size(), ands.data());
-            m_stats.m_xands++;
-        };
-        std::function<void (literal head, literal c, literal t, literal e)> on_ite = 
-            [&,this](literal head, literal c, literal t, literal e) {            
-            literal args[3] = { c, t, e };            
-            m_aig_cuts.add_node(head, ite_op, 3, args);
-            m_stats.m_xites++;
-        };
-        if (s.m_config.m_cut_aig) {
-            aig_finder af(s);
-            af.set(on_and);
-            af.set(on_ite);
-            af(clauses);        
-        }
-
-
-        std::function<void (literal_vector const&)> on_xor = 
-            [&,this](literal_vector const& xors) {
-            SASSERT(xors.size() > 1);
-            unsigned max_level = xors.back().var();
-            unsigned index = xors.size() - 1;
-            for (unsigned i = index; i-- > 0; ) {
-                literal l = xors[i];
-                if (l.var() > max_level) {
-                    max_level = l.var();
-                    index = i;
-                }
-            }
-            // head + t1 + t2 + .. = 1 
-            // <=> 
-            // ~head = t1 + t2 + ..
-            literal head = ~xors[index];
-            TRACE(cut_simplifier, tout << xors << "\n";);
-            unsigned sz = xors.size() - 1;
-            m_lits.reset();
-            for (unsigned i = xors.size(); i-- > 0; ) {
-                if (i != index) 
-                    m_lits.push_back(xors[i]);
-            }
-            m_aig_cuts.add_node(head, xor_op, sz, m_lits.data());
-            m_lits.reset();
-            m_stats.m_xxors++;            
-        };
-        if (s.m_config.m_cut_xor) {
-            xor_finder xf(s);
-            xf.set(on_xor);
-            xf(clauses);
-        }
-
-        std::function<void(uint64_t, bool_var_vector const&, bool_var)> on_lut = 
-            [&,this](uint64_t lut, bool_var_vector const& vars, bool_var v) {
-            m_stats.m_xluts++;
-            // m_aig_cuts.add_cut(v, lut, vars);
-            m_aig_cuts.add_node(v, lut, vars.size(), vars.data());
-        };
-
-        if (s.m_config.m_cut_npn3) {
-            npn3_finder nf(s);
-            // TBD: stubs for npn3
-            // question: perhaps just use a LUT interface?
-            // nf.set_on_mux
-            // nf.set_on_maj
-            // nf.set_on_orand
-            // nf.set_on_and
-            // nf.set_on_xor
-            // nf.set_on_andxor
-            // nf.set_on_xorand
-            // nf.set_on_gamble
-            // nf.set_on_onehot
-            // nf.set_on_dot
-            // nf(clauses);
-        }
-
-        if (s.m_config.m_cut_lut) {
-            lut_finder lf(s);
-            lf.set(on_lut);
-            lf(clauses);
-        }
-
-#if 0
-        statistics st;
-        collect_statistics(st);
-        st.display(std::cout);
-        exit(0);
-#endif
-    }
-
-    void cut_simplifier::aig2clauses() {
-        vector<cut_set> const& cuts = m_aig_cuts();
-        m_stats.m_num_cuts = m_aig_cuts.num_cuts();
-        add_dont_cares(cuts);
-        cuts2equiv(cuts);
-        cuts2implies(cuts);
-        simulate_eqs();
-    }
-
-    void cut_simplifier::cuts2equiv(vector<cut_set> const& cuts) {
-        map<cut const*, unsigned, cut::hash_proc, cut::eq_proc> cut2id;                
-        bool new_eq = false;
-        union_find_default_ctx ctx;
-        union_find<> uf(ctx);
-
-        for (unsigned i = 2*s.num_vars(); i--> 0; ) uf.mk_var();
-        auto add_eq = [&](literal l1, literal l2) {
-            uf.merge(l1.index(), l2.index());
-            uf.merge((~l1).index(), (~l2).index());
-            new_eq = true;
-        };
-
-        for (unsigned i = cuts.size(); i-- > 0; ) {
-            literal u(i, false);
-            for (auto& c : cuts[i]) {
-                unsigned j = 0;
-                cut nc(c);
-                nc.negate();
-                if (m_config.m_enable_units && c.is_true()) {
-                    assign_unit(c, u);
-                }
-                else if (m_config.m_enable_units && c.is_false()) {
-                    assign_unit(nc, ~u);
-                }
-                else if (cut2id.find(&c, j)) {
-                    literal v(j, false);
-                    assign_equiv(c, u, v);
-                    add_eq(u, v);
-                }
-                else if (cut2id.find(&nc, j)) {
-                    literal v(j, true);
-                    assign_equiv(c, u, v);
-                    add_eq(u, v);
-                }
-                else {
-                    cut2id.insert(&c, i);
-                }
-            }
-        }        
-        if (new_eq) {
-            uf2equiv(uf);
-        }
-    }
-
-    void cut_simplifier::assign_unit(cut const& c, literal lit) {
-        if (s.value(lit) != l_undef) 
-            return;
-        IF_VERBOSE(10, verbose_stream() << "new unit " << lit << "\n");
-        validate_unit(lit);
-        certify_unit(lit, c);
-        s.assign_unit(lit);
-        ++m_stats.m_num_units;        
-    }
-
-    void cut_simplifier::assign_equiv(cut const& c, literal u, literal v) {
-        if (u.var() == v.var()) return;
-        IF_VERBOSE(10, verbose_stream() << u << " " << v << " " << c << "\n";);
-        TRACE(cut_simplifier, tout << u << " == " << v << "\n";);                            
-        certify_equivalence(u, v, c);                    
-        validate_eq(u, v);
-    }
-
-    /**
-     * Convert a union-find over literals into input for eim_eqs.
-     */
-    void cut_simplifier::uf2equiv(union_find<> const& uf) {
-        union_find_default_ctx ctx;
-        union_find<> uf2(ctx);
-        bool new_eq = false;
-        for (unsigned i = 2*s.num_vars(); i--> 0; ) uf2.mk_var();
-        // extract equivalences over non-eliminated literals.
-        for (unsigned idx = 0; idx < uf.get_num_vars(); ++idx) {
-            if (!uf.is_root(idx) || 1 == uf.size(idx)) continue;
-            literal root = null_literal;
-            unsigned first = idx;
-            do {
-                literal lit = to_literal(idx);
-                if (!s.was_eliminated(lit)) {
-                    if (root == null_literal) {
-                        root = lit;
-                    }
-                    else {
-                        uf2.merge(lit.index(), root.index());
-                        new_eq = true;
-                        ++m_stats.m_num_eqs;
-                    }
-                }
-                idx = uf.next(idx);
-            }
-            while (first != idx);
-        }
-        for (unsigned i = s.num_vars(); i-- > 0; ) {
-            literal lit(i, false);
-            if (uf2.find(lit.index()) == uf2.find((~lit).index())) {
-                s.set_conflict();
-                return;
-            }
-        }
-        if (new_eq) {
-            elim_eqs elim(s);
-            elim(uf2);        
-        }
-    }
-
-    /**
-     * Extract binary clauses from cuts.
-     * A bit encoding of a LUT of u 
-     * that sets a subset of bits for LUT' of v establishes
-     * that u implies v.
-     */
-    void cut_simplifier::cuts2implies(vector<cut_set> const& cuts) {
-        if (!m_config.m_learn_implies) return;
-        vector<vector<std::pair<unsigned, cut const*>>> var_tables;
-        map<cut const*, unsigned, cut::dom_hash_proc, cut::dom_eq_proc> cut2tables;
-        unsigned j = 0;
-        big big(s.rand());
-        big.init(s, true);
-        for (auto const& cs : cuts) {
-            if (s.was_eliminated(cs.var())) 
-                continue;
-            for (auto const& c : cs) {
-                if (c.is_false() || c.is_true()) 
-                    continue;
-                if (!cut2tables.find(&c, j)) {
-                    j = var_tables.size();
-                    var_tables.push_back(vector<std::pair<unsigned, cut const*>>());
-                    cut2tables.insert(&c, j);
-                }
-                var_tables[j].push_back(std::make_pair(cs.var(), &c));
-            }
-        }
-        for (unsigned i = 0; i < var_tables.size(); ++i) {
-            auto const& vt = var_tables[i];
-            for (unsigned j = 0; j < vt.size(); ++j) {
-                literal u(vt[j].first, false);
-                cut const& c1 = *vt[j].second;
-                cut nc1(c1);
-                nc1.negate();
-                uint64_t t1 = c1.table();
-                uint64_t n1 = nc1.table();
-                for (unsigned k = j + 1; k < vt.size(); ++k) {
-                    literal v(vt[k].first, false);
-                    cut const& c2 = *vt[k].second;                
-                    uint64_t t2 = c2.table();
-                    uint64_t n2 = c2.ntable();
-                    if (t1 == t2 || t1 == n2) {
-                        // already handled
-                    }
-                    else if ((t1 | t2) == t2) {
-                        learn_implies(big, c1, u, v);
-                    }
-                    else if ((t1 | n2) == n2) {
-                        learn_implies(big, c1, u, ~v);
-                    }
-                    else if ((n1 | t2) == t2) {
-                        learn_implies(big, nc1, ~u, v);
-                    }
-                    else if ((n1 | n2) == n2) {
-                        learn_implies(big, nc1, ~u, ~v);
-                    }
-                }
-            }
-        }
-    }
-
-    void cut_simplifier::learn_implies(big& big, cut const& c, literal u, literal v) {
-        if (u == ~v) {
-            assign_unit(c, v);
-            return;
-        }
-        if (u == v) { 
-            return;
-        }
-        bin_rel q, p(~u, v);
-        if (m_bins.find(p, q) && q.op != op_code::none)
-            return;
-        if (big.connected(u, v)) 
-            return;
-        for (auto const& w : s.get_wlist(u))
-            if (w.is_binary_clause() && v == w.get_literal())
-                return;
-        certify_implies(u, v, c);
-        s.mk_clause(~u, v, sat::status::redundant());
-        // m_bins owns reference to ~u or v created by certify_implies
-        m_bins.insert(p); 
-        ++m_stats.m_num_learned_implies;
-    }
-
-    void cut_simplifier::simulate_eqs() {
-        if (!m_config.m_simulate_eqs) return;
-        auto var2val = m_aig_cuts.simulate(4);
-
-        // Assign higher cutset budgets to equality candidates that come from simulation
-        // touch them to trigger recomputation of cutsets.
-        u64_map<literal> val2lit;
-        unsigned i = 0, num_eqs = 0;
-        for (cut_val val : var2val) {
-            if (!s.was_eliminated(i) && s.value(i) == l_undef) {
-                literal u(i, false), v;
-                if (val2lit.find(val.m_t, v)) {
-                    
-                    m_aig_cuts.inc_max_cutset_size(i);
-                    m_aig_cuts.inc_max_cutset_size(v.var());
-                    num_eqs++;
-                }
-                else if (val2lit.find(val.m_f, v)) {
-                    m_aig_cuts.inc_max_cutset_size(i);
-                    m_aig_cuts.inc_max_cutset_size(v.var());
-                    num_eqs++;
-                }
-                else {
-                    val2lit.insert(val.m_t, u);
-                    val2lit.insert(val.m_f, ~u);
-                }
-            }
-            ++i;
-        }
-        IF_VERBOSE(2, verbose_stream() << "(sat.cut-simplifier num simulated eqs " << num_eqs << ")\n");
-    }
-
-    void cut_simplifier::track_binary(bin_rel const& p) {
-        if (!s.m_config.m_drat) 
-            return;
-        literal u, v;
-        p.to_binary(u, v);
-        track_binary(u, v);
-    }
-
-    void cut_simplifier::untrack_binary(bin_rel const& p) {
-        if (!s.m_config.m_drat) 
-            return;
-        literal u, v;
-        p.to_binary(u, v);
-        untrack_binary(u, v);
-    }
-
-    void cut_simplifier::track_binary(literal u, literal v) {
-        if (s.m_config.m_drat) {
-            s.m_drat.add(u, v, sat::status::redundant());
-        }
-    }
-
-    void cut_simplifier::untrack_binary(literal u, literal v) {
-        if (s.m_config.m_drat) {
-            s.m_drat.del(u, v);
-        }
-    }
-
-    void cut_simplifier::certify_unit(literal u, cut const& c) {
-        certify_implies(~u, u, c);
-    }
-
-    /**
-     * Equivalences modulo cuts are not necessarily DRAT derivable.
-     * To ensure that there is a DRAT derivation we create all resolvents
-     * of the LUT clauses until deriving binary u or ~v and ~u or v.
-     * each resolvent is DRAT derivable because there are two previous lemmas that
-     * contain complementary literals.
-     */
-    void cut_simplifier::certify_equivalence(literal u, literal v, cut const& c) {
-        certify_implies(u, v, c);
-        certify_implies(v, u, c);
-    }
-
-    /**
-     * certify that u implies v, where c is the cut for u.
-     * Then every position in c where u is true, it has to be 
-     * the case that v is too.
-     * Where u is false, v can have any value.
-     * Thus, for every clause C or u', where u' is u or ~u,
-     * it follows that C or ~u or v
-     */
-    void cut_simplifier::certify_implies(literal u, literal v, cut const& c) {
-        if (!s.m_config.m_drat) return;
-        
-        vector<literal_vector> clauses;
-        std::function<void(literal_vector const& clause)> on_clause = 
-            [&,this](literal_vector const& clause) { 
-            SASSERT(clause.back().var() == u.var()); 
-            clauses.push_back(clause);
-            clauses.back().back() = ~u;
-            if (~u != v) clauses.back().push_back(v);
-            s.m_drat.add(clauses.back());
-        };        
-        m_aig_cuts.cut2def(on_clause, c, u);
-
-        // create all resolvents over C. C is assumed to 
-        // contain all combinations of some set of literals.
-        unsigned i = 0, sz = clauses.size();
-        while (sz - i > 1) {
-            SASSERT((sz & (sz - 1)) == 0 && "sz is a power of 2");
-            for (; i < sz; ++i) {
-                auto const& clause = clauses[i];
-                if (clause[0].sign()) {
-                    literal_vector cl(clause.size() - 1, clause.data() + 1);
-                    clauses.push_back(cl);
-                    s.m_drat.add(cl);
-                }
-            }
-            i = sz;
-            sz = clauses.size();
-        }
-
-        IF_VERBOSE(10, for (auto const& clause : clauses) verbose_stream() << clause << "\n";);
-
-        // once we established equivalence, don't need auxiliary clauses for DRAT.
-        clauses.pop_back();
-        for (auto const& clause : clauses) {
-            s.m_drat.del(clause);            
-        }                      
-    }
-
-    void cut_simplifier::add_dont_cares(vector<cut_set> const& cuts) {
-        if (s.m_config.m_cut_dont_cares) {
-            cuts2bins(cuts);
-            bins2dont_cares();
-            dont_cares2cuts(cuts); 
-        }    
-        if (s.m_config.m_cut_redundancies) {
-            m_aig_cuts.simplify();
-        }
-    }
-
-    /**
-     * Collect binary relations between variables that occur in cut sets.
-     */
-    void cut_simplifier::cuts2bins(vector<cut_set> const& cuts) {
-        svector<bin_rel> dcs;
-        for (auto const& p : m_bins) 
-            if (p.op != op_code::none)
-                dcs.push_back(p);        
-        m_bins.reset();
-        for (auto const& cs : cuts) 
-            for (auto const& c : cs) 
-                for (unsigned i = c.size(); i-- > 0; ) 
-                    for (unsigned j = i; j-- > 0; ) 
-                        m_bins.insert(bin_rel(c[j],c[i]));
-
-        // don't lose previous don't cares
-        for (auto const& p : dcs) {
-            if (m_bins.contains(p)) {
-                m_bins.insert(p);
-            }
-            else {
-                untrack_binary(p);
-            }
-        }
-    }
-    
-    /**
-     * Compute masks for binary relations.
-     */
-    void cut_simplifier::bins2dont_cares() {
-        big b(s.rand());
-        b.init(s, true);
-        for (auto& p : m_bins) {
-            if (p.op != op_code::none) continue;
-            literal u(p.u, false), v(p.v, false);
-            // u -> v, then u & ~v is impossible
-            if (b.connected(u, v)) {
-                p.op = op_code::pn;
-            }
-            else if (b.connected(u, ~v)) {                
-                p.op = op_code::pp;
-            }
-            else if (b.connected(~u, v)) {
-                p.op = op_code::nn;
-            }
-            else if (b.connected(~u, ~v)) {
-                p.op = op_code::np;
-            }
-            if (p.op != op_code::none) {
-                track_binary(p);
-            }
-        }
-        IF_VERBOSE(2, {
-                unsigned n = 0; for (auto const& p : m_bins) if (p.op != op_code::none) ++n;
-                verbose_stream() << n << " / " << m_bins.size() << " don't cares\n";
-            });
-    }
-
-    /**
-     * Loop over cuts, if it is possible to add a new don't care combination 
-     * to a cut, then ensure that the variable is "touched" so that it participates
-     * in the next propagation.
-     */
-    void cut_simplifier::dont_cares2cuts(vector<cut_set> const& cuts) {
-        for (auto& cs : cuts) {
-            for (auto const& c : cs) {
-                if (add_dont_care(c)) {
-                    m_aig_cuts.touch(cs.var());
-                    m_stats.m_num_dont_care_reductions++;
-                }
-            }
-        }
-    }
-
-    /**
-     * compute masks for position i, j and op-code p.op
-     * For the don't care combination false, false, the first don't care
-     * position is 0. If it is true, false, the first don't care position
-     * is the position that encodes the first occurrence where i is true.
-     * It is 2^i. Cases for false, true and true, true are similar.
-     * Don't care positions are spaced apart by 2^{j+1}, 
-     * where j is the second variable position.
-     */ 
-    uint64_t cut_simplifier::op2dont_care(unsigned i, unsigned j, bin_rel const& p) {
-        SASSERT(i < j && j < 6);
-        if (p.op == op_code::none) return 0ull;
-        // first position of mask is offset into output bits contributed by i and j
-        bool i_is_0 = (p.op == op_code::np || p.op == op_code::nn);
-        bool j_is_0 = (p.op == op_code::pn || p.op == op_code::nn);
-        uint64_t first = (i_is_0 ? 0 : (1 << i)) + (j_is_0 ? 0 : (1 << j));
-        uint64_t inc = 1ull << (j + 1);
-        uint64_t r = 1ull << first; 
-        while (inc < 64ull) { r |= (r << inc); inc *= 2; }
-        return r;
-    }
-
-    /**
-     * Apply obtained dont_cares to cut sets.
-     * The don't care bits are added to the LUT, so that the
-     * output is always 1 on don't care combinations.
-     */
-    bool cut_simplifier::add_dont_care(cut const & c) {
-        uint64_t dc = 0;
-        for (unsigned i = 0; i < c.size(); ++i) {
-            for (unsigned j = i + 1; j < c.size(); ++j) {
-                bin_rel p(c[i], c[j]);
-                if (m_bins.find(p, p) && p.op != op_code::none) {
-                    dc |= op2dont_care(i, j, p);
-                }
-            }
-        }        
-        return (dc != c.dont_care()) && (c.add_dont_care(dc), true);
-    }
-
-    void cut_simplifier::collect_statistics(statistics& st) const {
-        st.update("sat-cut.eqs",   m_stats.m_num_eqs);
-        st.update("sat-cut.cuts",  m_stats.m_num_cuts);
-        st.update("sat-cut.ands",  m_stats.m_num_ands);
-        st.update("sat-cut.ites",  m_stats.m_num_ites);
-        st.update("sat-cut.xors",  m_stats.m_num_xors);
-        st.update("sat-cut.xands", m_stats.m_xands);
-        st.update("sat-cut.xites", m_stats.m_xites);
-        st.update("sat-cut.xxors", m_stats.m_xxors);
-        st.update("sat-cut.xluts", m_stats.m_xluts);
-        st.update("sat-cut.dc-reduce", m_stats.m_num_dont_care_reductions);
-    }
-
-    void cut_simplifier::validate_unit(literal lit) {
-        if (!m_config.m_validate_lemmas) return;
-        ensure_validator();
-        m_validator->validate(1, &lit);
-    }
-
-    void cut_simplifier::validate_eq(literal a, literal b) {
-        if (!m_config.m_validate_lemmas) return;
-        ensure_validator();
-        literal lits1[2] = { a, ~b };
-        literal lits2[2] = { ~a, b };
-        m_validator->validate(2, lits1);
-        m_validator->validate(2, lits2);
-    }
-
-    
-}
-
diff --git a/src/sat/sat_cut_simplifier.h b/src/sat/sat_cut_simplifier.h
deleted file mode 100644
index aae5d4cfe..000000000
--- a/src/sat/sat_cut_simplifier.h
+++ /dev/null
@@ -1,174 +0,0 @@
-/*++
-  Copyright (c) 2020 Microsoft Corporation
-
-  Module Name:
-
-   sat_cut_simplifier.h
-
-  Abstract:
-   
-    extract AIG definitions from clauses
-    Perform cut-set enumeration to identify equivalences.
-
-  Author:
-
-    Nikolaj Bjorner 2020-01-02
-
-  --*/
-
-#pragma once
-
-#include "util/union_find.h"
-#include "sat/sat_aig_finder.h"
-#include "sat/sat_aig_cuts.h"
-
-namespace sat {
-
-    class cut_simplifier {
-    public:
-        struct stats {
-            unsigned m_num_eqs, m_num_units, m_num_cuts, m_num_xors, m_num_ands, m_num_ites;
-            unsigned m_xxors, m_xands, m_xites, m_xluts;                         // extrated gates
-            unsigned m_num_calls, m_num_dont_care_reductions, m_num_learned_implies;
-            stats() { reset(); }
-            void reset() { memset(this, 0, sizeof(*this)); }
-        };
-        struct config {
-            bool m_enable_units;            // enable learning units
-            bool m_enable_dont_cares;       // enable applying don't cares to LUTs
-            bool m_learn_implies;           // learn binary clauses
-            bool m_learned2aig;             // add learned clauses to AIGs used by cut-set enumeration
-            bool m_validate_cuts;           // enable direct validation of generated cuts
-            bool m_validate_lemmas;         // enable direct validation of learned lemmas 
-            bool m_simulate_eqs;            // use symbolic simulation to control size of cutsets.
-            config():
-                m_enable_units(true),
-                m_enable_dont_cares(true),
-                m_learn_implies(false),
-                m_learned2aig(true),
-                m_validate_cuts(false), 
-                m_validate_lemmas(false),
-                m_simulate_eqs(false) {}
-        };
-    private:
-        struct report;
-        struct validator;
-
-        /**
-         * collect pairs of literal combinations that are impossible
-         * base on binary implication graph queries.  Apply the masks
-         * on cut sets so to allow detecting equivalences modulo
-         * implications.
-         *
-         * The encoding is as follows:
-         * a or b   -> op = nn because (~a & ~b) is a don't care
-         * ~a or b  -> op = pn because (a & ~b)  is a don't care
-         * a or ~b  -> op = np because (~a & b)  is a don't care
-         * ~a or ~b -> op = pp because (a & b)   is a don't care
-         *
-         */
-
-        enum class op_code { pp, pn, np, nn, none };
-
-        struct bin_rel {
-            unsigned u, v;
-            op_code op;
-            bin_rel(unsigned _u, unsigned _v): u(_u), v(_v), op(op_code::none) {
-                if (u > v) std::swap(u, v);
-            }
-            // convert binary clause into a bin-rel
-            bin_rel(literal _u, literal _v): u(_u.var()), v(_v.var()), op(op_code::none) {
-                if (_u.sign() && _v.sign()) op = op_code::pp;
-                else if (_u.sign()) op = op_code::pn;
-                else if (_v.sign()) op = op_code::np;
-                else op = op_code::nn;
-                if (u > v) {
-                    std::swap(u, v);
-                    if (op == op_code::np) op = op_code::pn;
-                    else if (op == op_code::pn) op = op_code::np;
-                }
-            }
-            bin_rel(): u(UINT_MAX), v(UINT_MAX), op(op_code::none) {}
-
-            struct hash {
-                unsigned operator()(bin_rel const& p) const { 
-                    return p.u + 65599*p.v; // Weinberger's should be a bit cheaper mk_mix(p.u, p.v, 1); 
-                }
-            };
-            struct eq {
-                bool operator()(bin_rel const& a, bin_rel const& b) const {
-                    return a.u == b.u && a.v == b.v;
-                }
-            };
-            void to_binary(literal& lu, literal& lv) const {
-                switch (op) {
-                case op_code::pp: lu = literal(u, true); lv = literal(v, true); break;
-                case op_code::pn: lu = literal(u, true); lv = literal(v, false); break;
-                case op_code::np: lu = literal(u, false); lv = literal(v, true); break;
-                case op_code::nn: lu = literal(u, false); lv = literal(v, false); break;
-                default: UNREACHABLE(); break;
-                }
-            }
-        };
-
-
-        solver&  s;
-        stats    m_stats;
-        config   m_config;
-        aig_cuts m_aig_cuts;
-        unsigned m_trail_size;
-        literal_vector m_lits;
-        validator* m_validator;
-        hashtable<bin_rel, bin_rel::hash, bin_rel::eq> m_bins;
-
-        void clauses2aig();
-        void aig2clauses();
-        void simulate_eqs();
-        void cuts2equiv(vector<cut_set> const& cuts);
-        void cuts2implies(vector<cut_set> const& cuts);
-        void uf2equiv(union_find<> const& uf);
-        void assign_unit(cut const& c, literal lit);
-        void assign_equiv(cut const& c, literal u, literal v);
-        void learn_implies(big& big, cut const& c, literal u, literal v);
-        void ensure_validator();
-        void validate_unit(literal lit);
-        void validate_eq(literal a, literal b);
-        void certify_unit(literal u, cut const& c);
-        void certify_implies(literal u, literal v, cut const& c);
-        void certify_equivalence(literal u, literal v, cut const& c);
-        void track_binary(literal u, literal v);
-        void untrack_binary(literal u, literal v);
-        void track_binary(bin_rel const& p);
-        void untrack_binary(bin_rel const& p);        
-
-        
-        void add_dont_cares(vector<cut_set> const& cuts);
-        void cuts2bins(vector<cut_set> const& cuts);
-        void bins2dont_cares();
-        void dont_cares2cuts(vector<cut_set> const& cuts);
-        bool add_dont_care(cut const & c);
-        uint64_t op2dont_care(unsigned i, unsigned j, bin_rel const& p);
-
-    public:
-        cut_simplifier(solver& s);
-        ~cut_simplifier();                
-        void operator()();
-        void collect_statistics(statistics& st) const;
-
-        /**
-         * The clausifier may know that some literal is defined as a 
-         * function of other literals. This API is exposed so that 
-         * the clausifier can instrument the simplifier with an initial
-         * AIG.
-         * set_root is issued from the equivalence finder.
-         */
-        void add_and(literal head, unsigned sz, literal const* args);
-        void add_or(literal head, unsigned sz, literal const* args);
-        void add_xor(literal head, unsigned sz, literal const* args);
-        void add_ite(literal head, literal c, literal t, literal e);
-        void add_iff(literal head, literal l1, literal l2);
-        void set_root(bool_var v, literal r);
-    };
-}
-
-
diff --git a/src/sat/sat_cutset.cpp b/src/sat/sat_cutset.cpp
deleted file mode 100644
index 2d31bcf14..000000000
--- a/src/sat/sat_cutset.cpp
+++ /dev/null
@@ -1,280 +0,0 @@
-/*++
-  Copyright (c) 2020 Microsoft Corporation
-
-  Module Name:
-
-   sat_cutset.cpp
-
-  Author:
-
-    Nikolaj Bjorner 2020-01-02
-
-  --*/
-
-
-#include "util/hashtable.h"
-#include "sat/sat_cutset.h"
-#include "sat/sat_cutset_compute_shift.h"
-#include <memory>
-#include <sstream>
-
-
-namespace sat {
-
-    /**
-       \brief
-       if c is subsumed by a member in cut_set, then c is not inserted.
-       otherwise, remove members that c subsumes.
-       Note that the cut_set maintains invariant that elements don't subsume each-other.
-       
-       TBD: this is a bottleneck.
-       Ideas:
-       - add Bloom filter to is_subset_of operation.
-       - pre-allocate fixed array instead of vector for cut_set to avoid overhead for memory allocation.
-    */
-    
-    bool cut_set::insert(on_update_t& on_add, on_update_t& on_del, cut const& c) {
-        unsigned i = 0, k = m_size;
-        for (; i < k; ++i) {
-            cut const& a = (*this)[i];
-            if (a.subset_of(c)) {
-                return false;
-            }
-            if (c.subset_of(a)) {
-                std::swap(m_cuts[i--], m_cuts[--k]);
-            }
-        }
-        // for DRAT make sure to add new element before removing old cuts
-        // the new cut may need to be justified relative to the old cut
-        push_back(on_add, c);
-        std::swap(m_cuts[i++], m_cuts[m_size-1]);
-        shrink(on_del, i);    
-        return true;
-    }
-    
-    bool cut_set::no_duplicates() const {
-        hashtable<cut const*, cut::hash_proc, cut::eq_proc> table;
-        for (auto const& cut : *this) {
-            VERIFY(!table.contains(&cut));
-            table.insert(&cut);
-        }
-        return true;
-    }
-
-    std::ostream& cut_set::display(std::ostream& out) const {
-        for (auto const& cut : *this) {
-            cut.display(out) << "\n";
-        }
-        return out;
-    }
-
-
-    void cut_set::shrink(on_update_t& on_del, unsigned j) { 
-        if (m_var != UINT_MAX && on_del) {
-            for (unsigned i = j; i < m_size; ++i) {
-                on_del(m_var, m_cuts[i]);
-            }
-        }
-        m_size = j; 
-    }
-
-    void cut_set::push_back(on_update_t& on_add, cut const& c) {
-        SASSERT(m_max_size > 0);
-        if (!m_cuts) {
-            m_cuts = new (*m_region) cut[m_max_size];
-        }
-        if (m_size == m_max_size) {
-            m_max_size *= 2;
-            cut* new_cuts = new (*m_region) cut[m_max_size];
-            std::uninitialized_copy(m_cuts, m_cuts + m_size, new_cuts);
-            m_cuts = new_cuts;
-        }
-        if (m_var != UINT_MAX && on_add) on_add(m_var, c);
-        m_cuts[m_size++] = c; 
-    }
-
-    void cut_set::evict(on_update_t& on_del, cut const& c) {
-        for (unsigned i = 0; i < m_size; ++i) {
-            if (m_cuts[i] == c) {
-                evict(on_del, i);
-                break;
-            }
-        }
-    }
-
-    void cut_set::evict(on_update_t& on_del, unsigned idx) {
-        if (m_var != UINT_MAX && on_del) on_del(m_var, m_cuts[idx]); 
-        m_cuts[idx] = m_cuts[--m_size]; 
-    }
-
-    void cut_set::init(region& r, unsigned max_sz, unsigned v) { 
-        m_var = v;
-        m_size = 0;
-        SASSERT(!m_region || m_cuts);
-        VERIFY(!m_region || m_max_size > 0);
-        if (!m_region) {
-            m_max_size = 2; // max_sz;
-            m_region = &r;
-            m_cuts = nullptr;
-        }
-    }
-
-    /**
-       \brief shift table 'a' by adding elements from 'c'.
-       a.shift_table(c)
-       
-       \pre 'a' is a subset of 'c'.
-       
-       Let 't' be the table for 'a'.
-       
-       i'th bit in t  is function of indices x0*2^0 + x2*2^1 = i
-       i'th bit in t' is function of indices x0*2^0 + x1*2^1 + x2*2^2 = i
-       
-       i -> assignment to coefficients in c, 
-       -> assignment to coefficients in a
-       -> compute j, 
-       -> t'[i] <- t[j]
-       
-       This is still time consuming:
-       Ideas: 
-       - pre-compute some shift operations.
-       - use strides on some common cases.
-       - what ABC does?
-    */       
-    uint64_t cut::shift_table(cut const& c) const {
-        SASSERT(subset_of(c));
-        unsigned index = 0;
-        for (unsigned i = 0, j = 0, x = (*this)[i], y = c[j]; x != UINT_MAX; ) {
-            if (x == y) {
-                index |= (1 << j);
-                x = (*this)[++i];
-            }
-            y = c[++j];
-        }
-        index |= (1 << c.m_size);
-        return compute_shift(table(), index);
-    }
-    
-    bool cut::operator==(cut const& other) const {
-        return table() == other.table() && dom_eq(other);
-    }
-    
-    unsigned cut::hash() const {
-        return get_composite_hash(*this, m_size, 
-                                  [](cut const& c) { return (unsigned)c.table(); }, 
-                                  [](cut const& c, unsigned i) { return c[i]; });
-    }
-
-    unsigned cut::dom_hash() const {
-        return get_composite_hash(*this, m_size, 
-                                  [](cut const& c) { return 3; }, 
-                                  [](cut const& c, unsigned i) { return c[i]; });
-    }
-
-    bool cut::dom_eq(cut const& other) const {
-        if (m_size != other.m_size) return false;
-        for (unsigned i = 0; i < m_size; ++i) {
-            if ((*this)[i] != other[i]) return false;
-        }
-        return true;
-    }
-
-    /**
-     * \brief create the masks
-     * i = 0: 101010101010101
-     * i = 1: 1100110011001100
-     * i = 2: 1111000011110000
-     * i = 3: 111111110000000011111111
-     */
-
-    uint64_t cut::effect_mask(unsigned i) {
-        SASSERT(i <= 6);
-        uint64_t m = 0;
-        if (i == 6) {
-            m = ~((uint64_t)0);
-        }
-        else {
-            m = (1ull << (1u << i)) - 1;   // i = 0: m = 1
-            unsigned w = 1u << (i + 1);    // i = 0: w = 2
-            while (w < 64) {
-                m |= (m << w);             // i = 0: m = 1 + 4
-                w *= 2;
-            }
-        }
-        return m;
-    }
-
-    /**
-       remove element from cut as it is deemed a don't care
-     */
-    void cut::remove_elem(unsigned i) {
-        for (unsigned j = i + 1; j < m_size; ++j) {
-            m_elems[j-1] = m_elems[j]; 
-        }
-        --m_size;
-        uint64_t m = effect_mask(i);
-        uint64_t t = 0;
-        for (unsigned j = 0, offset = 0; j < 64; ++j) {
-            if (0 != (m & (1ull << j))) {
-                t |= ((m_table >> j) & 1u) << offset;
-                ++offset;
-            }
-        }
-        m_table = t;
-        m_dont_care = 0;
-        unsigned f = 0;
-        for (unsigned e : *this) {
-            f |= (1u << (e & 0x1F));
-        }
-        m_filter = f;
-    }
-
-    /**
-       sat-sweep evaluation. Given 64 bits worth of possible values per variable, 
-       find possible values for function table encoded by cut.
-    */
-    cut_val cut::eval(cut_eval const& env) const {
-        cut_val v;
-        uint64_t t = table();
-        uint64_t n = table();
-        unsigned sz = size();
-        if (sz == 1 && t == 2) {
-            return env[m_elems[0]];
-        }
-        for (unsigned i = 0; i < 64; ++i) {
-            unsigned offset = 0;
-            for (unsigned j = 0; j < sz; ++j) {
-                offset |= (((env[m_elems[j]].m_t >> i) & 0x1) << j);
-            }
-            v.m_t |= ((t >> offset) & 0x1) << i;
-            v.m_f |= ((n >> offset) & 0x1) << i;
-        }
-        return v;
-    }
-    
-    std::ostream& cut::display(std::ostream& out) const {
-        out << "{";
-        for (unsigned i = 0; i < m_size; ++i) {
-            out << (*this)[i];
-            if (i + 1 < m_size) out << " ";
-        }        
-        out << "} ";
-        display_table(out, m_size, table());
-        return out;
-    }
-
-    std::ostream& cut::display_table(std::ostream& out, unsigned num_input, uint64_t table) {
-        for (unsigned i = 0; i < (1u << num_input); ++i) {
-            if (0 != (table & (1ull << i))) out << "1"; else out << "0";
-        }    
-        return out;
-    }
-
-    std::string cut::table2string(unsigned num_input, uint64_t table) {
-        std::ostringstream strm;
-        display_table(strm, num_input, table);
-        return std::move(strm).str();
-    }
-
-
-}
diff --git a/src/sat/sat_cutset.h b/src/sat/sat_cutset.h
deleted file mode 100644
index f8451d412..000000000
--- a/src/sat/sat_cutset.h
+++ /dev/null
@@ -1,201 +0,0 @@
-/*++
-  Copyright (c) 2020 Microsoft Corporation
-
-  Module Name:
-
-   sat_cutset.cpp
-
-  Author:
-
-    Nikolaj Bjorner 2020-01-02
-
-  --*/
-
-#pragma once
-#include "util/region.h"
-#include "util/debug.h"
-#include "util/util.h"
-#include "util/lbool.h"
-#include "util/vector.h"
-#include <algorithm>
-#include <cstring>
-#include <functional>
-
-namespace sat {
-
-    struct cut_val {
-        cut_val():m_t(0ull), m_f(0ull) {}
-        cut_val(uint64_t t, uint64_t f): m_t(t), m_f(f) {}
-        uint64_t m_t, m_f;
-    };
-    
-    typedef svector<cut_val> cut_eval;
-
-    class cut {
-        unsigned m_filter;
-        unsigned m_size;
-        unsigned m_elems[5];
-        uint64_t m_table;
-        mutable uint64_t m_dont_care;
-
-        uint64_t table_mask() const { return (1ull << (1ull << m_size)) - 1ull; }
-
-    public:
-        cut(): m_filter(0), m_size(0), m_table(0), m_dont_care(0) {
-            m_elems[0] = m_elems[1] = m_elems[2] = m_elems[3] = m_elems[4] = 0;
-        }
-
-        cut(unsigned id): m_filter(1u << (id & 0x1F)), m_size(1), m_table(2), m_dont_care(0) { 
-            m_elems[0] = id; 
-            m_elems[1] = m_elems[2] = m_elems[3] = m_elems[4] = 0;
-        }
-
-        cut_val eval(cut_eval const& env) const;
-
-        unsigned size() const { return m_size; }
-
-        unsigned filter() const { return m_filter; }
-
-        static unsigned max_cut_size() { return 5; }
-
-        unsigned const* begin() const { return m_elems; }
-        unsigned const* end() const  { return m_elems + m_size; }
-
-        bool add(unsigned i) {
-            if (m_size >= max_cut_size()) {
-                return false;
-            }
-            else {
-                m_elems[m_size++] = i;
-                m_filter |= (1u << (i & 0x1F));
-                return true;
-            }
-        }
-        void negate() { set_table(~m_table); }
-        void set_table(uint64_t t) { m_table = t & table_mask(); }
-        uint64_t table() const { return (m_table | m_dont_care) & table_mask(); }
-        uint64_t ntable() const { return (~m_table | m_dont_care) & table_mask(); }
-
-        uint64_t dont_care() const { return m_dont_care; }
-        void add_dont_care(uint64_t t) const { m_dont_care |= t; }
-
-        bool is_true()  const { return 0 == (table_mask() & ~table()); }
-        bool is_false() const { return 0 == (table_mask() & ~m_dont_care & m_table); }
-
-        bool operator==(cut const& other) const;
-        bool operator!=(cut const& other) const { return !(*this == other); }
-        unsigned hash() const;
-        unsigned dom_hash() const;
-        bool dom_eq(cut const& other) const;
-        struct eq_proc { 
-            bool operator()(cut const& a, cut const& b) const { return a == b; }
-            bool operator()(cut const* a, cut const* b) const { return *a == *b; }
-        };
-        struct hash_proc {
-            unsigned operator()(cut const& a) const { return a.hash(); }
-            unsigned operator()(cut const* a) const { return a->hash(); }
-        };
-
-        struct dom_eq_proc {
-            bool operator()(cut const& a, cut const& b) const { return a.dom_eq(b); }
-            bool operator()(cut const* a, cut const* b) const { return a->dom_eq(*b); }
-        };
-
-        struct dom_hash_proc {
-            unsigned operator()(cut const& a) const { return a.dom_hash(); }
-            unsigned operator()(cut const* a) const { return a->dom_hash(); }
-        };
-
-        unsigned operator[](unsigned idx) const {
-            return (idx >= m_size) ? UINT_MAX : m_elems[idx];
-        }
-
-        uint64_t shift_table(cut const& other) const;
-
-        bool merge(cut const& a, cut const& b) {
-            unsigned i = 0, j = 0;
-            unsigned x = a[i];
-            unsigned y = b[j];
-            while (x != UINT_MAX || y != UINT_MAX) {
-                if (!add(std::min(x, y))) {                    
-                    return false;
-                }
-                if (x < y) {
-                    x = a[++i];
-                }
-                else if (y < x) {
-                    y = b[++j];
-                }
-                else {
-                    x = a[++i];
-                    y = b[++j];
-                }
-            }
-            return true;
-        }
-
-        bool subset_of(cut const& other) const {
-            if (other.m_filter != (m_filter | other.m_filter)) {
-                return false;
-            }
-            unsigned i = 0;
-            unsigned other_id = other[i];
-            for (unsigned id : *this) {
-                while (id > other_id) {
-                    other_id = other[++i];
-                }
-                if (id != other_id) return false;
-                other_id = other[++i];
-            }
-            return true;
-        }
-
-        void remove_elem(unsigned i);
-
-        static uint64_t effect_mask(unsigned i);
-
-        std::ostream& display(std::ostream& out) const;
-
-        static std::ostream& display_table(std::ostream& out, unsigned num_input, uint64_t table);
-
-        static std::string table2string(unsigned num_input, uint64_t table);
-    };
-
-    class cut_set {
-        unsigned m_var;
-        region*  m_region;
-        unsigned m_size;
-        unsigned m_max_size;
-        cut *    m_cuts;
-    public:
-        typedef std::function<void(unsigned v, cut const& c)> on_update_t;
-
-        cut_set(): m_var(UINT_MAX), m_region(nullptr), m_size(0), m_max_size(0), m_cuts(nullptr) {}
-        void init(region& r, unsigned max_sz, unsigned v);
-        bool insert(on_update_t& on_add, on_update_t& on_del, cut const& c);
-        bool no_duplicates() const;
-        unsigned var() const { return m_var; }
-        unsigned size() const { return m_size; }
-        cut const * begin() const { return m_cuts; }
-        cut const * end() const { return m_cuts + m_size; }
-        cut const & back() { return m_cuts[m_size-1]; }
-        void push_back(on_update_t& on_add, cut const& c);
-        void reset(on_update_t& on_del) { shrink(on_del, 0); }
-        cut const & operator[](unsigned idx) const { return m_cuts[idx]; }
-        void shrink(on_update_t& on_del, unsigned j); 
-        void swap(cut_set& other) noexcept {
-            std::swap(m_var, other.m_var);
-            std::swap(m_size, other.m_size); 
-            std::swap(m_max_size, other.m_max_size); 
-            std::swap(m_cuts, other.m_cuts); 
-        }
-        void evict(on_update_t& on_del, unsigned idx);
-        void evict(on_update_t& on_del, cut const& c);
-
-        std::ostream& display(std::ostream& out) const;
-    };
-
-    inline std::ostream& operator<<(std::ostream& out, cut const& c) { return c.display(out); }
-    inline std::ostream& operator<<(std::ostream& out, cut_set const& cs) { return cs.display(out); }
-
-}
diff --git a/src/sat/sat_cutset_compute_shift.h b/src/sat/sat_cutset_compute_shift.h
deleted file mode 100644
index 45d2e1de8..000000000
--- a/src/sat/sat_cutset_compute_shift.h
+++ /dev/null
@@ -1,939 +0,0 @@
-/*++
-  Copyright (c) 2020 Microsoft Corporation
-
-  Module Name:
-
-   sat_cutset_compute_shift.h
-
-  Author:
-
-    Nikolaj Bjorner 2020-01-02
-
-  Notes:
-    
-    shifts truth table x using 'code'.
-    code encodes a mapping from bit-positions of the 
-    input truth table encoded with x into bit-positions
-    in the output truth table.
-    The truth table covers up to 6 inputs, which fits in 64 bits.
-
-  --*/
-#pragma once
-
-static uint64_t compute_shift(uint64_t x, unsigned code) {
-    switch (code) {
-#define _x0 (x & 1ull)
-#define _x1 _x0
-    case 1: return _x1;
-#define _x2 (_x1 | (_x1 << 1ull))
-    case 2: return _x2;
-#define _x3 (x & 3ull)
-#define _x4 _x3
-    case 3: return _x4;
-#define _x5 (_x2 | (_x2 << 2ull))
-    case 4: return _x5;
-#define _x6 (_x4 | (_x4 << 2ull))
-    case 5: return _x6;
-#define _x7 (x & 2ull)
-#define _x8 (_x7 << 1ull)
-#define _x9 (_x8 | (_x8 << 1ull))
-#define _x10 (_x2 | _x9)
-    case 6: return _x10;
-#define _x11 (x & 15ull)
-#define _x12 _x11
-    case 7: return _x12;
-#define _x13 (_x5 | (_x5 << 4ull))
-    case 8: return _x13;
-#define _x14 (_x6 | (_x6 << 4ull))
-    case 9: return _x14;
-#define _x15 (_x10 | (_x10 << 4ull))
-    case 10: return _x15;
-#define _x16 (_x12 | (_x12 << 4ull))
-    case 11: return _x16;
-#define _x17 (_x7 << 3ull)
-#define _x18 (_x17 | (_x17 << 1ull))
-#define _x19 (_x18 | (_x18 << 2ull))
-#define _x20 (_x5 | _x19)
-    case 12: return _x20;
-#define _x21 (x & 12ull)
-#define _x22 (_x21 << 2ull)
-#define _x23 (_x22 | (_x22 << 2ull))
-#define _x24 (_x6 | _x23)
-    case 13: return _x24;
-#define _x25 (x & 4ull)
-#define _x26 (_x25 << 2ull)
-#define _x27 (_x26 | (_x26 << 1ull))
-#define _x28 (x & 8ull)
-#define _x29 (_x28 << 3ull)
-#define _x30 (_x29 | (_x29 << 1ull))
-#define _x31 (_x27 | _x30)
-#define _x32 (_x10 | _x31)
-    case 14: return _x32;
-#define _x33 (x & 255ull)
-#define _x34 _x33
-    case 15: return _x34;
-#define _x35 (_x13 | (_x13 << 8ull))
-    case 16: return _x35;
-#define _x36 (_x14 | (_x14 << 8ull))
-    case 17: return _x36;
-#define _x37 (_x15 | (_x15 << 8ull))
-    case 18: return _x37;
-#define _x38 (_x16 | (_x16 << 8ull))
-    case 19: return _x38;
-#define _x39 (_x20 | (_x20 << 8ull))
-    case 20: return _x39;
-#define _x40 (_x24 | (_x24 << 8ull))
-    case 21: return _x40;
-#define _x41 (_x32 | (_x32 << 8ull))
-    case 22: return _x41;
-#define _x42 (_x34 | (_x34 << 8ull))
-    case 23: return _x42;
-#define _x43 (_x7 << 7ull)
-#define _x44 (_x43 | (_x43 << 1ull))
-#define _x45 (_x44 | (_x44 << 2ull))
-#define _x46 (_x45 | (_x45 << 4ull))
-#define _x47 (_x13 | _x46)
-    case 24: return _x47;
-#define _x48 (_x21 << 6ull)
-#define _x49 (_x48 | (_x48 << 2ull))
-#define _x50 (_x49 | (_x49 << 4ull))
-#define _x51 (_x14 | _x50)
-    case 25: return _x51;
-#define _x52 (_x25 << 6ull)
-#define _x53 (_x52 | (_x52 << 1ull))
-#define _x54 (_x28 << 7ull)
-#define _x55 (_x54 | (_x54 << 1ull))
-#define _x56 (_x53 | _x55)
-#define _x57 (_x56 | (_x56 << 4ull))
-#define _x58 (_x15 | _x57)
-    case 26: return _x58;
-#define _x59 (x & 240ull)
-#define _x60 (_x59 << 4ull)
-#define _x61 (_x60 | (_x60 << 4ull))
-#define _x62 (_x16 | _x61)
-    case 27: return _x62;
-#define _x63 (_x53 | (_x53 << 2ull))
-#define _x64 (_x28 << 9ull)
-#define _x65 (_x64 | (_x64 << 1ull))
-#define _x66 (_x65 | (_x65 << 2ull))
-#define _x67 (_x63 | _x66)
-#define _x68 (_x20 | _x67)
-    case 28: return _x68;
-#define _x69 (x & 48ull)
-#define _x70 (_x69 << 4ull)
-#define _x71 (_x70 | (_x70 << 2ull))
-#define _x72 (x & 192ull)
-#define _x73 (_x72 << 6ull)
-#define _x74 (_x73 | (_x73 << 2ull))
-#define _x75 (_x71 | _x74)
-#define _x76 (_x24 | _x75)
-    case 29: return _x76;
-#define _x77 (x & 16ull)
-#define _x78 (_x77 << 4ull)
-#define _x79 (_x78 | (_x78 << 1ull))
-#define _x80 (x & 32ull)
-#define _x81 (_x80 << 5ull)
-#define _x82 (_x81 | (_x81 << 1ull))
-#define _x83 (_x79 | _x82)
-#define _x84 (x & 64ull)
-#define _x85 (_x84 << 6ull)
-#define _x86 (_x85 | (_x85 << 1ull))
-#define _x87 (x & 128ull)
-#define _x88 (_x87 << 7ull)
-#define _x89 (_x88 | (_x88 << 1ull))
-#define _x90 (_x86 | _x89)
-#define _x91 (_x83 | _x90)
-#define _x92 (_x32 | _x91)
-    case 30: return _x92;
-#define _x93 (x & 65535ull)
-#define _x94 _x93
-    case 31: return _x94;
-#define _x95 (_x35 | (_x35 << 16ull))
-    case 32: return _x95;
-#define _x96 (_x36 | (_x36 << 16ull))
-    case 33: return _x96;
-#define _x97 (_x37 | (_x37 << 16ull))
-    case 34: return _x97;
-#define _x98 (_x38 | (_x38 << 16ull))
-    case 35: return _x98;
-#define _x99 (_x39 | (_x39 << 16ull))
-    case 36: return _x99;
-#define _x100 (_x40 | (_x40 << 16ull))
-    case 37: return _x100;
-#define _x101 (_x41 | (_x41 << 16ull))
-    case 38: return _x101;
-#define _x102 (_x42 | (_x42 << 16ull))
-    case 39: return _x102;
-#define _x103 (_x47 | (_x47 << 16ull))
-    case 40: return _x103;
-#define _x104 (_x51 | (_x51 << 16ull))
-    case 41: return _x104;
-#define _x105 (_x58 | (_x58 << 16ull))
-    case 42: return _x105;
-#define _x106 (_x62 | (_x62 << 16ull))
-    case 43: return _x106;
-#define _x107 (_x68 | (_x68 << 16ull))
-    case 44: return _x107;
-#define _x108 (_x76 | (_x76 << 16ull))
-    case 45: return _x108;
-#define _x109 (_x92 | (_x92 << 16ull))
-    case 46: return _x109;
-#define _x110 (_x94 | (_x94 << 16ull))
-    case 47: return _x110;
-#define _x111 (_x7 << 15ull)
-#define _x112 (_x111 | (_x111 << 1ull))
-#define _x113 (_x112 | (_x112 << 2ull))
-#define _x114 (_x113 | (_x113 << 4ull))
-#define _x115 (_x114 | (_x114 << 8ull))
-#define _x116 (_x35 | _x115)
-    case 48: return _x116;
-#define _x117 (_x21 << 14ull)
-#define _x118 (_x117 | (_x117 << 2ull))
-#define _x119 (_x118 | (_x118 << 4ull))
-#define _x120 (_x119 | (_x119 << 8ull))
-#define _x121 (_x36 | _x120)
-    case 49: return _x121;
-#define _x122 (_x25 << 14ull)
-#define _x123 (_x122 | (_x122 << 1ull))
-#define _x124 (_x28 << 15ull)
-#define _x125 (_x124 | (_x124 << 1ull))
-#define _x126 (_x123 | _x125)
-#define _x127 (_x126 | (_x126 << 4ull))
-#define _x128 (_x127 | (_x127 << 8ull))
-#define _x129 (_x37 | _x128)
-    case 50: return _x129;
-#define _x130 (_x59 << 12ull)
-#define _x131 (_x130 | (_x130 << 4ull))
-#define _x132 (_x131 | (_x131 << 8ull))
-#define _x133 (_x38 | _x132)
-    case 51: return _x133;
-#define _x134 (_x123 | (_x123 << 2ull))
-#define _x135 (_x28 << 17ull)
-#define _x136 (_x135 | (_x135 << 1ull))
-#define _x137 (_x136 | (_x136 << 2ull))
-#define _x138 (_x134 | _x137)
-#define _x139 (_x138 | (_x138 << 8ull))
-#define _x140 (_x39 | _x139)
-    case 52: return _x140;
-#define _x141 (_x69 << 12ull)
-#define _x142 (_x141 | (_x141 << 2ull))
-#define _x143 (_x72 << 14ull)
-#define _x144 (_x143 | (_x143 << 2ull))
-#define _x145 (_x142 | _x144)
-#define _x146 (_x145 | (_x145 << 8ull))
-#define _x147 (_x40 | _x146)
-    case 53: return _x147;
-#define _x148 (_x77 << 12ull)
-#define _x149 (_x148 | (_x148 << 1ull))
-#define _x150 (_x80 << 13ull)
-#define _x151 (_x150 | (_x150 << 1ull))
-#define _x152 (_x149 | _x151)
-#define _x153 (_x84 << 14ull)
-#define _x154 (_x153 | (_x153 << 1ull))
-#define _x155 (_x87 << 15ull)
-#define _x156 (_x155 | (_x155 << 1ull))
-#define _x157 (_x154 | _x156)
-#define _x158 (_x152 | _x157)
-#define _x159 (_x158 | (_x158 << 8ull))
-#define _x160 (_x41 | _x159)
-    case 54: return _x160;
-#define _x161 (x & 65280ull)
-#define _x162 (_x161 << 8ull)
-#define _x163 (_x162 | (_x162 << 8ull))
-#define _x164 (_x42 | _x163)
-    case 55: return _x164;
-#define _x165 (_x134 | (_x134 << 4ull))
-#define _x166 (_x28 << 21ull)
-#define _x167 (_x166 | (_x166 << 1ull))
-#define _x168 (_x167 | (_x167 << 2ull))
-#define _x169 (_x168 | (_x168 << 4ull))
-#define _x170 (_x165 | _x169)
-#define _x171 (_x47 | _x170)
-    case 56: return _x171;
-#define _x172 (_x142 | (_x142 << 4ull))
-#define _x173 (_x72 << 18ull)
-#define _x174 (_x173 | (_x173 << 2ull))
-#define _x175 (_x174 | (_x174 << 4ull))
-#define _x176 (_x172 | _x175)
-#define _x177 (_x51 | _x176)
-    case 57: return _x177;
-#define _x178 (_x152 | (_x152 << 4ull))
-#define _x179 (_x84 << 18ull)
-#define _x180 (_x179 | (_x179 << 1ull))
-#define _x181 (_x87 << 19ull)
-#define _x182 (_x181 | (_x181 << 1ull))
-#define _x183 (_x180 | _x182)
-#define _x184 (_x183 | (_x183 << 4ull))
-#define _x185 (_x178 | _x184)
-#define _x186 (_x58 | _x185)
-    case 58: return _x186;
-#define _x187 (x & 3840ull)
-#define _x188 (_x187 << 8ull)
-#define _x189 (_x188 | (_x188 << 4ull))
-#define _x190 (x & 61440ull)
-#define _x191 (_x190 << 12ull)
-#define _x192 (_x191 | (_x191 << 4ull))
-#define _x193 (_x189 | _x192)
-#define _x194 (_x62 | _x193)
-    case 59: return _x194;
-#define _x195 (_x149 | (_x149 << 2ull))
-#define _x196 (_x80 << 15ull)
-#define _x197 (_x196 | (_x196 << 1ull))
-#define _x198 (_x197 | (_x197 << 2ull))
-#define _x199 (_x195 | _x198)
-#define _x200 (_x180 | (_x180 << 2ull))
-#define _x201 (_x87 << 21ull)
-#define _x202 (_x201 | (_x201 << 1ull))
-#define _x203 (_x202 | (_x202 << 2ull))
-#define _x204 (_x200 | _x203)
-#define _x205 (_x199 | _x204)
-#define _x206 (_x68 | _x205)
-    case 60: return _x206;
-#define _x207 (x & 768ull)
-#define _x208 (_x207 << 8ull)
-#define _x209 (_x208 | (_x208 << 2ull))
-#define _x210 (x & 3072ull)
-#define _x211 (_x210 << 10ull)
-#define _x212 (_x211 | (_x211 << 2ull))
-#define _x213 (_x209 | _x212)
-#define _x214 (x & 12288ull)
-#define _x215 (_x214 << 12ull)
-#define _x216 (_x215 | (_x215 << 2ull))
-#define _x217 (x & 49152ull)
-#define _x218 (_x217 << 14ull)
-#define _x219 (_x218 | (_x218 << 2ull))
-#define _x220 (_x216 | _x219)
-#define _x221 (_x213 | _x220)
-#define _x222 (_x76 | _x221)
-    case 61: return _x222;
-#define _x223 (x & 256ull)
-#define _x224 (_x223 << 8ull)
-#define _x225 (_x224 | (_x224 << 1ull))
-#define _x226 (x & 512ull)
-#define _x227 (_x226 << 9ull)
-#define _x228 (_x227 | (_x227 << 1ull))
-#define _x229 (_x225 | _x228)
-#define _x230 (x & 1024ull)
-#define _x231 (_x230 << 10ull)
-#define _x232 (_x231 | (_x231 << 1ull))
-#define _x233 (x & 2048ull)
-#define _x234 (_x233 << 11ull)
-#define _x235 (_x234 | (_x234 << 1ull))
-#define _x236 (_x232 | _x235)
-#define _x237 (_x229 | _x236)
-#define _x238 (x & 4096ull)
-#define _x239 (_x238 << 12ull)
-#define _x240 (_x239 | (_x239 << 1ull))
-#define _x241 (x & 8192ull)
-#define _x242 (_x241 << 13ull)
-#define _x243 (_x242 | (_x242 << 1ull))
-#define _x244 (_x240 | _x243)
-#define _x245 (x & 16384ull)
-#define _x246 (_x245 << 14ull)
-#define _x247 (_x246 | (_x246 << 1ull))
-#define _x248 (x & 32768ull)
-#define _x249 (_x248 << 15ull)
-#define _x250 (_x249 | (_x249 << 1ull))
-#define _x251 (_x247 | _x250)
-#define _x252 (_x244 | _x251)
-#define _x253 (_x237 | _x252)
-#define _x254 (_x92 | _x253)
-    case 62: return _x254;
-#define _x255 (x & 4294967295ull)
-#define _x256 _x255
-    case 63: return _x256;
-#define _x257 (_x95 | (_x95 << 32ull))
-    case 64: return _x257;
-#define _x258 (_x96 | (_x96 << 32ull))
-    case 65: return _x258;
-#define _x259 (_x97 | (_x97 << 32ull))
-    case 66: return _x259;
-#define _x260 (_x98 | (_x98 << 32ull))
-    case 67: return _x260;
-#define _x261 (_x99 | (_x99 << 32ull))
-    case 68: return _x261;
-#define _x262 (_x100 | (_x100 << 32ull))
-    case 69: return _x262;
-#define _x263 (_x101 | (_x101 << 32ull))
-    case 70: return _x263;
-#define _x264 (_x102 | (_x102 << 32ull))
-    case 71: return _x264;
-#define _x265 (_x103 | (_x103 << 32ull))
-    case 72: return _x265;
-#define _x266 (_x104 | (_x104 << 32ull))
-    case 73: return _x266;
-#define _x267 (_x105 | (_x105 << 32ull))
-    case 74: return _x267;
-#define _x268 (_x106 | (_x106 << 32ull))
-    case 75: return _x268;
-#define _x269 (_x107 | (_x107 << 32ull))
-    case 76: return _x269;
-#define _x270 (_x108 | (_x108 << 32ull))
-    case 77: return _x270;
-#define _x271 (_x109 | (_x109 << 32ull))
-    case 78: return _x271;
-#define _x272 (_x110 | (_x110 << 32ull))
-    case 79: return _x272;
-#define _x273 (_x116 | (_x116 << 32ull))
-    case 80: return _x273;
-#define _x274 (_x121 | (_x121 << 32ull))
-    case 81: return _x274;
-#define _x275 (_x129 | (_x129 << 32ull))
-    case 82: return _x275;
-#define _x276 (_x133 | (_x133 << 32ull))
-    case 83: return _x276;
-#define _x277 (_x140 | (_x140 << 32ull))
-    case 84: return _x277;
-#define _x278 (_x147 | (_x147 << 32ull))
-    case 85: return _x278;
-#define _x279 (_x160 | (_x160 << 32ull))
-    case 86: return _x279;
-#define _x280 (_x164 | (_x164 << 32ull))
-    case 87: return _x280;
-#define _x281 (_x171 | (_x171 << 32ull))
-    case 88: return _x281;
-#define _x282 (_x177 | (_x177 << 32ull))
-    case 89: return _x282;
-#define _x283 (_x186 | (_x186 << 32ull))
-    case 90: return _x283;
-#define _x284 (_x194 | (_x194 << 32ull))
-    case 91: return _x284;
-#define _x285 (_x206 | (_x206 << 32ull))
-    case 92: return _x285;
-#define _x286 (_x222 | (_x222 << 32ull))
-    case 93: return _x286;
-#define _x287 (_x254 | (_x254 << 32ull))
-    case 94: return _x287;
-#define _x288 (_x256 | (_x256 << 32ull))
-    case 95: return _x288;
-#define _x289 (_x7 << 31ull)
-#define _x290 (_x289 | (_x289 << 1ull))
-#define _x291 (_x290 | (_x290 << 2ull))
-#define _x292 (_x291 | (_x291 << 4ull))
-#define _x293 (_x292 | (_x292 << 8ull))
-#define _x294 (_x293 | (_x293 << 16ull))
-#define _x295 (_x95 | _x294)
-    case 96: return _x295;
-#define _x296 (_x21 << 30ull)
-#define _x297 (_x296 | (_x296 << 2ull))
-#define _x298 (_x297 | (_x297 << 4ull))
-#define _x299 (_x298 | (_x298 << 8ull))
-#define _x300 (_x299 | (_x299 << 16ull))
-#define _x301 (_x96 | _x300)
-    case 97: return _x301;
-#define _x302 (_x25 << 30ull)
-#define _x303 (_x302 | (_x302 << 1ull))
-#define _x304 (_x28 << 31ull)
-#define _x305 (_x304 | (_x304 << 1ull))
-#define _x306 (_x303 | _x305)
-#define _x307 (_x306 | (_x306 << 4ull))
-#define _x308 (_x307 | (_x307 << 8ull))
-#define _x309 (_x308 | (_x308 << 16ull))
-#define _x310 (_x97 | _x309)
-    case 98: return _x310;
-#define _x311 (_x59 << 28ull)
-#define _x312 (_x311 | (_x311 << 4ull))
-#define _x313 (_x312 | (_x312 << 8ull))
-#define _x314 (_x313 | (_x313 << 16ull))
-#define _x315 (_x98 | _x314)
-    case 99: return _x315;
-#define _x316 (_x303 | (_x303 << 2ull))
-#define _x317 (_x28 << 33ull)
-#define _x318 (_x317 | (_x317 << 1ull))
-#define _x319 (_x318 | (_x318 << 2ull))
-#define _x320 (_x316 | _x319)
-#define _x321 (_x320 | (_x320 << 8ull))
-#define _x322 (_x321 | (_x321 << 16ull))
-#define _x323 (_x99 | _x322)
-    case 100: return _x323;
-#define _x324 (_x69 << 28ull)
-#define _x325 (_x324 | (_x324 << 2ull))
-#define _x326 (_x72 << 30ull)
-#define _x327 (_x326 | (_x326 << 2ull))
-#define _x328 (_x325 | _x327)
-#define _x329 (_x328 | (_x328 << 8ull))
-#define _x330 (_x329 | (_x329 << 16ull))
-#define _x331 (_x100 | _x330)
-    case 101: return _x331;
-#define _x332 (_x77 << 28ull)
-#define _x333 (_x332 | (_x332 << 1ull))
-#define _x334 (_x80 << 29ull)
-#define _x335 (_x334 | (_x334 << 1ull))
-#define _x336 (_x333 | _x335)
-#define _x337 (_x84 << 30ull)
-#define _x338 (_x337 | (_x337 << 1ull))
-#define _x339 (_x87 << 31ull)
-#define _x340 (_x339 | (_x339 << 1ull))
-#define _x341 (_x338 | _x340)
-#define _x342 (_x336 | _x341)
-#define _x343 (_x342 | (_x342 << 8ull))
-#define _x344 (_x343 | (_x343 << 16ull))
-#define _x345 (_x101 | _x344)
-    case 102: return _x345;
-#define _x346 (_x161 << 24ull)
-#define _x347 (_x346 | (_x346 << 8ull))
-#define _x348 (_x347 | (_x347 << 16ull))
-#define _x349 (_x102 | _x348)
-    case 103: return _x349;
-#define _x350 (_x316 | (_x316 << 4ull))
-#define _x351 (_x28 << 37ull)
-#define _x352 (_x351 | (_x351 << 1ull))
-#define _x353 (_x352 | (_x352 << 2ull))
-#define _x354 (_x353 | (_x353 << 4ull))
-#define _x355 (_x350 | _x354)
-#define _x356 (_x355 | (_x355 << 16ull))
-#define _x357 (_x103 | _x356)
-    case 104: return _x357;
-#define _x358 (_x325 | (_x325 << 4ull))
-#define _x359 (_x72 << 34ull)
-#define _x360 (_x359 | (_x359 << 2ull))
-#define _x361 (_x360 | (_x360 << 4ull))
-#define _x362 (_x358 | _x361)
-#define _x363 (_x362 | (_x362 << 16ull))
-#define _x364 (_x104 | _x363)
-    case 105: return _x364;
-#define _x365 (_x336 | (_x336 << 4ull))
-#define _x366 (_x84 << 34ull)
-#define _x367 (_x366 | (_x366 << 1ull))
-#define _x368 (_x87 << 35ull)
-#define _x369 (_x368 | (_x368 << 1ull))
-#define _x370 (_x367 | _x369)
-#define _x371 (_x370 | (_x370 << 4ull))
-#define _x372 (_x365 | _x371)
-#define _x373 (_x372 | (_x372 << 16ull))
-#define _x374 (_x105 | _x373)
-    case 106: return _x374;
-#define _x375 (_x187 << 24ull)
-#define _x376 (_x375 | (_x375 << 4ull))
-#define _x377 (_x190 << 28ull)
-#define _x378 (_x377 | (_x377 << 4ull))
-#define _x379 (_x376 | _x378)
-#define _x380 (_x379 | (_x379 << 16ull))
-#define _x381 (_x106 | _x380)
-    case 107: return _x381;
-#define _x382 (_x333 | (_x333 << 2ull))
-#define _x383 (_x80 << 31ull)
-#define _x384 (_x383 | (_x383 << 1ull))
-#define _x385 (_x384 | (_x384 << 2ull))
-#define _x386 (_x382 | _x385)
-#define _x387 (_x367 | (_x367 << 2ull))
-#define _x388 (_x87 << 37ull)
-#define _x389 (_x388 | (_x388 << 1ull))
-#define _x390 (_x389 | (_x389 << 2ull))
-#define _x391 (_x387 | _x390)
-#define _x392 (_x386 | _x391)
-#define _x393 (_x392 | (_x392 << 16ull))
-#define _x394 (_x107 | _x393)
-    case 108: return _x394;
-#define _x395 (_x207 << 24ull)
-#define _x396 (_x395 | (_x395 << 2ull))
-#define _x397 (_x210 << 26ull)
-#define _x398 (_x397 | (_x397 << 2ull))
-#define _x399 (_x396 | _x398)
-#define _x400 (_x214 << 28ull)
-#define _x401 (_x400 | (_x400 << 2ull))
-#define _x402 (_x217 << 30ull)
-#define _x403 (_x402 | (_x402 << 2ull))
-#define _x404 (_x401 | _x403)
-#define _x405 (_x399 | _x404)
-#define _x406 (_x405 | (_x405 << 16ull))
-#define _x407 (_x108 | _x406)
-    case 109: return _x407;
-#define _x408 (_x223 << 24ull)
-#define _x409 (_x408 | (_x408 << 1ull))
-#define _x410 (_x226 << 25ull)
-#define _x411 (_x410 | (_x410 << 1ull))
-#define _x412 (_x409 | _x411)
-#define _x413 (_x230 << 26ull)
-#define _x414 (_x413 | (_x413 << 1ull))
-#define _x415 (_x233 << 27ull)
-#define _x416 (_x415 | (_x415 << 1ull))
-#define _x417 (_x414 | _x416)
-#define _x418 (_x412 | _x417)
-#define _x419 (_x238 << 28ull)
-#define _x420 (_x419 | (_x419 << 1ull))
-#define _x421 (_x241 << 29ull)
-#define _x422 (_x421 | (_x421 << 1ull))
-#define _x423 (_x420 | _x422)
-#define _x424 (_x245 << 30ull)
-#define _x425 (_x424 | (_x424 << 1ull))
-#define _x426 (_x248 << 31ull)
-#define _x427 (_x426 | (_x426 << 1ull))
-#define _x428 (_x425 | _x427)
-#define _x429 (_x423 | _x428)
-#define _x430 (_x418 | _x429)
-#define _x431 (_x430 | (_x430 << 16ull))
-#define _x432 (_x109 | _x431)
-    case 110: return _x432;
-#define _x433 (x & 4294901760ull)
-#define _x434 (_x433 << 16ull)
-#define _x435 (_x434 | (_x434 << 16ull))
-#define _x436 (_x110 | _x435)
-    case 111: return _x436;
-#define _x437 (_x350 | (_x350 << 8ull))
-#define _x438 (_x28 << 45ull)
-#define _x439 (_x438 | (_x438 << 1ull))
-#define _x440 (_x439 | (_x439 << 2ull))
-#define _x441 (_x440 | (_x440 << 4ull))
-#define _x442 (_x441 | (_x441 << 8ull))
-#define _x443 (_x437 | _x442)
-#define _x444 (_x116 | _x443)
-    case 112: return _x444;
-#define _x445 (_x358 | (_x358 << 8ull))
-#define _x446 (_x72 << 42ull)
-#define _x447 (_x446 | (_x446 << 2ull))
-#define _x448 (_x447 | (_x447 << 4ull))
-#define _x449 (_x448 | (_x448 << 8ull))
-#define _x450 (_x445 | _x449)
-#define _x451 (_x121 | _x450)
-    case 113: return _x451;
-#define _x452 (_x365 | (_x365 << 8ull))
-#define _x453 (_x84 << 42ull)
-#define _x454 (_x453 | (_x453 << 1ull))
-#define _x455 (_x87 << 43ull)
-#define _x456 (_x455 | (_x455 << 1ull))
-#define _x457 (_x454 | _x456)
-#define _x458 (_x457 | (_x457 << 4ull))
-#define _x459 (_x458 | (_x458 << 8ull))
-#define _x460 (_x452 | _x459)
-#define _x461 (_x129 | _x460)
-    case 114: return _x461;
-#define _x462 (_x376 | (_x376 << 8ull))
-#define _x463 (_x190 << 36ull)
-#define _x464 (_x463 | (_x463 << 4ull))
-#define _x465 (_x464 | (_x464 << 8ull))
-#define _x466 (_x462 | _x465)
-#define _x467 (_x133 | _x466)
-    case 115: return _x467;
-#define _x468 (_x386 | (_x386 << 8ull))
-#define _x469 (_x454 | (_x454 << 2ull))
-#define _x470 (_x87 << 45ull)
-#define _x471 (_x470 | (_x470 << 1ull))
-#define _x472 (_x471 | (_x471 << 2ull))
-#define _x473 (_x469 | _x472)
-#define _x474 (_x473 | (_x473 << 8ull))
-#define _x475 (_x468 | _x474)
-#define _x476 (_x140 | _x475)
-    case 116: return _x476;
-#define _x477 (_x399 | (_x399 << 8ull))
-#define _x478 (_x214 << 36ull)
-#define _x479 (_x478 | (_x478 << 2ull))
-#define _x480 (_x217 << 38ull)
-#define _x481 (_x480 | (_x480 << 2ull))
-#define _x482 (_x479 | _x481)
-#define _x483 (_x482 | (_x482 << 8ull))
-#define _x484 (_x477 | _x483)
-#define _x485 (_x147 | _x484)
-    case 117: return _x485;
-#define _x486 (_x418 | (_x418 << 8ull))
-#define _x487 (_x238 << 36ull)
-#define _x488 (_x487 | (_x487 << 1ull))
-#define _x489 (_x241 << 37ull)
-#define _x490 (_x489 | (_x489 << 1ull))
-#define _x491 (_x488 | _x490)
-#define _x492 (_x245 << 38ull)
-#define _x493 (_x492 | (_x492 << 1ull))
-#define _x494 (_x248 << 39ull)
-#define _x495 (_x494 | (_x494 << 1ull))
-#define _x496 (_x493 | _x495)
-#define _x497 (_x491 | _x496)
-#define _x498 (_x497 | (_x497 << 8ull))
-#define _x499 (_x486 | _x498)
-#define _x500 (_x160 | _x499)
-    case 118: return _x500;
-#define _x501 (x & 16711680ull)
-#define _x502 (_x501 << 16ull)
-#define _x503 (_x502 | (_x502 << 8ull))
-#define _x504 (x & 4278190080ull)
-#define _x505 (_x504 << 24ull)
-#define _x506 (_x505 | (_x505 << 8ull))
-#define _x507 (_x503 | _x506)
-#define _x508 (_x164 | _x507)
-    case 119: return _x508;
-#define _x509 (_x382 | (_x382 << 4ull))
-#define _x510 (_x80 << 35ull)
-#define _x511 (_x510 | (_x510 << 1ull))
-#define _x512 (_x511 | (_x511 << 2ull))
-#define _x513 (_x512 | (_x512 << 4ull))
-#define _x514 (_x509 | _x513)
-#define _x515 (_x469 | (_x469 << 4ull))
-#define _x516 (_x87 << 49ull)
-#define _x517 (_x516 | (_x516 << 1ull))
-#define _x518 (_x517 | (_x517 << 2ull))
-#define _x519 (_x518 | (_x518 << 4ull))
-#define _x520 (_x515 | _x519)
-#define _x521 (_x514 | _x520)
-#define _x522 (_x171 | _x521)
-    case 120: return _x522;
-#define _x523 (_x396 | (_x396 << 4ull))
-#define _x524 (_x210 << 30ull)
-#define _x525 (_x524 | (_x524 << 2ull))
-#define _x526 (_x525 | (_x525 << 4ull))
-#define _x527 (_x523 | _x526)
-#define _x528 (_x479 | (_x479 << 4ull))
-#define _x529 (_x217 << 42ull)
-#define _x530 (_x529 | (_x529 << 2ull))
-#define _x531 (_x530 | (_x530 << 4ull))
-#define _x532 (_x528 | _x531)
-#define _x533 (_x527 | _x532)
-#define _x534 (_x177 | _x533)
-    case 121: return _x534;
-#define _x535 (_x412 | (_x412 << 4ull))
-#define _x536 (_x230 << 30ull)
-#define _x537 (_x536 | (_x536 << 1ull))
-#define _x538 (_x233 << 31ull)
-#define _x539 (_x538 | (_x538 << 1ull))
-#define _x540 (_x537 | _x539)
-#define _x541 (_x540 | (_x540 << 4ull))
-#define _x542 (_x535 | _x541)
-#define _x543 (_x491 | (_x491 << 4ull))
-#define _x544 (_x245 << 42ull)
-#define _x545 (_x544 | (_x544 << 1ull))
-#define _x546 (_x248 << 43ull)
-#define _x547 (_x546 | (_x546 << 1ull))
-#define _x548 (_x545 | _x547)
-#define _x549 (_x548 | (_x548 << 4ull))
-#define _x550 (_x543 | _x549)
-#define _x551 (_x542 | _x550)
-#define _x552 (_x186 | _x551)
-    case 122: return _x552;
-#define _x553 (x & 983040ull)
-#define _x554 (_x553 << 16ull)
-#define _x555 (_x554 | (_x554 << 4ull))
-#define _x556 (x & 15728640ull)
-#define _x557 (_x556 << 20ull)
-#define _x558 (_x557 | (_x557 << 4ull))
-#define _x559 (_x555 | _x558)
-#define _x560 (x & 251658240ull)
-#define _x561 (_x560 << 24ull)
-#define _x562 (_x561 | (_x561 << 4ull))
-#define _x563 (x & 4026531840ull)
-#define _x564 (_x563 << 28ull)
-#define _x565 (_x564 | (_x564 << 4ull))
-#define _x566 (_x562 | _x565)
-#define _x567 (_x559 | _x566)
-#define _x568 (_x194 | _x567)
-    case 123: return _x568;
-#define _x569 (_x409 | (_x409 << 2ull))
-#define _x570 (_x226 << 27ull)
-#define _x571 (_x570 | (_x570 << 1ull))
-#define _x572 (_x571 | (_x571 << 2ull))
-#define _x573 (_x569 | _x572)
-#define _x574 (_x537 | (_x537 << 2ull))
-#define _x575 (_x233 << 33ull)
-#define _x576 (_x575 | (_x575 << 1ull))
-#define _x577 (_x576 | (_x576 << 2ull))
-#define _x578 (_x574 | _x577)
-#define _x579 (_x573 | _x578)
-#define _x580 (_x488 | (_x488 << 2ull))
-#define _x581 (_x241 << 39ull)
-#define _x582 (_x581 | (_x581 << 1ull))
-#define _x583 (_x582 | (_x582 << 2ull))
-#define _x584 (_x580 | _x583)
-#define _x585 (_x545 | (_x545 << 2ull))
-#define _x586 (_x248 << 45ull)
-#define _x587 (_x586 | (_x586 << 1ull))
-#define _x588 (_x587 | (_x587 << 2ull))
-#define _x589 (_x585 | _x588)
-#define _x590 (_x584 | _x589)
-#define _x591 (_x579 | _x590)
-#define _x592 (_x206 | _x591)
-    case 124: return _x592;
-#define _x593 (x & 196608ull)
-#define _x594 (_x593 << 16ull)
-#define _x595 (_x594 | (_x594 << 2ull))
-#define _x596 (x & 786432ull)
-#define _x597 (_x596 << 18ull)
-#define _x598 (_x597 | (_x597 << 2ull))
-#define _x599 (_x595 | _x598)
-#define _x600 (x & 3145728ull)
-#define _x601 (_x600 << 20ull)
-#define _x602 (_x601 | (_x601 << 2ull))
-#define _x603 (x & 12582912ull)
-#define _x604 (_x603 << 22ull)
-#define _x605 (_x604 | (_x604 << 2ull))
-#define _x606 (_x602 | _x605)
-#define _x607 (_x599 | _x606)
-#define _x608 (x & 50331648ull)
-#define _x609 (_x608 << 24ull)
-#define _x610 (_x609 | (_x609 << 2ull))
-#define _x611 (x & 201326592ull)
-#define _x612 (_x611 << 26ull)
-#define _x613 (_x612 | (_x612 << 2ull))
-#define _x614 (_x610 | _x613)
-#define _x615 (x & 805306368ull)
-#define _x616 (_x615 << 28ull)
-#define _x617 (_x616 | (_x616 << 2ull))
-#define _x618 (x & 3221225472ull)
-#define _x619 (_x618 << 30ull)
-#define _x620 (_x619 | (_x619 << 2ull))
-#define _x621 (_x617 | _x620)
-#define _x622 (_x614 | _x621)
-#define _x623 (_x607 | _x622)
-#define _x624 (_x222 | _x623)
-    case 125: return _x624;
-#define _x625 (x & 65536ull)
-#define _x626 (_x625 << 16ull)
-#define _x627 (_x626 | (_x626 << 1ull))
-#define _x628 (x & 131072ull)
-#define _x629 (_x628 << 17ull)
-#define _x630 (_x629 | (_x629 << 1ull))
-#define _x631 (_x627 | _x630)
-#define _x632 (x & 262144ull)
-#define _x633 (_x632 << 18ull)
-#define _x634 (_x633 | (_x633 << 1ull))
-#define _x635 (x & 524288ull)
-#define _x636 (_x635 << 19ull)
-#define _x637 (_x636 | (_x636 << 1ull))
-#define _x638 (_x634 | _x637)
-#define _x639 (_x631 | _x638)
-#define _x640 (x & 1048576ull)
-#define _x641 (_x640 << 20ull)
-#define _x642 (_x641 | (_x641 << 1ull))
-#define _x643 (x & 2097152ull)
-#define _x644 (_x643 << 21ull)
-#define _x645 (_x644 | (_x644 << 1ull))
-#define _x646 (_x642 | _x645)
-#define _x647 (x & 4194304ull)
-#define _x648 (_x647 << 22ull)
-#define _x649 (_x648 | (_x648 << 1ull))
-#define _x650 (x & 8388608ull)
-#define _x651 (_x650 << 23ull)
-#define _x652 (_x651 | (_x651 << 1ull))
-#define _x653 (_x649 | _x652)
-#define _x654 (_x646 | _x653)
-#define _x655 (_x639 | _x654)
-#define _x656 (x & 16777216ull)
-#define _x657 (_x656 << 24ull)
-#define _x658 (_x657 | (_x657 << 1ull))
-#define _x659 (x & 33554432ull)
-#define _x660 (_x659 << 25ull)
-#define _x661 (_x660 | (_x660 << 1ull))
-#define _x662 (_x658 | _x661)
-#define _x663 (x & 67108864ull)
-#define _x664 (_x663 << 26ull)
-#define _x665 (_x664 | (_x664 << 1ull))
-#define _x666 (x & 134217728ull)
-#define _x667 (_x666 << 27ull)
-#define _x668 (_x667 | (_x667 << 1ull))
-#define _x669 (_x665 | _x668)
-#define _x670 (_x662 | _x669)
-#define _x671 (x & 268435456ull)
-#define _x672 (_x671 << 28ull)
-#define _x673 (_x672 | (_x672 << 1ull))
-#define _x674 (x & 536870912ull)
-#define _x675 (_x674 << 29ull)
-#define _x676 (_x675 | (_x675 << 1ull))
-#define _x677 (_x673 | _x676)
-#define _x678 (x & 1073741824ull)
-#define _x679 (_x678 << 30ull)
-#define _x680 (_x679 | (_x679 << 1ull))
-#define _x681 (x & 2147483648ull)
-#define _x682 (_x681 << 31ull)
-#define _x683 (_x682 | (_x682 << 1ull))
-#define _x684 (_x680 | _x683)
-#define _x685 (_x677 | _x684)
-#define _x686 (_x670 | _x685)
-#define _x687 (_x655 | _x686)
-#define _x688 (_x254 | _x687)
-    case 126: return _x688;
-    case 127: return x;
-    default:
-        UNREACHABLE();
-        return 0;
-    }
-}
-
-
-#if 0
-
-def consecutive(S):
-    for k in range(len(S)-1):
-        if S[k] + 1 != S[k+1]:
-            return False
-    return True
-
-def shift(x, k):
-    if k == 0:
-        return x
-    if k < 0:
-        return "(%s >> %dull)" % (x,-k)
-    return "(%s << %dull)" % (x, k)
-
-def hash(r, hashcons):
-    if r in hashcons:
-        return hashcons[r]
-    id = "_x%d" % len(hashcons)
-    print ("#define %s %s" % (id, r))
-    hashcons[r] = id
-    return id
-
-def compile(S, offset, hashcons):
-    if consecutive(S):
-        k = S[0]
-        l = len(S)
-        if l == 64:
-            return "x"
-        mask = ((1 << l)-1) << k
-        return hash(shift(hash("(x & %dull)" % mask, hashcons), offset - k), hashcons)
-    l2 = len(S) >> 1
-    S1 = S[0:l2]
-    S2 = S[l2:]
-    if S1 == S2:
-        r1 = compile(S1, offset, hashcons)        
-        return hash("(%s | (%s << %dull))" % (r1, r1, l2), hashcons)
-    r1 = compile(S1, offset, hashcons)
-    r2 = compile(S2, offset + l2, hashcons)
-    return hash("(%s | %s)" % (r1, r2), hashcons)
-
-def mems2index(mems, bound):
-    k = 0
-    i = 0
-    for m in mems:
-        if m:
-            k |= (1 << i)
-        i += 1
-    k |= (1 << i)
-    return k
-
-def precompute(mems, bound, hashcons):
-    K = 0
-    j = 0
-    coeff = {}
-    deficit = {}
-    for m in mems:
-        if m:
-            coeff[K] = (1 << j)
-            deficit[K] = j - K
-            K += 1
-        j += 1
-    indices = []
-    for j in range(1 << len(mems)):
-        k = 0
-        for i in range(K):
-            if 0 != (j & coeff[i]):
-                k += (1 << i)
-        indices += [k]
-    idx = mems2index(mems, bound)
-    instr = compile(indices, 0, hashcons)
-    print("    case %d: return %s;" % (idx, instr))
-
-def create_mems(mems, n):
-    if n == 0:
-        return ([], mems)
-    prefix, m1 = create_mems(mems, n - 1)
-    m2 = [m + [False] for m in m1]
-    m3 = [m + [True] for m in m1]
-    return prefix + m1, m2 + m3
-
-def combinations(n, m, hashcons):
-    prefix, S = create_mems([[]], 6)
-    mems = prefix + S
-    for mem in mems:
-        precompute(mem, m, hashcons)
-
-hashcons = {}
-combinations(7, 7, hashcons)
-        
-#endif
-
diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
index 7c39f5f41..2836d1130 100644
--- a/src/sat/sat_drat.h
+++ b/src/sat/sat_drat.h
@@ -21,7 +21,8 @@ Notes:
 --*/
 #pragma once
 
-#include "sat_types.h"
+#include "sat/sat_types.h"
+#include "sat/sat_clause.h"
 
 namespace sat {
     class justification;
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index 8ec2992c9..05e0fc3a8 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -229,9 +229,6 @@ namespace sat {
             literal r  = roots[v];
             SASSERT(v != r.var());
 
-            if (m_solver.m_cut_simplifier)
-                m_solver.m_cut_simplifier->set_root(v, r);
-
             bool set_root = m_solver.set_root(l, r);
             TRACE(elim_eqs, tout << l << " " << r << "\n";);
             if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !set_root))) {
diff --git a/src/sat/sat_lut_finder.cpp b/src/sat/sat_lut_finder.cpp
deleted file mode 100644
index 0e683eade..000000000
--- a/src/sat/sat_lut_finder.cpp
+++ /dev/null
@@ -1,289 +0,0 @@
-/*++
-  Copyright (c) 2020 Microsoft Corporation
-
-  Module Name:
-
-   sat_lut_finder.cpp
-
-  Abstract:
-   
-    lut finder
-
-  Author:
-
-    Nikolaj Bjorner 2020-01-02
-
-  Notes:
-  
-
-  --*/
-
-#include "sat/sat_lut_finder.h"
-#include "sat/sat_solver.h"
-
-namespace sat {
-
-    void lut_finder::operator()(clause_vector& clauses) {
-        m_removed_clauses.reset();
-        unsigned max_size = m_max_lut_size;
-        // we better have enough bits in the combination mask to 
-        // handle clauses up to max_size.
-        // max_size = 5 -> 32 bits
-        // max_size = 6 -> 64 bits
-        SASSERT(sizeof(m_combination)*8 >= (1ull << static_cast<uint64_t>(max_size)));
-        init_clause_filter();
-        for (unsigned i = 0; i <= 6; ++i) {
-            m_masks[i] = cut::effect_mask(i);
-        }
-        m_var_position.resize(s.num_vars());
-        for (clause* cp : clauses) {
-            cp->unmark_used();
-        }
-        for (; max_size > 2; --max_size) {
-            for (clause* cp : clauses) {
-                clause& c = *cp;
-                if (c.size() == max_size && !c.was_removed() && !c.is_learned() && !c.was_used()) {
-                    check_lut(c);
-                }
-            }
-        }
-        m_clause_filters.clear();
-        
-        for (clause* cp : clauses) cp->unmark_used();
-        for (clause* cp : m_removed_clauses) cp->mark_used();
-        std::function<bool(clause*)> not_used = [](clause* cp) { return !cp->was_used(); };
-        clauses.filter_update(not_used);
-    }
-
-    void lut_finder::check_lut(clause& c) {
-        SASSERT(c.size() > 2);
-        unsigned filter = get_clause_filter(c);
-        s.init_visited();
-        unsigned mask = 0, i = 0;        
-        m_vars.reset();
-        m_clause.reset();
-        for (literal l : c) {
-            m_clause.push_back(l);
-        }
-        // ensure that variables in returned LUT are sorted
-        std::sort(m_clause.begin(), m_clause.end());
-        for (literal l : m_clause) {
-            m_vars.push_back(l.var());
-            m_var_position[l.var()] = i;
-            s.mark_visited(l.var());
-            mask |= (l.sign() << (i++)); 
-        }
-        m_clauses_to_remove.reset();
-        m_clauses_to_remove.push_back(&c);
-        m_combination = 0;
-        m_num_combinations = 0;
-        set_combination(mask);
-        c.mark_used();
-        for (literal l : c) {
-            for (auto const& cf : m_clause_filters[l.var()]) {                
-                if ((filter == (filter | cf.m_filter)) && 
-                    !cf.m_clause->was_used() &&
-                    extract_lut(*cf.m_clause)) {
-                    add_lut();
-                    return;
-                }
-            }
-            // TBD: replace by BIG
-            // loop over binary clauses in watch list
-            for (watched const & w : s.get_wlist(l)) {
-                if (w.is_binary_clause() && s.is_visited(w.get_literal().var()) && w.get_literal().index() < l.index()) {
-                    if (extract_lut(~l, w.get_literal())) {
-                        add_lut();
-                        return;
-                    }
-                }
-            }
-            l.neg();
-            for (watched const & w : s.get_wlist(l)) {
-                if (w.is_binary_clause() && s.is_visited(w.get_literal().var()) && w.get_literal().index() < l.index()) {
-                    if (extract_lut(~l, w.get_literal())) {
-                        add_lut();
-                        return;
-                    }
-                }
-            }
-        }
-    }
-
-    void lut_finder::add_lut() {
-        DEBUG_CODE(for (clause* cp : m_clauses_to_remove) VERIFY(cp->was_used()););
-        m_removed_clauses.append(m_clauses_to_remove);
-        bool_var v;
-        uint64_t lut = convert_combination(m_vars, v);
-        TRACE(aig_simplifier,
-              for (clause* cp : m_clauses_to_remove) {
-                  tout << *cp << "\n" << v << ": " << m_vars << "\n";
-              }
-              display_mask(tout, lut, 1u << m_vars.size()) << "\n";);
-        m_on_lut(lut, m_vars, v);
-    }
-
-    bool lut_finder::extract_lut(literal l1, literal l2) {
-        SASSERT(s.m_visited.is_visited(l1.var()));
-        SASSERT(s.m_visited.is_visited(l2.var()));
-        m_missing.reset();
-        unsigned mask = 0;
-        for (unsigned i = 0; i < m_vars.size(); ++i) {
-            if (m_vars[i] == l1.var()) {
-                mask |= (l1.sign() << i);
-            }
-            else if (m_vars[i] == l2.var()) {
-                mask |= (l2.sign() << i);
-            }
-            else {
-                m_missing.push_back(i);
-            }
-        }
-        return update_combinations(mask);
-    }
-
-    bool lut_finder::extract_lut(clause& c2) {
-        for (literal l : c2) {            
-            if (!s.is_visited(l.var())) 
-                return false;
-        }
-        if (c2.size() == m_vars.size()) {
-            m_clauses_to_remove.push_back(&c2);
-            c2.mark_used();
-        }
-        // insert missing
-        unsigned mask = 0;
-        m_missing.reset();
-        SASSERT(c2.size() <= m_vars.size());
-        for (unsigned i = 0; i < m_vars.size(); ++i) {
-            m_clause[i] = null_literal;
-        }
-        for (literal l : c2) {
-            unsigned pos = m_var_position[l.var()];
-            m_clause[pos] = l;
-        }
-        for (unsigned j = 0; j < m_vars.size(); ++j) {
-            literal lit = m_clause[j];
-            if (lit == null_literal) {
-                m_missing.push_back(j);
-            }
-            else {
-                mask |= (m_clause[j].sign() << j);
-            }
-        }                    
-        return update_combinations(mask);
-    }
-
-    void lut_finder::set_combination(unsigned mask) {
-        if (!get_combination(mask)) { 
-            m_combination |= (1ull << mask); 
-            m_num_combinations++;
-        }
-    }
-
-    bool lut_finder::update_combinations(unsigned mask) {
-        unsigned num_missing = m_missing.size();
-        for (unsigned k = 0; k < (1ul << num_missing); ++k) {
-            unsigned mask2 = mask;
-            for (unsigned i = 0; i < num_missing; ++i) {
-                if ((k & (1 << i)) != 0) {
-                    mask2 |= 1ul << m_missing[i];
-                }
-            }
-            set_combination(mask2);
-        }
-        return lut_is_defined(m_vars.size());
-    }
-
-    bool lut_finder::lut_is_defined(unsigned sz) {
-        if (m_num_combinations < (1ull << (sz/2))) 
-            return false;
-        for (unsigned i = sz; i-- > 0; ) {
-            if (lut_is_defined(i, sz)) 
-                return true;
-        }
-        return false;
-    }
-
-    /**
-     * \brief check if all output combinations for variable i are defined.
-     */
-    bool lut_finder::lut_is_defined(unsigned i, unsigned sz) {
-        uint64_t c = m_combination | (m_combination >> (1ull << (uint64_t)i));
-        uint64_t m = m_masks[i];
-        if (sz < 6) m &= ((1ull << (1ull << sz)) - 1);
-        return (c & m) == m;
-    }
-
-    /**
-     * find variable where it is defined
-     * convert bit-mask to truth table for that variable.
-     * remove variable from vars, 
-     * return truth table.
-     */
-
-    uint64_t lut_finder::convert_combination(bool_var_vector& vars, bool_var& v) {
-        SASSERT(lut_is_defined(vars.size()));
-        unsigned i = 0;
-        for (i = vars.size(); i-- > 0; ) {
-            if (lut_is_defined(i, vars.size())) {
-                break;
-            }
-        }
-        SASSERT(i < vars.size());
-        v = vars[i];
-        vars.erase(v);
-        uint64_t r = 0;
-        uint64_t m = m_masks[i];
-        unsigned offset = 0;
-        // example, if i = 2, then we are examining 
-        // how m_combination evaluates at position xy0uv
-        // If it evaluates to 0, then it has to evaluate to 1 on position xy1uv
-        // Offset keeps track of the value of xyuv
-        // 
-        for (unsigned j = 0; j < 64; ++j) {
-            if (0 != (m & (1ull << j))) {
-                if (0 != (m_combination & (1ull << j))) {
-                    r |= 1ull << offset;
-                }
-                ++offset;
-            }
-        }
-        return r;
-    }
-
-    void lut_finder::init_clause_filter() {
-        m_clause_filters.reset();
-        m_clause_filters.resize(s.num_vars());
-        init_clause_filter(s.m_clauses);
-        init_clause_filter(s.m_learned);
-    }
-
-    void lut_finder::init_clause_filter(clause_vector& clauses) {
-        for (clause* cp : clauses) {
-            clause& c = *cp;
-            if (c.size() <= m_max_lut_size && s.all_distinct(c)) {
-                clause_filter cf(get_clause_filter(c), cp);
-                for (literal l : c) {
-                    m_clause_filters[l.var()].push_back(cf);
-                }            
-            }
-        }
-    }
-
-    unsigned lut_finder::get_clause_filter(clause const& c) {
-        unsigned filter = 0;
-        for (literal l : c) {
-            filter |= 1 << ((l.var() % 32));
-        }
-        return filter;
-    }
-
-    std::ostream& lut_finder::display_mask(std::ostream& out, uint64_t mask, unsigned sz) const {
-        for (unsigned i = 0; i < sz; ++i) {
-            out << ((0 != (((mask >> i)) & 0x1)) ? "1" : "0");
-        }
-        return out;
-    }
-
-}
diff --git a/src/sat/sat_lut_finder.h b/src/sat/sat_lut_finder.h
deleted file mode 100644
index d51f40388..000000000
--- a/src/sat/sat_lut_finder.h
+++ /dev/null
@@ -1,79 +0,0 @@
-/*++
-  Copyright (c) 2020 Microsoft Corporation
-
-  Module Name:
-
-   sat_lut_finder.h
-
-  Abstract:
-   
-    lut finder
-
-  Author:
-
-    Nikolaj Bjorner 2020-02-03
-
-  Notes:
-  
-    Find LUT with small input fan-ins
-
-  --*/
-
-#pragma once
-
-#include "util/params.h"
-#include "util/statistics.h"
-#include "sat/sat_clause.h"
-#include "sat/sat_types.h"
-#include "sat/sat_solver.h"
-
-namespace sat {
-
-    class lut_finder {
-        solver& s;
-        struct clause_filter {
-            unsigned m_filter;
-            clause*  m_clause;            
-            clause_filter(unsigned f, clause* cp):
-                m_filter(f), m_clause(cp) {}
-        };
-        unsigned                m_max_lut_size;
-        vector<svector<clause_filter>>   m_clause_filters;  // index of clauses.
-        uint64_t                m_combination;              // bit-mask of parities that have been found
-        unsigned                m_num_combinations;
-        clause_vector           m_clauses_to_remove;        // remove clauses that become luts
-        unsigned_vector         m_var_position;             // position of var in main clause
-        bool_var_vector         m_vars;                     // reference to variables being tested for LUT
-        literal_vector          m_clause;                   // reference clause with literals sorted according to main clause
-        unsigned_vector         m_missing;                  // set of indices not occurring in clause.
-        uint64_t                m_masks[7];
-        clause_vector           m_removed_clauses;
-        std::function<void (uint64_t, svector<bool_var> const& vars, bool_var v)> m_on_lut;
-
-        void set_combination(unsigned mask);
-        inline bool get_combination(unsigned mask) const { return (m_combination & (1ull << mask)) != 0; }
-        bool lut_is_defined(unsigned sz);
-        bool lut_is_defined(unsigned i, unsigned sz);
-        uint64_t convert_combination(bool_var_vector& vars, bool_var& v);
-        void check_lut(clause& c);
-        void add_lut();
-        bool extract_lut(literal l1, literal l2);
-        bool extract_lut(clause& c2);
-        bool update_combinations(unsigned mask);
-        void init_clause_filter();
-        void init_clause_filter(clause_vector& clauses);
-        unsigned get_clause_filter(clause const& c);
-        std::ostream& display_mask(std::ostream& out, uint64_t mask, unsigned sz) const;
-
-    public:
-        lut_finder(solver& s) : s(s), m_max_lut_size(5) { 
-            memset(m_masks, 0, sizeof(uint64_t)*7);
-        }
-
-        void set(std::function<void (uint64_t, bool_var_vector const&, bool_var)>& f) { m_on_lut = f; }
-
-        unsigned max_lut_size() const { return m_max_lut_size; }
-        void operator()(clause_vector& clauses);        
-
-    };
-}
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 4011b27ca..5c85d087a 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -32,7 +32,6 @@ Revision History:
 #include "sat/sat_ddfw_wrapper.h"
 #include "sat/sat_prob.h"
 #include "sat/sat_anf_simplifier.h"
-#include "sat/sat_cut_simplifier.h"
 #if defined(_MSC_VER) && !defined(_M_ARM) && !defined(_M_ARM64)
 # include <xmmintrin.h>
 #endif
@@ -2105,11 +2104,7 @@ namespace sat {
             anf();
             anf.collect_statistics(m_aux_stats);
             // TBD: throttle anf_delay based on yield
-        }
-        
-        if (m_cut_simplifier && m_simplifications > m_config.m_cut_delay && !inconsistent()) {
-            (*m_cut_simplifier)();
-        }
+        }        
 
         if (m_config.m_inprocess_out.is_non_empty_string()) {
             std::ofstream fout(m_config.m_inprocess_out.str());
@@ -3707,7 +3702,6 @@ namespace sat {
         SASSERT(new_v + 1 == m_justification.size()); // there are no active variables that have higher values
         literal lit = literal(new_v, false);
         m_user_scope_literals.push_back(lit);
-        m_cut_simplifier = nullptr; // for simplicity, wipe it out
         if (m_ext)
             m_ext->user_push();
         TRACE(sat, tout << "user_push: " << lit << "\n";);
@@ -3766,9 +3760,6 @@ namespace sat {
         m_slow_glue_backup.set_alpha(m_config.m_slow_glue_avg);
         m_trail_avg.set_alpha(m_config.m_slow_glue_avg);
 
-        if (m_config.m_cut_simplify && !m_cut_simplifier && m_user_scope_literals.empty()) {
-            m_cut_simplifier = alloc(cut_simplifier, *this);
-        }
     }
 
     void solver::collect_param_descrs(param_descrs & d) {
@@ -3788,7 +3779,6 @@ namespace sat {
         m_probing.collect_statistics(st);
         if (m_ext) m_ext->collect_statistics(st);
         if (m_local_search) m_local_search->collect_statistics(st);
-        if (m_cut_simplifier) m_cut_simplifier->collect_statistics(st);
         st.copy(m_aux_stats);
     }
 
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index da81c15c7..9aa00ae47 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -39,7 +39,6 @@ Revision History:
 #include "sat/sat_simplifier.h"
 #include "sat/sat_scc.h"
 #include "sat/sat_asymm_branch.h"
-#include "sat/sat_cut_simplifier.h"
 #include "sat/sat_probing.h"
 #include "sat/sat_mus.h"
 #include "sat/sat_drat.h"
@@ -97,7 +96,6 @@ namespace sat {
         config                  m_config;
         stats                   m_stats;
         scoped_ptr<extension>   m_ext;
-        scoped_ptr<cut_simplifier> m_cut_simplifier;
         parallel*               m_par;
         drat                    m_drat;          // DRAT for generating proofs
         clause_allocator        m_cls_allocator[2];
@@ -222,7 +220,6 @@ namespace sat {
         friend class scc;
         friend class pb::solver;
         friend class anf_simplifier;
-        friend class cut_simplifier;
         friend class parallel;
         friend class lookahead;
         friend class local_search;
@@ -450,7 +447,6 @@ namespace sat {
         bool is_incremental() const { return m_config.m_incremental; }
         extension* get_extension() const override { return m_ext.get(); }
         void       set_extension(extension* e) override;
-        cut_simplifier* get_cut_simplifier() override { return m_cut_simplifier.get(); }
         bool       set_root(literal l, literal r);
         void       flush_roots();
         typedef std::pair<literal, literal> bin_clause;
diff --git a/src/sat/sat_solver_core.h b/src/sat/sat_solver_core.h
index 5c8b7e315..cc0e6e023 100644
--- a/src/sat/sat_solver_core.h
+++ b/src/sat/sat_solver_core.h
@@ -23,7 +23,6 @@ Revision History:
 
 namespace sat {
 
-    class cut_simplifier;
     class extension;
 
     class solver_core {
@@ -58,8 +57,6 @@ namespace sat {
         // hooks for extension solver. really just ba_solver atm.
         virtual extension* get_extension() const { return nullptr; }
         virtual void       set_extension(extension* e) { if (e) throw default_exception("optional API not supported"); }
-
-        virtual cut_simplifier* get_cut_simplifier() { return nullptr; }
     };
 };
 
diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h
index 0a7c854fd..fce3efaac 100644
--- a/src/sat/smt/array_solver.h
+++ b/src/sat/smt/array_solver.h
@@ -16,6 +16,7 @@ Author:
 --*/
 #pragma once
 
+#include "util/union_find.h"
 #include "ast/ast_trail.h"
 #include "sat/smt/sat_th.h"
 #include "ast/array_decl_plugin.h"
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index 9cbee87f9..e059fd12f 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -16,6 +16,7 @@ Author:
 --*/
 #pragma once
 
+#include "util/union_find.h"
 #include "sat/smt/sat_th.h"
 #include "sat/smt/bv_ackerman.h"
 #include "ast/rewriter/bit_blaster/bit_blaster.h"
diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h
index 02f1300b8..514e9f79d 100644
--- a/src/sat/smt/dt_solver.h
+++ b/src/sat/smt/dt_solver.h
@@ -16,6 +16,7 @@ Author:
 --*/
 #pragma once
 
+#include "util/union_find.h"
 #include "sat/smt/sat_th.h"
 #include "ast/datatype_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index bf0853c20..abc112592 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -38,7 +38,6 @@ Notes:
 #include "model/model_v2_pp.h"
 #include "tactic/tactic.h"
 #include "ast/converters/generic_model_converter.h"
-#include "sat/sat_cut_simplifier.h"
 #include "sat/sat_drat.h"
 #include "sat/tactic/goal2sat.h"
 #include "sat/smt/pb_solver.h"
@@ -76,7 +75,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
     bool                        m_default_external;
     bool                        m_euf = false;
     bool                        m_top_level = false;
-    sat::literal_vector         aig_lits;
     
     imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
         m(_m),
@@ -91,10 +89,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         updt_params(p);
     }
 
-    sat::cut_simplifier* aig() {
-        return m_solver.get_cut_simplifier();
-    }
-
     void updt_params(params_ref const & p) {
         sat_params sp(p);
         m_ite_extra  = p.get_bool("ite_extra", true);
@@ -440,16 +434,11 @@ struct goal2sat::imp : public sat::sat_internalizer {
                        
             m_result_stack.push_back(~l);
             lits = m_result_stack.end() - num - 1;
-            if (aig()) {
-                aig_lits.reset();
-                aig_lits.append(num, lits);
-            }
+
             // remark: mk_clause may perform destructive updated to lits.
             // I have to execute it after the binary mk_clause above.
             mk_clause(num+1, lits, mk_tseitin(num+1, lits));
-            if (aig()) 
-                aig()->add_or(l, num, aig_lits.data());
-                        
+     
             m_solver.set_phase(~l);               
             m_result_stack.shrink(old_sz);
             if (sign)
@@ -497,14 +486,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
             }
             m_result_stack.push_back(l);
             lits = m_result_stack.end() - num - 1;
-            if (aig()) {
-                aig_lits.reset();
-                aig_lits.append(num, lits);
-            }
-            mk_clause(num+1, lits, mk_tseitin(num+1, lits));
-            if (aig()) {
-                aig()->add_and(l, num, aig_lits.data());
-            }        
+            mk_clause(num+1, lits, mk_tseitin(num+1, lits));      
             m_solver.set_phase(l);               
             if (sign)
                 l.neg();
@@ -546,7 +528,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 mk_clause(~t, ~e, l, mk_tseitin(~t, ~e, l));
                 mk_clause(t,  e, ~l, mk_tseitin(t, e, ~l));
             }
-            if (aig()) aig()->add_ite(l, c, t, e);
             if (sign)
                 l.neg();
 
@@ -645,7 +626,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
             mk_clause(~l, ~l1,  l2, mk_tseitin(~l, ~l1, l2));
             mk_clause(l,   l1,  l2, mk_tseitin(l, l1, l2));
             mk_clause(l,  ~l1, ~l2, mk_tseitin(l, ~l1, ~l2));
-            if (aig()) aig()->add_iff(l, l1, l2);
 
             cache(t, l);
             if (sign)
diff --git a/src/sat/tactic/sat2goal.cpp b/src/sat/tactic/sat2goal.cpp
index ab8b8d8ee..95446ee04 100644
--- a/src/sat/tactic/sat2goal.cpp
+++ b/src/sat/tactic/sat2goal.cpp
@@ -38,7 +38,6 @@ Notes:
 #include "model/model_v2_pp.h"
 #include "tactic/tactic.h"
 #include "ast/converters/generic_model_converter.h"
-#include "sat/sat_cut_simplifier.h"
 #include "sat/sat_drat.h"
 #include "sat/tactic/sat2goal.h"
 #include "sat/smt/pb_solver.h"