/**
   \brief Return true if n is of the form (= a b)
*/
static bool is_iff(ast_manager & m, expr * n, expr * & a, expr * & b) {
    if (m.is_iff(n, a, b))
        return true;
    if (m.is_eq(n, a, b) && m.is_bool(a))
        return true;
    return false;
}

fpa_util::fpa_util(ast_manager & m):
    m_manager(m),
    m_fid(m.mk_family_id("fpa")),
    m_a_util(m),
    m_bv_util(m) {
    m_plugin = static_cast<fpa_decl_plugin*>(m.get_plugin(m_fid));
}

 void mk_new_rule_tail(ast_manager & m, app * pred, var_idx_set const & non_local_vars, unsigned & next_idx, varidx2var_map & varidx2var, 
                       sort_ref_buffer & new_rule_domain, expr_ref_buffer & new_rule_args, app_ref & new_pred) {
     expr_ref_buffer new_args(m);
     unsigned n  = pred->get_num_args();
     for (unsigned i = 0; i < n; i++) {
         expr * arg = pred->get_arg(i);
         if (m.is_value(arg)) {
             new_args.push_back(arg);
         }
         else {
             SASSERT(is_var(arg));
             int vidx      = to_var(arg)->get_idx();
             var * new_var = 0;
             if (!varidx2var.find(vidx, new_var)) {
                 new_var = m.mk_var(next_idx, to_var(arg)->get_sort());
                 next_idx++;
                 varidx2var.insert(vidx, new_var);
                 if (non_local_vars.contains(vidx)) {
                     // other predicates used this variable... so it should be in the domain of the filter
                     new_rule_domain.push_back(to_var(arg)->get_sort());
                     new_rule_args.push_back(new_var);
                 }
             }
             SASSERT(new_var != 0);
             new_args.push_back(new_var);
         }
     }
     new_pred = m.mk_app(pred->get_decl(), new_args.size(), new_args.c_ptr());
 }

static void validate_quant_solution(ast_manager& m, expr* fml, expr* guard, qe::def_vector const& defs) {
    // verify:
    //    new_fml => fml[t/x]
    scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer(m);
    app_ref_vector xs(m);
    expr_substitution sub(m);
    for (unsigned i = 0; i < defs.size(); ++i) {
        xs.push_back(m.mk_const(defs.var(i)));
        sub.insert(xs.back(), defs.def(i));
    }
    rep->set_substitution(&sub);
    expr_ref fml1(fml, m);
    (*rep)(fml1);
    expr_ref tmp(m);
    tmp = m.mk_not(m.mk_implies(guard, fml1));
    front_end_params fp;
    smt::kernel solver(m, fp);
    solver.assert_expr(tmp);
    lbool res = solver.check();
    //SASSERT(res == l_false);
    if (res != l_false) {
        std::cout << "Validation failed: " << res << "\n";
        std::cout << mk_pp(tmp, m) << "\n";
        model_ref model;
        solver.get_model(model);
        model_smt2_pp(std::cout, m, *model, 0);
        fatal_error(0);
    }
}

 ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()):
     m(m), m_params(p), m_solver(m, m_front_p),  
     m_arith(m), m_mk_app(m), m_fn(m), m_num_steps(0), 
     m_cancel(false) {
     sort* i_sort = m_arith.mk_int();
     m_fn = m.mk_func_decl(symbol(0xbeef101), i_sort, m.mk_bool_sort());
 }

void func_entry::deallocate(ast_manager & m, unsigned arity) {
    for (unsigned i = 0; i < arity; i++) {
        m.dec_ref(m_args[i]);
    }
    m.dec_ref(m_result);
    small_object_allocator & allocator = m.get_allocator();
    unsigned sz = get_obj_size(arity);
    allocator.deallocate(sz, this);
}

