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";
           });

static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards) {
    return;
    // quant_elim option got removed...
    // verify:
    //    fml <=> guard_1 \/ guard_2 \/ ... 
    ast_manager& m = guards.get_manager();
    expr_ref tmp(m), fml2(m);
    tmp = m.mk_or(guards.size(), guards.c_ptr());
    expr* _x = x;
    std::cout << mk_pp(fml, m) << "\n";
    expr_abstract(m, 0, 1, &_x, fml, fml2);
    std::cout << mk_pp(fml2, m) << "\n";
    symbol name(x->get_decl()->get_name());
    sort* s = m.get_sort(x);
    fml2 = m.mk_exists(1, &s, &name, fml2);
    std::cout << mk_pp(fml2, m) << "\n";
    tmp = m.mk_not(m.mk_iff(fml2, tmp));
    std::cout << mk_pp(tmp, m) << "\n";
    front_end_params fp;
    smt::kernel solver(m, fp);
    solver.assert_expr(tmp);
    lbool res = solver.check();
    std::cout << "checked\n";
    SASSERT(res == l_false);
    if (res != l_false) {
        std::cout << res << "\n";
        fatal_error(0);
    }
}

 mbi_result prop_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl)  {
     lbool r = m_solver->check_sat(lits);
     switch (r) {
     case l_false:
         lits.reset();
         m_solver->get_unsat_core(lits);
         return mbi_unsat;
     case l_true:
         m_solver->get_model(mdl);
         lits.reset();
         for (unsigned i = 0, sz = mdl->get_num_constants(); i < sz; ++i) {
             func_decl* c = mdl->get_constant(i);
             if (m_shared.contains(c)) {
                 if (m.is_true(mdl->get_const_interp(c))) {
                     lits.push_back(m.mk_const(c));
                 }
                 else if (m.is_false(mdl->get_const_interp(c))) {
                     lits.push_back(m.mk_not(m.mk_const(c)));
                 }
             }
         }
         return mbi_sat;
     default:
         return mbi_undef;
     }
 }

void model_evaluator_array_util::eval_exprs(model& mdl, expr_ref_vector& es) {
    for (unsigned j = 0; j < es.size(); ++j) {
        if (m_array.is_as_array(es.get (j))) {
            expr_ref r (m);
            eval(mdl, es.get (j), r);
            es.set (j, r);
        }
    }
}

bool itp_solver::mk_proxies (expr_ref_vector &v, unsigned from)
{
    bool dirty = false;
    for (unsigned i = from, sz = v.size(); i < sz; ++i) {
        app *p = mk_proxy (v.get (i));
        dirty |= (v.get (i) != p);
        v[i] = p;
    }
    return dirty;
}

void itp_solver::undo_proxies (expr_ref_vector &r)
{
    app_ref e(m);
    // expand proxies
    for (unsigned i = 0, sz = r.size (); i < sz; ++i)
        if (is_proxy(r.get(i), e)) {
            SASSERT (m.is_or (e));
            r[i] = e->get_arg (1);
        }
}

void display(std::ostream & out, expr_ref_vector & r, bool ll=true) {
    ast_mark v;
    for (unsigned i = 0; i < r.size(); i++) {
        if (ll)
            ast_ll_pp(out, r.get_manager(), r.get(i), v);
        else
            out << mk_pp(r.get(i), r.get_manager());
        out << "\n";
    }
}

void atom2bool_var::mk_inv(expr_ref_vector & lit2expr) const {
    obj_map<expr, var>::iterator it  = m_mapping.begin();
    obj_map<expr, var>::iterator end = m_mapping.end();
    for (; it != end; ++it) {
        sat::literal l(static_cast<sat::bool_var>(it->m_value), false);
        lit2expr.set(l.index(), it->m_key);
        l.neg();
        lit2expr.set(l.index(), m().mk_not(it->m_key));
    }
}

void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, expr2expr_map& bool2dep, ref<filter_model_converter>& fmc) {
    expr2expr_map dep2bool;
    ptr_vector<expr> deps;
    ast_manager& m = g->m();
    expr_ref_vector clause(m);
    unsigned sz = g->size();
    for (unsigned i = 0; i < sz; i++) {
        expr * f            = g->form(i);
        expr_dependency * d = g->dep(i);
        if (d == 0 || !g->unsat_core_enabled()) {
            clauses.push_back(f);
        }
        else {
            // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f.
            clause.reset();
            clause.push_back(f);
            deps.reset();
            m.linearize(d, deps);
            SASSERT(!deps.empty()); // d != 0, then deps must not be empty
            ptr_vector<expr>::iterator it  = deps.begin();
            ptr_vector<expr>::iterator end = deps.end();
            for (; it != end; ++it) {
                expr * d = *it;
                if (is_uninterp_const(d) && m.is_bool(d)) {
                    // no need to create a fresh boolean variable for d
                    if (!bool2dep.contains(d)) {
                        assumptions.push_back(d);
                        bool2dep.insert(d, d);
                    }
                    clause.push_back(m.mk_not(d));
                }
                else {
                    // must normalize assumption
                    expr * b = 0;
                    if (!dep2bool.find(d, b)) {
                        b = m.mk_fresh_const(0, m.mk_bool_sort());
                        dep2bool.insert(d, b);
                        bool2dep.insert(b, d);
                        assumptions.push_back(b);
                        if (!fmc) {
                            fmc = alloc(filter_model_converter, m);
                        }
                        fmc->insert(to_app(b)->get_decl());
                    }
                    clause.push_back(m.mk_not(b));
                }
            }
            SASSERT(clause.size() > 1);
            expr_ref cls(m);
            cls = mk_or(m, clause.size(), clause.c_ptr());
            clauses.push_back(cls);
        }
    }
}

