z3-src 503.3.0

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    asserted_formulas.cpp

Abstract:

    <abstract>

Author:

    Leonardo de Moura (leonardo) 2008-06-11.

Revision History:

--*/
#include "util/warning.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/for_each_expr.h"
#include "ast/well_sorted.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/normal_forms/nnf.h"
#include "ast/pattern/pattern_inference.h"
#include "ast/macros/quasi_macros.h"
#include "ast/occurs.h"
#include "ast/bv_decl_plugin.h"
#include "solver/assertions/asserted_formulas.h"


asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_ref const& p):
    m(m),
    m_smt_params(sp),
    m_params(p),
    m_rewriter(m),
    m_substitution(m),
    m_scoped_substitution(m_substitution),
    m_defined_names(m),
    m_static_features(m),
    m_qhead(0),
    m_macro_manager(m),
    m_bv_sharing(m),
    m_inconsistent(false),
    m_has_quantifiers(false),
    m_reduce_asserted_formulas(*this),
    m_distribute_forall(*this),
    m_pattern_inference(*this),
    m_refine_inj_axiom(*this),
    m_max_bv_sharing_fn(*this),
    m_elim_term_ite(*this),
    m_qe_lite(*this),
    m_pull_nested_quantifiers(*this),
    m_elim_bvs_from_quantifiers(*this),
    m_cheap_quant_fourier_motzkin(*this),
    m_apply_bit2int(*this),
    m_bv_size_reduce(*this),
    m_lift_ite(*this),
    m_ng_lift_ite(*this),
    m_find_macros(*this),
    m_propagate_values(*this),
    m_nnf_cnf(*this),
    m_apply_quasi_macros(*this),
    m_flatten_clauses(*this),
    m_lazy_scopes(0) {

    m_macro_finder = alloc(macro_finder, m, m_macro_manager);

    m_elim_and = true;
    set_eliminate_and(false);

}

void asserted_formulas::setup() {
    switch (m_smt_params.m_lift_ite) {
    case lift_ite_kind::LI_FULL:
        m_smt_params.m_ng_lift_ite = lift_ite_kind::LI_NONE;
        break;
    case lift_ite_kind::LI_CONSERVATIVE:
        if (m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE)
            m_smt_params.m_ng_lift_ite = lift_ite_kind::LI_NONE;
        break;
    default:
        break;
    }

    if (m_smt_params.m_relevancy_lvl == 0)
        m_smt_params.m_relevancy_lemma = false;
}

void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_expr>& result) {
    if (inconsistent()) {
        return;
    }
    expr* e1 = nullptr;
    if (m.is_false(e)) {
        result.push_back(justified_expr(m, e, pr));
        m_inconsistent = true;
    }
    else if (m.is_true(e)) {
        // skip
    }
    else if (m.is_and(e)) {
        for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
            expr* arg = to_app(e)->get_arg(i);
            proof_ref _pr(m.proofs_enabled() ? m.mk_and_elim(pr, i) : nullptr, m);
            push_assertion(arg, _pr, result);
        }
    }
    else if (m.is_not(e, e1) && m.is_or(e1)) {
        for (unsigned i = 0; i < to_app(e1)->get_num_args(); ++i) {
            expr* arg = to_app(e1)->get_arg(i);
            proof_ref _pr(m.proofs_enabled() ? m.mk_not_or_elim(pr, i) : nullptr, m);
            expr_ref  narg(mk_not(m, arg), m);
            push_assertion(narg, _pr, result);
        }
    }
    else {
        result.push_back(justified_expr(m, e, pr));
    }
}

void asserted_formulas::updt_params(params_ref const& p) {
    m_params.append(p);
    m_reduce_pending = true;
}

