mising files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/asserted_formulas_new.cpp

@@ -0,0 +1,619 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    asserted_formulas_new.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 "smt/asserted_formulas_new.h"
+
+asserted_formulas_new::asserted_formulas_new(ast_manager & m, smt_params & p):
+    m(m),
+    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_pull_cheap_ite_trees(*this),
+    m_pull_nested_quantifiers(*this),
+    m_elim_bvs_from_quantifiers(*this),
+    m_cheap_quant_fourier_motzkin(*this),
+    m_apply_bit2int(*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_macro_finder = alloc(macro_finder, m, m_macro_manager);
+}
+
+void asserted_formulas_new::setup() {
+    switch (m_params.m_lift_ite) {
+    case LI_FULL:
+        m_params.m_ng_lift_ite = LI_NONE; 
+        break;
+    case LI_CONSERVATIVE:
+        if (m_params.m_ng_lift_ite == LI_CONSERVATIVE)
+            m_params.m_ng_lift_ite = LI_NONE;
+        break;
+    default:
+        break;
+    }
+ 
+    if (m_params.m_relevancy_lvl == 0)
+        m_params.m_relevancy_lemma = false;
+}
+
+
+asserted_formulas_new::~asserted_formulas_new() {
+}
+
+void asserted_formulas_new::push_assertion(expr * e, proof * pr, vector<justified_expr>& result) {
+    if (inconsistent()) {
+        SASSERT(!result.empty());
+        return;
+    }
+    expr* e1 = 0;
+    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.mk_and_elim(pr, i), 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), *e2;
+            proof_ref _pr(m.mk_not_or_elim(pr, i), m);
+            if (m.is_not(arg, e2)) {
+                push_assertion(e2, _pr, result);
+            }
+            else {
+                expr_ref narg(m.mk_not(arg), m);
+                push_assertion(narg, _pr, result);
+            }
+        }        
+    }
+    else {
+        result.push_back(justified_expr(m, e, pr));
+    }
+}
+
+void asserted_formulas_new::set_eliminate_and(bool flag) {
+    params_ref p;
+    p.set_bool("elim_and", true);
+    m_rewriter.updt_params(p);
+    flush_cache();
+}
+
+
+void asserted_formulas_new::assert_expr(expr * e, proof * _in_pr) {
+    proof_ref  in_pr(_in_pr, m), pr(_in_pr, m);
+    expr_ref   r(e, m);
+
+    if (inconsistent()) 
+        return;
+
+    m_has_quantifiers |= ::has_quantifiers(e);
+
+    if (m_params.m_preprocess) {
+        TRACE("assert_expr_bug", tout << r << "\n";);
+        set_eliminate_and(false); // do not eliminate and before nnf.
+        m_rewriter(e, r, pr);
+        if (m.proofs_enabled()) {
+            if (e == r)
+                pr = in_pr;
+            else
+                pr = m.mk_modus_ponens(in_pr, pr);
+        }
+        TRACE("assert_expr_bug", tout << "after...\n" << r << "\n";);
+    }
+    push_assertion(r, pr, m_formulas);
+    TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout););
+}
+
+void asserted_formulas_new::assert_expr(expr * e) {
+    if (!inconsistent()) 
+        assert_expr(e, m.mk_asserted(e));
+}
+
+void asserted_formulas_new::get_assertions(ptr_vector<expr> & result) const {
+    for (justified_expr const& je : m_formulas) result.push_back(je.get_fml());
+}
+
+void asserted_formulas_new::push_scope() {
+    SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.canceled());
+    TRACE("asserted_formulas_new_scopes", tout << "push:\n"; display(tout););    
+    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.canceled());
+    s.m_inconsistent_old = m_inconsistent;
+    m_defined_names.push();
+    m_bv_sharing.push_scope();
+    m_macro_manager.push_scope();
+    commit();
+}
+ 
+void asserted_formulas_new::pop_scope(unsigned num_scopes) {
+    TRACE("asserted_formulas_new_scopes", tout << "before pop " << num_scopes << "\n"; display(tout););
+    m_bv_sharing.pop_scope(num_scopes);
+    m_macro_manager.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_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_new_scopes", tout << "after pop " << num_scopes << "\n"; display(tout););
+}
+
+void asserted_formulas_new::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;
+}
+
+bool asserted_formulas_new::check_well_sorted() const {
+    for (justified_expr const& je : m_formulas) {
+        if (!is_well_sorted(m, je.get_fml())) return false; 
+    }
+    return true;
+}
+
+void asserted_formulas_new::reduce() {
+    if (inconsistent())
+        return;
+    if (canceled())
+        return;
+    if (m_qhead == m_formulas.size())
+        return;
+    if (!m_params.m_preprocess) 
+        return;    
+    if (m_macro_manager.has_macros()) 
+        expand_macros();
+
+    TRACE("before_reduce", display(tout););
+    CASSERT("well_sorted", check_well_sorted());
+          
+    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_cheap_ite_trees)) return;
+    if (!invoke(m_pull_nested_quantifiers)) return;
+    if (!invoke(m_lift_ite)) return;
+    if (!invoke(m_ng_lift_ite)) return;
+    if (!invoke(m_elim_term_ite)) 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_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_VERBOSE(10, verbose_stream() << "(smt.simplifier-done)\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_new::get_formulas_last_level() const {
+    if (m_scopes.empty()) {
+        return 0;
+    }
+    else {
+        return m_scopes.back().m_formulas_lim;
+    }
+}
+
+bool asserted_formulas_new::invoke(simplify_fmls& s) {
+    if (!s.should_apply()) return true;
+    IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << ")\n";);
+    s();
+    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());                         
+    if (inconsistent() || canceled()) {                                 
+        TRACE("after_reduce", display(tout););                          
+        TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); 
+        return false;
+    }                
+    else {
+        return true;
+    }
+}
+
+void asserted_formulas_new::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].get_fml(), m) << "\n";
+    }
+    out << "inconsistent: " << inconsistent() << "\n";
+}
+
+void asserted_formulas_new::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.get_fml(), pp_visited, true, false);
+        out << "asserted formulas:\n";
+        for (justified_expr const& f : m_formulas) 
+            out << "#" << f.get_fml()->get_id() << " ";
+        out << "\n";
+    }
+}
+
+void asserted_formulas_new::collect_statistics(statistics & st) const {
+}
+
+
+void asserted_formulas_new::swap_asserted_formulas(vector<justified_expr>& formulas) {
+    SASSERT(!inconsistent() || !formulas.empty());
+    m_formulas.shrink(m_qhead);
+    m_formulas.append(formulas);
+}
+
+void asserted_formulas_new::find_macros_fn::operator()() {
+    TRACE("before_find_macros", af.display(tout););
+    af.find_macros_core();
+    TRACE("after_find_macros", af.display(tout););
+}
+
+void asserted_formulas_new::find_macros_core() {
+    vector<justified_expr> new_fmls;
+    unsigned sz = m_formulas.size();
+    (*m_macro_finder)(sz - m_qhead, m_formulas.c_ptr() + m_qhead, new_fmls);
+    swap_asserted_formulas(new_fmls);
+    reduce_and_solve();
+}
+
+
+void asserted_formulas_new::expand_macros() {
+    IF_IVERBOSE(10, verbose_stream() << "(smt.expand-macros)\n";);
+    find_macros_core();
+}
+
+void asserted_formulas_new::apply_quasi_macros() {
+    TRACE("before_quasi_macros", display(tout););
+    vector<justified_expr> new_fmls;
+    quasi_macros proc(m, m_macro_manager);    
+    while (proc(m_formulas.size() - m_qhead, 
+                m_formulas.c_ptr() + m_qhead, 
+                new_fmls)) {
+        swap_asserted_formulas(new_fmls);
+        new_fmls.reset();
+    }
+    TRACE("after_quasi_macros", display(tout););
+    reduce_and_solve();
+}
+
+void asserted_formulas_new::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].get_fml();
+        TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m) << "\n";);
+        proof * pr  = m_formulas[i].get_proof();
+        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.mk_modus_ponens(pr, pr1);
+        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 = 0;
+            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_new::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);
+        if (m.proofs_enabled()) {
+            if (!result_pr) result_pr = m.mk_rewrite(j.get_fml(), result);
+            result_pr = m.mk_modus_ponens(j.get_proof(), result_pr);
+        }
+        if (j.get_fml() == result) {
+            new_fmls.push_back(j);
+        }
+        else {
+            af.push_assertion(result, result_pr, new_fmls);
+        }
+        if (af.canceled()) return;
+    }    
+    af.swap_asserted_formulas(new_fmls);                    
+    TRACE("asserted_formulas", af.display(tout););
+    post_op();
+}
+
+
+void asserted_formulas_new::reduce_and_solve() {
+    IF_IVERBOSE(10, verbose_stream() << "(smt.reducing)\n";);
+    flush_cache(); // collect garbage
+    m_reduce_asserted_formulas();
+}
+
+
+void asserted_formulas_new::commit() {
+    commit(m_formulas.size());
+}
+
+void asserted_formulas_new::commit(unsigned new_qhead) {
+    m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.c_ptr() + m_qhead);
+    m_expr2depth.reset();
+    for (unsigned i = m_qhead; i < new_qhead; ++i) {
+        justified_expr const& j = m_formulas[i];
+        update_substitution(j.get_fml(), j.get_proof());
+    }
+    m_qhead = new_qhead;
+}
+
+void asserted_formulas_new::propagate_values() {
+    TRACE("propagate_values", tout << "before:\n"; display(tout););
+    flush_cache();
+
+    unsigned num_prop = 0;
+    while (true) {
+        m_expr2depth.reset();
+        m_scoped_substitution.push();
+        unsigned prop = num_prop;
+        TRACE("propagate_values", tout << "before:\n"; display(tout););
+        IF_IVERBOSE(10, verbose_stream() << "(smt.propagate-values)\n";);
+        unsigned i  = m_qhead;
+        unsigned sz = m_formulas.size();
+        for (; i < sz; i++) {
+            prop += propagate_values(i);
+        }
+        flush_cache();
+        m_scoped_substitution.pop(1);
+        m_expr2depth.reset();
+        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););
+        if (num_prop == prop) {
+            break;
+        }
+        num_prop = prop;
+    }
+    if (num_prop > 0)
+        m_reduce_asserted_formulas();
+}
+
+unsigned asserted_formulas_new::propagate_values(unsigned i) {
+    expr * n = m_formulas[i].get_fml();
+    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].get_proof();
+        new_pr = m.mk_modus_ponens(pr, new_pr);                         
+    }
+    m_formulas[i] = justified_expr(m, new_n, new_pr);
+    update_substitution(new_n, new_pr);
+    return n != new_n ? 1 : 0;
+}
+
+void asserted_formulas_new::update_substitution(expr* n, proof* pr) {
+    expr* lhs, *rhs, *n1;
+    if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) {
+        compute_depth(lhs);
+        compute_depth(rhs);
+        if (is_gt(lhs, rhs)) {
+            m_scoped_substitution.insert(lhs, rhs, pr);
+            return;
+        }
+        if (is_gt(rhs, lhs)) {
+            m_scoped_substitution.insert(rhs, lhs, m.mk_symmetry(pr));
+            return;
+        }
+    }
+    if (m.is_not(n, n1)) {
+        m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr)); 
+    }
+    else {
+        m_scoped_substitution.insert(n, m.mk_true(), m.mk_iff_true(pr)); 
+    }
+}
+
+/**
+   \brief implement a Knuth-Bendix ordering on expressions.
+*/
+
+bool asserted_formulas_new::is_gt(expr* lhs, expr* rhs) {
+    if (lhs == rhs) {
+        return false;
+    }
+    if (m.is_value(rhs)) {
+        return true;
+    }
+    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;
+}
+
+void asserted_formulas_new::compute_depth(expr* e) {
+    ptr_vector<expr> todo;
+    todo.push_back(e);    
+    while (!todo.empty()) {
+        e = todo.back();
+        unsigned d = 0;
+        if (m_expr2depth.contains(e)) {
+            todo.pop_back();
+            continue;
+        }
+        if (is_app(e)) {
+            app* a = to_app(e);
+            bool visited = true;
+            for (expr* arg : *a) {
+                unsigned d1 = 0;
+                if (m_expr2depth.find(arg, d1)) {
+                    d = std::max(d, d1);
+                }
+                else {
+                    visited = false;
+                    todo.push_back(arg);
+                }
+            }
+            if (!visited) {
+                continue;
+            }
+        }
+        todo.pop_back();
+        m_expr2depth.insert(e, d + 1);
+    }
+}
+
+proof * asserted_formulas_new::get_inconsistency_proof() const {
+    if (!inconsistent())
+        return 0;
+    if (!m.proofs_enabled())
+        return 0;
+    for (justified_expr const& j : m_formulas) {
+        if (m.is_false(j.get_fml()))
+            return j.get_proof();
+    }
+    UNREACHABLE();
+    return 0;
+}
+
+void asserted_formulas_new::refine_inj_axiom_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { 
+    expr* f = j.get_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.get_fml();
+    }
+}
+
+
+unsigned asserted_formulas_new::get_total_size() const {
+    expr_mark visited;
+    unsigned r  = 0;
+    for (justified_expr const& j : m_formulas)
+        r += get_num_exprs(j.get_fml(), visited);
+    return r;
+}
+
+#ifdef Z3DEBUG
+void pp(asserted_formulas_new & f) {
+    f.display(std::cout);
+}
+#endif
+

