/*++
Copyright (c) 2013 Microsoft Corporation

Module Name:

    hnf.cpp

Abstract:

    Horn normal form conversion.

Author:

    Nikolaj Bjorner (nbjorner) 3-20-2013

Notes:

   Convert formula 

       (forall x f(x)) 

   into conjunction 
 
       (f1 xy) (f2 xy) (f3 xy)

   such that 

       (forall x f(x)) ~ /\ (forall xy (f_i xy))

   modulo definitions that are introduced.
    

   Convert proof with 
       asserted (forall xy (f' xy))

   To:      
       (forall xy (f' xy))             by mp~ 1, 2
    1. asserted/def-intro (forall xy (f xy)) 
    2. (forall xy (f xy))  ~ (forall xy (f' xy)) by trans, 3, 4
    3. (forall xy (f xy))  ~ (forall xy (f1 xy)) by pull quantifiers (rewrite)
    4. (forall xy (f1 xy)) ~ (forall xy (f' xy)) by oeq_quant_intro 5
    5. f1 xy ~ f' xy                             by sub-proof.
     
                
--*/
#include"hnf.h"
#include"warning.h"
#include"used_vars.h"
#include"well_sorted.h"
#include"var_subst.h"
#include"name_exprs.h"
#include"act_cache.h"
#include"cooperate.h"
#include"ast_pp.h"
#include"quant_hoist.h"
#include"dl_util.h"
#include"for_each_ast.h"
#include"for_each_expr.h"

class hnf::imp {
    ast_manager&          m;
    bool                  m_produce_proofs;
    volatile bool         m_cancel;
    expr_ref_vector       m_todo;
    proof_ref_vector      m_proofs;
    expr_ref_vector       m_refs;
    symbol                m_name;
    svector<symbol>       m_names;
    ptr_vector<sort>      m_sorts;
    quantifier_hoister    m_qh;
    obj_map<expr, app*>   m_memoize_disj;
    obj_map<expr, proof*> m_memoize_proof;
    func_decl_ref_vector  m_fresh_predicates;

public:
    imp(ast_manager & m):
        m(m),
        m_produce_proofs(false),
        m_cancel(false),
        m_todo(m),
        m_proofs(m),
        m_refs(m), 
        m_name("P"),
        m_qh(m),
        m_fresh_predicates(m) {
    }

    void operator()(expr * n, 
                    proof* p,
                    expr_ref_vector& result, 
                    proof_ref_vector& ps) {
        expr_ref fml(m);
        proof_ref pr(m);
        m_todo.reset();
        m_proofs.reset();
        m_refs.reset();
        m_memoize_disj.reset();
        m_memoize_proof.reset();
        m_fresh_predicates.reset();
        m_todo.push_back(n);
        m_proofs.push_back(p);
        m_produce_proofs = p != 0;
        while (!m_todo.empty() && !m_cancel) {
            fml = m_todo.back();
            pr = m_proofs.back();
            m_todo.pop_back();
            m_proofs.pop_back();
            mk_horn(fml, pr);
            if (fml) {
                result.push_back(fml);
                ps.push_back(pr);
            }
        }
        TRACE("hnf",
              tout << mk_pp(n, m) << "\n==>\n";
              for (unsigned i = 0; i < result.size(); ++i) {
                  tout << mk_pp(result[i].get(), m) << "\n";
              });
    }

    void set_cancel(bool f) {
        m_cancel = f;
    }

    void set_name(symbol const& n) {
        m_name = n;
    }

    func_decl_ref_vector const& get_fresh_predicates() {
        return m_fresh_predicates;
    }

    void reset() {
        m_cancel = false;
        m_todo.reset();
        m_proofs.reset();
        m_refs.reset();
        m_memoize_disj.reset();
        m_memoize_proof.reset();
        m_fresh_predicates.reset();
    }

    ast_manager& get_manager() { return m; }

private:

    bool produce_proofs() const {
        return m_produce_proofs;
    }

    bool is_predicate(expr* p) const {
        return is_app(p) && is_predicate(to_app(p)->get_decl());
    }

    bool is_predicate(func_decl* f) const {
        return m.is_bool(f->get_range()) && f->get_family_id() == null_family_id;
    }

    class contains_predicate_proc {
        imp const& m;
    public:
        struct found {};
        contains_predicate_proc(imp const& m): m(m) {}
        void operator()(var * n) {}
        void operator()(quantifier * n) {}
        void operator()(app* n) {
            if (m.is_predicate(n)) throw found();
        }
    };

    bool contains_predicate(expr* fml) const {
        contains_predicate_proc proc(*this);
        try {
            quick_for_each_expr(proc, fml);
        }
        catch (contains_predicate_proc::found) {
            return true;
        }
        return false;
    }


