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

extend model with the value of a fresh variable

Browse source
This commit is contained in:
Arie Gurfinkel 2016-03-23 19:05:21 -04:00
parent 96f113afee
commit ee125b4fe3
1 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/qe/qe_arrays.cpp
View file

@ -309,12 +309,19 @@ namespace qe {
expr_ref_vector args(m); expr_ref_vector args(m);
sort* range = get_array_range(m.get_sort(s)); sort* range = get_array_range(m.get_sort(s));
for (unsigned i = 0; i < idxs.size(); ++i) { 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); var = m.mk_fresh_const("value", range);
vars.push_back(var); vars.push_back(var);
args.reset(); args.reset();
args.push_back(result);
args.push_back (s);
args.append(idxs[i].m_values.size(), idxs[i].m_vars); 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); args.push_back(var);
result = a.mk_store(args.size(), args.c_ptr()); result = a.mk_store(args.size(), args.c_ptr());
} }
@ -398,6 +405,7 @@ namespace qe {
// TBD chase definition of nested array. // TBD chase definition of nested array.
return l_undef; return l_undef;
} }
// AG: Shouldn't this be l_false
return l_true; return l_true;
} }
}; };