void asserted_formulas::set_eliminate_and(bool flag) {
    if (flag == m_elim_and) return;
    m_elim_and = flag;
    m_reduce_pending = true;
    if (m_smt_params.m_pull_cheap_ite) m_params.set_bool("pull_cheap_ite", true);
    m_params.set_bool("elim_and", flag);
    m_params.set_bool("arith_ineq_lhs", true);
    m_params.set_bool("sort_sums", true);
    m_params.set_bool("rewrite_patterns", true);
    m_params.set_bool("eq2ineq", m_smt_params.m_arith_eq2ineq);
    m_params.set_bool("gcd_rounding", true);
    m_params.set_bool("expand_select_store", true);
    //m_params.set_bool("expand_nested_stores", true);
    m_params.set_bool("bv_sort_ac", true);
    // seq theory solver keeps terms in normal form and has to interact with side-effect of rewriting
    m_params.set_bool("coalesce_chars", m_smt_params.m_string_solver != symbol("seq"));
    m_params.set_bool("som", true);
    if (m_smt_params.m_arith_mode == arith_solver_id::AS_OLD_ARITH)
        m_params.set_bool("flat", true);
    m_rewriter.updt_params(m_params);
    flush_cache();
}


void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
    force_push();
    proof_ref  in_pr(_in_pr, m), pr(_in_pr, m);
    expr_ref   e_ref(e, m);
    expr_ref   r(e, m);
    SASSERT(m.is_bool(e));

    if (inconsistent())
        return;

    if (m.is_true(e))
        return;

    if (m_smt_params.m_preprocess) {
        TRACE(assert_expr_bug, tout << r << "\n";);
        set_eliminate_and(false); // do not eliminate and before nnf.
        m_rewriter(e_ref, r, pr);
        if (m.proofs_enabled()) {
            if (e_ref == r)
                pr = in_pr;
            else
                pr = m.mk_modus_ponens(in_pr, pr);
        }
        TRACE(assert_expr_bug, tout << "after...\n" << r << "\n" << pr << "\n";);
    }

    m_has_quantifiers |= ::has_quantifiers(e_ref);

    push_assertion(r, pr, m_formulas);
    m_reduce_pending = true;
    TRACE(asserted_formulas_bug, tout << "after assert_expr\n"; display(tout););
}

void asserted_formulas::assert_expr(expr * e) {
    assert_expr(e, m.proofs_enabled() ? m.mk_asserted(e) : nullptr);
}

void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
    for (justified_expr const& je : m_formulas) result.push_back(je.fml());
}

void asserted_formulas::push_scope() {
    ++m_lazy_scopes;
}

void asserted_formulas::push_scope_core() {
    reduce();
    commit();
    SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().is_canceled());
    TRACE(asserted_formulas_scopes, tout << "before push: " << m_scopes.size() << "\n");
    m_scoped_substitution.push();
    m_scopes.push_back(scope());
    scope & s = m_scopes.back();
    s.m_formulas_lim = m_formulas.size();
    SASSERT(inconsistent() || s.m_formulas_lim == m_qhead || m.limit().is_canceled());
    s.m_inconsistent_old = m_inconsistent;
    m_defined_names.push();
    m_elim_term_ite.push();
    m_bv_sharing.push_scope();
    m_macro_manager.push_scope();
    m_bv_size_reduce.push_scope();
    commit();
    TRACE(asserted_formulas_scopes, tout << "after push: " << m_scopes.size() << "\n");
}

void asserted_formulas::force_push() {
    for (; m_lazy_scopes > 0; --m_lazy_scopes)
        push_scope_core();
}