    void mk_horn(expr_ref& fml, proof_ref& premise) {
        expr* e1, *e2;
        expr_ref_vector body(m);
        proof_ref_vector defs(m);
        expr_ref fml0(m), fml1(m), fml2(m), head(m);
        proof_ref p(m);
        fml0 = fml;
        m_names.reset();
        m_sorts.reset();
        m_qh.pull_quantifier(true, fml0, &m_sorts, &m_names);
        if (premise){
            fml1 = bind_variables(fml0);
            if (!m_sorts.empty()) {
                proof* p1 = m.mk_pull_quant(fml, to_quantifier(fml1));
                premise = mk_modus_ponens(premise, p1);
            }
        }
        head = fml0;
        while (m.is_implies(head, e1, e2)) {
            body.push_back(e1);
            head = e2;
        }
        datalog::flatten_and(body);
        if (premise) {
            p = m.mk_rewrite(fml0, mk_implies(body, head));
        }

        //
        // Case:
        // A \/ B -> C
        // => 
        // A -> C
        // B -> C
        // 
        if (body.size() == 1 && m.is_or(body[0].get()) && contains_predicate(body[0].get())) {
            app* _or = to_app(body[0].get());
            unsigned sz = _or->get_num_args();
            expr* const* args = _or->get_args();
            for (unsigned i = 0; i < sz; ++i) {
                m_todo.push_back(bind_variables(m.mk_implies(args[i], head)));
                m_proofs.push_back(0);
            } 

            if (premise) {
                expr_ref f1 = bind_variables(mk_implies(body, head));
                expr* f2 = m.mk_and(sz, m_todo.c_ptr()+m_todo.size()-sz);
                proof_ref p2(m), p3(m);
                p2 = m.mk_def_axiom(m.mk_iff(f1, f2));
                p3 = mk_quant_intro(fml, f1, p);                    
                p2 = mk_transitivity(p3, p2);
                p2 = mk_modus_ponens(premise, p2);
                for (unsigned i = 0; i < sz; ++i) {
                    m_proofs[m_proofs.size()-sz+i] = m.mk_and_elim(p2, i);
                }
            }                
            fml = 0;
            return;
        }


        eliminate_disjunctions(body, defs);
        p = mk_congruence(p, body, head, defs);

        eliminate_quantifier_body(body, defs);
        p = mk_congruence(p, body, head, defs);          

        fml2 = mk_implies(body, head);

        fml = bind_variables(fml2);

        if (premise) {
            SASSERT(p);
            p = mk_quant_intro(fml1, fml, p);     
            premise = mk_modus_ponens(premise, p);
        }
    }

    proof* mk_quant_intro(expr* e1, expr* e2, proof* p) {
        if (m_sorts.empty()) {
            return p;
        }
        quantifier* q1 = to_quantifier(e1);
        quantifier* q2 = to_quantifier(e2);
        if (m.is_iff(m.get_fact(p))) {
            return m.mk_quant_intro(q1, q2, p);
        }
        if (m.is_oeq(m.get_fact(p))) {
            return m.mk_oeq_quant_intro(q1, q2, p);
        }
        UNREACHABLE();
        return p;
    }


    void eliminate_disjunctions(expr_ref_vector::element_ref& body, proof_ref_vector& proofs) {
        expr* b = body.get(); 
        expr* e1;
        bool negate_args = false;
        bool is_disj = false;
        unsigned num_disj = 0;
        expr* const* disjs = 0;
        if (!contains_predicate(b)) {
            return;
        }
        TRACE("hnf", tout << mk_pp(b, m) << "\n";);
        if (m.is_or(b)) {
            is_disj = true;
            negate_args = false;
            num_disj = to_app(b)->get_num_args();
            disjs = to_app(b)->get_args();
        }
        if (m.is_not(b, e1) && m.is_and(e1)) {
            is_disj = true;
            negate_args = true;
            num_disj = to_app(e1)->get_num_args();
            disjs = to_app(e1)->get_args();
        }
        if (is_disj) {
            app* old_head = 0;
            if (m_memoize_disj.find(b, old_head)) {
                body = old_head;
            }
            else {
                app_ref head = mk_fresh_head(b);
                proof_ref_vector defs(m);
                for (unsigned i = 0; i < num_disj; ++i) {
                    expr* e = disjs[i];
                    if (negate_args) {
                        e = m.mk_not(e);
                    }
                    m_todo.push_back(bind_variables(m.mk_implies(e, head)));
                    m_proofs.push_back(0);
                    if (produce_proofs()) {
                        defs.push_back(m.mk_def_intro(m_todo.back()));
                        m_proofs[m_proofs.size()-1] = defs.back();
                    }
                }
                if (produce_proofs()) {
                    proof* p = m.mk_apply_defs(body.get(), head, defs.size(), defs.c_ptr());
                    m_refs.push_back(p);
                    m_memoize_proof.insert(b, p);
                }
                m_memoize_disj.insert(b, head);
                m_refs.push_back(b);
                m_refs.push_back(head);
                // update the body to be the newly introduced head relation
                body = head;
            }

            if (produce_proofs()) {
                proofs.push_back(m_memoize_proof.find(b));
            }
        }
    }

