void finalize(pdecl_manager & m) {
     if (m_num_params == 0) {
         SASSERT(m_map.empty());
         if (m_const)
             m.m().dec_ref(m_const);
         m_const = 0;
     }
     else {
         SASSERT(m_const == 0);
         obj_map<sort, void *>::iterator it  = m_map.begin();
         obj_map<sort, void *>::iterator end = m_map.end();
         for (; it != end; ++it) {
             m.m().dec_ref((*it).m_key);
             if (m_num_params == 1) {
                 m.m().dec_ref(static_cast<sort*>((*it).m_value));
             }
             else {
                 psort_inst_cache * child = static_cast<psort_inst_cache*>((*it).m_value);
                 child->finalize(m);
                 child->~psort_inst_cache();
                 m.a().deallocate(sizeof(psort_inst_cache), child);
             }
         }
         m_map.reset();
     }
 }

 void add_entry(app* term, expr* value,
     obj_map<func_decl, func_interp*>& interpretations) {
     func_interp* fi = nullptr;
     func_decl * const declaration = term->get_decl();
     const unsigned sz = declaration->get_arity();
     SASSERT(sz == term->get_num_args());
     if (!interpretations.find(declaration, fi)) {
         fi = alloc(func_interp, m_m, sz);
         interpretations.insert(declaration, fi);
     }
     fi->insert_new_entry(term->get_args(), value);
 }

