From ebcacaa26d0a14c6d7893a28c154c8683243882b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Aug 2017 17:44:33 -0700 Subject: [PATCH] update new assertions Signed-off-by: Nikolaj Bjorner --- src/ast/ast.h | 36 ++++++++ src/ast/macros/macro_finder.cpp | 141 +++++++++++++++++++++++++++++ src/ast/macros/macro_finder.h | 3 + src/ast/macros/macro_manager.cpp | 8 ++ src/ast/macros/macro_manager.h | 1 + src/ast/macros/quasi_macros.cpp | 62 +++++++++++++ src/ast/macros/quasi_macros.h | 3 + src/ast/rewriter/CMakeLists.txt | 1 + src/ast/simplifier/CMakeLists.txt | 1 - src/ast/simplifier/bv_elim.cpp | 52 +++++------ src/ast/simplifier/bv_elim.h | 4 +- src/ast/simplifier/inj_axiom.cpp | 142 ------------------------------ src/ast/simplifier/inj_axiom.h | 27 ------ src/smt/CMakeLists.txt | 1 + src/smt/asserted_formulas.cpp | 2 +- src/smt/elim_term_ite.cpp | 18 ++++ src/smt/elim_term_ite.h | 28 ++++++ 17 files changed, 331 insertions(+), 199 deletions(-) delete mode 100644 src/ast/simplifier/inj_axiom.cpp delete mode 100644 src/ast/simplifier/inj_axiom.h diff --git a/src/ast/ast.h b/src/ast/ast.h index e6beec7e6..408ca4063 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2470,6 +2470,42 @@ public: void operator()(AST * n) { m_manager.inc_ref(n); } }; +class justified_expr { + ast_manager& m; + expr* m_fml; + proof* m_proof; + public: + justified_expr(ast_manager& m, expr* fml, proof* p): + m(m), + m_fml(fml), + m_proof(p) { + m.inc_ref(fml); + m.inc_ref(p); + } + + justified_expr& operator=(justified_expr& other) { + SASSERT(&m == &other.m); + if (this != &other) { + m.dec_ref(m_fml); + m.dec_ref(m_proof); + m_fml = other.get_fml(); + m_proof = other.get_proof(); + m.inc_ref(m_fml); + m.inc_ref(m_proof); + } + return *this; + } + + ~justified_expr() { + m.dec_ref(m_fml); + m.dec_ref(m_proof); + } + + expr* get_fml() const { return m_fml; } + proof* get_proof() const { return m_proof; } +}; + + #endif /* AST_H_ */ diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp index 1d441aee7..9a8e552fc 100644 --- a/src/ast/macros/macro_finder.cpp +++ b/src/ast/macros/macro_finder.cpp @@ -111,6 +111,71 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex return true; } +bool macro_finder::is_arith_macro(expr * n, proof * pr, vector& new_fmls) { + if (!is_quantifier(n) || !to_quantifier(n)->is_forall()) + return false; + expr * body = to_quantifier(n)->get_expr(); + unsigned num_decls = to_quantifier(n)->get_num_decls(); + + if (!m_autil.is_le(body) && !m_autil.is_ge(body) && !m_manager.is_eq(body)) + return false; + if (!m_autil.is_add(to_app(body)->get_arg(0))) + return false; + app_ref head(m_manager); + expr_ref def(m_manager); + bool inv = false; + if (!m_util.is_arith_macro(body, num_decls, head, def, inv)) + return false; + app_ref new_body(m_manager); + + if (!inv || m_manager.is_eq(body)) + new_body = m_manager.mk_app(to_app(body)->get_decl(), head, def); + else if (m_autil.is_le(body)) + new_body = m_autil.mk_ge(head, def); + else + new_body = m_autil.mk_le(head, def); + + quantifier_ref new_q(m_manager); + new_q = m_manager.update_quantifier(to_quantifier(n), new_body); + proof * new_pr = 0; + if (m_manager.proofs_enabled()) { + proof * rw = m_manager.mk_rewrite(n, new_q); + new_pr = m_manager.mk_modus_ponens(pr, rw); + } + if (m_manager.is_eq(body)) { + return m_macro_manager.insert(head->get_decl(), new_q, new_pr); + } + // is ge or le + // + TRACE("macro_finder", tout << "is_arith_macro: is_ge or is_le\n";); + func_decl * f = head->get_decl(); + func_decl * k = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range()); + app * k_app = m_manager.mk_app(k, head->get_num_args(), head->get_args()); + expr_ref_buffer new_rhs_args(m_manager); + expr_ref new_rhs2(m_autil.mk_add(def, k_app), m_manager); + expr * body1 = m_manager.mk_eq(head, new_rhs2); + expr * body2 = m_manager.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0)); + quantifier * q1 = m_manager.update_quantifier(new_q, body1); + expr * patterns[1] = { m_manager.mk_pattern(k_app) }; + quantifier * q2 = m_manager.update_quantifier(new_q, 1, patterns, body2); + proof* pr1 = 0, *pr2 = 0; + if (m_manager.proofs_enabled()) { + // new_pr : new_q + // rw : [rewrite] new_q ~ q1 & q2 + // mp : [modus_pones new_pr rw] q1 & q2 + // pr1 : [and-elim mp] q1 + // pr2 : [and-elim mp] q2 + app * q1q2 = m_manager.mk_and(q1,q2); + proof * rw = m_manager.mk_oeq_rewrite(new_q, q1q2); + proof * mp = m_manager.mk_modus_ponens(new_pr, rw); + pr1 = m_manager.mk_and_elim(mp, 0); + pr2 = m_manager.mk_and_elim(mp, 1); + } + new_fmls.push_back(justified_expr(m_manager, q1, pr1)); + new_fmls.push_back(justified_expr(m_manager, q2, pr2)); + return true; +} + /** n is of the form: (forall (X) (iff (= (f X) t) def[X])) @@ -152,6 +217,34 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e } } +static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, + vector& new_fmls) { + func_decl * f = head->get_decl(); + func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range()); + app * k_app = m.mk_app(k, head->get_num_args(), head->get_args()); + app * ite = m.mk_ite(def, t, k_app); + app * body_1 = m.mk_eq(head, ite); + app * body_2 = m.mk_not(m.mk_eq(k_app, t)); + quantifier * q1 = m.update_quantifier(q, body_1); + proof * pr1 = 0, *pr2 = 0; + expr * pats[1] = { m.mk_pattern(k_app) }; + quantifier * q2 = m.update_quantifier(q, 1, pats, body_2); // erase patterns + if (m.proofs_enabled()) { + // r : [rewrite] q ~ q1 & q2 + // pr : q + // mp : [modus_pones pr pr1] q1 & q2 + // pr1 : [and-elim mp] q1 + // pr2 : [and-elim mp] q2 + app * q1q2 = m.mk_and(q1,q2); + proof * r = m.mk_oeq_rewrite(q, q1q2); + proof * mp = m.mk_modus_ponens(pr, r); + pr1 = m.mk_and_elim(mp, 0); + pr2 = m.mk_and_elim(mp, 1); + } + new_fmls.push_back(justified_expr(m, q1, pr1)); + new_fmls.push_back(justified_expr(m, q2, pr2)); +} + macro_finder::macro_finder(ast_manager & m, macro_manager & mm): m_manager(m), m_macro_manager(mm), @@ -216,3 +309,51 @@ void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const } + +bool macro_finder::expand_macros(unsigned num, justified_expr const * fmls, vector& new_fmls) { + TRACE("macro_finder", tout << "starting expand_macros:\n"; + m_macro_manager.display(tout);); + bool found_new_macro = false; + for (unsigned i = 0; i < num; i++) { + expr * n = fmls[i].get_fml(); + proof * pr = m_manager.proofs_enabled() ? fmls[i].get_proof() : 0; + expr_ref new_n(m_manager), def(m_manager); + proof_ref new_pr(m_manager); + m_macro_manager.expand_macros(n, pr, new_n, new_pr); + app_ref head(m_manager), t(m_manager); + if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr)) { + TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";); + found_new_macro = true; + } + else if (is_arith_macro(new_n, new_pr, new_fmls)) { + TRACE("macro_finder_found", tout << "found new arith macro:\n" << new_n << "\n";); + found_new_macro = true; + } + else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) { + TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";); + pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_fmls); + found_new_macro = true; + } + else { + new_fmls.push_back(justified_expr(m_manager, new_n, new_pr)); + } + } + return found_new_macro; +} + +void macro_finder::operator()(unsigned n, justified_expr const* fmls, vector& new_fmls) { + TRACE("macro_finder", tout << "processing macros...\n";); + vector _new_fmls; + if (expand_macros(n, fmls, _new_fmls)) { + while (true) { + vector old_fmls; + _new_fmls.swap(old_fmls); + SASSERT(_new_fmls.empty()); + if (!expand_macros(old_fmls.size(), old_fmls.c_ptr(), _new_fmls)) + break; + } + } + new_fmls.append(_new_fmls); +} + + diff --git a/src/ast/macros/macro_finder.h b/src/ast/macros/macro_finder.h index 5807573ae..2bba07306 100644 --- a/src/ast/macros/macro_finder.h +++ b/src/ast/macros/macro_finder.h @@ -38,7 +38,9 @@ class macro_finder { macro_util & m_util; arith_util m_autil; bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); + bool expand_macros(unsigned n, justified_expr const * fmls, vector& new_fmls); bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); + bool is_arith_macro(expr * n, proof * pr, vector& new_fmls); bool is_macro(expr * n, app_ref & head, expr_ref & def); bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t); @@ -48,6 +50,7 @@ public: macro_finder(ast_manager & m, macro_manager & mm); ~macro_finder(); void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); + void operator()(unsigned n, justified_expr const* fmls, vector& new_fmls); }; #endif /* MACRO_FINDER_H_ */ diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp index bff1e7dae..7a2642fa3 100644 --- a/src/ast/macros/macro_manager.cpp +++ b/src/ast/macros/macro_manager.cpp @@ -152,6 +152,14 @@ void macro_manager::mark_forbidden(unsigned n, expr * const * exprs) { for_each_expr(p, visited, exprs[i]); } +void macro_manager::mark_forbidden(unsigned n, justified_expr const * exprs) { + expr_mark visited; + macro_manager_ns::proc p(m_forbidden_set, m_forbidden); + for (unsigned i = 0; i < n; i++) + for_each_expr(p, visited, exprs[i].get_fml()); +} + + void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const { app * body = to_app(q->get_expr()); SASSERT(m.is_eq(body) || m.is_iff(body)); diff --git a/src/ast/macros/macro_manager.h b/src/ast/macros/macro_manager.h index 71864a699..58fedf666 100644 --- a/src/ast/macros/macro_manager.h +++ b/src/ast/macros/macro_manager.h @@ -71,6 +71,7 @@ public: void pop_scope(unsigned num_scopes); void reset(); void mark_forbidden(unsigned n, expr * const * exprs); + void mark_forbidden(unsigned n, justified_expr const * exprs); void mark_forbidden(expr * e) { mark_forbidden(1, &e); } bool is_forbidden(func_decl * d) const { return m_forbidden_set.contains(d); } obj_hashtable const & get_forbidden_set() const { return m_forbidden_set; } diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp index 822532532..527b9656d 100644 --- a/src/ast/macros/quasi_macros.cpp +++ b/src/ast/macros/quasi_macros.cpp @@ -293,6 +293,44 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) { return res; } +bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) { + TRACE("quasi_macros", tout << "Finding quasi-macros in: " << std::endl; + for (unsigned i = 0 ; i < n ; i++) + tout << i << ": " << mk_pp(exprs[i].get_fml(), m_manager) << std::endl; ); + bool res = false; + m_occurrences.reset(); + + + // Find out how many non-ground appearences for each uninterpreted function there are + for ( unsigned i = 0 ; i < n ; i++ ) + find_occurrences(exprs[i].get_fml()); + + TRACE("quasi_macros", tout << "Occurrences: " << std::endl; + for (occurrences_map::iterator it = m_occurrences.begin(); + it != m_occurrences.end(); + it++) + tout << it->m_key->get_name() << ": " << it->m_value << std::endl; ); + + // Find all macros + for ( unsigned i = 0 ; i < n ; i++ ) { + app_ref a(m_manager); + expr_ref t(m_manager); + if (is_quasi_macro(exprs[i].get_fml(), a, t)) { + quantifier_ref macro(m_manager); + quasi_macro_to_macro(to_quantifier(exprs[i].get_fml()), a, t, macro); + TRACE("quasi_macros", tout << "Found quasi macro: " << mk_pp(exprs[i].get_fml(), m_manager) << std::endl; + tout << "Macro: " << mk_pp(macro, m_manager) << std::endl; ); + proof * pr = 0; + if (m_manager.proofs_enabled()) + pr = m_manager.mk_def_axiom(macro); + if (m_macro_manager.insert(a->get_decl(), macro, pr)) + res = true; + } + } + + return res; +} + void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { for ( unsigned i = 0 ; i < n ; i++ ) { expr_ref r(m_manager), rs(m_manager); @@ -319,3 +357,27 @@ bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const * return false; } } + +void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector& new_fmls) { + for ( unsigned i = 0 ; i < n ; i++ ) { + expr_ref r(m_manager), rs(m_manager); + proof_ref pr(m_manager), ps(m_manager); + proof * p = m_manager.proofs_enabled() ? fmls[i].get_proof() : 0; + m_macro_manager.expand_macros(fmls[i].get_fml(), p, r, pr); + m_rewriter(r); + new_fmls.push_back(justified_expr(m_manager, r, pr)); + } +} + +bool quasi_macros::operator()(unsigned n, justified_expr const* fmls, vector& new_fmls) { + if (find_macros(n, fmls)) { + apply_macros(n, fmls, new_fmls); + return true; + } else { + // just copy them over + for ( unsigned i = 0 ; i < n ; i++ ) { + new_fmls.push_back(fmls[i]); + } + return false; + } +} diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h index 29efe63c7..7288ac601 100644 --- a/src/ast/macros/quasi_macros.h +++ b/src/ast/macros/quasi_macros.h @@ -53,7 +53,9 @@ class quasi_macros { void find_occurrences(expr * e); bool find_macros(unsigned n, expr * const * exprs); + bool find_macros(unsigned n, justified_expr const* expr); void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); + void apply_macros(unsigned n, justified_expr const* fmls, vector& new_fmls); public: quasi_macros(ast_manager & m, macro_manager & mm); @@ -63,6 +65,7 @@ public: \brief Find pure function macros and apply them. */ bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); + bool operator()(unsigned n, justified_expr const* fmls, vector& new_fmls); }; #endif diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index 72bca53d4..c1b99bcae 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -15,6 +15,7 @@ z3_add_component(rewriter expr_safe_replace.cpp factor_rewriter.cpp fpa_rewriter.cpp + inj_axiom.cpp label_rewriter.cpp mk_simplified_app.cpp pb_rewriter.cpp diff --git a/src/ast/simplifier/CMakeLists.txt b/src/ast/simplifier/CMakeLists.txt index c5c310c07..b6fe9b1cd 100644 --- a/src/ast/simplifier/CMakeLists.txt +++ b/src/ast/simplifier/CMakeLists.txt @@ -12,7 +12,6 @@ z3_add_component(simplifier datatype_simplifier_plugin.cpp elim_bounds.cpp fpa_simplifier_plugin.cpp - inj_axiom.cpp maximise_ac_sharing.cpp poly_simplifier_plugin.cpp seq_simplifier_plugin.cpp diff --git a/src/ast/simplifier/bv_elim.cpp b/src/ast/simplifier/bv_elim.cpp index 1875e333b..1c0048a07 100644 --- a/src/ast/simplifier/bv_elim.cpp +++ b/src/ast/simplifier/bv_elim.cpp @@ -12,16 +12,16 @@ Copyright (c) 2015 Microsoft Corporation void bv_elim::elim(quantifier* q, quantifier_ref& r) { svector names, _names; - sort_ref_buffer sorts(m_manager), _sorts(m_manager); - expr_ref_buffer pats(m_manager); - expr_ref_buffer no_pats(m_manager); - expr_ref_buffer subst_map(m_manager), _subst_map(m_manager); - var_subst subst(m_manager); - bv_util bv(m_manager); - expr_ref new_body(m_manager); + sort_ref_buffer sorts(m), _sorts(m); + expr_ref_buffer pats(m); + expr_ref_buffer no_pats(m); + expr_ref_buffer subst_map(m), _subst_map(m); + var_subst subst(m); + bv_util bv(m); + expr_ref new_body(m); expr* old_body = q->get_expr(); unsigned num_decls = q->get_num_decls(); - family_id bfid = m_manager.mk_family_id("bv"); + family_id bfid = m.mk_family_id("bv"); // // Traverse sequence of bound variables to eliminate @@ -37,23 +37,23 @@ void bv_elim::elim(quantifier* q, quantifier_ref& r) { if (bv.is_bv_sort(s)) { // convert n-bit bit-vector variable into sequence of n-Booleans. unsigned num_bits = bv.get_bv_size(s); - expr_ref_buffer args(m_manager); - expr_ref bv(m_manager); + expr_ref_buffer args(m); + expr_ref bv(m); for (unsigned j = 0; j < num_bits; ++j) { std::ostringstream new_name; new_name << nm.str(); new_name << "_"; new_name << j; - var* v = m_manager.mk_var(var_idx++, m_manager.mk_bool_sort()); + var* v = m.mk_var(var_idx++, m.mk_bool_sort()); args.push_back(v); - _sorts.push_back(m_manager.mk_bool_sort()); + _sorts.push_back(m.mk_bool_sort()); _names.push_back(symbol(new_name.str().c_str())); } - bv = m_manager.mk_app(bfid, OP_MKBV, 0, 0, args.size(), args.c_ptr()); + bv = m.mk_app(bfid, OP_MKBV, 0, 0, args.size(), args.c_ptr()); _subst_map.push_back(bv.get()); } else { - _subst_map.push_back(m_manager.mk_var(var_idx++, s)); + _subst_map.push_back(m.mk_var(var_idx++, s)); _sorts.push_back(s); _names.push_back(nm); } @@ -78,26 +78,26 @@ void bv_elim::elim(quantifier* q, quantifier_ref& r) { subst(old_body, sub_size, sub, new_body); for (unsigned j = 0; j < q->get_num_patterns(); j++) { - expr_ref pat(m_manager); + expr_ref pat(m); subst(q->get_pattern(j), sub_size, sub, pat); pats.push_back(pat); } for (unsigned j = 0; j < q->get_num_no_patterns(); j++) { - expr_ref nopat(m_manager); + expr_ref nopat(m); subst(q->get_no_pattern(j), sub_size, sub, nopat); no_pats.push_back(nopat); } - r = m_manager.mk_quantifier(true, - names.size(), - sorts.c_ptr(), - names.c_ptr(), - new_body.get(), - q->get_weight(), - q->get_qid(), - q->get_skid(), - pats.size(), pats.c_ptr(), - no_pats.size(), no_pats.c_ptr()); + r = m.mk_quantifier(true, + names.size(), + sorts.c_ptr(), + names.c_ptr(), + new_body.get(), + q->get_weight(), + q->get_qid(), + q->get_skid(), + pats.size(), pats.c_ptr(), + no_pats.size(), no_pats.c_ptr()); } bool bv_elim_star::visit_quantifier(quantifier* q) { diff --git a/src/ast/simplifier/bv_elim.h b/src/ast/simplifier/bv_elim.h index 2b8a4778a..c027b1a9e 100644 --- a/src/ast/simplifier/bv_elim.h +++ b/src/ast/simplifier/bv_elim.h @@ -24,9 +24,9 @@ Revision History: #include "ast/simplifier/simplifier.h" class bv_elim { - ast_manager& m_manager; + ast_manager& m; public: - bv_elim(ast_manager& m) : m_manager(m) {}; + bv_elim(ast_manager& m) : m(m) {}; void elim(quantifier* q, quantifier_ref& r); }; diff --git a/src/ast/simplifier/inj_axiom.cpp b/src/ast/simplifier/inj_axiom.cpp deleted file mode 100644 index 2aa828ffa..000000000 --- a/src/ast/simplifier/inj_axiom.cpp +++ /dev/null @@ -1,142 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - inj_axiom.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-06-23. - -Revision History: - ---*/ -#include "ast/simplifier/inj_axiom.h" -#include "ast/ast_pp.h" -#include "ast/ast_ll_pp.h" -#include "ast/has_free_vars.h" -#include "ast/well_sorted.h" - -/** - \brief Little HACK for simplifying injectivity axioms - - \remark It is not covering all possible cases. -*/ -bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result) { - expr * n = q->get_expr(); - if (q->is_forall() && m.is_or(n) && to_app(n)->get_num_args() == 2) { - expr * arg1 = to_app(n)->get_arg(0); - expr * arg2 = to_app(n)->get_arg(1); - if (m.is_not(arg2)) - std::swap(arg1, arg2); - if (m.is_not(arg1) && - m.is_eq(to_app(arg1)->get_arg(0)) && - m.is_eq(arg2)) { - expr * app1 = to_app(to_app(arg1)->get_arg(0))->get_arg(0); - expr * app2 = to_app(to_app(arg1)->get_arg(0))->get_arg(1); - expr * var1 = to_app(arg2)->get_arg(0); - expr * var2 = to_app(arg2)->get_arg(1); - if (is_app(app1) && - is_app(app2) && - to_app(app1)->get_decl() == to_app(app2)->get_decl() && - to_app(app1)->get_num_args() == to_app(app2)->get_num_args() && - to_app(app1)->get_family_id() == null_family_id && - to_app(app1)->get_num_args() > 0 && - is_var(var1) && - is_var(var2) && - var1 != var2) { - app * f1 = to_app(app1); - app * f2 = to_app(app2); - bool found_vars = false; - unsigned num = f1->get_num_args(); - unsigned idx = UINT_MAX; - unsigned num_vars = 1; - for (unsigned i = 0; i < num; i++) { - expr * c1 = f1->get_arg(i); - expr * c2 = f2->get_arg(i); - if (!is_var(c1) && !is_uninterp_const(c1)) - return false; - if ((c1 == var1 && c2 == var2) || (c1 == var2 && c2 == var1)) { - if (found_vars) - return false; - found_vars = true; - idx = i; - } - else if (c1 == c2 && c1 != var1 && c1 != var2) { - if (is_var(c1)) { - ++num_vars; - } - } - else { - return false; - } - } - if (found_vars && !has_free_vars(q)) { - TRACE("inj_axiom", - tout << "Cadidate for simplification:\n" << mk_ll_pp(q, m) << mk_pp(app1, m) << "\n" << mk_pp(app2, m) << "\n" << - mk_pp(var1, m) << "\n" << mk_pp(var2, m) << "\nnum_vars: " << num_vars << "\n";); - // Building new (optimized) axiom - func_decl * decl = f1->get_decl(); - unsigned var_idx = 0; - ptr_buffer f_args, inv_vars; - ptr_buffer decls; - buffer names; - - expr * var = 0; - for (unsigned i = 0; i < num; i++) { - expr * c = f1->get_arg(i); - if (is_var(c)) { - names.push_back(symbol(i)); - sort * s = decl->get_domain(i); - decls.push_back(s); - expr * new_c = m.mk_var(var_idx, s); - var_idx++; - f_args.push_back(new_c); - if (i == idx) { - var = new_c; - } - else { - inv_vars.push_back(new_c); - } - } - else { - SASSERT(is_uninterp_const(c)); - f_args.push_back(c); - } - } - SASSERT(var != 0); - app * f = m.mk_app(decl, f_args.size(), f_args.c_ptr()); - - ptr_vector domain; - inv_vars.push_back(f); - for (unsigned i = 0; i < inv_vars.size(); ++i) { - domain.push_back(m.get_sort(inv_vars[i])); - } - sort * d = decl->get_domain(idx); - func_decl * inv_decl = m.mk_fresh_func_decl("inj", domain.size(), domain.c_ptr(), d); - - expr * proj = m.mk_app(inv_decl, inv_vars.size(), inv_vars.c_ptr()); - expr * eq = m.mk_eq(proj, var); - expr * p = m.mk_pattern(f); - - // decls are in the wrong order... - // Remark: the sort of the var 0 must be in the last position. - std::reverse(decls.begin(), decls.end()); - - result = m.mk_forall(decls.size(), decls.c_ptr(), names.c_ptr(), eq, - 0, symbol(), symbol(), 1, &p); - TRACE("inj_axiom", tout << "new axiom:\n" << mk_pp(result, m) << "\n";); - SASSERT(is_well_sorted(m, result)); - return true; - } - } - } - } - return false; -} - diff --git a/src/ast/simplifier/inj_axiom.h b/src/ast/simplifier/inj_axiom.h deleted file mode 100644 index a6df16515..000000000 --- a/src/ast/simplifier/inj_axiom.h +++ /dev/null @@ -1,27 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - inj_axiom.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-06-23. - -Revision History: - ---*/ -#ifndef INJ_AXIOM_H_ -#define INJ_AXIOM_H_ - -#include "ast/ast.h" - -bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result); - -#endif /* INJ_AXIOM_H_ */ - diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 41890dd05..b117db89b 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(smt arith_eq_adapter.cpp arith_eq_solver.cpp asserted_formulas.cpp + asserted_formulas_new.cpp cached_var_subst.cpp cost_evaluator.cpp dyn_ack.cpp diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 6f1c4cfcc..8b25e9263 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -24,6 +24,7 @@ Revision History: #include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/pull_ite_tree.h" #include "ast/rewriter/push_app_ite.h" +#include "ast/rewriter/inj_axiom.h" #include "ast/simplifier/arith_simplifier_plugin.h" #include "ast/simplifier/array_simplifier_plugin.h" #include "ast/simplifier/datatype_simplifier_plugin.h" @@ -31,7 +32,6 @@ Revision History: #include "ast/simplifier/seq_simplifier_plugin.h" #include "ast/simplifier/bv_simplifier_plugin.h" #include "ast/simplifier/bv_elim.h" -#include "ast/simplifier/inj_axiom.h" #include "ast/simplifier/elim_bounds.h" #include "ast/simplifier/bit2int.h" #include "ast/normal_forms/pull_quant.h" diff --git a/src/smt/elim_term_ite.cpp b/src/smt/elim_term_ite.cpp index b750e6bf5..d9cfac775 100644 --- a/src/smt/elim_term_ite.cpp +++ b/src/smt/elim_term_ite.cpp @@ -157,4 +157,22 @@ void elim_term_ite::reduce1_quantifier(quantifier * q) { } +br_status elim_term_ite_cfg::reduce_app(func_decl* f, unsigned n, expr * const* args, expr_ref& result, proof_ref& result_pr) { + if (!m.is_term_ite(f)) { + return BR_FAILED; + } + + expr_ref new_def(m); + proof_ref new_def_pr(m); + app_ref r(m.mk_app(f, n, args), m); + app_ref new_r(m); + if (!m_defined_names.mk_name(r, new_def, new_def_pr, new_r, result_pr)) { + return BR_FAILED; + } + result = new_r; + + CTRACE("elim_term_ite_bug", new_def.get() == 0, tout << mk_ismt2_pp(r, m) << "\n";); + m_new_defs.push_back(justified_expr(m, new_def, new_def_pr)); + return BR_DONE; +} diff --git a/src/smt/elim_term_ite.h b/src/smt/elim_term_ite.h index 2b9c66a64..94e5e0346 100644 --- a/src/smt/elim_term_ite.h +++ b/src/smt/elim_term_ite.h @@ -21,6 +21,7 @@ Revision History: #include "ast/simplifier/simplifier.h" #include "ast/normal_forms/defined_names.h" +#include "ast/rewriter/rewriter.h" class elim_term_ite : public simplifier { defined_names & m_defined_names; @@ -46,5 +47,32 @@ public: ); }; + + +class elim_term_ite_cfg : public default_rewriter_cfg { + ast_manager& m; + defined_names & m_defined_names; + vector m_new_defs; +public: + elim_term_ite_cfg(ast_manager & m, defined_names & d): m(m), m_defined_names(d) { + // TBD enable_ac_support(false); + } + virtual ~elim_term_ite_cfg() {} + vector const& new_defs() const { return m_new_defs; } + br_status reduce_app(func_decl* f, unsigned n, expr *const* args, expr_ref& result, proof_ref& result_pr); +}; + +class elim_term_ite_rw : public rewriter_tpl { + elim_term_ite_cfg m_cfg; +public: + elim_term_ite_rw(ast_manager& m, defined_names & dn): + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, dn) + {} + vector const& new_defs() const { return m_cfg.new_defs(); } +}; + + + #endif /* ELIM_TERM_ITE_H_ */