mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

Revert "Eliminated the dependency of the macro-finder on the simplifier."

Browse source 
This reverts commit 8310b24c52.
This commit is contained in:
Christoph M. Wintersteiger 2017-08-24 21:26:09 +01:00
parent 8310b24c52
commit 799fb4a0d1
8 changed files with 139 additions and 168 deletions
Download patch file Download diff file Expand all files Collapse all files

43
src/ast/macros/macro_finder.cpp
View file

@ -21,9 +21,8 @@ Revision History:
#include "ast/occurs.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/rewriter/arith_rewriter.h"
bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) const {
bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
return false;
TRACE("macro_finder", tout << "processing: " << mk_pp(n, m_manager) << "\n";);
@ -33,30 +32,30 @@ bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) const {
}
/**
\brief Detect macros of the form
\brief Detect macros of the form
1- (forall (X) (= (+ (f X) (R X)) c))
2- (forall (X) (<= (+ (f X) (R X)) c))
3- (forall (X) (>= (+ (f X) (R X)) c))
The second and third cases are first converted into
(forall (X) (= (f X) (+ c (* -1 (R x)) (k X))))
and
and
(forall (X) (<= (k X) 0)) when case 2
(forall (X) (>= (k X) 0)) when case 3
For case 2 & 3, the new quantifiers are stored in new_exprs and new_prs.
*/
bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) const {
bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
return false;
arith_rewriter & arw = m_util.get_arith_rw();
arith_util & au = m_util.get_arith_util();
arith_simplifier_plugin * as = get_arith_simp();
arith_util & autil = as->get_arith_util();
expr * body = to_quantifier(n)->get_expr();
unsigned num_decls = to_quantifier(n)->get_num_decls();
if (!au.is_le(body) && !au.is_ge(body) && !m_manager.is_eq(body))
if (!autil.is_le(body) && !autil.is_ge(body) && !m_manager.is_eq(body))
return false;
if (!au.is_add(to_app(body)->get_arg(0)))
if (!as->is_add(to_app(body)->get_arg(0)))
return false;
app_ref head(m_manager);
expr_ref def(m_manager);
@ -64,15 +63,15 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
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 (au.is_le(body))
new_body = au.mk_ge(head, def);
else if (as->is_le(body))
new_body = autil.mk_ge(head, def);
else
new_body = au.mk_le(head, def);
new_body = autil.mk_le(head, def);
quantifier_ref new_q(m_manager);
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()) {
@ -83,16 +82,16 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
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_manager);
arw.mk_add(def, k_app, new_rhs2);
as->mk_add(def, k_app, new_rhs2);
expr * body1 = m_manager.mk_eq(head, new_rhs2);
expr * body2 = m_manager.mk_app(new_body->get_decl(), k_app, au.mk_numeral(0, m_manager.get_sort(def)));
expr * body2 = m_manager.mk_app(new_body->get_decl(), k_app, as->mk_numeral(rational(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);
@ -119,7 +118,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
n is of the form: (forall (X) (iff (= (f X) t) def[X]))
Convert it into:
(forall (X) (= (f X) (ite def[X] t (k X))))
(forall (X) (not (= (k X) t)))
@ -127,13 +126,13 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
The new quantifiers and proofs are stored in new_exprs and new_prs
*/
static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr,
static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr,
expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
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_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);
expr * pats[1] = { m.mk_pattern(k_app) };
@ -184,7 +183,7 @@ bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * con
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)) {
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_exprs, new_prs);
found_new_macro = true;