mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

add verbose=1 log for mbp failure

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-02 18:03:56 -07:00
parent 7e1e64d027
commit 0bdb2f1691
2 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/qe/mbp/mbp_arith.cpp
View file

@ -215,6 +215,7 @@ namespace mbp {
linearize(mbo, eval, mul, t3, c, fmls, ts, tids); linearize(mbo, eval, mul, t3, c, fmls, ts, tids);
} }
else { else {
IF_VERBOSE(1, verbose_stream() << "mbp failed on if: " << mk_pp(t, m) << " := " << val << "\n");
throw default_exception("mbp evaluation didn't produce a truth value"); throw default_exception("mbp evaluation didn't produce a truth value");
} }
} }
@ -234,8 +235,10 @@ namespace mbp {
else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) { else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) {
rational r; rational r;
val = eval(t); val = eval(t);
if (!a.is_numeral(val, r)) if (!a.is_numeral(val, r)) {
IF_VERBOSE(1, verbose_stream() << "mbp failed on " << mk_pp(t, m) << " := " << val << "\n");
throw default_exception("mbp evaluation didn't produce an integer"); throw default_exception("mbp evaluation didn't produce an integer");
}
c += mul * r; c += mul * r;
rational c0(-r), mul0(1); rational c0(-r), mul0(1);
@ -335,8 +338,10 @@ namespace mbp {
expr_ref val = eval(v); expr_ref val = eval(v);
if (!m.inc()) if (!m.inc())
return false; return false;
if (!a.is_numeral(val, r)) if (!a.is_numeral(val, r)) {
IF_VERBOSE(1, verbose_stream() << "mbp failed on " << mk_pp(v, m) << " := " << val << "\n");
throw default_exception("evaluation did not produce a numeral"); throw default_exception("evaluation did not produce a numeral");
}
TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";); TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";);
tids.insert(v, mbo.add_var(r, a.is_int(v))); tids.insert(v, mbo.add_var(r, a.is_int(v)));
} }
@ -623,6 +628,7 @@ namespace mbp {
expr_ref val = eval(v); expr_ref val = eval(v);
if (!a.is_numeral(val, r)) { if (!a.is_numeral(val, r)) {
TRACE("qe", tout << eval.get_model() << "\n";); TRACE("qe", tout << eval.get_model() << "\n";);
IF_VERBOSE(1, verbose_stream() << "mbp failed on " << mk_pp(v, m) << " := " << val << "\n");
throw default_exception("mbp evaluation was only partial"); throw default_exception("mbp evaluation was only partial");
} }
id = mbo.add_var(r, a.is_int(v)); id = mbo.add_var(r, a.is_int(v));

4
src/qe/mbp/mbp_plugin.cpp
View file

@ -246,8 +246,10 @@ namespace mbp {
bool project_plugin::is_true(model_evaluator& eval, expr* e) { bool project_plugin::is_true(model_evaluator& eval, expr* e) {
expr_ref val = eval(e); expr_ref val = eval(e);
bool tt = m.is_true(val); bool tt = m.is_true(val);
if (!tt && !m.is_false(val) && contains_uninterpreted(val)) if (!tt && !m.is_false(val) && contains_uninterpreted(val)) {
IF_VERBOSE(1, verbose_stream() << "mbp failed on " << mk_pp(e, m) << " := " << val << "\n");
throw default_exception("could not evaluate Boolean in model"); throw default_exception("could not evaluate Boolean in model");
}
SASSERT(tt || m.is_false(val)); SASSERT(tt || m.is_false(val));
return tt; return tt;
} }