mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 02:25:32 +00:00
Code Activity

(mev) bug fix in expanding array equalities

Browse source 
The stores were processed in the wrong order so that

  (store (store a x y) x u)

was reduced to

  (store a x y)

instead of

  (store a x u)
This commit is contained in:
Arie Gurfinkel 2017-06-21 20:54:22 -04:00
parent e62e563e2d
commit d5ca902bf6
1 changed files with 22 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/model/model_evaluator.cpp
View file

@ -213,7 +213,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
args.append(stores[i].size(), stores[i].c_ptr());
val = m_ar.mk_store(args.size(), args.c_ptr());
}
}
}
}
bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
@ -291,13 +291,13 @@ struct evaluator_cfg : public default_rewriter_cfg {
else {
conj.push_back(m().mk_eq(else1, else2));
}
args1.push_back(a);
args2.push_back(b);
if (args_are_unique1 && args_are_unique2 && !stores1.empty()) {
return mk_array_eq(stores1, else1, stores2, else2, conj, result);
return mk_array_eq_core(stores1, else1, stores2, else2, conj, result);
}
// TBD: this is too inefficient.
args1.push_back(a);
args2.push_back(b);
stores1.append(stores2);
for (unsigned i = 0; i < stores1.size(); ++i) {
args1.resize(1); args1.append(stores1[i].size() - 1, stores1[i].c_ptr());
@ -338,20 +338,22 @@ struct evaluator_cfg : public default_rewriter_cfg {
typedef hashtable<expr*const*, args_hash, args_eq> args_table;
br_status mk_array_eq(vector<expr_ref_vector> const& stores1, expr* else1,
vector<expr_ref_vector> const& stores2, expr* else2,
expr_ref_vector& conj, expr_ref& result) {
br_status mk_array_eq_core(vector<expr_ref_vector> const& stores1, expr* else1,
vector<expr_ref_vector> const& stores2, expr* else2,
expr_ref_vector& conj, expr_ref& result) {
unsigned arity = stores1[0].size()-1; // TBD: fix arity.
args_hash ah(arity);
args_eq ae(arity);
args_table table1(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae);
args_table table2(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae);
for (unsigned i = 0; i < stores1.size(); ++i) {
table1.insert(stores1[i].c_ptr());
}
for (unsigned i = stores2.size(); i > 0; ) {
// stores with smaller index take precedence
for (unsigned i = stores1.size(); i > 0; ) {
--i;
table1.insert(stores1[i].c_ptr());
}
for (unsigned i = 0, sz = stores2.size(); i < sz; ++i) {
if (table2.contains(stores2[i].c_ptr())) {
// first insertion takes precedence.
continue;
@ -361,7 +363,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
expr* val = stores2[i][arity];
if (table1.find(stores2[i].c_ptr(), args)) {
switch (compare(args[arity], val)) {
case l_true: table1.remove(stores2[i].c_ptr()); break;
case l_true: table1.remove(args); break;
case l_false: result = m().mk_false(); return BR_DONE;
default: conj.push_back(m().mk_eq(val, args[arity])); break;
}
@ -389,10 +391,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
lbool compare(expr* a, expr* b) {
if (m().are_equal(a, b)) return l_true;
if (m().are_distinct(a, b)) return l_false;
return l_undef;
return l_undef;
}
bool args_are_values(expr_ref_vector const& store, bool& are_unique) {
bool are_values = true;
for (unsigned j = 0; are_values && j + 1 < store.size(); ++j) {
@ -402,7 +404,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
SASSERT(!are_unique || are_values);
return are_values;
}
bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case, bool& are_unique) {
SASSERT(m_ar.is_array(a));
@ -417,14 +419,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
stores.push_back(store);
a = to_app(a)->get_arg(0);
}
if (m_ar.is_const(a)) {
else_case = to_app(a)->get_arg(0);
return true;
}
if (!m_ar.is_as_array(a)) {
TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";);
TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";);
return false;
}
@ -444,7 +446,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
}
stores.push_back(store);
}
}
else_case = g->get_else();
if (!else_case) {
TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n";
@ -524,7 +526,7 @@ unsigned model_evaluator::get_num_steps() const {
void model_evaluator::cleanup(params_ref const & p) {
model_core & md = m_imp->cfg().m_model;
dealloc(m_imp);
m_imp = alloc(imp, md, p);
m_imp = alloc(imp, md, p);
}
void model_evaluator::reset(params_ref const & p) {