void asserted_formulas::pop_scope(unsigned num_scopes) {
    if (num_scopes <= m_lazy_scopes) {
        m_lazy_scopes -= num_scopes;
        return;
    }
    num_scopes -= m_lazy_scopes;
    m_lazy_scopes = 0;
    
    TRACE(asserted_formulas_scopes, tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";);
    m_bv_sharing.pop_scope(num_scopes);
    m_macro_manager.pop_scope(num_scopes);
    m_bv_size_reduce.pop_scope(num_scopes);
    unsigned new_lvl    = m_scopes.size() - num_scopes;
    scope & s           = m_scopes[new_lvl];
    m_inconsistent      = s.m_inconsistent_old;
    m_defined_names.pop(num_scopes);
    m_elim_term_ite.pop(num_scopes);
    m_scoped_substitution.pop(num_scopes);
    m_formulas.shrink(s.m_formulas_lim);
    m_qhead    = s.m_formulas_lim;
    m_scopes.shrink(new_lvl);
    flush_cache();
    TRACE(asserted_formulas_scopes, tout << "after pop " << num_scopes << "\n";);
}

void asserted_formulas::reset() {
    m_defined_names.reset();
    m_qhead = 0;
    m_formulas.reset();
    m_macro_manager.reset();
    m_bv_sharing.reset();
    m_rewriter.reset();
    m_inconsistent = false;
}

void asserted_formulas::finalize() {
    reset();
    m_substitution.cleanup();
}

bool asserted_formulas::check_well_sorted() const {
    for (justified_expr const& je : m_formulas) {
        if (!is_well_sorted(m, je.fml())) return false;
    }
    return true;
}

void asserted_formulas::reduce() {
    if (inconsistent())
        return;
    if (canceled())
        return;
    if (m_qhead == m_formulas.size())
        return;
    if (!m_has_quantifiers && !m_smt_params.m_preprocess)
        return;
    if (m_macro_manager.has_macros())
        invoke(m_find_macros);

    TRACE(before_reduce, display(tout););
    CASSERT("well_sorted", check_well_sorted());

    IF_VERBOSE(10, verbose_stream() << "(smt.simplify-begin :num-exprs " << get_total_size() << ")\n";);

    set_eliminate_and(false); // do not eliminate and before nnf.
    if (!invoke(m_propagate_values)) return;
    if (!invoke(m_find_macros)) return;
    if (!invoke(m_nnf_cnf)) return;
    set_eliminate_and(true);
    if (!invoke(m_reduce_asserted_formulas)) return;
    if (!invoke(m_pull_nested_quantifiers)) return;
    if (!invoke(m_lift_ite)) return;
    m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE);
    m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE);
    if (!invoke(m_ng_lift_ite)) return;
    if (!invoke(m_elim_term_ite)) return;
    if (!invoke(m_qe_lite)) return;
    if (!invoke(m_refine_inj_axiom)) return;
    if (!invoke(m_distribute_forall)) return;
    if (!invoke(m_find_macros)) return;
    if (!invoke(m_apply_quasi_macros)) return;
    if (!invoke(m_apply_bit2int)) return;
    if (!invoke(m_bv_size_reduce)) return;
    if (!invoke(m_cheap_quant_fourier_motzkin)) return;
    if (!invoke(m_pattern_inference)) return;
    if (!invoke(m_max_bv_sharing_fn)) return;
    if (!invoke(m_elim_bvs_from_quantifiers)) return;
    if (!invoke(m_reduce_asserted_formulas)) return;
    if (!invoke(m_flatten_clauses)) return;
//    if (!invoke(m_propagate_values)) return;

    IF_VERBOSE(10, verbose_stream() << "(smt.simplifier-done :num-exprs " << get_total_size() << ")\n";);
    TRACE(after_reduce, display(tout););
    TRACE(after_reduce_ll, ast_mark visited; display_ll(tout, visited););
    TRACE(macros, m_macro_manager.display(tout););
    flush_cache();
    CASSERT("well_sorted",check_well_sorted());

}


unsigned asserted_formulas::get_formulas_last_level() const {
    if (m_scopes.empty()) {
        return 0;
    }
    else {
        return m_scopes.back().m_formulas_lim;
    }
}

bool asserted_formulas::invoke(simplify_fmls& s) {
    if (!s.should_apply()) return true;
    s();
    IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << " :num-exprs " << get_total_size() << ")\n";);
    IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";);
    TRACE(reduce_step_ll, ast_mark visited; display_ll(tout, visited););
    CASSERT("well_sorted",check_well_sorted());
    TRACE(after_reduce, display(tout << s.id() << "\n"););
    if (inconsistent() || canceled()) {
        TRACE(after_reduce_ll, ast_mark visited; display_ll(tout, visited););
        return false;
    }
    else {
        return true;
    }
}

