/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    qe_tactic.cpp

Abstract:

    Quantifier elimination front-end for tactic framework.

Author:

    Leonardo de Moura (leonardo) 2011-12-28.

Revision History:

--*/
#include "tactic/tactical.h"
#include "tactic/filter_model_converter.h"
#include "util/cooperate.h"
#include "qe/qe.h"

class qe_tactic : public tactic {
    statistics               m_st;
    struct     imp {
        ast_manager &            m;
        smt_params               m_fparams;
        qe::expr_quant_elim      m_qe;

        imp(ast_manager & _m, params_ref const & p):
            m(_m),
            m_qe(m, m_fparams) {
            updt_params(p);
        }

        void updt_params(params_ref const & p) {
            m_fparams.updt_params(p);
            m_fparams.m_nlquant_elim = p.get_bool("qe_nonlinear", false);
            m_qe.updt_params(p);
        }

        void collect_param_descrs(param_descrs & r) {
            m_qe.collect_param_descrs(r);
        }

        void checkpoint() {
            if (m.canceled()) 
                throw tactic_exception(m.limit().get_cancel_msg());
            cooperate("qe");
        }

        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();
            g->elim_true();
            result.push_back(g.get());
            TRACE("qe", g->display(tout););
            SASSERT(g->is_well_sorted());
        }

        void collect_statistics(statistics & st) const {
            m_qe.collect_statistics(st);
        }

        void reset_statistics() {            
        }

    };
    
    imp *      m_imp;
    params_ref m_params;
public:
    qe_tactic(ast_manager & m, params_ref const & p):
        m_params(p) {
        m_imp = alloc(imp, m, p);
    }

    virtual tactic * translate(ast_manager & m) {
        return alloc(qe_tactic, m, m_params);
    }
        
    virtual ~qe_tactic() {
        dealloc(m_imp);
    }

    virtual void updt_params(params_ref const & p) {
        m_params = p;
        m_imp->updt_params(p);
    }

   
    virtual void collect_param_descrs(param_descrs & r) {
        r.insert("qe_nonlinear", CPK_BOOL, "(default: false) enable virtual term substitution.");
        m_imp->collect_param_descrs(r);
    }
    
    virtual void operator()(goal_ref const & in, 
                            goal_ref_buffer & result, 
                            model_converter_ref & mc, 
                            proof_converter_ref & pc,
                            expr_dependency_ref & core) {
        (*m_imp)(in, result, mc, pc, core);
        m_st.reset();
        m_imp->collect_statistics(m_st);
        
    }

    virtual void collect_statistics(statistics & st) const {
        st.copy(m_st);
    }

    virtual void reset_statistics() {
        m_st.reset();
    }

    
    virtual void cleanup() {
        ast_manager & m = m_imp->m;
        dealloc(m_imp);
        m_imp = alloc(imp, m, m_params);
    }
    
};

tactic * mk_qe_tactic(ast_manager & m, params_ref const & p) {
    return clean(alloc(qe_tactic, m, p));
}