mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-22 16:40:29 +00:00
Code Activity

fix param copy bug when setting conflicts, fix exception handling in the tactic, and fix some bugs with how we're chooseing split atoms in the cube function

Browse source
This commit is contained in:
Ilana Shapiro 2026-06-20 18:28:12 -07:00
parent f86feab060
commit 37f02a28f3
3 changed files with 45 additions and 54 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/smt_solver.cpp
View file

@ -435,7 +435,7 @@ namespace {
void solve_for(vector<solver::solution>& s) override { m_context.solve_for(s); }
expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) override {
expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override {
ast_manager& m = get_manager();
parallel_params pp(get_params());
if (!pp.cube_lookahead()) {
@ -477,8 +477,7 @@ namespace {
expr_ref_vector lits(m);
for (auto const &c : candidates) {
vars.push_back(c.e);
if (lits.size() < cutoff)
lits.push_back(c.e);
lits.push_back(c.e);
}
return lits;

91
src/solver/parallel_tactical2.cpp
View file

@ -107,7 +107,7 @@ static bool is_cancellation_exception(char const* msg) {
}
static void set_max_conflicts(solver_ref& s, unsigned max_conflicts) {
params_ref p;
params_ref p(s->get_params());
p.set_uint("max_conflicts", max_conflicts);
s->updt_params(p);
}
@ -1050,8 +1050,8 @@ class parallel_solver {
b.set_exception(ex.what());
}
catch (...) {
IF_VERBOSE(0, verbose_stream() << "Unknown exception in check_cube\n";);
throw;
if (!m.limit().is_canceled())
b.set_exception("unknown exception");
}
LOG_WORKER(1, " DONE checking cube " << r << "\n";);
return r;
@ -1108,53 +1108,32 @@ class parallel_solver {
}
expr_ref get_split_atom(node_lease const& lease, expr_ref_vector const& cube) {
expr_ref result(m);
if (cube.size() >= m_config.m_max_cube_depth)
return expr_ref(nullptr, m);
return result;
expr_ref_vector vars(m);
obj_hashtable<expr> rejected_atoms;
while (true) {
bool rejected = false;
try {
expr_ref_vector cands = s->cube(vars, 10);
for (expr *lit : cands) {
if (!lit)
continue;
if (m.is_true(lit) || m.is_false(lit))
continue;
if (b.path_contains_atom(m_l2g, lease, lit))
continue;
if (m_config.m_global_backbones && b.is_global_backbone_or_negation(m_l2g, lit)) {
expr *atom = lit;
m.is_not(lit, atom);
rejected_atoms.insert(atom);
rejected = true;
continue;
}
return expr_ref(lit, m);
}
expr_ref_vector placeholder_noop(m);
try {
expr_ref_vector cands = s->cube(placeholder_noop);
for (expr* lit : cands) {
if (!lit)
continue;
if (m.is_true(lit) || m.is_false(lit))
continue;
if (b.path_contains_atom(m_l2g, lease, lit))
continue;
if (m_config.m_global_backbones && b.is_global_backbone_or_negation(m_l2g, lit))
continue;
result = lit;
return result;
}
catch (...) {
if (m.limit().is_canceled())
return expr_ref(nullptr, m);
throw;
}
if (!rejected || vars.empty())
return expr_ref(nullptr, m);
expr_ref_vector next_vars(m);
for (expr* v : vars) {
expr* atom = v;
m.is_not(v, atom);
if (!rejected_atoms.contains(atom))
next_vars.push_back(v);
}
if (next_vars.empty() || next_vars.size() == vars.size())
return expr_ref(nullptr, m);
vars.reset();
vars.append(next_vars);
}
catch (...) {
if (!m.limit().is_canceled())
b.set_exception("unknown exception");
return result;
}
return result;
}
bb_candidates find_backbone_candidates(expr_ref_vector const& cube, unsigned k = 10) {
@ -1162,10 +1141,18 @@ class parallel_solver {
vector<solver::scored_literal> cands;
try {
s->get_backbone_candidates(cands, s->get_num_bool_vars());
} catch (z3_error& err) {
if (!m.limit().is_canceled())
b.set_exception(err.error_code());
return result;
} catch (z3_exception &ex) {
if (m.limit().is_canceled())
return result;
throw;
if (!m.limit().is_canceled() && !is_cancellation_exception(ex.what()))
b.set_exception(ex.what());
return result;
} catch (...) {
if (!m.limit().is_canceled())
b.set_exception("unknown exception");
return result;
}
for (auto const& cand : cands) {
expr* lit = cand.lit.get();
@ -2001,6 +1988,12 @@ public:
m_batch_manager.set_exception(ex.what());
else
m_batch_manager.set_canceled();
} catch (...) {
IF_VERBOSE(0, verbose_stream() << "Unknown exception in parallel solver\n");
if (!lim.is_canceled())
m_batch_manager.set_exception("unknown exception");
else
m_batch_manager.set_canceled();
}
};

3
src/solver/solver.h
View file

@ -255,7 +255,7 @@ public:
\brief extract a lookahead candidates for branching.
*/
virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) = 0;
virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level=0) = 0;
/**
\brief retrieve congruence closure root.
@ -353,4 +353,3 @@ typedef ref<solver> solver_ref;
inline std::ostream& operator<<(std::ostream& out, solver const& s) {
return s.display(out);
}