na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/smt/CMakeLists.txt

@@ -4,13 +4,14 @@ z3_add_component(sat_smt
     ba_internalize.cpp
     ba_solver.cpp
     bv_internalize.cpp
-    xor_solver.cpp
+    bv_solver.cpp
     euf_ackerman.cpp
     euf_internalize.cpp
     euf_model.cpp
     euf_proof.cpp
     euf_solver.cpp
     sat_th.cpp
+    xor_solver.cpp
   COMPONENT_DEPENDENCIES
     sat
     ast

src/sat/smt/bv_internalize.cpp

@@ -23,53 +23,227 @@ Author:
 namespace bv {
 
     euf::theory_var solver::mk_var(euf::enode* n) {
-        theory_var r  = euf::th_euf_solver::mk_var(n);
+        theory_var r = euf::th_euf_solver::mk_var(n);
         m_find.mk_var();
         m_bits.push_back(sat::literal_vector());
         m_wpos.push_back(0);
-        m_zero_one_bits.push_back(zero_one_bits());        
+        m_zero_one_bits.push_back(zero_one_bits());
         ctx.attach_th_var(n, this, r);
         return r;
     }
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) {
-        flet<bool> _is_learned(m_is_redundant, learned);
-        sat::scoped_stack _sc(m_stack);
-        unsigned sz = m_stack.size();
-        visit(e);
-        while (m_stack.size() > sz) {
-        loop:
-            if (!m.inc())
-                throw tactic_exception(m.limit().get_cancel_msg());
-            sat::eframe & fr = m_stack.back();
-            expr* e = fr.m_e;
-            if (visited(e)) {
-                m_stack.pop_back();
-                continue;
-            }
-            unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0;
-            
-            while (fr.m_idx < num) {
-                expr* arg = to_app(e)->get_arg(fr.m_idx);
-                fr.m_idx++;
-                visit(arg);
-                if (!visited(arg))
-                    goto loop;
-            }
-            visit(e);
-            SASSERT(visited(e));
-            m_stack.pop_back();
-        }        
-        SASSERT(visited(e));
+    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+        if (!visit_rec(m, e, sign, root, redundant))
+            return sat::null_literal;
         return sat::null_literal;
     }
 
     bool solver::visit(expr* e) {
-        return false;
+        if (!bv.is_bv(e)) {
+            ctx.internalize(e, false, false, m_is_redundant);
+            return true;
+        }
+        m_args.reset();
+        app* a = to_app(e);
+        for (expr* arg : *a) {
+            euf::enode* n = get_enode(arg);
+            if (n)
+                m_args.push_back(n);
+            else
+                m_stack.push_back(sat::eframe(arg));
+        }
+        if (m_args.size() != a->get_num_args())
+            return false;
+        if (!smt_params().m_bv_reflect)
+            m_args.reset();
+        euf::enode* n = mk_enode(a, m_args);
+        SASSERT(n->interpreted());
+        theory_var v = n->get_th_var(get_id());
+
+        switch (a->get_decl_kind()) {
+        case OP_BV_NUM:         internalize_num(a, v); break;
+        default:                break;
+        }
+        return true;
     }
 
     bool solver::visited(expr* e) {
-        return false;
+        return get_enode(e) != nullptr;
+    }
+
+    euf::enode * solver::mk_enode(app * n, ptr_vector<euf::enode> const& args) {
+        euf::enode * e = ctx.get_enode(n);
+        if (!e) {
+            e = ctx.mk_enode(n, args.size(), args.c_ptr());
+            mk_var(e);
+        }
+        return e;
+    }
+
+    void solver::register_true_false_bit(theory_var v, unsigned i) {
+
+    }
+
+    /**
+       \brief Add bit l to the given variable.
+    */
+    void solver::add_bit(theory_var v, literal l) {
+        literal_vector & bits = m_bits[v];
+        unsigned idx          = bits.size();
+        bits.push_back(l);
+#if 0
+        if (l.var() == true_bool_var) {
+            register_true_false_bit(v, idx);
+        }
+        else {
+            theory_id th_id = ctx.get_var_theory(l.var());
+            if (th_id == get_id()) {
+                atom * a = get_bv2a(l.var());
+                SASSERT(a && a->is_bit());
+                bit_atom * b = static_cast<bit_atom*>(a);
+                find_new_diseq_axioms(b->m_occs, v, idx);
+                ctx.push(add_var_pos_trail(b));
+                b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs);
+            }
+            else {
+                SASSERT(th_id == null_theory_id);
+                ctx.set_var_theory(l.var(), get_id());
+                SASSERT(ctx.get_var_theory(l.var()) == get_id());
+                bit_atom * b = new (get_region()) bit_atom();
+                insert_bv2a(l.var(), b);
+                ctx.push(mk_atom_trail(l.var()));
+                SASSERT(b->m_occs == 0);
+                b->m_occs = new (get_region()) var_pos_occ(v, idx);
+            }
+        }
+#endif
+    }
+
+    void solver::init_bits(euf::enode * n, expr_ref_vector const & bits) {
+        SASSERT(get_bv_size(n) == bits.size());
+        SASSERT(euf::null_theory_var != n->get_th_var(get_id()));
+        theory_var v = n->get_th_var(get_id());
+        unsigned sz = bits.size();
+        m_bits[v].reset();
+        for (expr* bit : bits)
+            add_bit(v, get_literal(bit));
+        find_wpos(v);
+    }
+
+    unsigned solver::get_bv_size(euf::enode* n) {
+        return bv.get_bv_size(n->get_owner());
+    }
+
+    void solver::internalize_num(app* n, theory_var v) {
+        numeral val;
+        unsigned sz = 0;
+        VERIFY(bv.is_numeral(n, val, sz));
+        expr_ref_vector bits(m);
+        m_bb.num2bits(val, sz, bits); 
+        literal_vector & c_bits = m_bits[v];
+        SASSERT(bits.size() == sz);
+        SASSERT(c_bits.empty());
+        for (unsigned i = 0; i < sz; i++) {
+            expr * l = bits.get(i);
+            SASSERT(m.is_true(l) || m.is_false(l));
+            c_bits.push_back(m.is_true(l) ? true_literal : false_literal);
+            register_true_false_bit(v, i);
+        }
+        fixed_var_eh(v);
+    }
+
+    void solver::internalize_add(app* n) {}
+    void solver::internalize_sub(app* n) {}
+    void solver::internalize_mul(app* n) {}
+    void solver::internalize_udiv(app* n) {}
+    void solver::internalize_sdiv(app* n) {}
+    void solver::internalize_urem(app* n) {}
+    void solver::internalize_srem(app* n) {}
+    void solver::internalize_smod(app* n) {}
+    void solver::internalize_shl(app* n) {}
+    void solver::internalize_lshr(app* n) {}
+    void solver::internalize_ashr(app* n) {}
+    void solver::internalize_ext_rotate_left(app* n) {}
+    void solver::internalize_ext_rotate_right(app* n) {}
+    void solver::internalize_and(app* n) {}
+    void solver::internalize_or(app* n) {}
+    void solver::internalize_not(app* n) {}
+    void solver::internalize_nand(app* n) {}
+    void solver::internalize_nor(app* n) {}
+    void solver::internalize_xor(app* n) {}
+    void solver::internalize_xnor(app* n) {}
+    void solver::internalize_concat(app* n) {}
+    void solver::internalize_sign_extend(app* n) {}
+    void solver::internalize_zero_extend(app* n) {}
+    void solver::internalize_extract(app* n) {}
+    void solver::internalize_redand(app* n) {}
+    void solver::internalize_redor(app* n) {}
+    void solver::internalize_comp(app* n) {}
+    void solver::internalize_rotate_left(app* n) {}
+    void solver::internalize_rotate_right(app* n) {}
+    void solver::internalize_bv2int(app* n) {}
+    void solver::internalize_int2bv(app* n) {}
+    void solver::internalize_mkbv(app* n) {}
+    void solver::internalize_umul_no_overflow(app* n) {}
+    void solver::internalize_smul_no_overflow(app* n) {}
+    void solver::internalize_smul_no_underflow(app* n) {}
+
+}
+
+
+
+#if 0
+
+        case OP_BADD:           internalize_add(term); return true;
+        case OP_BSUB:           internalize_sub(term); return true;
+        case OP_BMUL:           internalize_mul(term); return true;
+        case OP_BSDIV_I:        internalize_sdiv(term); return true;
+        case OP_BUDIV_I:        internalize_udiv(term); return true;
+        case OP_BSREM_I:        internalize_srem(term); return true;
+        case OP_BUREM_I:        internalize_urem(term); return true;
+        case OP_BSMOD_I:        internalize_smod(term); return true;
+        case OP_BAND:           internalize_and(term); return true;
+        case OP_BOR:            internalize_or(term); return true;
+        case OP_BNOT:           internalize_not(term); return true;
+        case OP_BXOR:           internalize_xor(term); return true;
+        case OP_BNAND:          internalize_nand(term); return true;
+        case OP_BNOR:           internalize_nor(term); return true;
+        case OP_BXNOR:          internalize_xnor(term); return true;
+        case OP_CONCAT:         internalize_concat(term); return true;
+        case OP_SIGN_EXT:       internalize_sign_extend(term); return true;
+        case OP_ZERO_EXT:       internalize_zero_extend(term); return true;
+        case OP_EXTRACT:        internalize_extract(term); return true;
+        case OP_BREDOR:         internalize_redor(term); return true;
+        case OP_BREDAND:        internalize_redand(term); return true;
+        case OP_BCOMP:          internalize_comp(term); return true;
+        case OP_BSHL:           internalize_shl(term); return true;
+        case OP_BLSHR:          internalize_lshr(term); return true;
+        case OP_BASHR:          internalize_ashr(term); return true;
+        case OP_ROTATE_LEFT:    internalize_rotate_left(term); return true;
+        case OP_ROTATE_RIGHT:   internalize_rotate_right(term); return true;
+        case OP_EXT_ROTATE_LEFT:  internalize_ext_rotate_left(term); return true;
+        case OP_EXT_ROTATE_RIGHT: internalize_ext_rotate_right(term); return true;
+        case OP_BSDIV0:         return false;
+        case OP_BUDIV0:         return false;
+        case OP_BSREM0:         return false;
+        case OP_BUREM0:         return false;
+        case OP_BSMOD0:         return false;
+        case OP_MKBV:           internalize_mkbv(term); return true;
+        case OP_INT2BV:
+            if (params().m_bv_enable_int2bv2int) {
+                internalize_int2bv(term);
+            }
+            return params().m_bv_enable_int2bv2int;
+        case OP_BV2INT:
+            if (params().m_bv_enable_int2bv2int) {
+                internalize_bv2int(term);
+            }
+            return params().m_bv_enable_int2bv2int;
+        default:
+            TRACE("bv_op", tout << "unsupported operator: " << mk_ll_pp(term, m) << "\n";);
+            UNREACHABLE();
+            return false;
     }
 
 }