pb2bv_model_converter::pb2bv_model_converter(ast_manager & _m, obj_map<func_decl, expr*> const & c2bit, bound_manager const & bm):
    m(_m) {
    obj_map<func_decl, expr*>::iterator it  = c2bit.begin();
    obj_map<func_decl, expr*>::iterator end = c2bit.end();
    for ( ; it != end; it++) {
        m_c2bit.push_back(func_decl_pair(it->m_key, to_app(it->m_value)->get_decl()));
        m.inc_ref(it->m_key);
        m.inc_ref(to_app(it->m_value)->get_decl());
    }      
    bound_manager::iterator it2  = bm.begin();
    bound_manager::iterator end2 = bm.end();
    for (; it2 != end2; ++it2) {
        expr * c = *it2;
        SASSERT(is_uninterp_const(c));
        func_decl * d = to_app(c)->get_decl();
        if (!c2bit.contains(d)) {
            SASSERT(d->get_arity() == 0);
            m.inc_ref(d);
            m_c2bit.push_back(func_decl_pair(d, static_cast<func_decl*>(nullptr)));
        }
    }
}

    virtual void operator()(
        goal_ref const & g, 
        goal_ref_buffer & result, 
        model_converter_ref & mc, 
        proof_converter_ref & pc,
        expr_dependency_ref & core) {
        SASSERT(g->is_well_sorted());
        mc = 0; pc = 0; core = 0;
        m_trail.reset();
        m_fd.reset();
        m_max.reset();
        m_nonfd.reset();
        m_bounds.reset();
        ref<bvmc> mc1 = alloc(bvmc);

        tactic_report report("eq2bv", *g);

        m_bounds(*g);

        for (unsigned i = 0; i < g->size(); i++) {            
            collect_fd(g->form(i));
        }
        cleanup_fd(mc1);
        
        if (m_max.empty()) {
            result.push_back(g.get());
            return;
        }

        for (unsigned i = 0; i < g->size(); i++) {            
            expr_ref   new_curr(m);
            proof_ref  new_pr(m);  
            if (is_bound(g->form(i))) {
                g->update(i, m.mk_true(), 0, 0);
                continue;
            }
            m_rw(g->form(i), new_curr, new_pr);
            if (m.proofs_enabled() && !new_pr) {
                new_pr = m.mk_rewrite(g->form(i), new_curr);
                new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
            }
            g->update(i, new_curr, new_pr, g->dep(i));
        }
        obj_map<expr, unsigned>::iterator it = m_max.begin(), end = m_max.end();
        for (; it != end; ++it) {
            expr* c = it->m_key;
            bool strict;
            rational r;
            if (m_bounds.has_lower(c, r, strict)) {
                SASSERT(!strict);
                expr* d = m_fd.find(c);
                g->assert_expr(bv.mk_ule(bv.mk_numeral(r, m.get_sort(d)), d), m_bounds.lower_dep(c));
            }
            if (m_bounds.has_upper(c, r, strict)) {
                SASSERT(!strict);
                expr* d = m_fd.find(c);
                g->assert_expr(bv.mk_ule(d, bv.mk_numeral(r, m.get_sort(d))), m_bounds.upper_dep(c));
            }
        }        
        g->inc_depth();
        mc = mc1.get();
        result.push_back(g.get());
        TRACE("pb", g->display(tout););

 void get_units(obj_map<expr, bool>& units) override { units.reset(); }

 void mk_const(func_decl * f, expr_ref & result) {
     SASSERT(f->get_family_id() == null_family_id);
     SASSERT(f->get_arity() == 0);
     expr * r;
     if (m_const2bits.find(f, r)) {
         result = r;
         return;
     }
     sort * s = f->get_range();
     SASSERT(butil().is_bv_sort(s));
     unsigned bv_size = butil().get_bv_size(s);
     if (bv_size == 1) {
         result = m().mk_const(f);
         return;
     }
     sort * b = butil().mk_sort(1);
     ptr_buffer<expr> bits;
     for (unsigned i = 0; i < bv_size; i++) {
         bits.push_back(m().mk_fresh_const(0, b));
     }
     r = butil().mk_concat(bits.size(), bits.c_ptr());
     m_saved.push_back(r);
     m_const2bits.insert(f, r);
     result = r;
 }

 void reset()
 {
     m_cache.reset();
     m_units.reset();
     m_hyps.reset();
     m_hypmark.reset();
     m_pinned.reset();
 }

 void cache_result(expr * t, subpaving::var x, mpz const & n, mpz const & d) {
     SASSERT(!m_cache.contains(t));
     SASSERT(m_cached_numerators.size()   == m_cached_vars.size());
     SASSERT(m_cached_denominators.size() == m_cached_vars.size());
     if (t->get_ref_count() <= 1) 
         return;
     unsigned idx = m_cached_vars.size();
     m_cache.insert(t, idx);
     m().inc_ref(t);
     m_cached_vars.push_back(x);
     m_cached_numerators.push_back(n);
     m_cached_denominators.push_back(d);
 }

void ctx_propagate_assertions::assert_eq_core(expr * t, app * val) {
    if (m_assertions.contains(t)) {
        // This branch can only happen when m_max_depth was reached.
        // It can happen when m_assertions contains an entry t->val',
        //  but (= t val) was not simplified to (= val' val)
        //  because the simplifier stopped at depth m_max_depth
        return;
    }

    CTRACE("assert_eq_bug", m_assertions.contains(t),
           tout << "t:\n" << mk_ismt2_pp(t, m) << "\nval:\n" << mk_ismt2_pp(val, m) << "\n";
           expr * old_val = 0;
           m_assertions.find(t, old_val);
           tout << "old_val:\n" << mk_ismt2_pp(old_val, m) << "\n";);

        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
            result_pr = 0;
            func_decl * new_f;
            if (m_f2f.find(f, new_f)) {
                result = m().mk_app(new_f, num, args);
                return BR_DONE;
            }

            if (!must_remap(f))
                return BR_FAILED;

            if (m().is_eq(f)) {
                result = m().mk_eq(args[0], args[1]);
                return BR_DONE;
            }

            if (m().is_ite(f)) {
                result = m().mk_ite(args[0], args[1], args[2]);
                return BR_DONE;
            }

            if (f->get_family_id() != null_family_id || f->get_info() != 0) {
                throw elim_distinct_exception("uninterpreted sort is used in interpreted function symbol");
            }

            new_f = remap(f);
            result = m().mk_app(new_f, num, args);
            return BR_DONE;
        }

    proof *mk_lemma_core(proof *pf, expr *fact)
    {
        ptr_buffer<expr> args;
        expr_ref lemma(m);

        if (m.is_or(fact)) {
            for (unsigned i = 0, sz = to_app(fact)->get_num_args(); i < sz; ++i) {
                expr *a = to_app(fact)->get_arg(i);
                if (!is_reduced(a))
                { args.push_back(a); }
            }
        } else if (!is_reduced(fact))
        { args.push_back(fact); }


        if (args.size() == 0) { return pf; }
        else if (args.size() == 1) {
            lemma = args.get(0);
        } else {
            lemma = m.mk_or(args.size(), args.c_ptr());
        }
        proof* res = m.mk_lemma(pf, lemma);
        m_pinned.push_back(res);

        if (m_hyps.contains(lemma))
        { m_units.insert(lemma, res); }
        return res;
    }

    // returns true if (hypothesis (not a)) would be reduced
    bool is_reduced(expr *a)
    {
        expr_ref e(m);
        if (m.is_not(a)) { e = to_app(a)->get_arg(0); }
        else { e = m.mk_not(a); }

        return m_units.contains(e);
    }

 func_decl * remap(func_decl * f) {
     ptr_buffer<sort> new_domain;
     sort * new_range = remap(f->get_range());
     for (unsigned i = 0; i < f->get_arity(); i++)
         new_domain.push_back(remap(f->get_domain(i)));
     func_decl * new_f = m().mk_func_decl(f->get_name(), new_domain.size(), new_domain.c_ptr(), new_range);
     m_asts.push_back(new_f);
     m_asts.push_back(f);
     m_f2f.insert(f, new_f);
     return new_f;
 }

 void pop(unsigned num_scopes) {
     SASSERT(m_bounds.empty()); // bounds must be flushed before pop.
     if (num_scopes > 0) {
         SASSERT(num_scopes <= m_enum_consts_lim.size());
         unsigned new_sz = m_enum_consts_lim.size() - num_scopes;
         unsigned lim = m_enum_consts_lim[new_sz];
         for (unsigned i = m_enum_consts.size(); i > lim; ) {
             --i;
             func_decl* f = m_enum_consts[i].get();
             func_decl* f_fresh = m_enum2bv.find(f);
             m_bv2enum.erase(f_fresh);
             m_enum2bv.erase(f);
             m_enum2def.erase(f);
         }
         m_enum_consts_lim.resize(new_sz);
         m_enum_consts.resize(lim);
         m_enum_defs.resize(lim);
         m_enum_bvs.resize(lim);
     }
     m_rw.reset();
 }

 void finalize(pdecl_manager & m) {
     if (m_num_params == 0) {
         SASSERT(m_map.empty());
         if (m_const)
             m.m().dec_ref(m_const);
         m_const = nullptr;
     }
     else {
         SASSERT(m_const == 0);
         for (auto kv : m_map) {
             m.m().dec_ref(kv.m_key);
             if (m_num_params == 1) {
                 m.m().dec_ref(static_cast<sort*>(kv.m_value));
             }
             else {
                 psort_inst_cache * child = static_cast<psort_inst_cache*>(kv.m_value);
                 child->finalize(m);
                 child->~psort_inst_cache();
                 m.a().deallocate(sizeof(psort_inst_cache), child);
             }
         }
         m_map.reset();
     }
 }

 void compute_marks(proof* pr)  {
     proof *p;
     proof_post_order pit(pr, m);
     while (pit.hasNext()) {
         p = pit.next();
         if (m.is_hypothesis(p)) {
             m_hypmark.mark(p, true);
             m_hyps.insert(m.get_fact(p));
         } 
         else {
             bool hyp_mark = compute_mark1(p);
             // collect units that are hyp-free and are used as hypotheses somewhere
             if (!hyp_mark && m.has_fact(p) && m_hyps.contains(m.get_fact(p))) { 
                 m_units.insert(m.get_fact(p), p); 
             }
         }
     }
 }

    subpaving::var process(expr * t, unsigned depth, mpz & n, mpz & d) {
        SASSERT(is_int_real(t));
        checkpoint();

        if (is_cached(t)) {
            unsigned idx = m_cache.find(t);
            qm().set(n, m_cached_numerators[idx]);
            qm().set(d, m_cached_denominators[idx]);
            return m_cached_vars[idx];
        }

        SASSERT(!is_quantifier(t));
        if (::is_var(t) || !m_autil.is_arith_expr(t)) {
            qm().set(n, 1);
            qm().set(d, 1);
            return mk_var_for(t);
        }

        return process_arith_app(to_app(t), depth, n, d);
    }

 void insert(expr* a, expr* b) {
     m_trail.push_back(b);
     m_mem.insert(a, b);
 }

    void reduce(proof* pf, proof_ref &out)
    {
        proof *res = nullptr;

        m_todo.reset();
        m_todo.push_back(pf);
        ptr_buffer<proof> args;
        bool dirty = false;

        while (!m_todo.empty()) {
            proof *p, *tmp, *pp;
            unsigned todo_sz;

            p = m_todo.back();
            if (m_cache.find(p, tmp)) {
                res = tmp;
                m_todo.pop_back();
                continue;
            }

            dirty = false;
            args.reset();
            todo_sz = m_todo.size();
            for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) {
                pp = m.get_parent(p, i);
                if (m_cache.find(pp, tmp)) {
                    args.push_back(tmp);
                    dirty = dirty || pp != tmp;
                } else {
                    m_todo.push_back(pp);
                }
            }

            if (todo_sz < m_todo.size()) { continue; }
            else { m_todo.pop_back(); }

            if (m.is_hypothesis(p)) {
                // hyp: replace by a corresponding unit
                if (m_units.find(m.get_fact(p), tmp)) {
                    res = tmp;
                } else { res = p; }
            }

            else if (!dirty) { res = p; }

            else if (m.is_lemma(p)) {
                //lemma: reduce the premise; remove reduced consequences from conclusion
                SASSERT(args.size() == 1);
                res = mk_lemma_core(args.get(0), m.get_fact(p));
                compute_mark1(res);
            } else if (m.is_unit_resolution(p)) {
                // unit: reduce units; reduce the first premise; rebuild unit resolution
                res = mk_unit_resolution_core(args.size(), args.c_ptr());
                compute_mark1(res);
            } else  {
                // other: reduce all premises; reapply
                if (m.has_fact(p)) { args.push_back(to_app(m.get_fact(p))); }
                SASSERT(p->get_decl()->get_arity() == args.size());
                res = m.mk_app(p->get_decl(), args.size(), (expr * const*)args.c_ptr());
                m_pinned.push_back(res);
                compute_mark1(res);
            }

            SASSERT(res);
            m_cache.insert(p, res);

            if (m.has_fact(res) && m.is_false(m.get_fact(res))) { break; }
        }

        out = res;
    }

 bool is_cached(expr * t) {
     return t->get_ref_count() > 1 && m_cache.contains(t);
 }