bool sym_mux::is_homogenous(const expr_ref_vector & vect, unsigned idx) const
{
    expr * const * begin = vect.c_ptr();
    expr * const * end = begin + vect.size();
    for (expr * const * it = begin; it != end; it++) {
        if (!is_homogenous_formula(*it, idx)) {
            return false;
        }
    }
    return true;
}

 bool euf_arith_mbi_plugin::get_literals(model_ref& mdl, expr_ref_vector& lits) {
     lits.reset();
     for (expr* e : m_atoms) {
         if (mdl->is_true(e)) {
             lits.push_back(e);
         }
         else if (mdl->is_false(e)) {
             lits.push_back(m.mk_not(e));
         }
     }
     TRACE("qe", tout << "atoms from model: " << lits << "\n";);

 void flush_assertions() const {
     proof_ref proof(m);
     expr_ref fml(m);
     expr_ref_vector fmls(m);
     for (unsigned i = 0; i < m_assertions.size(); ++i) {
         m_rewriter(m_assertions[i].get(), fml, proof);
         m_solver->assert_expr(fml);
     }
     m_rewriter.flush_side_constraints(fmls);
     m_solver->assert_expr(fmls);
     m_assertions.reset();
 }

static void test_cs(app* x, expr_ref_vector& c, vector<expr_ref_vector> const& cs) {
    if (c.size() == cs.size()) {
        test_c(x, c);
        return;
    }
    expr_ref_vector const& c1 = cs[c.size()];
    for (unsigned i = 0; i < c1.size(); ++i) {
        c.push_back(c1[i]);
        test_cs(x, c, cs);
        c.pop_back();
    }
}

void sym_mux::filter_non_model_lits(expr_ref_vector & vect) const
{
    unsigned i = 0;
    while (i < vect.size()) {
        if (!has_nonmodel_symbol(vect[i].get())) {
            i++;
            continue;
        }
        vect[i] = vect.back();
        vect.pop_back();
    }
}

void sym_mux::conv_formula_vector(const expr_ref_vector & vect, unsigned src_idx, unsigned tgt_idx,
                                  expr_ref_vector & res) const
{
    res.reset();
    expr * const * begin = vect.c_ptr();
    expr * const * end = begin + vect.size();
    for (expr * const * it = begin; it != end; it++) {
        expr_ref converted(m);
        conv_formula(*it, src_idx, tgt_idx, converted);
        res.push_back(converted);
    }
}

    void aig_exporter::assert_pred_id(func_decl *decl, const expr_ref_vector& vars, expr_ref_vector& exprs) {
        unsigned id = 0;
        if (decl && !m_decl_id_map.find(decl, id)) {
            id = m_next_decl_id++;
            SASSERT(id < (1U << vars.size()));
            m_decl_id_map.insert(decl, id);
        }

        for (unsigned i = 0; i < vars.size(); ++i) {
            exprs.push_back((id & (1U << i)) ? vars[i] : m.mk_not(vars[i]));
        }
    }

 void get_renaming_args(const unsigned_vector & map, const relation_signature & orig_sig, 
         expr_ref_vector & renaming_arg) {
     ast_manager & m = renaming_arg.get_manager();
     unsigned sz = map.size();
     unsigned ofs = sz-1;
     renaming_arg.resize(sz, static_cast<expr *>(0));
     for(unsigned i=0; i<sz; i++) {
         if(map[i]!=UINT_MAX) {
             renaming_arg.set(ofs-i, m.mk_var(map[i], orig_sig[i]));
         }
     }
 }

 void get_bits(expr * t, expr_ref_vector & out_bits) {
     if (butil().is_mkbv(t)) {
         out_bits.append(to_app(t)->get_num_args(), to_app(t)->get_args());
     }
     else {
         unsigned bv_size = butil().get_bv_size(t);
         for (unsigned i = 0; i < bv_size; i++) {
             parameter p(i);
             out_bits.push_back(m().mk_app(butil().get_family_id(), OP_BIT2BOOL, 1, &p, 1, &t));
         }
         SASSERT(bv_size == out_bits.size());
     }
 }

void sym_mux::partition_o_idx(
    expr_ref_vector const& lits,
    expr_ref_vector& o_lits,
    expr_ref_vector& other, unsigned idx) const
{

    for (unsigned i = 0; i < lits.size(); ++i) {
        if (contains(lits[i], idx) && is_homogenous_formula(lits[i], idx)) {
            o_lits.push_back(lits[i]);
        } else {
            other.push_back(lits[i]);
        }
    }
}

/**
 * expands equivalence classes to all derivable equalities
 */
bool equiv_to_expr_full(expr_equiv_class &equiv, expr_ref_vector &out) {
    ast_manager &m = out.get_manager();
    bool dirty = false;
    for (auto eq_class : equiv) {
        for (auto a = eq_class.begin(), end = eq_class.end(); a != end; ++a) {
            expr_equiv_class::iterator b(a);
            for (++b; b != end; ++b) {
                out.push_back(m.mk_eq(*a, *b));
                dirty = true;
            }
        }
    }
    return dirty;
}