mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

Bugfix for macro finder. Fixes #832.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-01-17 15:44:03 +00:00
parent 0fae048e3e
commit 6d34899c46
3 changed files with 42 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/ast/macros/macro_manager.cpp
View file

@ -106,7 +106,7 @@ bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) {
if (!m_deps.insert(f, s)) {
return false;
}
// add macro
m_decl2macro.insert(f, m);
m_decls.push_back(f);
@ -117,8 +117,8 @@ bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) {
}
TRACE("macro_insert", tout << "A macro was successfully created for: " << f->get_name() << "\n";);
// Nothing's forbidden anymore; if something's bad, we detected it earlier.
// Nothing's forbidden anymore; if something's bad, we detected it earlier.
// mark_forbidden(m->get_expr());
return true;
}
@ -144,7 +144,7 @@ namespace macro_manager_ns {
\brief Mark all func_decls used in exprs as forbidden.
*/
void macro_manager::mark_forbidden(unsigned n, expr * const * exprs) {
expr_mark visited;
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]);
@ -187,9 +187,9 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter
app * head;
expr * def;
get_head_def(q, f, head, def);
TRACE("macro_bug",
TRACE("macro_bug",
tout << f->get_name() << "\n" << mk_pp(head, m_manager) << "\n" << mk_pp(q, m_manager) << "\n";);
m_util.mk_macro_interpretation(head, def, interp);
m_util.mk_macro_interpretation(head, q->get_num_decls(), def, interp);
return f;
}
@ -237,7 +237,7 @@ void macro_manager::macro_expander::reduce1_quantifier(quantifier * q) {
erase_patterns = true;
}
for (unsigned i = 0; !erase_patterns && i < q->get_num_no_patterns(); i++) {
if (q->get_no_pattern(i) != new_q->get_no_pattern(i))
if (q->get_no_pattern(i) != new_q->get_no_pattern(i))
erase_patterns = true;
}
}
@ -254,7 +254,7 @@ bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref
return false;
app * n = to_app(_n);
quantifier * q = 0;
func_decl * d = n->get_decl();
func_decl * d = n->get_decl();
TRACE("macro_manager_bug", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
if (m_macro_manager.m_decl2macro.find(d, q)) {
TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n";);
@ -308,7 +308,7 @@ void macro_manager::expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref
if (r.get() == old_n.get())
return;
old_n = r;
old_pr = new_pr;
old_pr = new_pr;
}
}
else {

51
src/ast/macros/macro_util.cpp
View file

@ -405,7 +405,7 @@ bool macro_util::is_quasi_macro_head(expr * n, unsigned num_decls) const {
\brief Convert a quasi-macro head into a macro head, and store the conditions under
which it is valid in cond.
*/
void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned num_decls, app_ref & head, expr_ref & cond) const {
void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decls, app_ref & head, expr_ref & cond) const {
unsigned num_args = qhead->get_num_args();
sbuffer<bool> found_vars;
found_vars.resize(num_decls, false);
@ -431,6 +431,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned num_decls,
}
get_basic_simp()->mk_and(new_conds.size(), new_conds.c_ptr(), cond);
head = m_manager.mk_app(qhead->get_decl(), new_args.size(), new_args.c_ptr());
num_decls = next_var_idx;
}
/**
@ -440,10 +441,10 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned num_decls,
See normalize_expr
*/
void macro_util::mk_macro_interpretation(app * head, expr * def, expr_ref & interp) const {
void macro_util::mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const {
SASSERT(is_macro_head(head, head->get_num_args()));
SASSERT(!occurs(head->get_decl(), def));
normalize_expr(head, def, interp);
normalize_expr(head, num_decls, def, interp);
}
/**
@ -456,36 +457,27 @@ void macro_util::mk_macro_interpretation(app * head, expr * def, expr_ref & inte
f(x_1, x_2) --> f(x_0, x_1)
f(x_3, x_2) --> f(x_0, x_1)
*/
void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
expr_ref_buffer var_mapping(m_manager);
void macro_util::normalize_expr(app * head, unsigned num_decls, expr * t, expr_ref & norm_t) const {
expr_ref_buffer var_mapping(m_manager);
var_mapping.resize(num_decls);
bool changed = false;
unsigned num_args = head->get_num_args();
unsigned max_var_idx = 0;
for (unsigned i = 0; i < num_args; i++) {
var const * v = to_var(head->get_arg(i));
if (v->get_idx() > max_var_idx)
max_var_idx = v->get_idx();
}
TRACE("macro_util",
tout << "head: " << mk_pp(head, m_manager) << "\n";
tout << "applying substitution to:\n" << mk_bounded_pp(t, m_manager) << "\n";);
for (unsigned i = 0; i < num_args; i++) {
var * v = to_var(head->get_arg(i));
if (v->get_idx() != i) {
unsigned vi = v->get_idx();
SASSERT(vi < num_decls);
if (vi != i) {
changed = true;
var_ref new_var(m_manager.mk_var(i, v->get_sort()), m_manager);
var_mapping.setx(max_var_idx - v->get_idx(), new_var);
var_mapping.setx(num_decls - vi - 1, new_var);
}
else
var_mapping.setx(max_var_idx - i, v);
var_mapping.setx(num_decls - i - 1, v);
}
for (unsigned i = num_args; i <= max_var_idx; i++)
// CMW: Won't be used, but dictates a larger binding size,
// so that the indexes between here and in the rewriter match.
// It's possible that we don't see the true max idx of all vars here.
var_mapping.setx(max_var_idx - i, 0);
if (changed) {
// REMARK: t may have nested quantifiers... So, I must use the std order for variable substitution.
var_subst subst(m_manager, true);
@ -573,7 +565,7 @@ bool is_hint_atom(expr * lhs, expr * rhs) {
return !occurs(to_app(lhs)->get_decl(), rhs) && vars_of_is_subset(rhs, vars);
}
void hint_to_macro_head(ast_manager & m, app * head, unsigned num_decls, app_ref & new_head) {
void hint_to_macro_head(ast_manager & m, app * head, unsigned & num_decls, app_ref & new_head) {
unsigned num_args = head->get_num_args();
ptr_buffer<expr> new_args;
sbuffer<bool> found_vars;
@ -595,6 +587,7 @@ void hint_to_macro_head(ast_manager & m, app * head, unsigned num_decls, app_ref
new_args.push_back(new_var);
}
new_head = m.mk_app(head->get_decl(), new_args.size(), new_args.c_ptr());
num_decls = next_var_idx;
}
/**
@ -671,12 +664,12 @@ void macro_util::macro_candidates::insert(func_decl * f, expr * def, expr * cond
//
// -----------------------------
void macro_util::insert_macro(app * head, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r) {
void macro_util::insert_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r) {
expr_ref norm_def(m_manager);
expr_ref norm_cond(m_manager);
normalize_expr(head, def, norm_def);
normalize_expr(head, num_decls, def, norm_def);
if (cond != 0)
normalize_expr(head, cond, norm_cond);
normalize_expr(head, num_decls, cond, norm_cond);
else if (!hint)
norm_cond = m_manager.mk_true();
SASSERT(!hint || norm_cond.get() == 0);
@ -698,11 +691,14 @@ void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def,
}
else {
hint_to_macro_head(m_manager, head, num_decls, new_head);
TRACE("macro_util",
tout << "hint macro head: " << mk_ismt2_pp(new_head, m_manager) << std::endl;
tout << "hint macro def: " << mk_ismt2_pp(def, m_manager) << std::endl; );
}
insert_macro(new_head, def, new_cond, ineq, satisfy_atom, hint, r);
insert_macro(new_head, num_decls, def, new_cond, ineq, satisfy_atom, hint, r);
}
else {
insert_macro(head, def, cond, ineq, satisfy_atom, hint, r);
insert_macro(head, num_decls, def, cond, ineq, satisfy_atom, hint, r);
}
}
@ -879,6 +875,9 @@ void macro_util::collect_arith_macro_candidates(expr * atom, unsigned num_decls,
*/
void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls, macro_candidates & r) {
expr* lhs, *rhs;
TRACE("macro_util", tout << "Candidate check for: " << mk_ismt2_pp(atom, m_manager) << std::endl;);
if (m_manager.is_eq(atom, lhs, rhs) || m_manager.is_iff(atom, lhs, rhs)) {
if (is_quasi_macro_head(lhs, num_decls) &&
!is_forbidden(to_app(lhs)->get_decl()) &&

16
src/ast/macros/macro_util.h
View file

@ -74,9 +74,9 @@ private:
void collect_arith_macros(expr * n, unsigned num_decls, unsigned max_macros, bool allow_cond_macros,
macro_candidates & r);
void normalize_expr(app * head, expr * t, expr_ref & norm_t) const;
void insert_macro(app * head, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r);
void insert_quasi_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint,
void normalize_expr(app * head, unsigned num_decls, expr * t, expr_ref & norm_t) const;
void insert_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r);
void insert_quasi_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint,
macro_candidates & r);
expr * m_curr_clause; // auxiliary var used in collect_macro_candidates.
@ -105,7 +105,7 @@ public:
bool is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const;
bool is_right_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const;
bool is_simple_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref & def) const {
return is_left_simple_macro(n, num_decls, head, def) || is_right_simple_macro(n, num_decls, head, def);
return is_left_simple_macro(n, num_decls, head, def) || is_right_simple_macro(n, num_decls, head, def);
}
bool is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const;
@ -113,20 +113,20 @@ public:
bool inv;
return is_arith_macro(n, num_decls, head, def, inv);
}
bool is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t);
bool is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def);
bool is_quasi_macro_head(expr * n, unsigned num_decls) const;
void quasi_macro_head_to_macro_head(app * qhead, unsigned num_decls, app_ref & head, expr_ref & cond) const;
void quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decls, app_ref & head, expr_ref & cond) const;
void mk_macro_interpretation(app * head, expr * def, expr_ref & interp) const;
void mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const;
void collect_macro_candidates(expr * atom, unsigned num_decls, macro_candidates & r);
void collect_macro_candidates(quantifier * q, macro_candidates & r);
//
// Auxiliary goodness that allows us to manipulate BV and Arith polynomials.
// Auxiliary goodness that allows us to manipulate BV and Arith polynomials.
//
bool is_bv(expr * n) const;
bool is_bv_sort(sort * s) const;