add c-cube's recursive function theory

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

src/smt/CMakeLists.txt

@@ -60,6 +60,7 @@ z3_add_component(smt
     theory_lra.cpp
     theory_opt.cpp
     theory_pb.cpp
+    theory_recfun.cpp
     theory_seq.cpp
     theory_str.cpp
     theory_utvpi.cpp

src/smt/params/smt_params.cpp

@@ -27,6 +27,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_random_seed = p.random_seed();
     m_relevancy_lvl = p.relevancy();
     m_ematching   = p.ematching();
+    m_recfun_max_depth = p.recfun_max_depth();
     m_phase_selection = static_cast<phase_selection>(p.phase_selection());
     m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
     m_restart_factor = p.restart_factor();

src/smt/params/smt_params.h

@@ -108,6 +108,9 @@ struct smt_params : public preprocessor_params,
     bool             m_new_core2th_eq;
     bool             m_ematching;
 
+    // TODO: move into its own file?
+    unsigned         m_recfun_max_depth;
+
     // -----------------------------------
     //
     // Case split strategy
@@ -261,6 +264,7 @@ struct smt_params : public preprocessor_params,
         m_display_features(false),
         m_new_core2th_eq(true),
         m_ematching(true),
+        m_recfun_max_depth(50),
         m_case_split_strategy(CS_ACTIVITY_DELAY_NEW),
         m_rel_case_split_order(0),
         m_lookahead_diseq(false),

src/smt/params/smt_params_helper.pyg

@@ -95,5 +95,7 @@ def_module_params(module_name='smt',
                           ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),
                           ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'),
                           ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'),
-                          ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy')
+                          ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'),
+                          ('recfun.native', BOOL, False, 'use native rec-fun solver'),
+                          ('recfun.max_depth', UINT, 500, 'maximum depth of unrolling for recursive functions')
                           ))

src/smt/smt_context.h

@@ -1614,6 +1614,35 @@ namespace smt {
         void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); }
     };
 
+
+    struct pp_lit {
+        smt::context & ctx;
+        smt::literal lit;
+        pp_lit(smt::context & ctx, smt::literal lit) : ctx(ctx), lit(lit) {}
+    };
+
+    inline std::ostream & operator<<(std::ostream & out, pp_lit const & pp) {
+        pp.ctx.display_detailed_literal(out, pp.lit);
+        return out;
+    }
+
+    struct pp_lits {
+        smt::context & ctx;
+        smt::literal *lits;
+        unsigned len;
+        pp_lits(smt::context & ctx, unsigned len, smt::literal *lits) : ctx(ctx), lits(lits), len(len) {}
+    };
+
+    inline std::ostream & operator<<(std::ostream & out, pp_lits const & pp) {
+        out << "clause{";
+        bool first = true;
+        for (unsigned i = 0; i < pp.len; ++i) {
+            if (first) { first = false; } else { out << " ∨ "; }
+            pp.ctx.display_detailed_literal(out, pp.lits[i]);
+        }
+        return out << "}";
+    }
+
 };
 
 #endif /* SMT_CONTEXT_H_ */

src/smt/smt_setup.cpp

@@ -28,6 +28,7 @@ Revision History:
 #include "smt/theory_array_full.h"
 #include "smt/theory_bv.h"
 #include "smt/theory_datatype.h"
+#include "smt/theory_recfun.h"
 #include "smt/theory_dummy.h"
 #include "smt/theory_dl.h"
 #include "smt/theory_seq_empty.h"