proof_checker::proof_checker(ast_manager& m) : m(m), m_todo(m), m_marked(), m_pinned(m), m_nil(m), 
                                               m_dump_lemmas(false), m_logic("AUFLIA"), m_proof_lemma_id(0) {
    symbol fam_name("proof_hypothesis");
    if (!m.has_plugin(fam_name)) {
        m.register_plugin(fam_name, alloc(hyp_decl_plugin));
    }
    m_hyp_fid = m.mk_family_id(fam_name);
    // m_spc_fid = m.get_family_id("spc");
    m_nil = m.mk_const(m_hyp_fid, OP_NIL);
}

static_features::static_features(ast_manager & m):
    m_manager(m),
    m_autil(m),
    m_bfid(m.get_basic_family_id()),
    m_afid(m.get_family_id("arith")),
    m_lfid(m.get_family_id("label")),
    m_label_sym("label"),
    m_pattern_sym("pattern"),
    m_expr_list_sym("expr-list") {
    reset();
}

 pb_fuzzer(ast_manager& m): m(m), rand(0), ctx(m, params), vars(m) {
     params.m_model = true;
     params.m_pb_enable_simplex = true;
     unsigned N = 3;
     for (unsigned i = 0; i < N; ++i) {
         std::stringstream strm;
         strm << "b" << i;
         vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()));
         std::cout << "(declare-const " << strm.str() << " Bool)\n";
     }
 }