void asserted_formulas::display(std::ostream & out) const {
    out << "asserted formulas:\n";
    for (unsigned i = 0; i < m_formulas.size(); ++i) {
        if (i == m_qhead)
            out << "[HEAD] ==>\n";
        out << mk_pp(m_formulas[i].fml(), m) << "\n";
    }
    out << "inconsistent: " << inconsistent() << "\n";
}

void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) const {
    if (!m_formulas.empty()) {
        for (justified_expr const& f : m_formulas)
            ast_def_ll_pp(out, m, f.fml(), pp_visited, true, false);
        out << "asserted formulas:\n";
        for (justified_expr const& f : m_formulas)
            out << "#" << f.fml()->get_id() << " ";
        out << "\n";
    }
}

void asserted_formulas::collect_statistics(statistics & st) const {
}


void asserted_formulas::swap_asserted_formulas(vector<justified_expr>& formulas) {
    SASSERT(!inconsistent() || !formulas.empty());
    m_formulas.shrink(m_qhead);
    m_formulas.append(formulas);
}


void asserted_formulas::find_macros_core() {
    vector<justified_expr> new_fmls;
    unsigned sz = m_formulas.size();
    (*m_macro_finder)(sz - m_qhead, m_formulas.data() + m_qhead, new_fmls);
    swap_asserted_formulas(new_fmls);
    reduce_and_solve();
}

/**
   \brief rewrite (a or (b & c)) to (a or b), (a or c) if the conjunction (b & c)
   occurs as a disjunct of a single top-level clause and nowhere else.
   This avoids the literal for (b & c).

   A conjunction that is a disjunct of several clauses is left alone: distributing
   it would copy its conjuncts into every clause. Without the check,
   (or (and a1 .. an) (and b1 .. bm)) is first rewritten to the m clauses
   (or (and a1 .. an) (not bj)), and a second round would then distribute
   (and a1 .. an) into each of them, producing n*m clauses.

   The occurrence count only sees the clauses that are pending in the current
   round. The conjunction e = (not d), d = (or b1 .. bn), can also be shared with
   a formula asserted in an earlier round, which the context has internalized,
   or occur elsewhere, as in (or d x) after splitting (ite d x y). Then d has,
   or gets, a literal, and distributing e would copy the conjuncts next to it,
   once per assertion in incremental use. This sharing shows in the reference
   count of d: it is 1 when the negation e is its only parent. The reference
   count of e is not used; it is also raised by the rewriter caches and by the
   assertion that the caller keeps alive.
*/
void asserted_formulas::flatten_clauses() {
    if (m.proofs_enabled()) return;
    bool change = true;
    vector<justified_expr> new_fmls;
    auto mk_not = [this](expr* e) { return m.is_not(e, e) ? e : m.mk_not(e); };
    auto is_conjunction = [this](expr* e) { return m.is_not(e, e) && m.is_or(e); };
    expr *a = nullptr, *b = nullptr, *c = nullptr;
    obj_map<expr, unsigned> occurrences;
    while (change) {
        change = false;        
        new_fmls.reset();
        occurrences.reset();
        unsigned sz = m_formulas.size();
        for (unsigned i = m_qhead; i < sz; ++i) {
            expr* f = m_formulas.get(i).fml();
            if (!m.is_or(f, a, b))
                continue;
            if (is_conjunction(a))
                occurrences.insert_if_not_there(a, 0)++;
            if (is_conjunction(b))
                occurrences.insert_if_not_there(b, 0)++;
        }
        auto can_distribute = [&](expr* e) {
            unsigned n = 0;
            expr* d = nullptr;
            return occurrences.find(e, n) && n == 1 && m.is_not(e, d) && d->get_ref_count() == 1;
        };
        for (unsigned i = m_qhead; i < sz; ++i) {
            auto const& j = m_formulas.get(i);
            expr* f = j.fml();
            bool decomposed = false;
            if (m.is_or(f, a, b) && can_distribute(b)) {
                m.is_not(b, b);
                decomposed = true;
            }
            else if (m.is_or(f, b, a) && can_distribute(b)) {
                m.is_not(b, b);
                decomposed = true;
            }            
            if (decomposed) {
                for (expr* arg : *to_app(b)) {
                    justified_expr j1(m, m.mk_or(a, mk_not(arg)), nullptr);
                    new_fmls.push_back(j1);
                }
                change = true;
                continue;
            }
            if (m.is_ite(f, a, b, c)) {
                new_fmls.push_back(justified_expr(m, m.mk_or(mk_not(a), b), nullptr));
                new_fmls.push_back(justified_expr(m, m.mk_or(a, c), nullptr));
                change = true;
                continue;
            }
            new_fmls.push_back(j);            
        }
        swap_asserted_formulas(new_fmls);
    }
}


