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());
     ast_manager & m = g->m();
     bool produce_proofs = g->proofs_enabled();
     rw r(m, produce_proofs);
     #pragma omp critical (tactic_cancel)
     {
         m_rw = &r;
     }
     mc = 0; pc = 0; core = 0; result.reset();
     tactic_report report("distribute-forall", *g);
     
     expr_ref   new_curr(m);
     proof_ref  new_pr(m);
     unsigned size = g->size();
     for (unsigned idx = 0; idx < size; idx++) {
         if (g->inconsistent())
             break;
         expr * curr = g->form(idx);
         r(curr, new_curr, new_pr);
         if (g->proofs_enabled()) {
             proof * pr = g->pr(idx);
             new_pr     = m.mk_modus_ponens(pr, new_pr);
         }
         g->update(idx, new_curr, new_pr, g->dep(idx));
     }
     
     g->inc_depth();
     result.push_back(g.get());
     TRACE("distribute-forall", g->display(tout););

        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;
            tactic_report report("elim-term-ite", *g);
            bool produce_proofs = g->proofs_enabled();
            m_rw.cfg().m_produce_models = g->models_enabled();

            m_rw.m_cfg.m_num_fresh = 0;
            m_rw.m_cfg.m_goal = g.get();
            expr_ref   new_curr(m);
            proof_ref  new_pr(m);
            unsigned   size = g->size();
            for (unsigned idx = 0; idx < size; idx++) {
                expr * curr = g->form(idx);
                m_rw(curr, new_curr, new_pr);
                if (produce_proofs) {
                    proof * pr = g->pr(idx);
                    new_pr     = m.mk_modus_ponens(pr, new_pr);
                }
                g->update(idx, new_curr, new_pr, g->dep(idx));
            }
            mc = m_rw.m_cfg.m_mc.get();
            report_tactic_progress(":elim-term-ite-consts", m_rw.m_cfg.m_num_fresh);
            g->inc_depth();
            result.push_back(g.get());
            TRACE("elim_term_ite", g->display(tout););

        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;
            tactic_report report("qe", *g);
            m_fparams.m_model = g->models_enabled();
            proof_ref new_pr(m);
            expr_ref new_f(m);
            bool produce_proofs = g->proofs_enabled();

            unsigned sz = g->size();
            for (unsigned i = 0; i < sz; i++) {
                checkpoint();
                if (g->inconsistent())
                    break;
                expr * f = g->form(i);
                if (!has_quantifiers(f))
                    continue;
                m_qe(m.mk_true(), f, new_f);
                new_pr = 0;
                if (produce_proofs) {
                    new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
                }
                g->update(i, new_f, new_pr, g->dep(i));                
            }
            g->inc_depth();
            result.push_back(g.get());
            TRACE("qe", g->display(tout););

 void operator()(goal_ref const & g,
                 goal_ref_buffer & result,
                 model_converter_ref & mc,
                 proof_converter_ref & pc,
                 expr_dependency_ref & core) override {
     mc = nullptr; pc = nullptr; core = nullptr;
     bool produce_proofs = g->proofs_enabled();
     tactic_report report("dt2bv", *g);
     unsigned   size = g->size();
     expr_fast_mark1 visited;
     check_fd proc(*this);
     for (unsigned i = 0; i < size; ++i) {
         quick_for_each_expr(proc, visited, g->form(i));
     }
     obj_hashtable<sort>::iterator it = m_non_fd_sorts.begin(), end = m_non_fd_sorts.end();
     for (; it != end; ++it) {
         m_fd_sorts.remove(*it);
     }
     if (!m_fd_sorts.empty()) {
         ref<extension_model_converter> ext = alloc(extension_model_converter, m);
         ref<filter_model_converter> filter = alloc(filter_model_converter, m);
         enum2bv_rewriter rw(m, m_params);
         rw.set_is_fd(&m_is_fd);            
         expr_ref   new_curr(m);
         proof_ref  new_pr(m);
         for (unsigned idx = 0; idx < size; idx++) {
             rw(g->form(idx), new_curr, new_pr);
             if (produce_proofs) {
                 proof * pr = g->pr(idx);
                 new_pr = m.mk_modus_ponens(pr, new_pr);
             }
             g->update(idx, new_curr, new_pr, g->dep(idx));
         }
         expr_ref_vector bounds(m);
         rw.flush_side_constraints(bounds);
         for (unsigned i = 0; i < bounds.size(); ++i) {
             g->assert_expr(bounds[i].get());
         }
         {
             obj_map<func_decl, func_decl*>::iterator it = rw.enum2bv().begin(), end = rw.enum2bv().end();
             for (; it != end; ++it) {
                 filter->insert(it->m_value);
             }
         }
         {
             obj_map<func_decl, expr*>::iterator it = rw.enum2def().begin(), end = rw.enum2def().end();
             for (; it != end; ++it) {
                 ext->insert(it->m_key, it->m_value);
             }
         }
         
         mc = concat(filter.get(), ext.get());
         report_tactic_progress(":fd-num-translated", rw.num_translated());
     }
     g->inc_depth();
     result.push_back(g.get());
     TRACE("dt2bv", g->display(tout););

        void operator()(goal_ref const & g, 
                        goal_ref_buffer & result) {
            SASSERT(g->is_well_sorted());
            fail_if_proof_generation("occf", g);

            bool produce_models = g->models_enabled();
            tactic_report report("occf", *g);
            
            m_mc = nullptr;
            
            ptr_vector<expr> new_lits;
            
            cnstr2bvar c2b;
            
            unsigned sz = g->size();
            for (unsigned i = 0; i < sz; i++) {
                checkpoint();
                expr * f = g->form(i);
                expr_dependency * d = g->dep(i);
                if (!m.is_or(f))
                    continue;
                app * cls = to_app(f);
                if (!is_target(cls))
                    continue;
                if (produce_models && !m_mc) {
                    m_mc = alloc(generic_model_converter, m, "occf");
                    g->add(m_mc);
                }
                expr * keep = nullptr;
                new_lits.reset();
                unsigned num = cls->get_num_args();
                for (unsigned j = 0; j < num; j++) {
                    expr * l = cls->get_arg(j);
                    if (is_constraint(l)) {
                        expr * new_l = get_aux_lit(c2b, l, g);
                        if (new_l != nullptr) {
                            new_lits.push_back(new_l);
                        }
                        else if (keep == nullptr) {
                            keep = l;
                        }
                        else {
                            new_l = mk_aux_lit(c2b, l, produce_models, g);
                            new_lits.push_back(new_l);
                        }
                    }
                    else {
                        new_lits.push_back(l);
                    }
                }
                if (keep != nullptr)
                    new_lits.push_back(keep);
                g->update(i, m.mk_or(new_lits.size(), new_lits.c_ptr()), nullptr, d);
            }
            g->inc_depth();
            result.push_back(g.get());
            TRACE("occf", g->display(tout););

 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; result.reset();
     
     TRACE("sls", g->display(tout););

 virtual void operator()(goal_ref const & g, 
                         goal_ref_buffer & result, 
                         model_converter_ref & mc, 
                         proof_converter_ref & pc,
                         expr_dependency_ref & core) {
     fail_if_proof_generation("aig", g);
     mc = 0; pc = 0; core = 0;
     operator()(g);
     g->inc_depth();
     result.push_back(g.get());
 }

 virtual void operator()(goal_ref const & in, 
                         goal_ref_buffer & result, 
                         model_converter_ref & mc, 
                         proof_converter_ref & pc,
                         expr_dependency_ref & core) {
     
     mc = 0; pc = 0; core = 0;
     reduce(*(in.get()));
     in->inc_depth();
     result.push_back(in.get());
 }

 void reduce_core(goal_ref const& g, goal_ref_buffer& result) {
     init(g);
     m_context.push();
     assert_clauses(g);
     m_context.push();   // internalize assertions. 
     prune_clauses();
     goal_ref r(g);
     insert_result(r);
     r->elim_true();
     result.push_back(r.get());        
     m_context.pop(2);
     TRACE("unit_subsumption_tactic", g->display(tout); r->display(tout););

        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());
            m_proofs_enabled      = g->proofs_enabled();
            m_produce_models      = g->models_enabled();
            m_produce_unsat_cores = g->unsat_core_enabled();

            mc = 0; pc = 0; core = 0; result.reset();
            tactic_report report("fpa2bv", *g);
            m_rw.reset();

            TRACE("fpa2bv", tout << "BEFORE: " << std::endl; g->display(tout););

 void operator()(goal_ref const & g, 
                 goal_ref_buffer & result) {
     tactic_report report("add-bounds", *g);
     bound_manager bm(m);
     expr_fast_mark1 visited;
     add_bound_proc proc(bm, *(g.get()), m_lower, m_upper);
     unsigned sz = g->size();
     for (unsigned i = 0; i < sz; i++)
         quick_for_each_expr(proc, visited, g->form(i));
     visited.reset();
     g->inc_depth();
     result.push_back(g.get());
     if (proc.m_num_bounds > 0) 
         g->updt_prec(goal::UNDER);
     report_tactic_progress(":added-bounds", proc.m_num_bounds);
     TRACE("add_bounds", g->display(tout););

    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());
        pc = 0; core = 0;

        if (g->proofs_enabled()) {
            throw tactic_exception("pb-preprocess does not support proofs");
        }

        pb_preproc_model_converter* pp = alloc(pb_preproc_model_converter, m);
        mc = pp;

        g->inc_depth();        
        result.push_back(g.get());       
        while (simplify(g, *pp));
        // decompose(g);
    }

    void operator()(goal_ref const & g, goal_ref_buffer & result,
                    model_converter_ref & mc, proof_converter_ref & pc,
                    expr_dependency_ref & core) override {
        mc = nullptr;
        tactic_report report("collect-statistics", *g);

        collect_proc cp(m, m_stats);
        expr_mark visited;
        const unsigned sz = g->size();
        for (unsigned i = 0; i < sz; i++)
            for_each_expr(cp, visited, g->form(i));

        std::cout << "(" << std::endl;
        stats_type::iterator it = m_stats.begin();
        stats_type::iterator end = m_stats.end();
        for (; it != end; it++)
            std::cout << " :" << it->first << "    " << it->second << std::endl;
        std::cout << ")" << std::endl;

        g->inc_depth();
        result.push_back(g.get());
    }

 void operator()(goal_ref const & g, 
                 goal_ref_buffer & result, 
                 model_converter_ref & mc, 
                 proof_converter_ref & pc,
                 expr_dependency_ref & core) {
     mc = 0; pc = 0; core = 0;
     
     if (!is_target(*g))
         throw tactic_exception("bv1 blaster cannot be applied to goal");
     
     tactic_report report("bv1-blaster", *g);
     m_num_steps = 0;
     
     bool proofs_enabled = g->proofs_enabled();
     expr_ref   new_curr(m());
     proof_ref  new_pr(m());
     unsigned   size = g->size();
     for (unsigned idx = 0; idx < size; idx++) {
         if (g->inconsistent())
             break;
         expr * curr = g->form(idx);
         m_rw(curr, new_curr, new_pr);
         m_num_steps += m_rw.get_num_steps();
         if (proofs_enabled) {
             proof * pr = g->pr(idx);
             new_pr     = m().mk_modus_ponens(pr, new_pr);
         }
         g->update(idx, new_curr, new_pr, g->dep(idx));
     }
     
     if (g->models_enabled())
         mc = mk_bv1_blaster_model_converter(m(), m_rw.cfg().m_const2bits);
     g->inc_depth();
     result.push_back(g.get());
     m_rw.cfg().cleanup();
 }

    virtual void operator()(goal_ref const & in,
                            goal_ref_buffer & result,
                            model_converter_ref & mc,
                            proof_converter_ref & pc,
                            expr_dependency_ref & core) {

        bool models_enabled = in->models_enabled();
        bool proofs_enabled = in->proofs_enabled();
        bool cores_enabled  = in->unsat_core_enabled();

        ast_manager & m = in->m();
        goal_ref_buffer      r1;
        model_converter_ref mc1;
        proof_converter_ref pc1;
        expr_dependency_ref core1(m);
        result.reset();
        mc   = 0;
        pc   = 0;
        core = 0;
        m_t1->operator()(in, r1, mc1, pc1, core1);
        SASSERT(!is_decided(r1) || (!pc1 && !core1)); // the pc and core of decided goals is 0
        unsigned r1_size = r1.size();
        SASSERT(r1_size > 0);
        checkpoint();
        if (r1_size == 1) {
            if (r1[0]->is_decided()) {
                result.push_back(r1[0]);
                if (models_enabled) mc = mc1;
                SASSERT(!pc); SASSERT(!core);
                return;
            }
            goal_ref r1_0 = r1[0];
            m_t2->operator()(r1_0, result, mc, pc, core);
            if (models_enabled) mc = concat(mc1.get(), mc.get());
            if (proofs_enabled) pc = concat(pc1.get(), pc.get());
            if (cores_enabled) core = m.mk_join(core1.get(), core);
        }
        else {
            if (cores_enabled) core = core1;
            proof_converter_ref_buffer pc_buffer;
            model_converter_ref_buffer mc_buffer;
            sbuffer<unsigned>          sz_buffer;
            goal_ref_buffer            r2;
            for (unsigned i = 0; i < r1_size; i++) {
                checkpoint();
                goal_ref g = r1[i];
                r2.reset();
                model_converter_ref mc2;
                proof_converter_ref pc2;
                expr_dependency_ref  core2(m);
                m_t2->operator()(g, r2, mc2, pc2, core2);
                if (is_decided(r2)) {
                    SASSERT(r2.size() == 1);
                    if (is_decided_sat(r2)) {
                        // found solution...
                        result.push_back(r2[0]);
                        if (models_enabled) {
                            // mc2 contains the actual model
                            model_ref md;
                            md = alloc(model, m);
                            apply(mc2, md, 0);
                            apply(mc1, md, i);
                            mc   = model2model_converter(md.get());
                        }
                        SASSERT(!pc); SASSERT(!core);
                        return;
                    }
                    else {
                        SASSERT(is_decided_unsat(r2));
                        // the proof and unsat core of a decided_unsat goal are stored in the node itself.
                        // pc2 and core2 must be 0.
                        SASSERT(!pc2);
                        SASSERT(!core2);
                        if (models_enabled) mc_buffer.push_back(0);
                        if (proofs_enabled) pc_buffer.push_back(proof2proof_converter(m, r2[0]->pr(0)));
                        if (models_enabled || proofs_enabled) sz_buffer.push_back(0);
                        if (cores_enabled) core = m.mk_join(core.get(), r2[0]->dep(0));
                    }
                }
                else {
                    result.append(r2.size(), r2.c_ptr());
                    if (models_enabled) mc_buffer.push_back(mc2.get());
                    if (proofs_enabled) pc_buffer.push_back(pc2.get());
                    if (models_enabled || proofs_enabled) sz_buffer.push_back(r2.size());
                    if (cores_enabled) core = m.mk_join(core.get(), core2.get());
                }
            }

            if (result.empty()) {
                // all subgoals were shown to be unsat.
                // create an decided_unsat goal with the proof
                in->reset_all();
                proof_ref pr(m);
                if (proofs_enabled)
                    apply(m, pc1, pc_buffer, pr);
                SASSERT(cores_enabled || core == 0);
                in->assert_expr(m.mk_false(), pr, core);
                core = 0;
                result.push_back(in.get());
                SASSERT(!mc); SASSERT(!pc); SASSERT(!core);
//.........这里部分代码省略.........

    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););

 subgoal_proof_converter(proof_converter* pc, unsigned n, goal * const* goals):
     m_pc(pc)
 {
     for (unsigned i = 0; i < n; ++i) m_goals.push_back(goals[i]);
 }