+#endif

src/sat/smt/bv_solver.cpp

@@ -0,0 +1,56 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    bv_internalize.cpp
+
+Abstract:
+
+    Internalize utilities for bit-vector solver plugin.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-02
+
+--*/
+
+#include "sat/smt/bv_solver.h"
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/sat_th.h"
+#include "tactic/tactic_exception.h"
+
+namespace bv {
+
+    void solver::fixed_var_eh(theory_var v) {
+        
+    }
+
+    /**
+       \brief Find an unassigned bit for m_wpos[v], if such bit cannot be found invoke fixed_var_eh
+    */
+    void solver::find_wpos(theory_var v) {
+        literal_vector const & bits = m_bits[v];
+        unsigned sz                 = bits.size();
+        unsigned & wpos             = m_wpos[v];
+        unsigned init               = wpos;
+        for (; wpos < sz; wpos++) {
+            TRACE("find_wpos", tout << "curr bit: " << bits[wpos] << "\n";);
+            if (s().value(bits[wpos]) == l_undef) {
+                TRACE("find_wpos", tout << "moved wpos of v" << v << " to " << wpos << "\n";);
+                return;
+            }
+        }
+        wpos = 0;
+        for (; wpos < init; wpos++) {
+            if (s().value(bits[wpos]) == l_undef) {
+                TRACE("find_wpos", tout << "moved wpos of v" << v << " to " << wpos << "\n";);
+                return;
+            }
+        }
+        TRACE("find_wpos", tout << "v" << v << " is a fixed variable.\n";);
+        fixed_var_eh(v);
+    }
+
+
+}