void asserted_formulas::apply_quasi_macros() {
    TRACE(before_quasi_macros, display(tout););
    vector<justified_expr> new_fmls;
    quasi_macros proc(m, m_macro_manager);
    while (m_qhead == 0 && 
           proc(m_formulas.size() - m_qhead,
                m_formulas.data() + m_qhead,
                new_fmls)) {
        swap_asserted_formulas(new_fmls);
        new_fmls.reset();
    }
    TRACE(after_quasi_macros, display(tout););
    reduce_and_solve();
}

void asserted_formulas::nnf_cnf() {
    nnf              apply_nnf(m, m_defined_names);
    vector<justified_expr> new_fmls;
    expr_ref_vector  push_todo(m);
    proof_ref_vector push_todo_prs(m);

    unsigned i  = m_qhead;
    unsigned sz = m_formulas.size();
    TRACE(nnf_bug, tout << "i: " << i << " sz: " << sz << "\n";);
    for (; i < sz; ++i) {
        expr * n    = m_formulas[i].fml();
        TRACE(nnf_bug, tout << "processing:\n" << mk_pp(n, m) << "\n";);
        proof_ref pr(m_formulas[i].pr(), m);
        expr_ref   r1(m);
        proof_ref  pr1(m);
        push_todo.reset();
        push_todo_prs.reset();
        CASSERT("well_sorted", is_well_sorted(m, n));
        apply_nnf(n, push_todo, push_todo_prs, r1, pr1);
        CASSERT("well_sorted",is_well_sorted(m, r1));
        pr = m.proofs_enabled() ? m.mk_modus_ponens(pr, pr1) : nullptr;
        push_todo.push_back(r1);
        push_todo_prs.push_back(pr);

        if (canceled()) {
            return;
        }
        unsigned sz2 = push_todo.size();
        for (unsigned k = 0; k < sz2; ++k) {
            expr * n   = push_todo.get(k);
            pr = nullptr;
            m_rewriter(n, r1, pr1);
            CASSERT("well_sorted",is_well_sorted(m, r1));
            if (canceled()) {
                return;
            }
            if (m.proofs_enabled())
                pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1);
            push_assertion(r1, pr, new_fmls);
        }
    }
    swap_asserted_formulas(new_fmls);
}

void asserted_formulas::simplify_fmls::operator()() {
    vector<justified_expr> new_fmls;
    unsigned sz = af.m_formulas.size();
    for (unsigned i = af.m_qhead; i < sz; ++i) {
        auto& j = af.m_formulas[i];
        expr_ref result(m);
        proof_ref result_pr(m);
        simplify(j, result, result_pr);
        SASSERT(is_well_sorted(m, j.fml()));
        if (m.proofs_enabled()) {
            if (!result_pr) result_pr = m.mk_rewrite(j.fml(), result);
            result_pr = m.mk_modus_ponens(j.pr(), result_pr);
        }
        if (j.fml() == result) {
            new_fmls.push_back(j);
        }
        else {
            af.push_assertion(result, result_pr, new_fmls);
            af.m_reduce_pending = true;
        }
        if (af.canceled())
            return;
    }
    af.swap_asserted_formulas(new_fmls);
    TRACE(asserted_formulas, af.display(tout););
    post_op();
}


