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

fix #3006

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-16 23:46:58 -10:00
parent d25db0d3e9
commit 8428970a1f
2 changed files with 21 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/array_rewriter.cpp
View file

@ -247,6 +247,7 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
// select(as-array[f], I) --> f(I)
func_decl * f = m_util.get_as_array_func_decl(to_app(args[0]));
result = m().mk_app(f, num_args - 1, args + 1);
TRACE("array", tout << mk_pp(args[0], m()) << " " << result << "\n";);
return BR_REWRITE1;
}

26
src/model/model_evaluator.cpp
View file

@ -164,7 +164,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
expr * val = m_model.get_const_interp(f);
if (val != nullptr) {
result = val;
return m_ar.is_as_array(val)? BR_REWRITE1 : BR_DONE;
st = m_ar.is_as_array(val)? BR_REWRITE1 : BR_DONE;
TRACE("model_evaluator", tout << result << "\n";);
return st;
}
else if (m_model_completion) {
sort * s = f->get_range();
@ -255,6 +257,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
result = ev(result);
m_pinned.push_back(result);
m_def_cache.insert(g, result);
TRACE("model_evaluator", tout << mk_pp(g, m) << " " << result << "\n";);
return BR_DONE;
}
}
@ -370,7 +373,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << "\n";);
TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << " "
<< mk_pp(a, m) << " " << mk_pp(b, m) << "\n";);
if (a == b) {
result = m.mk_true();
return BR_DONE;
@ -396,7 +400,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
conj.push_back(m.mk_eq(else1, else2));
}
if (args_are_unique1 && args_are_unique2 && !stores1.empty()) {
TRACE("model_evalator", tout << "argss are unique";);
TRACE("model_evaluator", tout << "args are unique " << conj << "\n";);
return mk_array_eq_core(stores1, else1, stores2, else2, conj, result);
}
@ -413,8 +417,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
result = mk_and(conj);
TRACE("model_evaluator", tout << mk_pp(a, m) << " == " << mk_pp(b, m) << " -> " << conj << "\n";
for (auto& s : stores1) tout << "store: " << s << "\n";
);
for (auto& s : stores1) tout << "store: " << s << "\n"; );
return BR_REWRITE_FULL;
}
return m_ar_rw.mk_eq_core(a, b, result);
@ -454,6 +457,13 @@ struct evaluator_cfg : public default_rewriter_cfg {
args_eq ae(arity);
args_table table1(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae);
args_table table2(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae);
TRACE("model_evaluator",
tout << "arity " << arity << "\n";
for (auto& v : stores1) tout << "stores1: " << v << "\n";
for (auto& v : stores2) tout << "stores2: " << v << "\n";
tout << "else1: " << mk_pp(else1, m) << "\n";
tout << "else2: " << mk_pp(else2, m) << "\n";
tout << "conj: " << conj << "\n";);
// stores with smaller index take precedence
for (unsigned i = stores1.size(); i-- > 0; ) {
@ -463,19 +473,23 @@ struct evaluator_cfg : public default_rewriter_cfg {
for (unsigned i = 0, sz = stores2.size(); i < sz; ++i) {
if (table2.contains(stores2[i].c_ptr())) {
// first insertion takes precedence.
TRACE("model_evaluator", tout << "duplicate " << stores2[i] << "\n";);
continue;
}
table2.insert(stores2[i].c_ptr());
expr * const* args = nullptr;
expr* val = stores2[i][arity];
if (table1.find(stores2[i].c_ptr(), args)) {
TRACE("model_evaluator", tout << "found value " << stores2[i] << "\n";);
table1.remove(args);
switch (compare(args[arity], val)) {
case l_true: table1.remove(args); break;
case l_true: break;
case l_false: result = m.mk_false(); return BR_DONE;
default: conj.push_back(m.mk_eq(val, args[arity])); break;
}
}
else {
TRACE("model_evaluator", tout << "not found value " << stores2[i] << "\n";);
switch (compare(else1, val)) {
case l_true: break;
case l_false: result = m.mk_false(); return BR_DONE;