/**
   \brief Little HACK for simplifying injectivity axioms
   
   \remark It is not covering all possible cases.
*/
bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result) {
    expr * n = q->get_expr();
    if (q->is_forall() && m.is_or(n) && to_app(n)->get_num_args() == 2) {
        expr * arg1 = to_app(n)->get_arg(0);
        expr * arg2 = to_app(n)->get_arg(1);
        if (m.is_not(arg2)) 
            std::swap(arg1, arg2);
        if (m.is_not(arg1) && 
            m.is_eq(to_app(arg1)->get_arg(0)) && 
            m.is_eq(arg2)) {
            expr * app1 = to_app(to_app(arg1)->get_arg(0))->get_arg(0);
            expr * app2 = to_app(to_app(arg1)->get_arg(0))->get_arg(1);
            expr * var1 = to_app(arg2)->get_arg(0);
            expr * var2 = to_app(arg2)->get_arg(1);
            if (is_app(app1) &&
                is_app(app2) && 
                to_app(app1)->get_decl() == to_app(app2)->get_decl() &&
                to_app(app1)->get_num_args() == to_app(app2)->get_num_args() &&
                to_app(app1)->get_family_id() == null_family_id &&
                to_app(app1)->get_num_args() > 0 &&
                is_var(var1) && 
                is_var(var2) && 
                var1 != var2) {
                app * f1          = to_app(app1);
                app * f2          = to_app(app2);
                bool found_vars   = false;
                unsigned num      = f1->get_num_args();
                unsigned idx      = UINT_MAX;
                unsigned num_vars = 1;
                for (unsigned i = 0; i < num; i++) {
                    expr  * c1 = f1->get_arg(i);
                    expr  * c2 = f2->get_arg(i);
                    if (!is_var(c1) && !is_uninterp_const(c1))
                        return false;
                    if ((c1 == var1 && c2 == var2) || (c1 == var2 && c2 == var1)) {
                        if (found_vars)
                            return false;
                        found_vars = true;
                        idx = i;
                    }
                    else if (c1 == c2 && c1 != var1 && c1 != var2) {
                        if (is_var(c1)) {
                            ++num_vars;
                        }
                    }
                    else {
                        return false;
                    }
                }
                if (found_vars && !has_free_vars(q)) {
                    TRACE("inj_axiom", 
                          tout << "Cadidate for simplification:\n" << mk_ll_pp(q, m) << mk_pp(app1, m) << "\n" << mk_pp(app2, m) << "\n" <<
                          mk_pp(var1, m) << "\n" << mk_pp(var2, m) << "\nnum_vars: " << num_vars << "\n";);

void mk_bits(ast_manager & m, char const * prefix, unsigned sz, expr_ref_vector & r) {
    sort_ref b(m);
    b = m.mk_bool_sort();
    for (unsigned i = 0; i < sz; ++i) {
        char buffer[128];
#ifdef _WINDOWS
        sprintf_s(buffer, ARRAYSIZE(buffer), "%s%d.smt", prefix, i);
#else
        sprintf(buffer, "%s%d.smt", prefix, i);
#endif
        r.push_back(m.mk_const(symbol(buffer), b));
    }
}

func_entry::func_entry(ast_manager & m, unsigned arity, expr * const * args, expr * result):
    m_args_are_values(true),
    m_result(result) {
    SASSERT(is_ground(result));
    m.inc_ref(result);
    for (unsigned i = 0; i < arity; i++) {
        expr * arg = args[i];
        SASSERT(is_ground(arg));
        if (!m.is_value(arg))
            m_args_are_values = false;
        m.inc_ref(arg);
        m_args[i] = arg;
    }
}

void tst_match(ast_manager & m, app * t, app * i) {
    substitution s(m);
    s.reserve(2, 10); // reserving a big number of variables to be safe.

    matcher      match;
    std::cout << "Is " << mk_pp(i, m) << " an instance of " << mk_pp(t, m) << "\n";
    if (match(t, i, s)) {
        std::cout << "yes\n";
        s.display(std::cout);
    }
    else {
        std::cout << "no\n";
    }

    s.reset();
    
    if (t->get_decl() == i->get_decl()) {
        // trying to match the arguments of t and i
        std::cout << "Are the arguments of " << mk_pp(i, m) << " an instance of the arguments of " << mk_pp(t, m) << "\n";
        unsigned num_args = t->get_num_args();
        unsigned j;
        for (j = 0; j < num_args; j++) {
            if (!match(t->get_arg(j), i->get_arg(j), s))
                break;
        }
        if (j == num_args) {
            std::cout << "yes\n";
            s.display(std::cout);
            
            // create some dummy term to test for applying the substitution.
            sort_ref S(          m.mk_uninterpreted_sort(symbol("S")),    m);
            sort * domain[3]   = {S, S, S};
            func_decl_ref r(     m.mk_func_decl(symbol("r"), 3, domain, S), m);
            expr_ref x1(         m.mk_var(0, S), m);
            expr_ref x2(         m.mk_var(1, S), m);
            expr_ref x3(         m.mk_var(2, S), m);
            app_ref  rxyzw(      m.mk_app(r, x1.get(), x2.get(), x3.get()), m);
            expr_ref result(m);
            unsigned deltas[2] = {0,0};
            s.apply(2, deltas, expr_offset(rxyzw, 0), result);
            std::cout << "applying substitution to\n" << mk_pp(rxyzw,m) << "\nresult:\n" << mk_pp(result,m) << "\n";
        }
        else {
            std::cout << "no\n";
        }
    }
    
    std::cout << "\n";
}

expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app* const* bound, expr* n) {
    expr_ref result(m);
    expr_abstract(m, 0, num_bound, (expr* const*)bound, n, result);    
    if (num_bound > 0) {
        ptr_vector<sort> sorts;
        svector<symbol> names;
        for (unsigned i = 0; i < num_bound; ++i) {
            sorts.push_back(m.get_sort(bound[i]));
            names.push_back(bound[i]->get_decl()->get_name());
        }
        result = m.mk_quantifier(is_forall, num_bound, sorts.c_ptr(), names.c_ptr(), result);
    }
    return result;

}

 virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) {
     // Let m_clause be of the form (l_0 or ... or l_{num_source - 1})
     // Each source[i] proof is a proof for "false" using l_i as a hypothesis
     // So, I use lemma for producing a proof for (not l_i) that does not contain the hypothesis,
     // and unit_resolution for building a proof for the goal.
     SASSERT(num_source == m_clause->get_num_args());
     proof_ref_buffer prs(m);
     prs.push_back(m_clause_pr);
     for (unsigned i = 0; i < num_source; i++) {
         proof * pr_i  = source[i];
         expr * not_li = m.mk_not(m_clause->get_arg(i));
         prs.push_back(m.mk_lemma(pr_i, not_li));
     }
     result = m.mk_unit_resolution(prs.size(), prs.c_ptr());
 }

unsigned get_clause_num_literals(ast_manager & m, expr * cls) {
    SASSERT(is_clause(m, cls));
    if (is_literal(m, cls))
        return 1;
    SASSERT(m.is_or(cls));
    return to_app(cls)->get_num_args();
}

macro_substitution::macro_substitution(ast_manager & m, bool cores_enabled, bool proofs_enabled):
    m_manager(m),
    m_cores_enabled(cores_enabled),
    m_proofs_enabled(proofs_enabled) {
    SASSERT(!proofs_enabled || m.proofs_enabled());
    init();
}

 inc_sat_solver(ast_manager& m, params_ref const& p):
     m(m), m_solver(p, m.limit(), 0),
     m_params(p), m_optimize_model(false),
     m_fmls(m),
     m_asmsf(m),
     m_fmls_head(0),
     m_core(m),
     m_map(m),
     m_bb_rewriter(m, p),
     m_num_scopes(0),
     m_dep_core(m),
     m_unknown("no reason given") {
     m_params.set_bool("elim_vars", false);
     m_solver.updt_params(m_params);
     params_ref simp2_p = p;
     simp2_p.set_bool("som", true);
     simp2_p.set_bool("pull_cheap_ite", true);
     simp2_p.set_bool("push_ite_bv", false);
     simp2_p.set_bool("local_ctx", true);
     simp2_p.set_uint("local_ctx_limit", 10000000);
     simp2_p.set_bool("flat", true); // required by som
     simp2_p.set_bool("hoist_mul", false); // required by som
     simp2_p.set_bool("elim_and", true);
     m_preprocess =
         and_then(mk_card2bv_tactic(m, m_params),
                  using_params(mk_simplify_tactic(m), simp2_p),
                  mk_max_bv_sharing_tactic(m),
                  mk_bit_blaster_tactic(m, &m_bb_rewriter),
                  //mk_aig_tactic(),
                  using_params(mk_simplify_tactic(m), simp2_p));
 }

cost_parser::cost_parser(ast_manager & m):
    simple_parser(m),
    m_util(m),
    m_vars(m) {
    family_id fid;
    fid = m.get_basic_family_id();
    add_builtin_op("true",    fid, OP_TRUE);
    add_builtin_op("false",   fid, OP_FALSE);
    add_builtin_op("not",     fid, OP_NOT);
    add_builtin_op("and",     fid, OP_AND);
    add_builtin_op("implies", fid, OP_IMPLIES);
    add_builtin_op("or",      fid, OP_OR);
    add_builtin_op("ite",     fid, OP_ITE);
    add_builtin_op("=",       fid, OP_EQ);
    add_builtin_op("iff",     fid, OP_IFF);
    add_builtin_op("xor",     fid, OP_XOR);

    fid = m_util.get_family_id();
    add_builtin_op("+",  fid, OP_ADD);
    add_builtin_op("*",  fid, OP_MUL);
    add_builtin_op("-",  fid, OP_SUB);
    add_builtin_op("/",  fid, OP_DIV);
    add_builtin_op("<=", fid, OP_LE);
    add_builtin_op(">=", fid, OP_GE);
    add_builtin_op("<",  fid, OP_LT);
    add_builtin_op(">",  fid, OP_GT);
}

proof_ref replace_proof_converter::operator()(ast_manager & m, unsigned num_source, proof * const * source) {    
    SASSERT(num_source == 1);
    replace_map replace(m);
    proof_ref p(m);
    expr_ref tmp(source[0], m), e(m), f(m);
    
    // apply the substitution to the prefix before inserting it.
    for (unsigned i = 0; i < m_proofs.size(); ++i) {
        p = m_proofs[i].get();
        e = p;
        replace.apply(e);
        f = m.mk_asserted(m.get_fact(p));
        replace.insert(f, e);
        TRACE("proof_converter", tout << f->get_id() << " " << mk_pp(f, m) << 
              "\n|-> " << mk_pp(e, m) << "\n";);
    }