void asserted_formulas::reduce_and_solve() {
    flush_cache(); // collect garbage
    m_reduce_asserted_formulas();
    IF_VERBOSE(10, verbose_stream() << "(smt.reduced " << get_total_size() << ")\n";);
}


void asserted_formulas::commit() {
    commit(m_formulas.size());
}

void asserted_formulas::commit(unsigned new_qhead) {
    m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.data() + m_qhead);
    for (unsigned i = m_qhead; i < new_qhead; ++i) {
        justified_expr const& j = m_formulas[i];
        update_substitution(j.fml(), j.pr());
    }
    m_qhead = new_qhead;
}

void asserted_formulas::propagate_values() {
    if (m.proofs_enabled())
        return;
    flush_cache();

    unsigned num_prop = 0;
    unsigned sz = m_formulas.size();
    unsigned delta_prop = sz;
    while (!inconsistent() && sz/20 < delta_prop) {
        m_scoped_substitution.push();
        unsigned prop = num_prop;
        TRACE(propagate_values, display(tout << "before:\n"););
        unsigned i  = m_qhead;
        for (; i < sz; ++i) {
            prop += propagate_values(i);
        }
        flush_cache();
        m_scoped_substitution.pop(1);
        m_scoped_substitution.push();
        TRACE(propagate_values, tout << "middle:\n"; display(tout););
        i = sz;
        while (i > m_qhead) {
            --i;
            prop += propagate_values(i);
        }
        m_scoped_substitution.pop(1);
        flush_cache();
        TRACE(propagate_values, tout << "after:\n"; display(tout););
        delta_prop = prop - num_prop;
        num_prop = prop;
        if (sz <= m_formulas.size())
            break;
        sz = m_formulas.size();
    }
    TRACE(asserted_formulas, tout << num_prop << "\n";);
    if (num_prop > 0)
        m_reduce_asserted_formulas();
}

unsigned asserted_formulas::propagate_values(unsigned i) {
    expr_ref n(m_formulas[i].fml(), m);
    expr_ref new_n(m);
    proof_ref new_pr(m);
    m_rewriter(n, new_n, new_pr);
    if (m.proofs_enabled()) {
        proof * pr  = m_formulas[i].pr();
        new_pr = m.mk_modus_ponens(pr, new_pr);
    }
    justified_expr j(m, new_n, new_pr);
    if (n != new_n)
        m_reduce_pending = true;
    m_formulas[i] = j;
    if (m.is_false(j.fml())) {
        m_inconsistent = true;
    }
    update_substitution(new_n, new_pr);
    return (n != new_n) ? 1 : 0;
}

