/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    expr_replacer.cpp

Abstract:

    Abstract (functor) for replacing constants with expressions.

Author:

    Leonardo (leonardo) 2011-04-29

Notes:

--*/
#include "ast/rewriter/expr_replacer.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/rewriter/th_rewriter.h"

void expr_replacer::operator()(expr * t, expr_ref & result, proof_ref & result_pr) {
    expr_dependency_ref result_dep(m());
    operator()(t, result, result_pr, result_dep);
}

void expr_replacer::operator()(expr * t, expr_ref & result) {
    proof_ref pr(m());
    operator()(t, result, pr);
}

struct expr_replacer::scoped_set_subst {
    expr_replacer & m_r;
    scoped_set_subst(expr_replacer & r, expr_substitution & s):m_r(r) { m_r.set_substitution(&s); }
    ~scoped_set_subst() { m_r.set_substitution(nullptr); }
};

void expr_replacer::apply_substitution(expr * s, expr * def, proof * def_pr, expr_ref & t) { 
    expr_substitution sub(m()); 
    sub.insert(s, def, def_pr);
    scoped_set_subst set(*this, sub);
    (*this)(t);
}
    
void expr_replacer::apply_substitution(expr * s, expr * def, expr_ref & t) { 
    expr_substitution sub(m()); 
    sub.insert(s, def);
    scoped_set_subst set(*this, sub);
    (*this)(t);
}

struct default_expr_replacer_cfg : public default_rewriter_cfg  {
    ast_manager &        m;
    expr_substitution *  m_subst;
    expr_dependency_ref  m_used_dependencies;

    default_expr_replacer_cfg(ast_manager & _m):
        m(_m),
        m_subst(nullptr),
        m_used_dependencies(_m) {
    }

    bool get_subst(expr * s, expr * & t, proof * & pr) { 
        if (m_subst == nullptr)
            return false;
        expr_dependency * d = nullptr;
        if (m_subst->find(s, t, pr, d)) {
            m_used_dependencies = m.mk_join(m_used_dependencies, d);
            return true;
        }
        return false;
    }

    bool max_steps_exceeded(unsigned num_steps) const { 
        return false;
    }
};

template class rewriter_tpl<default_expr_replacer_cfg>;

class default_expr_replacer : public expr_replacer {
    default_expr_replacer_cfg               m_cfg;
    rewriter_tpl<default_expr_replacer_cfg> m_replacer;
public:
    default_expr_replacer(ast_manager & m, bool proofs_enabled):
        m_cfg(m),
        m_replacer(m, m.proofs_enabled() && proofs_enabled, m_cfg) {
    }
    
    ast_manager & m() const override { return m_replacer.m(); }

    void set_substitution(expr_substitution * s) override {
        m_replacer.cleanup();
        m_replacer.cfg().m_subst = s;
    }
    
    void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & result_dep) override {
        result_dep = nullptr;
        m_replacer.operator()(t, result, result_pr);
        if (m_cfg.m_used_dependencies != 0) {
            result_dep = m_cfg.m_used_dependencies;
            m_replacer.reset(); // reset cache
            m_cfg.m_used_dependencies = nullptr;
        }
    }


    unsigned get_num_steps() const override {
        return m_replacer.get_num_steps();
    }

    void reset() override {
        m_replacer.reset();
    }
};

expr_replacer * mk_default_expr_replacer(ast_manager & m, bool proofs_allowed) {
    return alloc(default_expr_replacer, m, proofs_allowed);
}

/**
   \brief Adapter for using th_rewriter as an expr_replacer.
 */
class th_rewriter2expr_replacer : public expr_replacer {
    th_rewriter m_r;
public:
    th_rewriter2expr_replacer(ast_manager & m, params_ref const & p):
        m_r(m, p) {
    }

    ~th_rewriter2expr_replacer() override {}

    ast_manager & m() const override { return m_r.m(); }

    void set_substitution(expr_substitution * s) override { m_r.set_substitution(s); }

    void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & result_dep) override {
        m_r(t, result, result_pr);
        result_dep = m_r.get_used_dependencies();
        m_r.reset_used_dependencies();
    }

    unsigned get_num_steps() const override {
        return m_r.get_num_steps();
    }

    void reset() override {
        m_r.reset();
    }

};

expr_replacer * mk_expr_simp_replacer(ast_manager & m, params_ref const & p) {
    return alloc(th_rewriter2expr_replacer, m, p);
}