mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Propagate reason for undef as exception to improve error reporting in scenarios such as #5009

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-09 16:58:01 -08:00
parent 5c04b9eee2
commit 4c3c15c015
1 changed files with 19 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/solver/parallel_tactic.cpp
View file

@ -376,6 +376,7 @@ private:
unsigned m_last_depth; unsigned m_last_depth;
int m_exn_code; int m_exn_code;
std::string m_exn_msg; std::string m_exn_msg;
std::string m_reason_undef;
void init() { void init() {
parallel_params pp(m_params); parallel_params pp(m_params);
@ -452,7 +453,10 @@ private:
m_models.push_back(mdl.get()); m_models.push_back(mdl.get());
} }
else if (m_models.empty()) { else if (m_models.empty()) {
m_has_undef = true; if (!m_has_undef) {
m_has_undef = true;
m_reason_undef = "incomplete";
}
} }
if (!m_allsat) { if (!m_allsat) {
m_queue.shutdown(); m_queue.shutdown();
@ -475,8 +479,14 @@ private:
} }
} }
void report_undef(solver_state& s) { void report_undef(solver_state& s, std::string const& reason) {
m_has_undef = true; {
std::lock_guard<std::mutex> lock(m_mutex);
if (!m_has_undef) {
m_has_undef = true;
m_reason_undef = reason;
}
}
close_branch(s, l_undef); close_branch(s, l_undef);
} }
@ -512,7 +522,7 @@ private:
case l_false: report_unsat(s); return; case l_false: report_unsat(s); return;
} }
if (canceled(s)) return; if (canceled(s)) return;
if (s.giveup()) { report_undef(s); return; } if (s.giveup()) { report_undef(s, s.get_solver().reason_unknown()); return; }
if (memory_pressure()) { if (memory_pressure()) {
goto simplify_again; goto simplify_again;
@ -529,7 +539,7 @@ private:
expr_ref_vector c = s.get_solver().cube(vars, cutoff); expr_ref_vector c = s.get_solver().cube(vars, cutoff);
if (c.empty() || (cube.size() == 1 && m.is_true(c.back()))) { if (c.empty() || (cube.size() == 1 && m.is_true(c.back()))) {
if (num_simplifications > 1) { if (num_simplifications > 1) {
report_undef(s); report_undef(s, std::string("cube simplifications exceeded"));
return; return;
} }
goto simplify_again; goto simplify_again;
@ -777,9 +787,10 @@ public:
g->assert_expr(m.mk_false(), pr, lcore); g->assert_expr(m.mk_false(), pr, lcore);
break; break;
case l_undef: case l_undef:
if (!m.inc()) { if (!m.inc())
throw tactic_exception(Z3_CANCELED_MSG); throw tactic_exception(Z3_CANCELED_MSG);
} if (m_has_undef)
throw tactic_exception(m_reason_undef.c_str());
break; break;
} }
result.push_back(g.get()); result.push_back(g.get());
@ -816,6 +827,7 @@ public:
void reset_statistics() override { void reset_statistics() override {
m_stats.reset(); m_stats.reset();
} }
}; };