自学教程：C++ to_app函数代码示例

static bool is_lp(goal const & g) {    ast_manager & m = g.m();    arith_util u(m);    unsigned sz = g.size();    for (unsigned i = 0; i < sz; i++) {        expr * f  = g.form(i);        bool sign = false;        while (m.is_not(f, f))            sign = !sign;        if (m.is_eq(f) && !sign) {            if (m.get_sort(to_app(f)->get_arg(0))->get_family_id() != u.get_family_id())                return false;            continue;        }        if (u.is_le(f) || u.is_ge(f) || u.is_lt(f) || u.is_gt(f))            continue;        return false;    }    return true;}

void arith_simplifier_plugin::get_monomial_gcd(expr_ref_vector& monomials, numeral& g) {    g = numeral::zero();    numeral n;    for (unsigned  i = 0; !g.is_one() && i < monomials.size(); ++i) {        expr* e = monomials[i].get();        if (is_numeral(e, n)) {            g = gcd(abs(n), g);        }        else if (is_mul(e) && is_numeral(to_app(e)->get_arg(0), n)) {            g = gcd(abs(n), g);                }        else {            g = numeral::one();            return;        }    }    if (g.is_zero()) {        g = numeral::one();    }}

    subpaving::var process(expr * t, unsigned depth, mpz & n, mpz & d) {        SASSERT(is_int_real(t));        checkpoint();        if (is_cached(t)) {            unsigned idx = m_cache.find(t);            qm().set(n, m_cached_numerators[idx]);            qm().set(d, m_cached_denominators[idx]);            return m_cached_vars[idx];        }        SASSERT(!is_quantifier(t));        if (::is_var(t) || !m_autil.is_arith_expr(t)) {            qm().set(n, 1);            qm().set(d, 1);            return mk_var_for(t);        }        return process_arith_app(to_app(t), depth, n, d);    }

    void operator()(app * n) {        family_id fid = n->get_family_id();        if (fid != null_family_id && fid != fu.get_family_id())            throw found();        sort * s = get_sort(n);        if (fid == fu.get_family_id()) {            if (!fu.is_float(s) && !fu.is_rm(s) &&                to_app(n)->get_decl_kind() != OP_FPA_TO_REAL)                throw found();        }        else if (fid == null_family_id) {            if (!fu.is_float(s) && !fu.is_rm(s) && !m.is_bool(s))                throw found();        }        else if (fid == m.get_basic_family_id())            return;        else            throw found();    }

