mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Fixed binding substitution in macro_util

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-08-20 17:56:52 -04:00
parent 879f792125
commit 47e95f8676
1 changed files with 17 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -458,28 +458,32 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
expr_ref_buffer var_mapping(m_manager); expr_ref_buffer var_mapping(m_manager);
bool changed = false; bool changed = false;
unsigned num_args = head->get_num_args(); unsigned num_args = head->get_num_args();
unsigned max = num_args; unsigned max_var_idx = 0;
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
var * v = to_var(head->get_arg(i)); var const * v = to_var(head->get_arg(i));
if (v->get_idx() >= max) if (v->get_idx() > max_var_idx)
max = v->get_idx() + 1; max_var_idx = v->get_idx();
} }
TRACE("normalize_expr_bug", TRACE("normalize_expr_bug",
tout << "head: " << mk_pp(head, m_manager) << "\n"; tout << "head: " << mk_pp(head, m_manager) << "\n";
tout << "applying substitution to:\n" << mk_bounded_pp(t, m_manager) << "\n";); tout << "applying substitution to:\n" << mk_bounded_pp(t, m_manager) << "\n";);
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
var * v = to_var(head->get_arg(i)); var * v = to_var(head->get_arg(i));
if (v->get_idx() != i) { if (v->get_idx() != i) {
changed = true; changed = true;
var * new_var = m_manager.mk_var(i, v->get_sort()); var_ref new_var(m_manager.mk_var(i, v->get_sort()), m_manager);
CTRACE("normalize_expr_bug", v->get_idx() >= num_args, tout << mk_pp(v, m_manager) << ", num_args: " << num_args << "\n";); var_mapping.setx(max_var_idx - v->get_idx(), new_var);
SASSERT(v->get_idx() < max);
var_mapping.setx(max - v->get_idx() - 1, new_var);
}
else {
var_mapping.setx(max - i - 1, v);
} }
else
var_mapping.setx(max_var_idx - i, 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) { if (changed) {
// REMARK: t may have nested quantifiers... So, I must use the std order for variable substitution. // REMARK: t may have nested quantifiers... So, I must use the std order for variable substitution.
var_subst subst(m_manager, true); var_subst subst(m_manager, true);
@ -488,7 +492,7 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitution:\n"; tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitution:\n";
for (unsigned i = 0; i < var_mapping.size(); i++) { for (unsigned i = 0; i < var_mapping.size(); i++) {
if (var_mapping[i] != 0) if (var_mapping[i] != 0)
tout << "#" << i << " -> " << mk_pp(var_mapping[i], m_manager) << "\n"; tout << "#" << i << " -> " << mk_ll_pp(var_mapping[i], m_manager);
}); });
subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t); subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t);
} }