bool asserted_formulas::update_substitution(expr* n, proof* pr) {
    expr* lhs, *rhs, *n1;
    proof_ref pr1(m);
    if (is_ground(n) && m.is_eq(n, lhs, rhs)) {
        if (is_gt(lhs, rhs)) {
            TRACE(propagate_values, tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";);
            m_scoped_substitution.insert(lhs, rhs, pr);
            return true;
        }
        if (is_gt(rhs, lhs)) {
            TRACE(propagate_values, tout << "insert " << mk_pp(rhs, m) << " -> " << mk_pp(lhs, m) << "\n";);
            pr1 = m.proofs_enabled() ? m.mk_symmetry(pr) : nullptr;
            m_scoped_substitution.insert(rhs, lhs, pr1);
            return true;
        }
        TRACE(propagate_values, tout << "incompatible " << mk_pp(n, m) << "\n";);
    }
    if (m.is_not(n, n1)) {
        pr1 = m.proofs_enabled() ? m.mk_iff_false(pr) : nullptr;
        m_scoped_substitution.insert(n1, m.mk_false(), pr1);
    }
    else {
        pr1 = m.proofs_enabled() ? m.mk_iff_true(pr) : nullptr;
        m_scoped_substitution.insert(n, m.mk_true(), pr1);
    }
    return false;
}


/**
   \brief implement a Knuth-Bendix ordering on expressions.
*/

bool asserted_formulas::is_gt(expr* lhs, expr* rhs) {
    if (lhs == rhs) {
        return false;
    }
    // values are always less in ordering than non-values.
    bool v1 = m.is_value(lhs);
    bool v2 = m.is_value(rhs);
    if (!v1 && v2) {
        return true;
    }
    if (v1 && !v2) {
        return false;
    }
    SASSERT(is_ground(lhs) && is_ground(rhs));
    if (depth(lhs) > depth(rhs)) {
        return true;
    }
    if (depth(lhs) == depth(rhs) && is_app(lhs) && is_app(rhs)) {
        app* l = to_app(lhs);
        app* r = to_app(rhs);
        if (l->get_decl()->get_id() != r->get_decl()->get_id()) {
            return l->get_decl()->get_id() > r->get_decl()->get_id();
        }
        if (l->get_num_args() != r->get_num_args()) {
            return l->get_num_args() > r->get_num_args();
        }
        for (unsigned i = 0; i < l->get_num_args(); ++i) {
            if (l->get_arg(i) != r->get_arg(i)) {
                return is_gt(l->get_arg(i), r->get_arg(i));
            }
        }
        UNREACHABLE();
    }

    return false;
}

proof * asserted_formulas::get_inconsistency_proof() const {
    if (!inconsistent())
        return nullptr;
    if (!m.proofs_enabled())
        return nullptr;
    if (!m.inc())
        return nullptr;
    for (justified_expr const& j : m_formulas) {
        if (m.is_false(j.fml()))
            return j.pr();
    }
    return nullptr;
}

void asserted_formulas::refine_inj_axiom_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) {
    expr* f = j.fml();
    if (is_quantifier(f) && simplify_inj_axiom(m, to_quantifier(f), n)) {
        TRACE(inj_axiom, tout << "simplifying...\n" << mk_pp(f, m) << "\n" << n << "\n";);
    }
    else {
        n = j.fml();
    }
}


void asserted_formulas::bv_size_reduce_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) {
    bv_util bv(m);
    expr* f = j.fml();
    expr* a, *b, *x;
    unsigned lo, hi;
    rational r;
    expr_ref new_term(m);
    auto check_reduce = [&](expr* a, expr* b) {
        if (bv.is_extract(a, lo, hi, x) && lo > 0 && hi + 1 == bv.get_bv_size(x) && bv.is_numeral(b, r) && r == 0) {
            // insert x -> x[0,lo-1] ++ n into sub
            new_term = bv.mk_concat(b, bv.mk_extract(lo - 1, 0, x));
            m_sub.insert(x, new_term);
            n = j.fml();
            return true;
        }
        return false;
    };
    if (m.is_eq(f, a, b) && (check_reduce(a, b) || check_reduce(b, a))) {
        // done
    }
    else {
        n = j.fml();
        m_sub(n);
    }
}

void asserted_formulas::bv_size_reduce_fn::push_scope() {
    m_sub.push_scope();
}

void asserted_formulas::bv_size_reduce_fn::pop_scope(unsigned n) {
    m_sub.pop_scope(n);
}

unsigned asserted_formulas::get_total_size() const {
    expr_mark visited;
    unsigned r  = 0;
    for (justified_expr const& j : m_formulas)
        r += get_num_exprs(j.fml(), visited);
    return r;
}


#ifdef Z3DEBUG
#include <iostream>
void pp(asserted_formulas & f) {
    f.display(std::cout);
}
#endif