/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    pdr_util.cpp

Abstract:

    Utility functions for PDR.

Author:

    Krystof Hoder (t-khoder) 2011-8-19.

Revision History:


Notes: 
    

--*/

#include <sstream>
#include "arith_simplifier_plugin.h"
#include "array_decl_plugin.h"
#include "ast_pp.h"
#include "basic_simplifier_plugin.h"
#include "bv_simplifier_plugin.h"
#include "bool_rewriter.h"
#include "dl_util.h"
#include "for_each_expr.h"
#include "smt_params.h"
#include "model.h"
#include "ref_vector.h"
#include "rewriter.h"
#include "rewriter_def.h"
#include "util.h"
#include "pdr_manager.h"
#include "pdr_util.h"
#include "arith_decl_plugin.h"
#include "expr_replacer.h"
#include "model_smt2_pp.h"
#include "poly_rewriter.h"
#include "poly_rewriter_def.h"
#include "arith_rewriter.h"
#include "scoped_proof.h"



namespace pdr {

    unsigned ceil_log2(unsigned u) {
        if (u == 0) { return 0; }
        unsigned pow2 = next_power_of_two(u);
        return get_num_1bits(pow2-1);
    }

    std::string pp_cube(const ptr_vector<expr>& model, ast_manager& m) {
        return pp_cube(model.size(), model.c_ptr(), m);
    }

    std::string pp_cube(const expr_ref_vector& model, ast_manager& m) {
        return pp_cube(model.size(), model.c_ptr(), m);
    }

    std::string pp_cube(const app_ref_vector& model, ast_manager& m) {
        return pp_cube(model.size(), model.c_ptr(), m);
    }
    
    std::string pp_cube(const app_vector& model, ast_manager& m) {
        return pp_cube(model.size(), model.c_ptr(), m);
    }

    std::string pp_cube(unsigned sz, app * const * lits, ast_manager& m) {
        return pp_cube(sz, (expr * const *)(lits), m);
    }

