From 9b53646a342dd65b5f48a45cad11da81ed5199f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 26 Aug 2017 01:43:06 -0700 Subject: [PATCH] mising files Signed-off-by: Nikolaj Bjorner --- src/smt/asserted_formulas_new.cpp | 619 ++++++++++++++++++++++++++++++ src/smt/asserted_formulas_new.h | 269 +++++++++++++ 2 files changed, 888 insertions(+) create mode 100644 src/smt/asserted_formulas_new.cpp create mode 100644 src/smt/asserted_formulas_new.h diff --git a/src/smt/asserted_formulas_new.cpp b/src/smt/asserted_formulas_new.cpp new file mode 100644 index 000000000..51bba9f7f --- /dev/null +++ b/src/smt/asserted_formulas_new.cpp @@ -0,0 +1,619 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + asserted_formulas_new.cpp + +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& 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 & 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& 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 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 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 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 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 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 + diff --git a/src/smt/asserted_formulas_new.h b/src/smt/asserted_formulas_new.h new file mode 100644 index 000000000..dc51c86ae --- /dev/null +++ b/src/smt/asserted_formulas_new.h @@ -0,0 +1,269 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + asserted_formulas_new.h + +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 m_formulas; + unsigned m_qhead; + macro_manager m_macro_manager; + scoped_ptr 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 m_scopes; + obj_map 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& new_fmls); + void push_assertion(expr * e, proof * pr, vector& 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 & 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_ */ +