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

Merge pull request #531 from seahorn/qearrays

Browse source 
extend model with the value of a fresh variable
This commit is contained in:
Nikolaj Bjorner 2016-03-23 16:54:16 -07:00
parent 96f113afee 4e7b6b6586
commit 8a4624e21f
1 changed files with 13 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/qe/qe_arrays.cpp
View file

@ -309,12 +309,19 @@ namespace qe {
expr_ref_vector args(m);
sort* range = get_array_range(m.get_sort(s));
for (unsigned i = 0; i < idxs.size(); ++i) {
app_ref var(m);
app_ref var(m), sel(m);
expr_ref val(m);
var = m.mk_fresh_const("value", range);
vars.push_back(var);
args.reset();
args.push_back(result);
args.push_back (s);
args.append(idxs[i].m_values.size(), idxs[i].m_vars);
sel = a.mk_select (args.size (), args.c_ptr ());
VERIFY (model.eval (sel, val));
model.register_decl (var->get_decl (), val);
args[0] = result;
args.push_back(var);
result = a.mk_store(args.size(), args.c_ptr());
}
@ -390,15 +397,15 @@ namespace qe {
}
lbool compare(expr* val1, expr* val2) {
if (val1 == val2) {
return l_true;
}
if (m.are_equal (val1, val2)) return l_true;
if (m.are_distinct (val1, val2)) return l_false;
if (is_uninterp(val1) ||
is_uninterp(val2)) {
// TBD chase definition of nested array.
return l_undef;
}
return l_true;
return l_undef;
}
};