inline bool shared_occs::process(expr * t, shared_occs_mark & visited) {    switch (t->get_kind()) {    case AST_APP: {        unsigned num_args = to_app(t)->get_num_args();        if (t->get_ref_count() > 1 && (m_track_atomic || num_args > 0)) {            if (visited.is_marked(t)) {                insert(t);                return true;            }            visited.mark(t);        }        if (num_args == 0)            return true; // done with t        m_stack.push_back(frame(t, 0)); // need to create frame if num_args > 0        return false;     }    case AST_VAR:        if (m_track_atomic && t->get_ref_count() > 1) {            if (visited.is_marked(t))                insert(t);            else                visited.mark(t);        }        return true; // done with t    case AST_QUANTIFIER:        if (t->get_ref_count() > 1) {            if (visited.is_marked(t)) {                insert(t);                return true; // done with t            }            visited.mark(t);        }        if (!m_visit_quantifiers)            return true;         m_stack.push_back(frame(t, 0));        return false;     default:        UNREACHABLE();        return true;    }}

    unsigned aig_exporter::expr_to_aig(const expr *e) {        unsigned id;        if (m_aig_expr_id_map.find(e, id))            return id;        if (is_uninterp_const(e))            return get_var(e);        switch (e->get_kind()) {        case AST_APP: {            const app *a = to_app(e);            switch (a->get_decl_kind()) {            case OP_OR:                SASSERT(a->get_num_args() > 0);                id = expr_to_aig(a->get_arg(0));                for (unsigned i = 1; i < a->get_num_args(); ++i) {                    id = mk_or(id, expr_to_aig(a->get_arg(i)));                }                m_aig_expr_id_map.insert(e, id);                return id;            case OP_NOT:                return neg(expr_to_aig(a->get_arg(0)));            case OP_FALSE:                return 0;            case OP_TRUE:                return 1;            }            break;}        case AST_VAR:            return get_var(e);        default:            UNREACHABLE();        }                UNREACHABLE();        return 0;    }

 bool solve_nl(app * lhs, expr * rhs, expr* eq, app_ref& var, expr_ref & def, proof_ref & pr) {     SASSERT(m_a_util.is_add(lhs));     if (m_a_util.is_int(lhs)) return false;     unsigned num = lhs->get_num_args();     expr_ref div(m());     for (unsigned i = 0; i < num; i++) {         expr * arg = lhs->get_arg(i);         if (is_app(arg) && isolate_var(to_app(arg), var, div, i, lhs, rhs)) {             ptr_vector<expr> args;             for (unsigned k = 0; k < num; ++k) {                 if (k != i) args.push_back(lhs->get_arg(k));             }             def = m_a_util.mk_sub(rhs, m_a_util.mk_add(args.size(), args.c_ptr()));             def = m_a_util.mk_div(def, div);             if (m_produce_proofs)                 pr = m().mk_rewrite(eq, m().mk_eq(var, def));             return true;         }     }     return false; }

 std::ostream& theory::display_app(std::ostream & out, app * n) const {     func_decl * d = n->get_decl();     if (n->get_num_args() == 0) {         out << d->get_name();         display_parameters(out, d->get_num_parameters(), d->get_parameters());     }     else if (n->get_family_id() == get_family_id()) {         out << "(" << d->get_name();         display_parameters(out, d->get_num_parameters(), d->get_parameters());         unsigned num = n->get_num_args();         for (unsigned i = 0; i < num; i++) {             out << " ";             display_app(out, to_app(n->get_arg(i)));         }         out << ")";     }     else {         out << "#" << n->get_id();     }     return out; }

    proof *mk_unit_resolution_core(unsigned num_args, proof* const *args)    {        ptr_buffer<proof> pf_args;        pf_args.push_back(args [0]);        app *cls_fact = to_app(m.get_fact(args[0]));        ptr_buffer<expr> cls;        if (m.is_or(cls_fact)) {            for (unsigned i = 0, sz = cls_fact->get_num_args(); i < sz; ++i)            { cls.push_back(cls_fact->get_arg(i)); }        } else { cls.push_back(cls_fact); }        // construct new resovent        ptr_buffer<expr> new_fact_cls;        bool found;        // XXX quadratic        for (unsigned i = 0, sz = cls.size(); i < sz; ++i) {            found = false;            for (unsigned j = 1; j < num_args; ++j) {                if (m.is_complement(cls.get(i), m.get_fact(args [j]))) {                    found = true;                    pf_args.push_back(args [j]);                    break;                }            }            if (!found) {                new_fact_cls.push_back(cls.get(i));            }        }        SASSERT(new_fact_cls.size() + pf_args.size() - 1 == cls.size());        expr_ref new_fact(m);        new_fact = mk_or(m, new_fact_cls.size(), new_fact_cls.c_ptr());        // create new proof step        proof *res = m.mk_unit_resolution(pf_args.size(), pf_args.c_ptr(), new_fact);        m_pinned.push_back(res);        return res;    }

br_status datatype_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {    if (!is_app(lhs) || !is_app(rhs) || !m_util.is_constructor(to_app(lhs)) || !m_util.is_constructor(to_app(rhs)))        return BR_FAILED;    if (to_app(lhs)->get_decl() != to_app(rhs)->get_decl()) {        result = m().mk_false();        return BR_DONE;    }    // Remark: In datatype_simplifier_plugin, we used    // m_basic_simplifier to create '=' and 'and' applications in the    // following code. This trick not guarantee that the final expression    // will be fully simplified.    //    // Example:    // The assertion    // (assert (= (cons a1 (cons a2 (cons a3 (cons (+ a4 1) (cons (+ a5 c5) (cons a6 nil))))))    //         (cons b1 (cons b2 (cons b3 (cons b4 (cons b5 (cons b6 nil))))))))    //    // After applying asserted_formulas::reduce(), the following formula was generated.    //    //   (= a1 b1)    //   (= a2 b2)    //   (= a3 b3)    //   (= (+ a4 (* (- 1) b4)) (- 1))    //   (= (+ c5 a5) b5)                    <<< NOT SIMPLIFIED WITH RESPECT TO ARITHMETIC    //   (= (cons a6 nil) (cons b6 nil)))    <<< NOT SIMPLIFIED WITH RESPECT TO DATATYPE theory    //    // Note that asserted_formulas::reduce() applied the simplier many times.    // After the first simplification step we had:    //  (= a1 b1)    //  (= (cons a2 (cons a3 (cons (+ a4 1) (cons (+ a5 c5) (cons a6 nil))))))    //     (cons b2 (cons b3 (cons b4 (cons b5 (cons b6 nil))))))    ptr_buffer<expr> eqs;    unsigned num = to_app(lhs)->get_num_args();    SASSERT(num == to_app(rhs)->get_num_args());    for (unsigned i = 0; i < num; ++i) {        eqs.push_back(m().mk_eq(to_app(lhs)->get_arg(i), to_app(rhs)->get_arg(i)));    }    result = m().mk_and(eqs.size(), eqs.c_ptr());    return BR_REWRITE2;}

 bool isolate_var(app* arg, app_ref& var, expr_ref& div, unsigned i, app* lhs, expr* rhs) {     if (!m_a_util.is_mul(arg)) return false;     unsigned n = arg->get_num_args();     for (unsigned j = 0; j < n; ++j) {         expr* e = arg->get_arg(j);         bool ok = is_uninterp_const(e) && check_occs(e) && !occurs(e, rhs) && !occurs_except(e, lhs, i);         if (!ok) continue;         var = to_app(e);         for (unsigned k = 0; ok && k < n; ++k) {             expr* arg_k = arg->get_arg(k);             ok = k == j || (!occurs(var, arg_k) && is_nonzero(arg_k));         }         if (!ok) continue;         ptr_vector<expr> args;         for (unsigned k = 0; k < n; ++k) {             if (k != j) args.push_back(arg->get_arg(k));         }         div = m_a_util.mk_mul(args.size(), args.c_ptr());         return true;     }     return false; }

    void display_fact(context & ctx, app * f, std::ostream & out)    {        func_decl * pred_decl = f->get_decl();        unsigned arity = f->get_num_args();        out << "/t(";        for(unsigned i = 0; i < arity; i++) {            if (i != 0) {                out << ',';            }            expr * arg = f->get_arg(i);            uint64 sym_num;            SASSERT(is_app(arg));            VERIFY( ctx.get_decl_util().is_numeral_ext(to_app(arg), sym_num) );            relation_sort sort = pred_decl->get_domain(i);                        out << ctx.get_argument_name(pred_decl, i) << '=';            ctx.print_constant_name(sort, sym_num, out);            out << '(' << sym_num << ')';        }        out << ")/n";    }

/* * iterative post-order depth-first search (DFS) through the proof DAG */proof* proof_post_order::next(){    while (!m_todo.empty()) {        proof* currentNode = m_todo.back();        // if we haven't already visited the current unit        if (!m_visited.is_marked(currentNode)) {            bool existsUnvisitedParent = false;            // add unprocessed premises to stack for DFS.             // If there is at least one unprocessed premise, don't compute the result            // for currentProof now, but wait until those unprocessed premises are processed.            for (unsigned i = 0; i < m.get_num_parents(currentNode); ++i) {                SASSERT(m.is_proof(currentNode->get_arg(i)));                proof* premise = to_app(currentNode->get_arg(i));                // if we haven't visited the current premise yet                if (!m_visited.is_marked(premise)) {                    // add it to the stack                    m_todo.push_back(premise);                    existsUnvisitedParent = true;                }            }            // if we already visited all parent-inferences, we can visit the inference too            if (!existsUnvisitedParent) {                m_visited.mark(currentNode, true);                m_todo.pop_back();                return currentNode;            }        } else {            m_todo.pop_back();        }    }    // we have already iterated through all inferences    return nullptr;}

 void context::check_sorts(ast * n) {     if (!m().check_sorts(n)) {         switch(n->get_kind()) {         case AST_APP: {             std::ostringstream buffer;             app * a = to_app(n);             buffer << mk_pp(a->get_decl(), m()) << " applied to: ";             if (a->get_num_args() > 1) buffer << "/n";             for (unsigned i = 0; i < a->get_num_args(); ++i) {                 buffer << mk_bounded_pp(a->get_arg(i), m(), 3) << " of sort ";                 buffer << mk_pp(m().get_sort(a->get_arg(i)), m()) << "/n";             }             warning_msg("%s",buffer.str().c_str());             break;         }         case AST_VAR:         case AST_QUANTIFIER:         case AST_SORT:         case AST_FUNC_DECL:             break;         }         set_error_code(Z3_SORT_ERROR);     } }

    Z3_ast Z3_API Z3_qe_lite (Z3_context c, Z3_ast_vector vars, Z3_ast body)    {        Z3_TRY;        LOG_Z3_qe_lite (c, vars, body);        RESET_ERROR_CODE();        ast_ref_vector &vVars = to_ast_vector_ref (vars);        app_ref_vector vApps (mk_c(c)->m());        for (unsigned i = 0; i < vVars.size (); ++i) {            app *a = to_app (vVars.get (i));            if (a->get_kind () != AST_APP) {                SET_ERROR_CODE (Z3_INVALID_ARG);                RETURN_Z3(0);            }            vApps.push_back (a);        }        expr_ref result (mk_c(c)->m ());        result = to_expr (body);        params_ref p;        qe_lite qe (mk_c(c)->m (), p);        qe (vApps, result);        // -- copy back variables that were not eliminated        if (vApps.size () < vVars.size ()) {            vVars.reset ();            for (app* v : vApps) {                vVars.push_back (v);            }        }        mk_c(c)->save_ast_trail (result.get ());        return of_expr (result);        Z3_CATCH_RETURN(0);    }

 void get_lit(expr * n, bool sign, expr_ref & r) { start:     if (!is_app(n) ||         to_app(n)->get_num_args() == 0) {         mk_lit(n, sign, r);         return;     }     func_decl * f = to_app(n)->get_decl();     if (f->get_family_id() != m.get_basic_family_id()) {         mk_lit(n, sign, r);         return;     }     app * l;     switch (f->get_decl_kind()) {     case OP_NOT:         n    = to_app(n)->get_arg(0);         sign = !sign;         goto start;     case OP_OR:     case OP_IFF:         l = 0;         m_cache.find(to_app(n), l);         SASSERT(l != 0);         mk_lit(l, sign, r);         return;     case OP_ITE:     case OP_EQ:         if (m.is_bool(to_app(n)->get_arg(1))) {             l = 0;             m_cache.find(to_app(n), l);             SASSERT(l != 0);             mk_lit(l, sign, r);             return;         }         mk_lit(n, sign, r);         return;     default:         TRACE("tseitin_cnf_bug", tout << f->get_name() << "/n";);         UNREACHABLE();         return;     }

bool bool_rewriter::simp_nested_eq_ite(expr * t, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result) {    bool neg = false;    m_local_ctx_cost += 3;    if (m().is_not(t)) {        neg = true;        t = to_app(t)->get_arg(0);    }    if (m().is_iff(t) || m().is_eq(t)) {        bool modified = false;        expr * new_lhs = simp_arg(to_app(t)->get_arg(0), neg_lits, pos_lits, modified);        expr * new_rhs = simp_arg(to_app(t)->get_arg(1), neg_lits, pos_lits, modified);        if (!modified)            return false;        mk_eq(new_lhs, new_rhs, result);        if (neg)            mk_not(result, result);        return true;    }    if (m().is_ite(t)) {        bool modified = false;        expr * new_c = simp_arg(to_app(t)->get_arg(0), neg_lits, pos_lits, modified);        expr * new_t = simp_arg(to_app(t)->get_arg(1), neg_lits, pos_lits, modified);        expr * new_e = simp_arg(to_app(t)->get_arg(2), neg_lits, pos_lits, modified);        if (!modified)            return false;        // It is not safe to invoke mk_ite here, since it can recursively call        // local_ctx_simp by        //     - transforming the ITE into an OR        //     - and invoked mk_or, that will invoke local_ctx_simp        // mk_ite(new_c, new_t, new_e, result);        mk_nested_ite(new_c, new_t, new_e, result);        if (neg)            mk_not(result, result);        return true;    }    return false;}

bool arith_solver_plugin::solve(expr * lhs, expr * rhs, expr_mark const & forbidden, app_ref & var, expr_ref & subst) {    rational k;    if (!m_simplifier.is_numeral(rhs, k))        return false;    bool _is_int = m_simplifier.is_int(lhs);    ptr_buffer<expr> monomials;    ptr_buffer<expr> todo;    bool already_found = false;    rational c;    todo.push_back(lhs);    while (!todo.empty()) {        expr * curr = todo.back();        todo.pop_back();        rational coeff;        if (m_simplifier.is_add(curr)) {            SASSERT(to_app(curr)->get_num_args() == 2);            todo.push_back(to_app(curr)->get_arg(1));            todo.push_back(to_app(curr)->get_arg(0));        }        else {            if (!already_found) {                if (m_simplifier.is_mul(curr) &&                     m_simplifier.is_numeral(to_app(curr)->get_arg(0), coeff) && !coeff.is_zero() && (!_is_int || coeff.is_minus_one()) &&                     is_uninterp_const(to_app(curr)->get_arg(1)) &&                    !forbidden.is_marked(to_app(curr)->get_arg(1))) {                    c             = coeff;                    var           = to_app(to_app(curr)->get_arg(1));                    already_found = true;                }                else if (is_uninterp_const(curr) && !forbidden.is_marked(curr)) {                    c             = rational::one();                    var           = to_app(curr);                    already_found = true;                }                else {                    monomials.push_back(curr);                }            }            else {                monomials.push_back(curr);            }        }    }    if (!already_found)        return false;    SASSERT(!c.is_zero());    k /= c;    expr_ref_vector new_monomials(m_manager);    if (!k.is_zero())        new_monomials.push_back(m_simplifier.mk_numeral(k, _is_int));    c.neg();    expr_ref inv_c(m_manager);    if (!c.is_one()) {        rational inv(1);        inv /= c;        inv_c = m_simplifier.mk_numeral(inv, _is_int);    }    // divide monomials by c    unsigned sz = monomials.size();    for (unsigned i = 0; i < sz; i++) {        expr * m       = monomials[i];        expr_ref new_m(m_manager);         if (!c.is_one())            m_simplifier.mk_mul(inv_c, m, new_m);        else            new_m = m;        new_monomials.push_back(new_m);    }    if (new_monomials.empty())         subst = m_simplifier.mk_numeral(rational(0), _is_int);    else        m_simplifier.mk_add(new_monomials.size(), new_monomials.c_ptr(), subst);    TRACE("arith_solver", tout << "solving:/n" << mk_pp(lhs, m_manager) << "/n" << mk_pp(rhs, m_manager)           << "/nresult:/n" << mk_pp(var, m_manager) << "/n" << mk_pp(subst, m_manager) << "/n";);

 bool is_int(expr * t) {     if (m_a_util.is_uminus(t))         t = to_app(t)->get_arg(0);     return m_a_util.is_numeral(t); }

static bool is_neg_var(ast_manager & m, expr * e, unsigned num_decls) {    return m.is_not(e) && is_var(to_app(e)->get_arg(0)) && to_var(to_app(e)->get_arg(0))->get_idx() < num_decls;}

float cost_evaluator::eval(expr * f) const {#define E(IDX) eval(to_app(f)->get_arg(IDX))    if (is_app(f)) {        unsigned num_args;        family_id fid = to_app(f)->get_family_id();        if (fid == m_manager.get_basic_family_id()) {            switch (to_app(f)->get_decl_kind()) {            case OP_TRUE:     return 1.0f;            case OP_FALSE:    return 0.0f;            case OP_NOT:      return E(0) == 0.0f ? 1.0f : 0.0f;            case OP_AND:                      num_args = to_app(f)->get_num_args();                for (unsigned i = 0; i < num_args; i++)                     if (E(i) == 0.0f)                        return 0.0f;                return 1.0f;            case OP_OR:                num_args = to_app(f)->get_num_args();                for (unsigned i = 0; i < num_args; i++)                     if (E(i) != 0.0f)                        return 1.0f;                return 0.0f;            case OP_ITE:      return E(0) != 0.0f ? E(1) : E(2);            case OP_EQ:            case OP_IFF:      return E(0) == E(1) ? 1.0f : 0.0f;            case OP_XOR:      return E(0) != E(1) ? 1.0f : 0.0f;            case OP_IMPLIES:                  if (E(0) == 0.0f)                    return 1.0f;                return E(1) != 0.0f ? 1.0f : 0.0f;            default:                ;            }        }        else if (fid == m_util.get_family_id()) {            switch (to_app(f)->get_decl_kind()) {            case OP_NUM: {                rational r = to_app(f)->get_decl()->get_parameter(0).get_rational();                return static_cast<float>(numerator(r).get_int64())/static_cast<float>(denominator(r).get_int64());            }             case OP_LE:       return E(0) <= E(1) ? 1.0f : 0.0f;            case OP_GE:       return E(0) >= E(1) ? 1.0f : 0.0f;            case OP_LT:       return E(0) <  E(1) ? 1.0f : 0.0f;            case OP_GT:       return E(0) >  E(1) ? 1.0f : 0.0f;            case OP_ADD:      return E(0) + E(1);            case OP_SUB:      return E(0) - E(1);            case OP_UMINUS:   return - E(0);            case OP_MUL:      return E(0) * E(1);            case OP_DIV: {                     float q = E(1);                if (q == 0.0f) {                    warning_msg("cost function division by zero");                    return 1.0f;                }                return E(0) / q;            }            default:                ;            }        }    }    else if (is_var(f)) {        unsigned idx = to_var(f)->get_idx();        if (idx < m_num_args)            return m_args[m_num_args - idx - 1];    }    warning_msg("cost function evaluation error");    return 1.0f;}

 // Return true if n is uninterpreted with respect to arithmetic. bool is_uninterp(expr * n) {     return is_app(n) && to_app(n)->get_family_id() != m_util.get_family_id(); }

void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {        expr * curr = 0, *b = 0;    SASSERT(n->get_ref_count() > 0);    m_stack.push_back(n);    for (unsigned i = 0; i < num_bound; ++i) {        b = bound[i];        expr* v = m.mk_var(base + num_bound - i - 1, m.get_sort(b));        m_pinned.push_back(v);        m_map.insert(b, v);    }    while(!m_stack.empty()) {        curr = m_stack.back();        if (m_map.contains(curr)) {            m_stack.pop_back();            continue;        }        switch(curr->get_kind()) {        case AST_VAR: {            m_map.insert(curr, curr);            m_stack.pop_back();            break;        }        case AST_APP: {            app* a = to_app(curr);            bool all_visited = true;            m_args.reset();            for (unsigned i = 0; i < a->get_num_args(); ++i) {                if (!m_map.find(a->get_arg(i), b)) {                    m_stack.push_back(a->get_arg(i));                    all_visited = false;                }                else {                    m_args.push_back(b);                }            }            if (all_visited) {                b = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr());                m_pinned.push_back(b);                m_map.insert(curr, b);                m_stack.pop_back();            }            break;        }        case AST_QUANTIFIER: {            quantifier* q = to_quantifier(curr);            expr_ref_buffer patterns(m);            expr_ref result1(m);            unsigned new_base = base + q->get_num_decls();                    for (unsigned i = 0; i < q->get_num_patterns(); ++i) {                expr_abstract(m, new_base, num_bound, bound, q->get_pattern(i), result1);                patterns.push_back(result1.get());            }            expr_abstract(m, new_base, num_bound, bound, q->get_expr(), result1);            b = m.update_quantifier(q, patterns.size(), patterns.c_ptr(), result1.get());            m_pinned.push_back(b);                        m_map.insert(curr, b);            m_stack.pop_back();                        break;        }        default:            UNREACHABLE();        }    }    VERIFY (m_map.find(n, b));    result = b;    m_pinned.reset();    m_map.reset();    m_stack.reset();    m_args.reset();   }

void used_vars::process(expr * n, unsigned delta) {    unsigned j, idx;    m_cache.reset();    m_todo.reset();    m_todo.push_back(expr_delta_pair(n, delta));    while (!m_todo.empty()) {        expr_delta_pair const & p = m_todo.back();        n     = p.m_node;        if (n->get_ref_count() > 1 && m_cache.contains(p)) {            m_todo.pop_back();            continue;        }                if (n->get_ref_count() > 1) {            // cache only shared and non-constant nodes            m_cache.insert(p);        }        delta = p.m_delta;        m_todo.pop_back();                switch (n->get_kind()) {        case AST_APP:            j = to_app(n)->get_num_args();            while (j > 0) {                --j;                expr * arg = to_app(n)->get_arg(j);                m_todo.push_back(expr_delta_pair(arg, delta));            }            break;        case AST_VAR:            idx = to_var(n)->get_idx();            if (idx >= delta) {                idx = idx - delta;                if (idx >= m_found_vars.size())                    m_found_vars.resize(idx + 1, 0);                m_found_vars[idx] = to_var(n)->get_sort();            }            break;        case AST_QUANTIFIER:            // recurse so that memoization is correct with respect to 'delta'.            delta += to_quantifier(n)->get_num_decls();            j      = to_quantifier(n)->get_num_patterns();            while (j > 0) {                --j;                m_todo.push_back(expr_delta_pair(to_quantifier(n)->get_pattern(j), delta));            }            j      = to_quantifier(n)->get_num_no_patterns();            while (j > 0) {                --j;                m_todo.push_back(expr_delta_pair(to_quantifier(n)->get_no_pattern(j), delta));            }            m_todo.push_back(expr_delta_pair(to_quantifier(n)->get_expr(), delta));            break;        default:            break;        }    }}

 bool checker::check_core(expr * n, bool is_true) {     SASSERT(m_manager.is_bool(n));     if (m_context.b_internalized(n) && m_context.is_relevant(n)) {         lbool val = m_context.get_assignment(n);         return val != l_undef && is_true == (val == l_true);     }     if (!is_app(n))         return false;     app * a = to_app(n);     if (a->get_family_id() == m_manager.get_basic_family_id()) {         switch (a->get_decl_kind()) {         case OP_TRUE:             return is_true;         case OP_FALSE:             return !is_true;         case OP_NOT:             return check(a->get_arg(0), !is_true);         case OP_OR:             return is_true ? any_arg(a, true) : all_args(a, false);         case OP_AND:             return is_true ? all_args(a, true) : any_arg(a, false);         case OP_IFF:             if (is_true) {                 return                      (check(a->get_arg(0), true) &&                      check(a->get_arg(1), true)) ||                     (check(a->get_arg(0), false) &&                      check(a->get_arg(1), false));             }             else {                 return                      (check(a->get_arg(0), true) &&                      check(a->get_arg(1), false)) ||                     (check(a->get_arg(0), false) &&                      check(a->get_arg(1), true));             }         case OP_ITE: {             if (m_context.lit_internalized(a->get_arg(0)) && m_context.is_relevant(a->get_arg(0))) {                 switch (m_context.get_assignment(a->get_arg(0))) {                 case l_false: return check(a->get_arg(2), is_true);                 case l_undef: return false;                 case l_true:  return check(a->get_arg(1), is_true);                 }             }             return check(a->get_arg(1), is_true) && check(a->get_arg(2), is_true);         }         case OP_EQ: {             enode * lhs = get_enode_eq_to(a->get_arg(0));             enode * rhs = get_enode_eq_to(a->get_arg(1));             if (lhs && rhs && m_context.is_relevant(lhs) && m_context.is_relevant(rhs)) {                 if (is_true && lhs->get_root() == rhs->get_root())                     return true;                 // if (!is_true && m_context.is_ext_diseq(lhs, rhs, 2))                 if (!is_true && m_context.is_diseq(lhs, rhs))                     return true;             }             return false;         }         default:             break;         }     }     enode * e = get_enode_eq_to(a);     if (e && e->is_bool() && m_context.is_relevant(e)) {         lbool val = m_context.get_assignment(e->get_owner());         return val != l_undef && is_true == (val == l_true);     }     return false; }

 void register_predicate(expr* a) {     SASSERT(is_predicate(a));     m_ctx.register_predicate(to_app(a)->get_decl(), false); }

    void reduce(proof* pf, proof_ref &out)    {        proof *res = nullptr;        m_todo.reset();        m_todo.push_back(pf);        ptr_buffer<proof> args;        bool dirty = false;        while (!m_todo.empty()) {            proof *p, *tmp, *pp;            unsigned todo_sz;            p = m_todo.back();            if (m_cache.find(p, tmp)) {                res = tmp;                m_todo.pop_back();                continue;            }            dirty = false;            args.reset();            todo_sz = m_todo.size();            for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) {                pp = m.get_parent(p, i);                if (m_cache.find(pp, tmp)) {                    args.push_back(tmp);                    dirty = dirty || pp != tmp;                } else {                    m_todo.push_back(pp);                }            }            if (todo_sz < m_todo.size()) { continue; }            else { m_todo.pop_back(); }            if (m.is_hypothesis(p)) {                // hyp: replace by a corresponding unit                if (m_units.find(m.get_fact(p), tmp)) {                    res = tmp;                } else { res = p; }            }            else if (!dirty) { res = p; }            else if (m.is_lemma(p)) {                //lemma: reduce the premise; remove reduced consequences from conclusion                SASSERT(args.size() == 1);                res = mk_lemma_core(args.get(0), m.get_fact(p));                compute_mark1(res);            } else if (m.is_unit_resolution(p)) {                // unit: reduce units; reduce the first premise; rebuild unit resolution                res = mk_unit_resolution_core(args.size(), args.c_ptr());                compute_mark1(res);            } else  {                // other: reduce all premises; reapply                if (m.has_fact(p)) { args.push_back(to_app(m.get_fact(p))); }                SASSERT(p->get_decl()->get_arity() == args.size());                res = m.mk_app(p->get_decl(), args.size(), (expr * const*)args.c_ptr());                m_pinned.push_back(res);                compute_mark1(res);            }            SASSERT(res);            m_cache.insert(p, res);            if (m.has_fact(res) && m.is_false(m.get_fact(res))) { break; }        }        out = res;    }

 bool is_real_expression(expr* e) {     return is_app(e) && (to_app(e)->get_family_id() == u().get_family_id()); }

 quantifier_stat * quantifier_stat_gen::operator()(quantifier * q, unsigned generation) {     reset();     quantifier_stat * r = new (m_region) quantifier_stat(generation);     m_todo.push_back(entry(q->get_expr()));     while (!m_todo.empty()) {         entry & e       = m_todo.back();         expr * n        = e.m_expr;         unsigned depth  = e.m_depth;         bool depth_only = e.m_depth_only;         m_todo.pop_back();         unsigned old_depth;         if (m_already_found.find(n, old_depth)) {             if (old_depth >= depth)                 continue;             depth_only  = true;         }         m_already_found.insert(n, depth);         if (depth >= r->m_depth)              r->m_depth = depth;         if (!depth_only) {             r->m_size++;             if (is_quantifier(n))                 r->m_num_nested_quantifiers ++;             if (is_app(n) && to_app(n)->get_family_id() == m_manager.get_basic_family_id()) {                 unsigned num_args = to_app(n)->get_num_args();                 // Remark: I'm approximating the case_split factor.                 // I'm also ignoring the case split factor due to theories.                 switch (to_app(n)->get_decl_kind()) {                 case OP_OR:                     if (depth == 0)                         m_case_split_factor *= num_args;                     else                         m_case_split_factor *= (num_args + 1);                     break;                 case OP_AND:                     if (depth > 0)                         m_case_split_factor *= (num_args + 1);                     break;                 case OP_IFF:                     if (depth == 0)                         m_case_split_factor *= 4;                     else                         m_case_split_factor *= 9;                     break;                 case OP_ITE:                     if (depth == 0)                         m_case_split_factor *= 4;                     else                         m_case_split_factor *= 9;                     break;                 default:                     break;                 }             }         }         if (is_app(n)) {             unsigned j = to_app(n)->get_num_args();             while (j > 0) {                 --j;                 m_todo.push_back(entry(to_app(n)->get_arg(j), depth + 1, depth_only));             }         }     }     r->m_case_split_factor = m_case_split_factor.get_value();     return r; }

 bool is_predicate(expr* a) {     SASSERT(m.is_bool(a));     return is_app(a) && to_app(a)->get_decl()->get_family_id() == null_family_id; }