mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-05 06:46:11 +00:00
Code Activity

catch exceptions from cube and backbone calls. They can throw

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-15 14:02:43 -06:00
parent 2b9b9a9623
commit 48ae786c4c
1 changed files with 29 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

46
src/solver/parallel_tactical2.cpp
View file

@ -1064,23 +1064,30 @@ class parallel_solver {
expr_ref_vector vars(m); expr_ref_vector vars(m);
obj_hashtable<expr> rejected_atoms; obj_hashtable<expr> rejected_atoms;
while (true) { while (true) {
expr_ref_vector cands = s->cube(vars, 10);
bool rejected = false; bool rejected = false;
for (expr* lit : cands) { try {
if (!lit) expr_ref_vector cands = s->cube(vars, 10);
continue; for (expr *lit : cands) {
if (m.is_true(lit) || m.is_false(lit)) if (!lit)
continue; continue;
if (b.path_contains_atom(m_l2g, lease, lit)) if (m.is_true(lit) || m.is_false(lit))
continue; continue;
if (m_config.m_global_backbones && b.is_global_backbone_or_negation(m_l2g, lit)) { if (b.path_contains_atom(m_l2g, lease, lit))
expr* atom = lit; continue;
m.is_not(lit, atom); if (m_config.m_global_backbones && b.is_global_backbone_or_negation(m_l2g, lit)) {
rejected_atoms.insert(atom); expr *atom = lit;
rejected = true; m.is_not(lit, atom);
continue; rejected_atoms.insert(atom);
rejected = true;
continue;
}
return expr_ref(lit, m);
} }
return expr_ref(lit, m); }
catch (...) {
if (!m.inc())
return expr_ref(nullptr, m);
throw;
} }
if (!rejected || vars.empty()) if (!rejected || vars.empty())
@ -1103,8 +1110,13 @@ class parallel_solver {
bb_candidates find_backbone_candidates(expr_ref_vector const& cube, unsigned k = 10) { bb_candidates find_backbone_candidates(expr_ref_vector const& cube, unsigned k = 10) {
bb_candidates result; bb_candidates result;
vector<solver::scored_literal> cands; vector<solver::scored_literal> cands;
s->get_backbone_candidates(cands, s->get_num_bool_vars()); try {
s->get_backbone_candidates(cands, s->get_num_bool_vars());
} catch (z3_exception &ex) {
if (!m.inc())
return result;
throw;
}
for (auto const& cand : cands) { for (auto const& cand : cands) {
expr* lit = cand.lit.get(); expr* lit = cand.lit.get();
if (m_config.m_global_backbones && if (m_config.m_global_backbones &&