mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

check equalities with unknown evaluations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-20 11:27:52 -07:00
parent 419f99c329
commit 41c9e2b1a4
1 changed files with 15 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/muz/pdr/pdr_util.cpp
View file

@ -112,8 +112,8 @@ namespace pdr {
set_value(e, val);
}
else {
IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << "\n";);
TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << "\n";);
IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";);
TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";);
set_x(e);
}
}
@ -672,7 +672,19 @@ namespace pdr {
eval_array_eq(e, arg1, arg2);
}
else if (is_x(arg1) || is_x(arg2)) {
set_x(e);
expr_ref eq(m), vl(m);
eq = m.mk_eq(arg1, arg2);
m_model->eval(eq, vl);
if (m.is_true(vl)) {
set_bool(e, true);
}
else if (m.is_false(vl)) {
set_bool(e, false);
}
else {
TRACE("pdr", tout << "cannot evaluate: " << mk_pp(vl, m) << "\n";);
set_x(e);
}
}
else if (m.is_bool(arg1)) {
bool val = is_true(arg1) == is_true(arg2);