@@ -222,6 +223,7 @@ namespace smt {
     void setup::setup_QF_DT() {
         setup_QF_UF();
         setup_datatypes();
+        setup_recfuns();
     }
 
     void setup::setup_QF_BVRE() {
@@ -878,6 +880,13 @@ namespace smt {
         m_context.register_plugin(alloc(theory_datatype, m_manager, m_params));
     }
 
+    void setup::setup_recfuns() {
+        TRACE("recfun", tout << "registering theory recfun...\n";);
+        theory_recfun * th = alloc(theory_recfun, m_manager);
+        m_context.register_plugin(th);
+        th->setup_params();
+    }
+
     void setup::setup_dl() {
         m_context.register_plugin(mk_theory_dl(m_manager));
     }
@@ -936,6 +945,7 @@ namespace smt {
         setup_arrays();
         setup_bv();
         setup_datatypes();
+        setup_recfuns();
         setup_dl();
         setup_seq_str(st);
         setup_card();

src/smt/smt_setup.h

@@ -94,6 +94,7 @@ namespace smt {
         void setup_unknown(static_features & st);
         void setup_arrays();
         void setup_datatypes();
+        void setup_recfuns();
         void setup_bv();
         void setup_arith();
         void setup_dl();

src/smt/theory_jobscheduler.cpp

@@ -94,20 +94,29 @@ namespace smt {
         symbol key, val;
         rational r;
         expr* job, *resource;
-        unsigned j = 0, res = 0, cap = 0, loadpct = 100;
+        unsigned j = 0, res = 0, cap = 0, loadpct = 100, level = 0;
         time_t start = 0, end = std::numeric_limits<time_t>::max(), capacity = 0;
+        js_job_goal goal;
+        js_optimization_objective obj;
         properties ps;
         if (u.is_set_preemptable(cmd, job) && u.is_job(job, j)) {
             set_preemptable(j, true);            
         }
-        else if (u.is_add_resource_available(cmd, resource, loadpct, start, end, ps) && u.is_resource(resource, res)) {
+        else if (u.is_add_resource_available(cmd, resource, loadpct, cap, start, end, ps) && u.is_resource(resource, res)) {
             std::sort(ps.begin(), ps.end(), symbol_cmp());
+            (void) cap; // TBD
             add_resource_available(res, loadpct, start, end, ps);
         }
         else if (u.is_add_job_resource(cmd, job, resource, loadpct, capacity, end, ps) && u.is_job(job, j) && u.is_resource(resource, res)) {
             std::sort(ps.begin(), ps.end(), symbol_cmp());
             add_job_resource(j, res, loadpct, capacity, end, ps);
         }
+        else if (u.is_job_goal(cmd, goal, level, job) && u.is_job(job, j)) {
+            // skip
+        }
+        else if (u.is_objective(cmd, obj)) {
+            // skip
+        }
         else {
             invalid_argument("command not recognized ", cmd);
         }
@@ -487,7 +496,7 @@ namespace smt {
 
     std::ostream& theory_jobscheduler::display(std::ostream & out, job_info const& j) const {
         for (job_resource const& jr : j.m_resources) {
-            display(out << "  ", jr);
+            display(out << "  ", jr) << "\n";
         }
         return out;
     }
@@ -507,10 +516,10 @@ namespace smt {
     void theory_jobscheduler::display(std::ostream & out) const {
         out << "jobscheduler:\n";
         for (unsigned j = 0; j < m_jobs.size(); ++j) {
-            display(out << "job " << j << ":\n", m_jobs[j]);
+            display(out << "job " << j << ":\n", m_jobs[j]) << "\n";
         }
         for (unsigned r = 0; r < m_resources.size(); ++r) {
-            display(out << "resource " << r << ":\n", m_resources[r]);
+            display(out << "resource " << r << ":\n", m_resources[r]) << "\n";
         }
     }
         
@@ -615,8 +624,8 @@ namespace smt {
 
     void theory_jobscheduler::add_job_resource(unsigned j, unsigned r, unsigned loadpct, uint64_t cap, time_t end, properties const& ps) {
         SASSERT(get_context().at_base_level());
-        SASSERT(1 <= loadpct && loadpct <= 100);
-        SASSERT(0 < cap);
+        SASSERT(0 <= loadpct && loadpct <= 100);
+        SASSERT(0 <= cap);
         m_jobs.reserve(j + 1);
         m_resources.reserve(r + 1);
         job_info& ji = m_jobs[j];
@@ -690,7 +699,8 @@ namespace smt {
         }
 
         literal lit;
-
+        unsigned job_id = 0;
+        
         for (job_info const& ji : m_jobs) {
             if (ji.m_resources.empty()) {
                 throw default_exception("every job should be associated with at least one resource");
@@ -719,6 +729,10 @@ namespace smt {
                 // TBD: more accurate estimates for runtime_lb based on gaps
                 // TBD: correct estimate of runtime_ub taking gaps into account.
             }
+            CTRACE("csp", (start_lb > end_ub), tout << "there is no associated resource working time\n";);
+            if (start_lb > end_ub) {
+                warning_msg("Job %d has no associated resource working time", job_id);
+            }
 
             // start(j) >= start_lb
             lit = mk_ge(ji.m_start, start_lb);
@@ -730,6 +744,8 @@ namespace smt {
 
             // start(j) + runtime_lb <= end(j)
             // end(j) <= start(j) + runtime_ub 
+
+            ++job_id;
         }        
         
         TRACE("csp", tout << "add-done end\n";);

src/smt/theory_recfun.cpp

@@ -0,0 +1,370 @@
+
+#include "util/stats.h"
+#include "ast/ast_util.h"
+#include "smt/theory_recfun.h"
+#include "smt/params/smt_params_helper.hpp"
+
+#define DEBUG(x) TRACE("recfun", tout << x << '\n';)
+
+
+namespace smt {
+
+    theory_recfun::theory_recfun(ast_manager & m)
+        : theory(m.mk_family_id("recfun")), 
+          m_plugin(*reinterpret_cast<recfun_decl_plugin*>(m.get_plugin(get_family_id()))),
+          m_util(m_plugin.u()), 
+          m_trail(*this),
+          m_guards(), m_max_depth(0), m_q_case_expand(), m_q_body_expand(), m_q_clauses()
+        {
+        }
+
+    theory_recfun::~theory_recfun() {
+        reset_queues();
+        for (auto & kv : m_guards) {
+            m().dec_ref(kv.m_key);
+        }
+        m_guards.reset();
+    }
+
+    char const * theory_recfun::get_name() const { return "recfun"; }
+
+    void theory_recfun::setup_params() {
+        // obtain max depth via parameters
+        smt_params_helper p(get_context().get_params());
+        set_max_depth(p.recfun_max_depth());
+    }
+
+    theory* theory_recfun::mk_fresh(context* new_ctx) {
+        return alloc(theory_recfun, new_ctx->get_manager());
+    }
+
+    bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) {
+        context & ctx = get_context();
+        if (! ctx.e_internalized(atom)) {
+            unsigned num_args = atom->get_num_args();
+            for (unsigned i = 0; i < num_args; ++i)
+                ctx.internalize(atom->get_arg(i), false);
+            ctx.mk_enode(atom, false, true, false);
+        }
+        if (! ctx.b_internalized(atom)) {
+            bool_var v = ctx.mk_bool_var(atom);
+            ctx.set_var_theory(v, get_id());
+        }
+        return true;
+    }
+
+    bool theory_recfun::internalize_term(app * term) {
+        context & ctx = get_context();
+        for (expr* e : *term) ctx.internalize(e, false);
+        // the internalization of the arguments may have triggered the internalization of term.
+        if (ctx.e_internalized(term))
+            return true;
+        ctx.mk_enode(term, false, false, true);
+        return true; // the theory doesn't actually map terms to variables
+    }
+
+    void theory_recfun::reset_queues() {
+        m_q_case_expand.reset();
+        m_q_body_expand.reset();
+        m_q_clauses.reset();
+    }
+
+    void theory_recfun::reset_eh() {
+        m_trail.reset();
+        reset_queues();   
+        m_stats.reset();
+        theory::reset_eh();
+    }
+
+    /*
+     * when `n` becomes relevant, if it's `f(t1…tn)` with `f` defined,
+     * then case-expand `n`. If it's a macro we can also immediately
+     * body-expand it.
+     */
+    void theory_recfun::relevant_eh(app * n) {
+        SASSERT(get_context().relevancy());
+        if (u().is_defined(n)) {
+            DEBUG("relevant_eh: (defined) " <<  mk_pp(n, m()));
+        
+            case_expansion e(u(), n);
+            push_case_expand(std::move(e));
+        }
+    }
+
+    void theory_recfun::push_scope_eh() {
+        DEBUG("push_scope");
+        theory::push_scope_eh();
+        m_trail.push_scope();
+    }
+
+    void theory_recfun::pop_scope_eh(unsigned num_scopes) {
+        DEBUG("pop_scope " << num_scopes);
+        m_trail.pop_scope(num_scopes);
+        theory::pop_scope_eh(num_scopes);
+        reset_queues();
+    }
+    
+    void theory_recfun::restart_eh() {
+        DEBUG("restart");
+        reset_queues();
+        theory::restart_eh();
+    }
+
+    bool theory_recfun::can_propagate() {
+        return ! (m_q_case_expand.empty() &&
+                  m_q_body_expand.empty() &&
+                  m_q_clauses.empty());
+    }
+
+    void theory_recfun::propagate() {
+        context & ctx = get_context();
+
+        for (literal_vector & c : m_q_clauses) {
+            DEBUG("add axiom " << pp_lits(ctx, c.size(), c.c_ptr()));
+            ctx.mk_th_axiom(get_id(), c.size(), c.c_ptr());
+        }
+        m_q_clauses.clear();
+
+        for (case_expansion & e : m_q_case_expand) {
+            if (e.m_def->is_fun_macro()) {
+                // body expand immediately
+                assert_macro_axiom(e);
+            }
+            else {
+                // case expand
+                SASSERT(e.m_def->is_fun_defined());
+                assert_case_axioms(e);                
+            }
+        }
+        m_q_case_expand.clear();
+
+        for (body_expansion & e : m_q_body_expand) {
+            assert_body_axiom(e);
+        }
+        m_q_body_expand.clear();
+    }
+
+    void theory_recfun::max_depth_conflict() {
+        DEBUG("max-depth conflict");
+        context & ctx = get_context();
+        literal_vector c;
+        // make clause `depth_limit => V_{g : guards} ~ g`
+        {
+            // first literal must be the depth limit one
+            app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth());
+            ctx.internalize(dlimit, false);
+            c.push_back(~ ctx.get_literal(dlimit));
+            SASSERT(ctx.get_assignment(ctx.get_literal(dlimit)) == l_true);
+        }
+        for (auto& kv : m_guards) {
+            expr * g = & kv.get_key();
+            c.push_back(~ ctx.get_literal(g));
+        }
+        DEBUG("max-depth limit: add clause " << pp_lits(ctx, c.size(), c.c_ptr()));
+        SASSERT(std::all_of(c.begin(), c.end(), [&](literal & l) { return ctx.get_assignment(l) == l_false; })); // conflict
+
+        m_q_clauses.push_back(std::move(c));
+    }
+
+    // if `is_true` and `v = C_f_i(t1…tn)`, then body-expand i-th case of `f(t1…tn)`
+    void theory_recfun::assign_eh(bool_var v, bool is_true) {
+        expr* e = get_context().bool_var2expr(v);
+        if (!is_true) return;
+        if (!is_app(e)) return;
+        app* a = to_app(e);
+        if (u().is_case_pred(a)) {
+            DEBUG("assign_case_pred_true "<< mk_pp(e,m()));
+            // add to set of local assumptions, for depth-limit purpose
+            {
+                m_guards.insert(e, empty());
+                m().inc_ref(e);
+                insert_ref_map<theory_recfun,guard_set,ast_manager,expr*> trail_elt(m(), m_guards, e);
+                m_trail.push(trail_elt);
+            }
+            if (m_guards.size() > get_max_depth()) {
+                // too many body-expansions: depth-limit conflict
+                max_depth_conflict();
+            }
+            else {
+                // body-expand
+                body_expansion b_e(u(), a);
+                push_body_expand(std::move(b_e));
+            }
+        }
+    }
+
+     // replace `vars` by `args` in `e`
+    expr_ref theory_recfun::apply_args(recfun::vars const & vars,
+                                       ptr_vector<expr> const & args,
+                                       expr * e) {
+        // check that var order is standard
+        SASSERT(vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0);
+        var_subst subst(m(), true);
+        expr_ref new_body(m());
+        new_body = subst(e, args.size(), args.c_ptr());
+        get_context().get_rewriter()(new_body); // simplify
+        return new_body;
+    }
+    
+    app_ref theory_recfun::apply_pred(recfun::case_pred const & p,
+                                       ptr_vector<expr> const & args){
+        app_ref res(u().mk_case_pred(p, args), m());
+        return res;
+    }
+    
+    void theory_recfun::assert_macro_axiom(case_expansion & e) {
+        DEBUG("assert_macro_axiom " << pp_case_expansion(e,m()));
+        SASSERT(e.m_def->is_fun_macro());
+        expr_ref lhs(e.m_lhs, m());
+        context & ctx = get_context();
+        auto & vars = e.m_def->get_vars();
+        // substitute `e.args` into the macro RHS
+        expr_ref rhs(apply_args(vars, e.m_args, e.m_def->get_macro_rhs()), m());
+        DEBUG("macro expansion yields" << mk_pp(rhs,m()));
+        // now build the axiom `lhs = rhs`
+        ctx.internalize(rhs, false);
+        // add unit clause `lhs=rhs`
+        literal l(mk_eq(lhs, rhs, true));
+        ctx.mark_as_relevant(l);
+        literal_vector lits;
+        lits.push_back(l);
+        DEBUG("assert_macro_axiom: " << pp_lits(ctx, lits.size(), lits.c_ptr()));
+        ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());   
+    }
+
+    void theory_recfun::assert_case_axioms(case_expansion & e) {
+        DEBUG("assert_case_axioms "<< pp_case_expansion(e,m())
+              << " with " << e.m_def->get_cases().size() << " cases");
+        SASSERT(e.m_def->is_fun_defined());
+        context & ctx = get_context();
+        // add case-axioms for all case-paths
+        auto & vars = e.m_def->get_vars();
+        for (recfun::case_def const & c : e.m_def->get_cases()) {
+            // applied predicate to `args`
+            app_ref pred_applied = apply_pred(c.get_pred(), e.m_args);
+            SASSERT(u().owns_app(pred_applied));
+            // substitute arguments in `path`
+            expr_ref_vector path(m());
+            for (auto & g : c.get_guards()) {
+                expr_ref g_applied = apply_args(vars, e.m_args, g);
+                path.push_back(g_applied);
+            }
+            // assert `p(args) <=> And(guards)` (with CNF on the fly)
+            ctx.internalize(pred_applied, false);
+            ctx.mark_as_relevant(ctx.get_bool_var(pred_applied));
+            literal concl = ctx.get_literal(pred_applied);
+            {
+                // assert `guards=>p(args)`
+                literal_vector c;
+                c.push_back(concl);
+                for (expr* g : path) {
+                    ctx.internalize(g, false);
+                    c.push_back(~ ctx.get_literal(g));
+                }
+
+                //TRACE("recfun", tout << "assert_case_axioms " << pp_case_expansion(e)
+                //    << " axiom " << mk_pp(*l) <<"\n";);
+                DEBUG("assert_case_axiom " << pp_lits(get_context(), path.size()+1, c.c_ptr()));
+                get_context().mk_th_axiom(get_id(), path.size()+1, c.c_ptr());
+            }
+            {
+                // assert `p(args) => guards[i]` for each `i`
+                for (expr * _g : path) {
+                    SASSERT(ctx.b_internalized(_g));
+                    literal g = ctx.get_literal(_g);
+                    literal c[2] = {~ concl, g};
+
+                    DEBUG("assert_case_axiom " << pp_lits(get_context(), 2, c));
+                    get_context().mk_th_axiom(get_id(), 2, c);
+                }
+            }
+
+            // also body-expand paths that do not depend on any defined fun
+            if (c.is_immediate()) {
+                body_expansion be(c, e.m_args);
+                assert_body_axiom(be);
+            }
+        }
+    }
+
+    void theory_recfun::assert_body_axiom(body_expansion & e) {
+        DEBUG("assert_body_axioms "<< pp_body_expansion(e,m()));
+        context & ctx = get_context();
+        recfun::def & d = *e.m_cdef->get_def();
+        auto & vars = d.get_vars();
+        auto & args = e.m_args;
+        // check that var order is standard
+        SASSERT(vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0);
+        expr_ref lhs(u().mk_fun_defined(d, args), m());
+        // substitute `e.args` into the RHS of this particular case
+        expr_ref rhs = apply_args(vars, args, e.m_cdef->get_rhs());
+        // substitute `e.args` into the guard of this particular case, to make
+        // the `condition` part of the clause `conds => lhs=rhs`
+        expr_ref_vector guards(m());
+        for (auto & g : e.m_cdef->get_guards()) {
+            expr_ref new_guard = apply_args(vars, args, g);
+            guards.push_back(new_guard);
+        }        
+        // now build the axiom `conds => lhs = rhs`
+        ctx.internalize(rhs, false);
+        for (auto& g : guards) ctx.internalize(g, false);
+        
+        // add unit clause `conds => lhs=rhs`
+        literal_vector clause;
+        for (auto& g : guards) {
+            ctx.internalize(g, false);
+            literal l = ~ ctx.get_literal(g);
+            ctx.mark_as_relevant(l);
+            clause.push_back(l);
+        }
+        literal l(mk_eq(lhs, rhs, true));
+        ctx.mark_as_relevant(l);
+        clause.push_back(l);
+        DEBUG("assert_body_axiom " << pp_lits(ctx, clause.size(), clause.c_ptr()));
+        ctx.mk_th_axiom(get_id(), clause.size(), clause.c_ptr());   
+    }
+    
+    final_check_status theory_recfun::final_check_eh() {
+        return FC_DONE;
+    }
+
+    void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) {
+        app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth());
+        DEBUG("add_theory_assumption " << mk_pp(dlimit.get(), m()));
+        assumptions.push_back(dlimit);
+    }
+
+
+    // if `dlimit` occurs in unsat core, return "unknown"
+    lbool theory_recfun::validate_unsat_core(expr_ref_vector & unsat_core) {
+        for (auto & e : unsat_core) {
+            if (is_app(e) && m_util.is_depth_limit(to_app(e)))
+                return l_undef;
+        }
+        return l_false;
+    }
+
+    void theory_recfun::display(std::ostream & out) const {
+        out << "recfun{}";
+    }
+
+    void theory_recfun::collect_statistics(::statistics & st) const {
+        st.update("recfun macro expansion", m_stats.m_macro_expansions);
+        st.update("recfun case expansion", m_stats.m_case_expansions);
+        st.update("recfun body expansion", m_stats.m_body_expansions);
+    }
+
+#ifdef Z3DEBUG
+    std::ostream& operator<<(std::ostream & out, theory_recfun::pp_case_expansion const & e) {
+        return out << "case_exp(" << mk_pp(e.e.m_lhs, e.m) << ")";
+    }
+
+    std::ostream& operator<<(std::ostream & out, theory_recfun::pp_body_expansion const & e) {
+        out << "body_exp(" << e.e.m_cdef->get_name();
+        for (auto* t : e.e.m_args) {
+            out << " " << mk_pp(t,e.m);
+        }
+        return out << ")";
+    }
+#endif
+}

src/smt/theory_recfun.h

@@ -0,0 +1,158 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    theory_recfun.h
+
+Abstract:
+
+    Theory responsible for unrolling recursive functions
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-10-31.
+
+Revision History:
+
+--*/
+#ifndef THEORY_RECFUN_H_
+#define THEORY_RECFUN_H_
+
+#include "smt/smt_theory.h"
+#include "smt/smt_context.h"
+#include "ast/ast_pp.h"
+#include "ast/recfun_decl_plugin.h"
+
+namespace smt {
+
+    class theory_recfun : public theory {
+        struct stats {
+            unsigned m_case_expansions, m_body_expansions, m_macro_expansions;
+            void reset() { memset(this, 0, sizeof(stats)); }
+            stats() { reset(); }
+        };
+
+        // one case-expansion of `f(t1…tn)`
+        struct case_expansion {
+            expr *              m_lhs; // the term to expand
+            recfun_def *        m_def;
+            ptr_vector<expr>    m_args;
+            case_expansion(recfun_util& u, app * n) : m_lhs(n), m_def(0), m_args()
+            {
+                SASSERT(u.is_defined(n));
+                func_decl * d = n->get_decl();
+                const symbol& name = d->get_name();
+                m_def = &u.get_def(name);
+                m_args.append(n->get_num_args(), n->get_args());
+            }
+            case_expansion(case_expansion const & from)
+                : m_lhs(from.m_lhs),
+                  m_def(from.m_def),
+                  m_args(from.m_args) {}
+            case_expansion(case_expansion && from)
+                : m_lhs(from.m_lhs),
+                  m_def(from.m_def),
+                  m_args(std::move(from.m_args)) {}
+        };
+
+        struct pp_case_expansion {
+            case_expansion & e;
+            ast_manager & m;
+            pp_case_expansion(case_expansion & e, ast_manager & m) : e(e), m(m) {}
+        };
+
+        friend std::ostream& operator<<(std::ostream&, pp_case_expansion const &);
+
+        // one body-expansion of `f(t1…tn)` using a `C_f_i(t1…tn)`
+        struct body_expansion {
+            recfun_case_def const * m_cdef;
+            ptr_vector<expr>        m_args;
+
+            body_expansion(recfun_util& u, app * n) : m_cdef(0), m_args() {
+                SASSERT(u.is_case_pred(n));
+                func_decl * d = n->get_decl();
+                const symbol& name = d->get_name();
+                m_cdef = &u.get_case_def(name);
+                for (unsigned i = 0; i < n->get_num_args(); ++i)
+                    m_args.push_back(n->get_arg(i));
+            }
+            body_expansion(recfun_case_def const & d, ptr_vector<expr> & args) : m_cdef(&d), m_args(args) {}
+            body_expansion(body_expansion const & from): m_cdef(from.m_cdef), m_args(from.m_args) {}
+            body_expansion(body_expansion && from) : m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {}
+        };
+
+        struct pp_body_expansion {
+            body_expansion & e;
+            ast_manager & m;
+            pp_body_expansion(body_expansion & e, ast_manager & m) : e(e), m(m) {}
+        };
+
+        friend std::ostream& operator<<(std::ostream&, pp_body_expansion const &);
+        
+        struct empty{};
+
+        typedef trail_stack<theory_recfun>  th_trail_stack;
+        typedef obj_map<expr, empty> guard_set;
+
+        recfun_decl_plugin& m_plugin;
+        recfun_util&        m_util;
+        stats               m_stats;
+        th_trail_stack      m_trail;
+        guard_set           m_guards; // true case-preds
+        unsigned            m_max_depth; // for fairness and termination
+
+        vector<case_expansion>      m_q_case_expand;
+        vector<body_expansion>      m_q_body_expand;
+        vector<literal_vector>      m_q_clauses;
+
+        recfun_util & u() const { return m_util; }
+        ast_manager & m() { return get_manager(); }
+        bool is_defined(app * f) const { return u().is_defined(f); }
+        bool is_case_pred(app * f) const { return u().is_case_pred(f); }
+
+        bool is_defined(enode * e) const { return is_defined(e->get_owner()); }
+        bool is_case_pred(enode * e) const { return is_case_pred(e->get_owner()); }
+
+        void reset_queues();
+        expr_ref apply_args(recfun::vars const & vars, ptr_vector<expr> const & args, expr * e); //!< substitute variables by args
+        app_ref apply_pred(recfun::case_pred const & p, ptr_vector<expr> const & args); //<! apply predicate to args
+        void assert_macro_axiom(case_expansion & e);
+        void assert_case_axioms(case_expansion & e);
+        void assert_body_axiom(body_expansion & e);
+        void max_depth_conflict(void);
+    protected:
+        void push_case_expand(case_expansion&& e) { m_q_case_expand.push_back(e); }
+        void push_body_expand(body_expansion&& e) { m_q_body_expand.push_back(e); }
+
+        bool internalize_atom(app * atom, bool gate_ctx) override;
+        bool internalize_term(app * term) override;
+        void reset_eh() override;
+        void relevant_eh(app * n) override;
+        char const * get_name() const override;
+        final_check_status final_check_eh() override;
+        void assign_eh(bool_var v, bool is_true) override;
+        void push_scope_eh() override;
+        void pop_scope_eh(unsigned num_scopes) override;
+        void restart_eh() override;
+        bool can_propagate() override;
+        void propagate() override;
+        lbool validate_unsat_core(expr_ref_vector &) override;
+
+        void new_eq_eh(theory_var v1, theory_var v2) override {}
+        void new_diseq_eh(theory_var v1, theory_var v2) override {}
+        void add_theory_assumptions(expr_ref_vector & assumptions) override;
+
+    public:
+        theory_recfun(ast_manager & m);
+        virtual ~theory_recfun() override;
+        void setup_params(); // read parameters
+        virtual theory * mk_fresh(context * new_ctx) override;
+        virtual void display(std::ostream & out) const override;
+        virtual void collect_statistics(::statistics & st) const override;
+        unsigned get_max_depth() const { return m_max_depth; }
+        void set_max_depth(unsigned n) { SASSERT(n>0); m_max_depth = n; }
+    };
+}
+
+#endif