    app_ref mk_fresh_head(expr* e) {
        ptr_vector<sort> sorts0, sorts1;
        get_free_vars(e, sorts0);
        expr_ref_vector args(m);
        for (unsigned i = 0; i < sorts0.size(); ++i) {
            if (sorts0[i]) {
                args.push_back(m.mk_var(i, sorts0[i]));
                sorts1.push_back(sorts0[i]);
            }
        }
        func_decl_ref f(m);
        f = m.mk_fresh_func_decl(m_name.str().c_str(), "", sorts1.size(), sorts1.c_ptr(), m.mk_bool_sort());
        m_fresh_predicates.push_back(f);
        return app_ref(m.mk_app(f, args.size(), args.c_ptr()), m);
    }

    void eliminate_disjunctions(expr_ref_vector& body, proof_ref_vector& proofs) {
        for (unsigned i = 0; i < body.size(); ++i) {
            expr_ref_vector::element_ref r = body[i];
            eliminate_disjunctions(r, proofs);
        }
    }

    void eliminate_quantifier_body(expr_ref_vector::element_ref& body, proof_ref_vector& proofs) {
        if (is_forall(body.get()) && contains_predicate(body.get())) {
            quantifier* q = to_quantifier(body.get());
            expr* e = q->get_expr();
            if (!is_predicate(e)) {
                app_ref head = mk_fresh_head(e);
                m_todo.push_back(bind_variables(m.mk_implies(e, head)));
                m_proofs.push_back(0);
                body = m.update_quantifier(q, head);
                if (produce_proofs()) {
                    proof* def_intro = m.mk_def_intro(m_todo.back());
                    proof* def_proof = m.mk_apply_def(e, head, def_intro);
                    proofs.push_back(m.mk_nnf_neg(q, body.get(), 1, &def_proof));
                    m_proofs[m_proofs.size()-1] = def_intro;
                }
            }
        }
    }

    void eliminate_quantifier_body(expr_ref_vector& body, proof_ref_vector& proofs) {
        for (unsigned i = 0; i < body.size(); ++i) {
            expr_ref_vector::element_ref r = body[i];
            eliminate_quantifier_body(r, proofs);
        }
    }

    app_ref mk_implies(expr_ref_vector const& body, expr* head) {
        switch (body.size()) {
        case 0: 
            return app_ref(to_app(head), m);
        case 1: 
            return app_ref(m.mk_implies(body[0], head), m);
        default:
            return app_ref(m.mk_implies(m.mk_and(body.size(), body.c_ptr()), head), m);
        }        
    }


    proof_ref mk_congruence(proof* p1, expr_ref_vector const& body, expr* head, proof_ref_vector& defs) {
        if (defs.empty()) {
            return proof_ref(p1, m);
        }
        else {
            SASSERT(p1);
            proof_ref p2(m), p3(m);
            app_ref fml = mk_implies(body, head);
            expr* fact = m.get_fact(p1);
            if (m.is_iff(fact)) {
                p1 = m.mk_iff_oeq(p1);
                fact = m.get_fact(p1);
            }
            VERIFY (m.is_oeq(fact) || m.is_eq(fact));
            app* e2 = to_app(to_app(fact)->get_arg(1));
            p2 = m.mk_oeq_congruence(e2, fml, defs.size(), defs.c_ptr());
            p3 = mk_transitivity(p1, p2);
            defs.reset();
            return proof_ref(p3, m);
        }
    }

    proof_ref mk_modus_ponens(proof* premise, proof* eq) {
        proof_ref result(m);
        result = m.mk_modus_ponens(premise, eq);
        if (m.get_fact(premise) == m.get_fact(result)) {
            result = premise;
        }
        return result;
    }

    proof* mk_transitivity(proof* p1, proof* p2) {
        if (p1) {
            app* f = to_app(m.get_fact(p1));
            if (f->get_arg(0) == f->get_arg(1)) {
                return p2;
            }
        }
        if (p2) {
            app* f = to_app(m.get_fact(p2));
            if (f->get_arg(0) == f->get_arg(1)) {
                return p1;
            }
        }
        return m.mk_transitivity(p1, p2);
    }

    expr_ref bind_variables(expr* e) {
        SASSERT(m_sorts.size() == m_names.size());
        if (m_sorts.empty()) {
            return expr_ref(e, m);
        }
        return expr_ref(m.mk_forall(m_sorts.size(), m_sorts.c_ptr(), m_names.c_ptr(), e), m);
    }

};

hnf::hnf(ast_manager & m) {
    m_imp = alloc(imp, m);
}

hnf::~hnf() {
    dealloc(m_imp);
}
    
void hnf::operator()(expr * n, proof* p, expr_ref_vector & rs, proof_ref_vector& ps) {
    m_imp->operator()(n, p, rs, ps);    
    TRACE("hnf", 
          ast_manager& m = rs.get_manager();
          tout << mk_ismt2_pp(n, m) << "\nHNF result:\n";
          for (unsigned i = 0; i < rs.size(); ++i) {
              tout << mk_pp(rs[i].get(), m) << "\n";
          }
          );
}

void hnf::set_cancel(bool f) {
    m_imp->set_cancel(f);
}

void hnf::set_name(symbol const& n) {
    m_imp->set_name(n);
}

void hnf::reset() {
    m_imp->reset();
}

func_decl_ref_vector const& hnf::get_fresh_predicates() {
    return m_imp->get_fresh_predicates();
}