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

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-26 01:33:19 -07:00
commit c03be16039
15 changed files with 487 additions and 438 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -25,89 +25,94 @@ Revision History:
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";);
TRACE("macro_finder", tout << "processing: " << mk_pp(n, m) << "\n";);
expr * body = to_quantifier(n)->get_expr();
unsigned num_decls = to_quantifier(n)->get_num_decls();
return m_util.is_simple_macro(body, num_decls, head, def);
}
/**
\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) {
bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_dependency * dep, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
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))
if (!m_autil.is_le(body) && !m_autil.is_ge(body) && !m.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);
app_ref head(m);
expr_ref def(m);
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);
app_ref new_body(m);
if (!inv || m.is_eq(body))
new_body = m.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);
quantifier_ref new_q(m);
new_q = m.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.proofs_enabled()) {
proof * rw = m.mk_rewrite(n, new_q);
new_pr = m.mk_modus_ponens(pr, rw);
}
if (m_manager.is_eq(body)) {
return m_macro_manager.insert(head->get_decl(), new_q, new_pr);
expr_dependency * new_dep = dep;
if (m.is_eq(body)) {
return m_macro_manager.insert(head->get_decl(), new_q, new_pr, new_dep);
}
// 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);
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());
expr_ref_buffer new_rhs_args(m);
expr_ref new_rhs2(m_autil.mk_add(def, k_app), m);
expr * body1 = m.mk_eq(head, new_rhs2);
expr * body2 = m.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0));
quantifier * q1 = m.update_quantifier(new_q, body1);
expr * patterns[1] = { m.mk_pattern(k_app) };
quantifier * q2 = m.update_quantifier(new_q, 1, patterns, body2);
new_exprs.push_back(q1);
new_exprs.push_back(q2);
if (m_manager.proofs_enabled()) {
if (m.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);
proof * pr1 = m_manager.mk_and_elim(mp, 0);
proof * pr2 = m_manager.mk_and_elim(mp, 1);
app * q1q2 = m.mk_and(q1,q2);
proof * rw = m.mk_oeq_rewrite(new_q, q1q2);
proof * mp = m.mk_modus_ponens(new_pr, rw);
proof * pr1 = m.mk_and_elim(mp, 0);
proof * pr2 = m.mk_and_elim(mp, 1);
new_prs.push_back(pr1);
new_prs.push_back(pr2);
}
if (dep) {
new_deps.push_back(new_dep);
new_deps.push_back(new_dep);
}
return true;
}
@ -117,62 +122,62 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, vector<justified_expr>&
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))
if (!m_autil.is_le(body) && !m_autil.is_ge(body) && !m.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);
app_ref head(m);
expr_ref def(m);
bool inv = false;
if (!m_util.is_arith_macro(body, num_decls, head, def, inv))
return false;
app_ref new_body(m_manager);
app_ref new_body(m);
if (!inv || m_manager.is_eq(body))
new_body = m_manager.mk_app(to_app(body)->get_decl(), head, def);
if (!inv || m.is_eq(body))
new_body = m.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);
quantifier_ref new_q(m);
new_q = m.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.proofs_enabled()) {
proof * rw = m.mk_rewrite(n, new_q);
new_pr = m.mk_modus_ponens(pr, rw);
}
if (m_manager.is_eq(body)) {
if (m.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);
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());
expr_ref_buffer new_rhs_args(m);
expr_ref new_rhs2(m_autil.mk_add(def, k_app), m);
expr * body1 = m.mk_eq(head, new_rhs2);
expr * body2 = m.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0));
quantifier * q1 = m.update_quantifier(new_q, body1);
expr * patterns[1] = { m.mk_pattern(k_app) };
quantifier * q2 = m.update_quantifier(new_q, 1, patterns, body2);
proof* pr1 = 0, *pr2 = 0;
if (m_manager.proofs_enabled()) {
if (m.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);
app * q1q2 = m.mk_and(q1,q2);
proof * rw = m.mk_oeq_rewrite(new_q, q1q2);
proof * mp = m.mk_modus_ponens(new_pr, rw);
pr1 = m.mk_and_elim(mp, 0);
pr2 = m.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));
new_fmls.push_back(justified_expr(m, q1, pr1));
new_fmls.push_back(justified_expr(m, q2, pr2));
return true;
}
@ -180,7 +185,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, vector<justified_expr>&
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)))
@ -188,13 +193,13 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, vector<justified_expr>&
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,
expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, expr_dependency * dep,
expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps ) {
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) };
@ -215,6 +220,8 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e
new_prs.push_back(pr1);
new_prs.push_back(pr2);
}
new_deps.push_back(dep);
new_deps.push_back(dep);
}
static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr,
@ -246,7 +253,7 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e
}
macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
m_manager(m),
m(m),
m_macro_manager(mm),
m_util(mm.get_util()),
m_autil(m) {
@ -255,57 +262,67 @@ macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
macro_finder::~macro_finder() {
}
bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
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 = exprs[i];
proof * pr = m_manager.proofs_enabled() ? prs[i] : 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)) {
proof * pr = m.proofs_enabled() ? prs[i] : 0;
expr_dependency * depi = deps != 0 ? deps[i] : 0;
expr_ref new_n(m), def(m);
proof_ref new_pr(m);
expr_dependency_ref new_dep(m);
m_macro_manager.expand_macros(n, pr, depi, new_n, new_pr, new_dep);
app_ref head(m), t(m);
if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr, new_dep)) {
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_exprs, new_prs)) {
else if (is_arith_macro(new_n, new_pr, new_dep, new_exprs, new_prs, new_deps)) {
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);
pseudo_predicate_macro2macro(m, head, t, def, to_quantifier(new_n), new_pr, new_dep, new_exprs, new_prs, new_deps);
found_new_macro = true;
}
else {
new_exprs.push_back(new_n);
if (m_manager.proofs_enabled())
if (m.proofs_enabled())
new_prs.push_back(new_pr);
if (deps != 0)
new_deps.push_back(new_dep);
}
}
return found_new_macro;
}
void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
TRACE("macro_finder", tout << "processing macros...\n";);
expr_ref_vector _new_exprs(m_manager);
proof_ref_vector _new_prs(m_manager);
if (expand_macros(num, exprs, prs, _new_exprs, _new_prs)) {
expr_ref_vector _new_exprs(m);
proof_ref_vector _new_prs(m);
expr_dependency_ref_vector _new_deps(m);
if (expand_macros(num, exprs, prs, deps, _new_exprs, _new_prs, _new_deps)) {
while (true) {
expr_ref_vector old_exprs(m_manager);
proof_ref_vector old_prs(m_manager);
expr_ref_vector old_exprs(m);
proof_ref_vector old_prs(m);
expr_dependency_ref_vector old_deps(m);
_new_exprs.swap(old_exprs);
_new_prs.swap(old_prs);
_new_deps.swap(old_deps);
SASSERT(_new_exprs.empty());
SASSERT(_new_prs.empty());
if (!expand_macros(old_exprs.size(), old_exprs.c_ptr(), old_prs.c_ptr(), _new_exprs, _new_prs))
SASSERT(_new_deps.empty());
if (!expand_macros(old_exprs.size(), old_exprs.c_ptr(), old_prs.c_ptr(), old_deps.c_ptr(),
_new_exprs, _new_prs, _new_deps))
break;
}
}
new_exprs.append(_new_exprs);
new_prs.append(_new_prs);
new_deps.append(_new_deps);
}
@ -316,11 +333,12 @@ bool macro_finder::expand_macros(unsigned num, justified_expr const * fmls, vect
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);
proof * pr = m.proofs_enabled() ? fmls[i].get_proof() : 0;
expr_ref new_n(m), def(m);
proof_ref new_pr(m);
expr_dependency_ref new_dep(m);
m_macro_manager.expand_macros(n, pr, 0, new_n, new_pr, new_dep);
app_ref head(m), t(m);
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;
@ -331,11 +349,11 @@ bool macro_finder::expand_macros(unsigned num, justified_expr const * fmls, vect
}
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);
pseudo_predicate_macro2macro(m, 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));
new_fmls.push_back(justified_expr(m, new_n, new_pr));
}
}
return found_new_macro;