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

make sure split atoms are not already used on the path

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-13 17:01:09 -07:00
parent f2d5d6fecf
commit f2270d4654
3 changed files with 22 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -523,7 +523,8 @@ public:
for (sat::bool_var v : candidates) {
expr* e = bool_var2expr(v);
if (e) {
fmls.push_back(e);
if (fmls.size() < backtrack_level)
fmls.push_back(e);
vs.push_back(e);
}
}

3
src/smt/smt_solver.cpp
View file

@ -477,7 +477,8 @@ namespace {
expr_ref_vector lits(m);
for (auto const &c : candidates) {
vars.push_back(c.e);
lits.push_back(c.e);
if (lits.size() < cutoff)
lits.push_back(c.e);
}
return lits;

21
src/solver/parallel_tactical2.cpp
View file

@ -675,6 +675,19 @@ class parallel_solver {
}
}
bool path_contains_atom(ast_translation& l2g, node_lease const& lease, expr* atom) {
std::scoped_lock lock(mux);
if (!lease.leased_node)
return false;
if (m_state != state::is_running)
return false;
if (m_search_tree.is_lease_canceled(lease.leased_node, lease.cancel_epoch))
return false;
expr_ref _atom(l2g(atom), m);
return lease.leased_node->path_contains_atom(_atom);
}
void try_split(ast_translation& l2g, unsigned worker_id,
node_lease const& lease,
expr* atom, unsigned effort) {
@ -1038,20 +1051,22 @@ class parallel_solver {
m_shared_units_prefix = prefix_sz;
}
expr_ref get_split_atom(expr_ref_vector const& cube) {
expr_ref get_split_atom(node_lease const& lease, expr_ref_vector const& cube) {
if (cube.size() >= m_config.m_max_cube_depth)
return expr_ref(nullptr, m);
expr_ref_vector vars(m);
obj_hashtable<expr> rejected_atoms;
while (true) {
expr_ref_vector cands = s->cube(vars, 1);
expr_ref_vector cands = s->cube(vars, 10);
bool rejected = false;
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);
@ -1161,7 +1176,7 @@ class parallel_solver {
LOG_WORKER(1, " found undef cube\n");
if (m_config.m_max_cube_depth <= cube.size())
goto check_cube_start;
expr_ref atom = get_split_atom(cube);
expr_ref atom = get_split_atom(lease, cube);
if (atom) {
b.try_split(m_l2g, id, lease, atom.get(),
m_config.m_threads_max_conflicts);