    std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& m) {
        std::stringstream res;
        res << "(";
        expr * const * end = lits+sz;
        for (expr * const * it = lits; it!=end; it++) {
            res << mk_pp(*it, m);
            if (it+1!=end) {
                res << ", ";
            }
        }
        res << ")";
        return res.str();
    }

    void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
        ast_manager& m = fml.get_manager();
        expr_ref_vector conjs(m);
        flatten_and(fml, conjs);
        obj_map<expr, unsigned> diseqs;
        expr* n, *lhs, *rhs;
        for (unsigned i = 0; i < conjs.size(); ++i) {
            if (m.is_not(conjs[i].get(), n) &&
                m.is_eq(n, lhs, rhs)) {
                if (!m.is_value(rhs)) {
                    std::swap(lhs, rhs);
                }
                if (!m.is_value(rhs)) {
                    continue;
                }
                diseqs.insert_if_not_there2(lhs, 0)->get_data().m_value++;
            }
        }
        expr_substitution sub(m);

        unsigned orig_size = conjs.size();
        unsigned num_deleted = 0;
        expr_ref val(m), tmp(m);
        proof_ref pr(m);
        pr = m.mk_asserted(m.mk_true());
        obj_map<expr, unsigned>::iterator it  = diseqs.begin();
        obj_map<expr, unsigned>::iterator end = diseqs.end();
        for (; it != end; ++it) {
            if (it->m_value >= threshold) {
                model.eval(it->m_key, val);
                sub.insert(it->m_key, val, pr);
                conjs.push_back(m.mk_eq(it->m_key, val));
                num_deleted += it->m_value;
            }
        }
        if (orig_size < conjs.size()) {
            scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer(m);
            rep->set_substitution(&sub);
            for (unsigned i = 0; i < orig_size; ++i) {
                tmp = conjs[i].get();
                (*rep)(tmp);
                if (m.is_true(tmp)) {
                    conjs[i] = conjs.back();
                    SASSERT(orig_size <= conjs.size());
                    conjs.pop_back();
                    SASSERT(orig_size <= 1 + conjs.size());
                    if (i + 1 == orig_size) {
                        // no-op.
                    }
                    else if (orig_size <= conjs.size()) {
                        // no-op
                    }
                    else {
                        SASSERT(orig_size == 1 + conjs.size());
                        --orig_size;
                        --i;
                    }
                }
                else {
                    conjs[i] = tmp;
                }
            }            
            IF_VERBOSE(2, verbose_stream() << "Deleted " << num_deleted << " disequalities " << conjs.size() << " conjuncts\n";);
        }
        fml = m.mk_and(conjs.size(), conjs.c_ptr());        
    }

    class test_diff_logic {
        ast_manager& m;
        arith_util a;
        bv_util    bv;
        bool m_is_dl;
        bool m_test_for_utvpi;

        bool is_numeric(expr* e) const {
            if (a.is_numeral(e)) {
                return true;
            }
            expr* cond, *th, *el;
            if (m.is_ite(e, cond, th, el)) {
                return is_numeric(th) && is_numeric(el);
            }
            return false;
        }
        
        bool is_arith_expr(expr *e) const {
            return is_app(e) && a.get_family_id() == to_app(e)->get_family_id();
        }

        bool is_offset(expr* e) const {
            if (a.is_numeral(e)) {
                return true;
            }
            expr* cond, *th, *el, *e1, *e2;
            if (m.is_ite(e, cond, th, el)) {
                return is_offset(th) && is_offset(el);
            }
            // recognize offsets.
            if (a.is_add(e, e1, e2)) {
                if (is_numeric(e1)) {
                    return is_offset(e2);
                }
                if (is_numeric(e2)) {
                    return is_offset(e1);
                }
                return false;
            }
            if (m_test_for_utvpi) {
                if (a.is_mul(e, e1, e2)) {
                    if (is_minus_one(e1)) {
                        return is_offset(e2);
                    }
                    if (is_minus_one(e2)) {
                        return is_offset(e1);
                    }
                }
            }
            return !is_arith_expr(e);
        }

        bool is_minus_one(expr const * e) const { 
            rational r; return a.is_numeral(e, r) && r.is_minus_one(); 
        }

        bool test_ineq(expr* e) const {
            SASSERT(a.is_le(e) || a.is_ge(e) || m.is_eq(e));
            SASSERT(to_app(e)->get_num_args() == 2);
            expr * lhs = to_app(e)->get_arg(0);
            expr * rhs = to_app(e)->get_arg(1);
            if (is_offset(lhs) && is_offset(rhs)) 
                return true;    
            if (!is_numeric(rhs)) 
                std::swap(lhs, rhs);
            if (!is_numeric(rhs)) 
                return false;    
            // lhs can be 'x' or '(+ x (* -1 y))'
            if (is_offset(lhs))
                return true;
            expr* arg1, *arg2;
            if (!a.is_add(lhs, arg1, arg2)) 
                return false;    
            // x
            if (m_test_for_utvpi) {
                return is_offset(arg1) && is_offset(arg2);
            }
            if (is_arith_expr(arg1)) 
                std::swap(arg1, arg2);
            if (is_arith_expr(arg1))
                return false;
            // arg2: (* -1 y)
            expr* m1, *m2;
            if (!a.is_mul(arg2, m1, m2))
                return false;
            return is_minus_one(m1) && is_offset(m2);
        }

        bool test_eq(expr* e) const {
            expr* lhs, *rhs;
            VERIFY(m.is_eq(e, lhs, rhs));
            if (!a.is_int_real(lhs)) {
                return true;
            }
            if (a.is_numeral(lhs) || a.is_numeral(rhs)) {
                return test_ineq(e);
            }
            return 
                test_term(lhs) && 
                test_term(rhs) &&
                !a.is_mul(lhs) &&
                !a.is_mul(rhs);
        }

        bool test_term(expr* e) const {
            if (m.is_bool(e)) {
                return true;
            }
            if (a.is_numeral(e)) {
                return true;
            }
            if (is_offset(e)) {
                return true;
            }
            expr* lhs, *rhs;
            if (a.is_add(e, lhs, rhs)) {
                if (!a.is_numeral(lhs)) {
                    std::swap(lhs, rhs);
                }
                return a.is_numeral(lhs) && is_offset(rhs);
            }
            if (a.is_mul(e, lhs, rhs)) {
                return is_minus_one(lhs) || is_minus_one(rhs);
            }
            return false;
        }

        bool is_non_arith_or_basic(expr* e) {
            if (!is_app(e)) {
                return false;
            }
            family_id fid = to_app(e)->get_family_id();

            if (fid == null_family_id && 
                !m.is_bool(e) && 
                to_app(e)->get_num_args() > 0) {
                return true;
            }
            return 
                fid != m.get_basic_family_id() &&
                fid != null_family_id &&
                fid != a.get_family_id() &&
                fid != bv.get_family_id();
        }

    public:
        test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true), m_test_for_utvpi(false) {}
       
        void test_for_utvpi() { m_test_for_utvpi = true; }

        void operator()(expr* e) {
            if (!m_is_dl) {
                return;
            }
            if (a.is_le(e) || a.is_ge(e)) {
                m_is_dl = test_ineq(e);
            }
            else if (m.is_eq(e)) {
                m_is_dl = test_eq(e);
            }
            else if (is_non_arith_or_basic(e)) {
                m_is_dl = false;
            }
            else if (is_app(e)) {
                app* a = to_app(e);                
                for (unsigned i = 0; m_is_dl && i < a->get_num_args(); ++i) {
                    m_is_dl = test_term(a->get_arg(i));
                }
            }

            if (!m_is_dl) {
                char const* msg = "non-diff: ";
                if (m_test_for_utvpi) {
                    msg = "non-utvpi: ";
                }
                IF_VERBOSE(1, verbose_stream() << msg << mk_pp(e, m) << "\n";);
            }
        }

        bool is_dl() const { return m_is_dl; }
    };

    bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) {
        test_diff_logic test(m);
        expr_fast_mark1 mark;
        for (unsigned i = 0; i < num_fmls; ++i) {
            quick_for_each_expr(test, mark, fmls[i]);
        } 
        return test.is_dl();
    }  

    bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) {
        test_diff_logic test(m);
        test.test_for_utvpi();
        expr_fast_mark1 mark;
        for (unsigned i = 0; i < num_fmls; ++i) {
            quick_for_each_expr(test, mark, fmls[i]);
        } 
        return test.is_dl();
    }  

    class arith_normalizer : public poly_rewriter<arith_rewriter_core> {
        ast_manager& m;
        arith_util   m_util;
        enum op_kind { LE, GE, EQ };
    public:
        arith_normalizer(ast_manager& m, params_ref const& p = params_ref()): poly_rewriter<arith_rewriter_core>(m, p), m(m), m_util(m) {}
        
        br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
            br_status st = BR_FAILED;
            if (m.is_eq(f)) {
                SASSERT(num_args == 2); return mk_eq_core(args[0], args[1], result);
            }

            if (f->get_family_id() != get_fid()) {
                return st;
            }
            switch (f->get_decl_kind()) {
            case OP_NUM: st = BR_FAILED; break;
            case OP_IRRATIONAL_ALGEBRAIC_NUM: st = BR_FAILED; break;
            case OP_LE:  SASSERT(num_args == 2); st = mk_le_core(args[0], args[1], result); break;
            case OP_GE:  SASSERT(num_args == 2); st = mk_ge_core(args[0], args[1], result); break;
            case OP_LT:  SASSERT(num_args == 2); st = mk_lt_core(args[0], args[1], result); break;
            case OP_GT:  SASSERT(num_args == 2); st = mk_gt_core(args[0], args[1], result); break;
            default: st = BR_FAILED; break;
            }
            return st;
        }      

    private:
        
        br_status mk_eq_core(expr* arg1, expr* arg2, expr_ref& result) {
            return mk_le_ge_eq_core(arg1, arg2, EQ, result);
        }
        br_status mk_le_core(expr* arg1, expr* arg2, expr_ref& result) {
            return mk_le_ge_eq_core(arg1, arg2, LE, result);
        }
        br_status mk_ge_core(expr* arg1, expr* arg2, expr_ref& result) {
            return mk_le_ge_eq_core(arg1, arg2, GE, result);
        }
        br_status mk_lt_core(expr* arg1, expr* arg2, expr_ref& result) {
            result = m.mk_not(m_util.mk_ge(arg1, arg2));
            return BR_REWRITE2;
        }
        br_status mk_gt_core(expr* arg1, expr* arg2, expr_ref& result) {
            result = m.mk_not(m_util.mk_le(arg1, arg2));
            return BR_REWRITE2;
        }

        br_status mk_le_ge_eq_core(expr* arg1, expr* arg2, op_kind kind, expr_ref& result) {
            if (m_util.is_real(arg1)) {
                numeral g(0);
                get_coeffs(arg1, g);
                get_coeffs(arg2, g);
                if (!g.is_one() && !g.is_zero()) {
                    SASSERT(g.is_pos());
                    expr_ref new_arg1 = rdiv_polynomial(arg1, g);
                    expr_ref new_arg2 = rdiv_polynomial(arg2, g);
                    switch(kind) {
                    case LE: result = m_util.mk_le(new_arg1, new_arg2); return BR_DONE;
                    case GE: result = m_util.mk_ge(new_arg1, new_arg2); return BR_DONE;
                    case EQ: result = m_util.mk_eq(new_arg1, new_arg2); return BR_DONE;
                    }
                }
            }
            return BR_FAILED;
        }

        void update_coeff(numeral const& r, numeral& g) {
            if (g.is_zero() || abs(r) < g) {
                g = abs(r);
            }
        }        

        void get_coeffs(expr* e, numeral& g) {
            rational r;
            unsigned sz;
            expr* const* args = get_monomials(e, sz);
            for (unsigned i = 0; i < sz; ++i) {
                expr* arg = args[i];
                if (!m_util.is_numeral(arg, r)) {
                    get_power_product(arg, r);
                }
                update_coeff(r, g);
            }
        }

        expr_ref rdiv_polynomial(expr* e, numeral const& g) {
            rational r;
            SASSERT(g.is_pos());
            SASSERT(!g.is_one());
            expr_ref_vector monomes(m);
            unsigned sz;           
            expr* const* args = get_monomials(e, sz);
            for (unsigned i = 0; i < sz; ++i) {
                expr* arg = args[i];
                if (m_util.is_numeral(arg, r)) {
                    monomes.push_back(m_util.mk_numeral(r/g, false));
                }
                else {
                    expr* p = get_power_product(arg, r);
                    r /= g;
                    if (r.is_one()) {
                        monomes.push_back(p);
                    }
                    else {
                        monomes.push_back(m_util.mk_mul(m_util.mk_numeral(r, false), p));
                    }
                }
            }
            expr_ref result(m);
            mk_add(monomes.size(), monomes.c_ptr(), result);
            return result;
        }
                
    };
    

    struct arith_normalizer_cfg: public default_rewriter_cfg {
        arith_normalizer m_r;
        bool rewrite_patterns() const { return false; }
        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
            return m_r.mk_app_core(f, num, args, result);
        }
        arith_normalizer_cfg(ast_manager & m, params_ref const & p):m_r(m,p) {}        
    };

    class arith_normalizer_star : public rewriter_tpl<arith_normalizer_cfg> {
        arith_normalizer_cfg m_cfg;
    public:
        arith_normalizer_star(ast_manager & m, params_ref const & p):
            rewriter_tpl<arith_normalizer_cfg>(m, false, m_cfg),
            m_cfg(m, p) {}
    };


    void normalize_arithmetic(expr_ref& t) {
        ast_manager& m = t.get_manager();
        scoped_no_proof _sp(m);
        params_ref p;
        arith_normalizer_star rw(m, p);
        expr_ref tmp(m);
        rw(t, tmp);
        t = tmp;                
    }

}

template class rewriter_tpl<pdr::arith_normalizer_cfg>;