src/smt/asserted_formulas_new.h

@@ -0,0 +1,269 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    asserted_formulas_new.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-06-11.
+
+Revision History:
+
+--*/
+#ifndef ASSERTED_FORMULAS_NEW_H_
+#define ASSERTED_FORMULAS_NEW_H_
+
+#include "util/statistics.h"
+#include "ast/static_features.h"
+#include "ast/expr_substitution.h"
+#include "ast/rewriter/th_rewriter.h"
+#include "ast/rewriter/bit2int.h"
+#include "ast/rewriter/maximize_ac_sharing.h"
+#include "ast/rewriter/distribute_forall.h"
+#include "ast/rewriter/pull_ite_tree.h"
+#include "ast/rewriter/push_app_ite.h"
+#include "ast/rewriter/inj_axiom.h"
+#include "ast/rewriter/bv_elim2.h"
+#include "ast/rewriter/der.h"
+#include "ast/rewriter/elim_bounds2.h"
+#include "ast/macros/macro_manager.h"
+#include "ast/macros/macro_finder.h"
+#include "ast/normal_forms/defined_names.h"
+#include "ast/normal_forms/pull_quant.h"
+#include "ast/pattern/pattern_inference.h"
+#include "smt/params/smt_params.h"
+#include "smt/elim_term_ite.h"
+
+
+class asserted_formulas_new {
+    
+    ast_manager &               m;
+    smt_params &                m_params;
+    th_rewriter                 m_rewriter;
+    expr_substitution           m_substitution;
+    scoped_expr_substitution    m_scoped_substitution;
+    defined_names               m_defined_names;
+    static_features             m_static_features;
+    vector<justified_expr>      m_formulas;
+    unsigned                    m_qhead;
+    macro_manager               m_macro_manager;
+    scoped_ptr<macro_finder>    m_macro_finder;  
+    maximize_bv_sharing_rw      m_bv_sharing;
+    bool                        m_inconsistent;
+    bool                        m_has_quantifiers;
+    struct scope {
+        unsigned                m_formulas_lim;
+        bool                    m_inconsistent_old;
+    };
+    svector<scope>              m_scopes;
+    obj_map<expr, unsigned>     m_expr2depth;
+
+    class simplify_fmls {
+    protected:
+        asserted_formulas_new& af;
+        ast_manager&           m;
+        char const*            m_id;
+    public:
+        simplify_fmls(asserted_formulas_new& af, char const* id): af(af), m(af.m), m_id(id) {}
+        char const* id() const { return m_id; }
+        virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) = 0;
+        virtual bool should_apply() const { return true;}
+        virtual void post_op() {}
+        virtual void operator()();
+    };
+
+    class reduce_asserted_formulas_fn : public simplify_fmls {
+    public:
+        reduce_asserted_formulas_fn(asserted_formulas_new& af): simplify_fmls(af, "reduce-asserted") {}
+        virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { af.m_rewriter(j.get_fml(), n, p); }
+    };
+
+    class find_macros_fn : public simplify_fmls {
+    public:
+        find_macros_fn(asserted_formulas_new& af): simplify_fmls(af, "find-macros") {}
+        virtual void operator()();
+        virtual bool should_apply() const { return af.m_params.m_macro_finder && af.has_quantifiers(); }
+        virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { UNREACHABLE(); }
+    };
+
+    class apply_quasi_macros_fn : public simplify_fmls {
+    public:
+        apply_quasi_macros_fn(asserted_formulas_new& af): simplify_fmls(af, "find-quasi-macros") {}
+        virtual void operator()() { af.apply_quasi_macros(); }
+        virtual bool should_apply() const { return af.m_params.m_quasi_macros && af.has_quantifiers(); }
+        virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { UNREACHABLE(); }
+    };
+
+    class nnf_cnf_fn : public simplify_fmls {
+    public:
+        nnf_cnf_fn(asserted_formulas_new& af): simplify_fmls(af, "nnf-cnf") {}
+        virtual void operator()() { af.nnf_cnf(); }
+        virtual bool should_apply() const { return af.m_params.m_nnf_cnf || (af.m_params.m_mbqi && af.has_quantifiers()); }
+        virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { UNREACHABLE(); }
+    };
+
+    class propagate_values_fn : public simplify_fmls {
+    public:
+        propagate_values_fn(asserted_formulas_new& af): simplify_fmls(af, "propagate-values") {}
+        virtual void operator()() { af.propagate_values(); }
+        virtual bool should_apply() const { return af.m_params.m_propagate_values; }
+        virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { UNREACHABLE(); }
+    };
+
+    class distribute_forall_fn : public simplify_fmls {
+        distribute_forall m_functor;
+    public:
+        distribute_forall_fn(asserted_formulas_new& af): simplify_fmls(af, "distribute-forall"), m_functor(af.m) {}
+        virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { m_functor(j.get_fml(), n); }
+        virtual bool should_apply() const { return af.m_params.m_distribute_forall && af.has_quantifiers(); }
+        virtual void post_op() { af.reduce_and_solve();  TRACE("asserted_formulas", af.display(tout);); }
+    };
+
+    class pattern_inference_fn : public simplify_fmls {
+        pattern_inference_rw m_infer;
+    public:
+        pattern_inference_fn(asserted_formulas_new& af): simplify_fmls(af, "pattern-inference"), m_infer(af.m, af.m_params) {}
+        virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { m_infer(j.get_fml(), n, p); }
+        virtual bool should_apply() const { return af.m_params.m_ematching && af.has_quantifiers(); }
+    };
+
+    class refine_inj_axiom_fn : public simplify_fmls {
+    public:
+        refine_inj_axiom_fn(asserted_formulas_new& af): simplify_fmls(af, "refine-injectivity") {}
+        virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p);
+        virtual bool should_apply() const { return af.m_params.m_refine_inj_axiom && af.has_quantifiers(); }
+    };
+
+    class max_bv_sharing_fn : public simplify_fmls {
+    public:
+        max_bv_sharing_fn(asserted_formulas_new& af): simplify_fmls(af, "maximizing-bv-sharing") {}
+        virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { af.m_bv_sharing(j.get_fml(), n, p); }
+        virtual bool should_apply() const { return af.m_params.m_max_bv_sharing; }
+        virtual void post_op() { af.m_reduce_asserted_formulas(); }
+    };
+
+    class elim_term_ite_fn : public simplify_fmls {
+        elim_term_ite_rw m_elim;
+    public:
+        elim_term_ite_fn(asserted_formulas_new& af): simplify_fmls(af, "elim-term-ite"), m_elim(af.m, af.m_defined_names) {}
+        virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { m_elim(j.get_fml(), n, p); }
+        virtual bool should_apply() const { return af.m_params.m_eliminate_term_ite && af.m_params.m_lift_ite != LI_FULL; }
+        virtual void post_op() { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); }
+    };
+
+#define MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, ARG, REDUCE)            \
+    class NAME : public simplify_fmls {                                 \
+        FUNCTOR m_functor;                                              \
+    public:                                                             \
+        NAME(asserted_formulas_new& af):simplify_fmls(af, MSG), m_functor ARG {} \
+        virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { \
+            m_functor(j.get_fml(), n, p);                               \
+        }                                                               \
+        virtual void post_op() { if (REDUCE) af.reduce_and_solve(); }   \
+        virtual bool should_apply() const { return APP; }               \
+    };                                                                  \
+
+#define MK_SIMPLIFIERF(NAME, FUNCTOR, MSG, APP, REDUCE) MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, (af.m), REDUCE)
+
+    MK_SIMPLIFIERF(pull_cheap_ite_trees, pull_cheap_ite_tree_rw, "pull-cheap-ite-trees", af.m_params.m_pull_cheap_ite_trees, false);
+    MK_SIMPLIFIERF(pull_nested_quantifiers, pull_nested_quant, "pull-nested-quantifiers", af.m_params.m_pull_nested_quantifiers && af.has_quantifiers(), false);
+    MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_params.m_eliminate_bounds && af.has_quantifiers(), true);
+    MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_params.m_bb_quantifiers, true);
+    MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_params.m_simplify_bit2int, true);
+    MK_SIMPLIFIERA(lift_ite, push_app_ite_rw, "lift-ite", af.m_params.m_lift_ite != LI_NONE, (af.m, af.m_params.m_lift_ite == LI_CONSERVATIVE), true);
+    MK_SIMPLIFIERA(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_params.m_ng_lift_ite != LI_NONE, (af.m, af.m_params.m_ng_lift_ite == LI_CONSERVATIVE), true);
+
+
+    reduce_asserted_formulas_fn m_reduce_asserted_formulas;
+    distribute_forall_fn        m_distribute_forall;
+    pattern_inference_fn        m_pattern_inference;
+    refine_inj_axiom_fn         m_refine_inj_axiom;
+    max_bv_sharing_fn           m_max_bv_sharing_fn;
+    elim_term_ite_fn            m_elim_term_ite;
+    pull_cheap_ite_trees        m_pull_cheap_ite_trees;
+    pull_nested_quantifiers     m_pull_nested_quantifiers;
+    elim_bvs_from_quantifiers   m_elim_bvs_from_quantifiers;
+    cheap_quant_fourier_motzkin m_cheap_quant_fourier_motzkin;
+    apply_bit2int               m_apply_bit2int;
+    lift_ite                    m_lift_ite;
+    ng_lift_ite                 m_ng_lift_ite;
+    find_macros_fn              m_find_macros;
+    propagate_values_fn         m_propagate_values;
+    nnf_cnf_fn                  m_nnf_cnf;
+    apply_quasi_macros_fn       m_apply_quasi_macros;
+
+    bool invoke(simplify_fmls& s);
+    void swap_asserted_formulas(vector<justified_expr>& new_fmls);
+    void push_assertion(expr * e, proof * pr, vector<justified_expr>& result);
+    bool canceled() { return m.canceled(); }
+    bool check_well_sorted() const;
+    unsigned get_total_size() const;
+
+    void find_macros_core();
+    void expand_macros();
+    void apply_quasi_macros();
+    void nnf_cnf();
+    void reduce_and_solve();
+    void flush_cache() { m_rewriter.reset(); }
+    void set_eliminate_and(bool flag);
+    void propagate_values();
+    unsigned propagate_values(unsigned i);
+    void update_substitution(expr* n, proof* p);
+    bool is_gt(expr* lhs, expr* rhs);
+    void compute_depth(expr* e);
+    unsigned depth(expr* e) { return m_expr2depth[e]; }
+    bool pull_cheap_ite_trees();
+
+public:
+    asserted_formulas_new(ast_manager & m, smt_params & p);
+    ~asserted_formulas_new();
+
+    bool has_quantifiers() const { return m_has_quantifiers; }
+    void setup();
+    void assert_expr(expr * e, proof * in_pr);
+    void assert_expr(expr * e);
+    void reset();
+    void push_scope();
+    void pop_scope(unsigned num_scopes);
+    bool inconsistent() const { return m_inconsistent; }
+    proof * get_inconsistency_proof() const;
+    void reduce();
+    unsigned get_num_formulas() const { return m_formulas.size(); }
+    unsigned get_formulas_last_level() const;
+    unsigned get_qhead() const { return m_qhead; }
+    void commit(); 
+    void commit(unsigned new_qhead); 
+    expr *  get_formula(unsigned idx) const { return m_formulas[idx].get_fml(); }
+    proof * get_formula_proof(unsigned idx) const { return m_formulas[idx].get_proof(); }
+    
+    th_rewriter & get_rewriter() { return m_rewriter; }
+    void get_assertions(ptr_vector<expr> & result) const;
+    bool empty() const { return m_formulas.empty(); }
+    void display(std::ostream & out) const;
+    void display_ll(std::ostream & out, ast_mark & pp_visited) const;
+    void collect_statistics(statistics & st) const;
+    
+    // -----------------------------------
+    //
+    // Macros
+    //
+    // -----------------------------------
+    unsigned get_num_macros() const { return m_macro_manager.get_num_macros(); }
+    unsigned get_first_macro_last_level() const { return m_macro_manager.get_first_macro_last_level(); }
+    func_decl * get_macro_func_decl(unsigned i) const { return m_macro_manager.get_macro_func_decl(i); }
+    func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_macro_manager.get_macro_interpretation(i, interp); }
+    quantifier * get_macro_quantifier(func_decl * f) const { return m_macro_manager.get_macro_quantifier(f); }
+    // auxiliary function used to create a logic context based on a model.
+    void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_macro_manager.insert(f, m, pr); }
+    void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency* dep) { m_macro_manager.insert(f, m, pr, dep); }
+
+};
+
+#endif /* ASSERTED_FORMULAS_NEW_H_ */
+