mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-08-23 11:44:48 -03:00
parent 0a09d5ff52 b03dc0af3b
commit b5c521e4b2
2 changed files with 24 additions and 16 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);
bool changed = false;
unsigned num_args = head->get_num_args();
unsigned max = num_args;
unsigned max_var_idx = 0;
for (unsigned i = 0; i < num_args; i++) {
var * v = to_var(head->get_arg(i));
if (v->get_idx() >= max)
max = v->get_idx() + 1;
var const * v = to_var(head->get_arg(i));
if (v->get_idx() > max_var_idx)
max_var_idx = v->get_idx();
}
TRACE("normalize_expr_bug",
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));
var * v = to_var(head->get_arg(i));
if (v->get_idx() != i) {
changed = true;
var * new_var = m_manager.mk_var(i, v->get_sort());
CTRACE("normalize_expr_bug", v->get_idx() >= num_args, tout << mk_pp(v, m_manager) << ", num_args: " << num_args << "\n";);
SASSERT(v->get_idx() < max);
var_mapping.setx(max - v->get_idx() - 1, new_var);
}
else {
var_mapping.setx(max - i - 1, v);
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);
}
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) {
// REMARK: t may have nested quantifiers... So, I must use the std order for variable substitution.
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";
for (unsigned i = 0; i < var_mapping.size(); i++) {
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);
}

10
src/parsers/smt/smtparser.cpp
View file

@ -1573,7 +1573,8 @@ private:
return false;
}
}
expr * p = m_manager.mk_pattern(ts.size(), (app*const*)(ts.c_ptr()));
expr_ref p(m_manager);
p = m_manager.mk_pattern(ts.size(), (app*const*)(ts.c_ptr()));
if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) {
set_error("invalid pattern", children[0]);
return false;
@ -1581,8 +1582,11 @@ private:
patterns.push_back(p);
}
else if (children[0]->string() == symbol("ex_act") && ts.size() == 1) {
app * sk_hack = m_manager.mk_app(m_sk_hack, 1, ts.c_ptr());
expr * p = m_manager.mk_pattern(1, &sk_hack);
app_ref sk_hack(m_manager);
sk_hack = m_manager.mk_app(m_sk_hack, 1, ts.c_ptr());
app * sk_hackp = sk_hack.get();
expr_ref p(m_manager);
p = m_manager.mk_pattern(1, &sk_hackp);
if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) {
set_error("invalid pattern", children[0]);
return false;