src/sat/smt/bv_solver.h

@@ -17,6 +17,7 @@ Author:
 #pragma once
 
 #include "sat/smt/sat_th.h"
+#include "ast/rewriter/bit_blaster/bit_blaster.h"
 
 namespace bv {
 
@@ -85,10 +86,9 @@ namespace bv {
             bool is_bit() const override { return false; }
         };
 
-        euf::solver&             ctx;
-        bv_util                  m_util;
+        bv_util                  bv;
         arith_util               m_autil;
-//        bit_blaster              m_bb;
+        bit_blaster              m_bb;
         th_union_find            m_find;
         vector<literal_vector>   m_bits;     // per var, the bits of a given variable.
         ptr_vector<expr>         m_bits_expr;
@@ -96,11 +96,59 @@ namespace bv {
         vector<zero_one_bits>    m_zero_one_bits; // per var, see comment in the struct zero_one_bit
 //        bool_var2atom            m_bool_var2atom;
         sat::solver* m_solver;
-        svector<sat::eframe>     m_stack;
-        bool                     m_is_redundant{ false };
+        sat::solver& s() { return *m_solver;  }
+
+        // internalize:
+        sat::literal false_literal;
+        sat::literal true_literal;
+        bool visit(expr* e) override;
+        bool visited(expr* e) override;
+        bool post_visit(expr* e, bool sign, bool root) override;
+        unsigned get_bv_size(euf::enode* n);
+        euf::enode* mk_enode(app* n, ptr_vector<euf::enode> const& args);
+        void fixed_var_eh(theory_var v);
+        void register_true_false_bit(theory_var v, unsigned i);
+        void add_bit(theory_var v, sat::literal lit);
+        void init_bits(euf::enode * n, expr_ref_vector const & bits);
+        void internalize_num(app * n, theory_var v);
+        void internalize_add(app * n);
+        void internalize_sub(app * n);
+        void internalize_mul(app * n);
+        void internalize_udiv(app * n);
+        void internalize_sdiv(app * n);
+        void internalize_urem(app * n);
+        void internalize_srem(app * n);
+        void internalize_smod(app * n);
+        void internalize_shl(app * n);
+        void internalize_lshr(app * n);
+        void internalize_ashr(app * n);
+        void internalize_ext_rotate_left(app * n);
+        void internalize_ext_rotate_right(app * n);
+        void internalize_and(app * n);
+        void internalize_or(app * n);
+        void internalize_not(app * n);
+        void internalize_nand(app * n);
+        void internalize_nor(app * n);
+        void internalize_xor(app * n);
+        void internalize_xnor(app * n);
+        void internalize_concat(app * n);
+        void internalize_sign_extend(app * n);
+        void internalize_zero_extend(app * n);
+        void internalize_extract(app * n);
+        void internalize_redand(app * n);
+        void internalize_redor(app * n);
+        void internalize_comp(app * n);
+        void internalize_rotate_left(app * n);
+        void internalize_rotate_right(app * n);
+        void internalize_bv2int(app* n);
+        void internalize_int2bv(app* n);
+        void internalize_mkbv(app* n);
+        void internalize_umul_no_overflow(app *n);
+        void internalize_smul_no_overflow(app *n);
+        void internalize_smul_no_underflow(app *n);
+
+        void find_wpos(theory_var v);
 
-        bool visit(expr* e);
-        bool visited(expr* e);
     public:
         solver(euf::solver& ctx);
         ~solver() override {}

src/sat/smt/euf_internalize.cpp

@@ -17,56 +17,27 @@ Author:
 
 #include "ast/ast_pp.h"
 #include "ast/pb_decl_plugin.h"
-#include "tactic/tactic_exception.h"
 #include "sat/smt/euf_solver.h"
 
 namespace euf {
 
     sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
-        flet<bool> _is_learned(m_is_redundant, redundant);
+        if (si.is_bool_op(e))
+            return si.internalize(e, redundant);
         auto* ext = get_solver(e);
         if (ext)
             return ext->internalize(e, sign, root, redundant);
-        IF_VERBOSE(110, verbose_stream() << "internalize: " << mk_pp(e, m) << "\n");
-        SASSERT(!si.is_bool_op(e));
-        sat::scoped_stack _sc(m_stack);
-        unsigned sz = m_stack.size();
-        euf::enode* n = visit(e);
-        while (m_stack.size() > sz) {
-        loop:
-            if (!m.inc())
-                throw tactic_exception(m.limit().get_cancel_msg());
-            sat::eframe & fr = m_stack.back();
-            expr* e = fr.m_e;
-            if (m_egraph.find(e)) {
-                m_stack.pop_back();
-                continue;
-            }
-            unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0;
-            
-            while (fr.m_idx < num) {
-                expr* arg = to_app(e)->get_arg(fr.m_idx);
-                fr.m_idx++;
-                n = visit(arg);
-                if (!n)
-                    goto loop;
-            }
-            m_args.reset();
-            for (unsigned i = 0; i < num; ++i)
-                m_args.push_back(m_egraph.find(to_app(e)->get_arg(i)));
-            if (root && internalize_root(to_app(e), sign))
-                return sat::null_literal;
-            n = m_egraph.mk(e, num, m_args.c_ptr());
-            attach_node(n);
-        }        
+
+        if (!visit_rec(m, e, sign, root, redundant))
+            return sat::null_literal;
         SASSERT(m_egraph.find(e));
         return literal(m_expr2var.to_bool_var(e), sign);
     }
 
-    euf::enode* solver::visit(expr* e) {
+    bool solver::visit(expr* e) {
         euf::enode* n = m_egraph.find(e);
         if (n)
-            return n;
+            return true;
         if (si.is_bool_op(e)) {
             sat::literal lit = si.internalize(e, m_is_redundant);
             n = m_var2node.get(lit.var(), nullptr);
@@ -77,15 +48,31 @@ namespace euf {
             attach_lit(lit, n);
             if (!m.is_true(e) && !m.is_false(e)) 
                 s().set_external(lit.var());
-            return n;
+            return true;
         }
         if (is_app(e) && to_app(e)->get_num_args() > 0) {
             m_stack.push_back(sat::eframe(e));
-            return nullptr;
+            return false;
         }
         n = m_egraph.mk(e, 0, nullptr);
         attach_node(n);
-        return n;
+        return true;
+    }
+
+    bool solver::post_visit(expr* e, bool sign, bool root) {
+        unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0;
+        m_args.reset();
+        for (unsigned i = 0; i < num; ++i)
+            m_args.push_back(m_egraph.find(to_app(e)->get_arg(i)));
+        if (root && internalize_root(to_app(e), sign))
+            return false;
+        enode* n = m_egraph.mk(e, num, m_args.c_ptr());
+        attach_node(n);
+        return true;
+    }
+
+    bool solver::visited(expr* e) {
+        return m_egraph.find(e) != nullptr;
     }
 
     void solver::attach_node(euf::enode* n) {

src/sat/smt/euf_solver.cpp

@@ -236,11 +236,13 @@ namespace euf {
     }
 
     enode* solver::mk_true() {
-        return visit(m.mk_true());
+        VERIFY(visit(m.mk_true()));
+        return m_egraph.find(m.mk_true());
     }
 
     enode* solver::mk_false() {
-        return visit(m.mk_false());
+        VERIFY(visit(m.mk_false()));
+        return m_egraph.find(m.mk_false());
     }
 
     sat::check_result solver::check() { 

src/sat/smt/euf_solver.h

@@ -20,12 +20,12 @@ Author:
 #include "util/trail.h"
 #include "ast/ast_translation.h"
 #include "ast/euf/euf_egraph.h"
-#include "smt/params/smt_params.h"
 #include "tactic/model_converter.h"
 #include "sat/sat_extension.h"
 #include "sat/smt/atom2bool_var.h"
 #include "sat/smt/sat_th.h"
 #include "sat/smt/euf_ackerman.h"
+#include "smt/params/smt_params.h"
 
 namespace euf {
     typedef sat::literal literal;
@@ -83,8 +83,6 @@ namespace euf {
 
         ptr_vector<euf::enode>                          m_var2node;
         ptr_vector<unsigned>                            m_explain;
-        euf::enode_vector                               m_args;
-        svector<sat::eframe>                            m_stack;
         unsigned                                        m_num_scopes { 0 };
         unsigned_vector                                 m_var_trail;
         svector<scope>                                  m_scopes;
@@ -99,8 +97,10 @@ namespace euf {
         unsigned * base_ptr() { return reinterpret_cast<unsigned*>(this); }
 
         // internalization
-        bool m_is_redundant { false };
-        euf::enode* visit(expr* e);
+
+        bool visit(expr* e) override;
+        bool visited(expr* e) override;
+        bool post_visit(expr* e, bool sign, bool root) override;
         void attach_node(euf::enode* n);
         void attach_lit(sat::literal lit, euf::enode* n);
         void add_distinct_axiom(app* e, euf::enode* const* args);
@@ -109,6 +109,7 @@ namespace euf {
         bool internalize_root(app* e, bool sign);
         euf::enode* mk_true();
         euf::enode* mk_false();
+        
 
         // extensions
         th_solver* get_solver(func_decl* f);
@@ -181,6 +182,11 @@ namespace euf {
         sat::sat_internalizer& get_si() { return si; }
         ast_manager& get_manager() { return m; }
         enode* get_enode(expr* e) { return m_egraph.find(e); }
+        sat::literal get_literal(expr* e) { return literal(m_expr2var.to_bool_var(e), false); }
+        smt_params const& get_config() { return m_config; }
+        region& get_region() { return m_region; }
+        template <typename C>
+        void push(C const& c) { m_trail.push_back(new (m_region) C(c));  }
 
         void updt_params(params_ref const& p);
         void set_solver(sat::solver* s) override { m_solver = s; m_drat = s->get_config().m_drat; }
@@ -214,12 +220,16 @@ namespace euf {
         bool check_model(sat::model const& m) const override;
         unsigned max_var(unsigned w) const override;
 
+        // decompile
         bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
                         std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override;
 
         bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
+
+        // internalize
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
         void attach_th_var(enode* n, th_solver* th, theory_var v) { m_egraph.add_th_var(n, v, th->get_id()); }
+        euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, n, args); }
 
         void update_model(model_ref& mdl);
 

src/sat/smt/sat_th.cpp

@@ -17,15 +17,62 @@ Author:
 
 #include "sat/smt/sat_th.h"
 #include "sat/smt/euf_solver.h"
+#include "tactic/tactic_exception.h"
 
 namespace euf {
 
+    bool th_internalizer::visit_rec(ast_manager& m, expr* a, bool sign, bool root, bool redundant) {
+        IF_VERBOSE(110, verbose_stream() << "internalize: " << mk_pp(a, m) << "\n");
+        flet<bool> _is_learned(m_is_redundant, redundant);
+        sat::scoped_stack _sc(m_stack);
+        unsigned sz = m_stack.size();
+        visit(a);
+        while (m_stack.size() > sz) {
+        loop:
+            if (!m.inc())
+                throw tactic_exception(m.limit().get_cancel_msg());
+            sat::eframe& fr = m_stack.back();
+            expr* e = fr.m_e;
+            if (visited(e)) {
+                m_stack.pop_back();
+                continue;
+            }
+            unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0;
+
+            while (fr.m_idx < num) {
+                expr* arg = to_app(e)->get_arg(fr.m_idx);
+                fr.m_idx++;
+                if (!visit(arg))
+                    goto loop;
+            }
+            if (!post_visit(e, sign, root && a == e))
+                return false;
+            m_stack.pop_back();
+        }
+        return true;
+    }
 
     th_euf_solver::th_euf_solver(euf::solver& ctx, euf::theory_id id):
         th_solver(ctx.get_manager(), id),
         ctx(ctx)
     {}
 
+    smt_params const& th_euf_solver::get_config() const {
+        return ctx.get_config(); 
+    }
+
+    region& th_euf_solver::get_region() {
+        return ctx.get_region();
+    }
+
+    enode* th_euf_solver::get_enode(expr* e) const { 
+        return ctx.get_enode(e); 
+    }
+
+    sat::literal th_euf_solver::get_literal(expr* e) const {
+        return ctx.get_literal(e);
+    }
+
     theory_var th_euf_solver::mk_var(enode * n) {
         SASSERT(!is_attached_to_var(n));
         euf::theory_var v = m_var2enode.size();

src/sat/smt/sat_th.h

@@ -19,12 +19,23 @@ Author:
 #include "util/top_sort.h"
 #include "sat/smt/sat_smt.h"
 #include "ast/euf/euf_egraph.h"
+#include "smt/params/smt_params.h"
 
 namespace euf {
 
     class solver;
     
     class th_internalizer {
+    protected:
+        euf::enode_vector     m_args;
+        svector<sat::eframe>  m_stack;
+        bool                  m_is_redundant { false };
+
+        bool visit_rec(ast_manager& m, expr* e, bool sign, bool root, bool redundant);
+
+        virtual bool visit(expr* e) { return false; }
+        virtual bool visited(expr* e) { return false; }
+        virtual bool post_visit(expr* e, bool sign, bool root) { return false; }
     public:
         virtual ~th_internalizer() {}
 
@@ -91,11 +102,16 @@ namespace euf {
         solver &            ctx;
         euf::enode_vector   m_var2enode;
         unsigned_vector     m_var2enode_lim;
+
+        smt_params const& get_config() const;
+        sat::literal get_literal(expr* e) const;
+        region& get_region();
     public:
         th_euf_solver(euf::solver& ctx, euf::theory_id id);
         virtual ~th_euf_solver() {}
         virtual theory_var mk_var(enode * n);
         unsigned get_num_vars() const { return m_var2enode.size();}
+        enode* get_enode(expr* e) const; 
         enode* get_enode(theory_var v) const { return m_var2enode[v]; }
         expr* get_expr(theory_var v) const { return get_enode(v)->get_owner(); }
         theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); }