mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 15:15:35 +00:00
Code Activity

Merge branch 'Z3Prover:master' into master

Browse source
This commit is contained in:
Adriteyo Das 2026-05-12 09:14:06 +05:30 • committed by GitHub
commit 759ab463b9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 948 additions and 314 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/params/smt_parallel_params.pyg
View file

@ -4,6 +4,9 @@ def_module_params('smt_parallel',
params=(
('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'),
('sls', BOOL, False, 'add sls-tactic as a separate worker thread outside the search tree parallelism'),
('failed_literal_backbones', BOOL, False, 'use failed literal backbone test'),
('num_global_bb_threads', UINT, 0, 'default is 0 (off), can configure to 1 (negative mode only) or 2 (negative and positive mode) separate worker thread(s) outside the search tree parallelism'),
))
('num_global_bb_fl_threads', UINT, 0, 'run failed-literal backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'),
('num_global_bb_batch_threads', UINT, 0, 'run Janota-style chunking backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'),
('local_backbones', BOOL, False, 'enable local backbones experiment within the search tree parallelism'),
('core_minimize', BOOL, True, 'minimize unsat cores used for parallel cube backtracking'),
('ablate_backtracking', BOOL, False, 'ablation: pass entire cube as core instead of unsat core during backtracking'),
))

1097
src/smt/smt_parallel.cpp
View file

File diff suppressed because it is too large Load diff

121
src/smt/smt_parallel.h
View file

@ -21,6 +21,7 @@ Revision History:
#include "smt/smt_context.h"
#include "util/search_tree.h"
#include "ast/sls/sls_smt_solver.h"
#include <atomic>
#include <thread>
#include <mutex>
#include <condition_variable>
@ -36,6 +37,8 @@ namespace smt {
class parallel {
context& ctx;
class core_minimizer_worker;
using node = search_tree::node<cube_config>;
struct shared_clause {
unsigned source_worker_id;
@ -52,11 +55,7 @@ namespace smt {
using bb_candidates = vector<bb_candidate>;
struct node_lease {
search_tree::node<cube_config>* node = nullptr;
// Version counter for structural mutations of this node (e.g., split/close).
// Used to detect stale leases: if a worker's lease.epoch != node.epoch,
// the node has changed since it was acquired and must not be mutated.
unsigned epoch = 0;
node* leased_node = nullptr;
// Cancellation generation counter for this node/subtree.
// Incremented when the node is closed; used to signal that all
@ -82,13 +81,22 @@ namespace smt {
struct stats {
unsigned m_max_cube_depth = 0;
unsigned m_num_cubes = 0;
unsigned m_backbones_found = 0;
unsigned m_core_min_jobs_enqueued = 0;
unsigned m_core_min_jobs_published = 0;
unsigned m_core_min_jobs_skipped = 0;
unsigned m_core_min_global_unsat = 0;
};
struct core_min_job {
node* source = nullptr;
expr_ref_vector core;
core_min_job(ast_manager& m, node* source) : source(source), core(m) {}
};
ast_manager& m;
parallel& p;
std::mutex mux;
state m_state = state::is_running;
stats m_stats;
using node = search_tree::node<cube_config>;
search_tree::tree<cube_config> m_search_tree;
vector<node_lease> m_worker_leases;
@ -100,7 +108,8 @@ namespace smt {
bb_candidates m_bb_candidates;
unsigned m_max_global_bb_candidates = 100;
unsigned m_bb_batch_size = 150;
expr_ref_vector m_global_backbones;
obj_hashtable<expr> m_global_backbones;
std::atomic<unsigned> m_bb_candidate_epoch = 0;
// Backbone job queue
std::condition_variable m_bb_cv;
@ -110,6 +119,12 @@ namespace smt {
unsigned_vector m_bb_last_batch_processed;
unsigned m_bb_cancel_epoch = 0; // When a backbone worker finishes early, it increments m_bb_cancel_epoch and notifies all
// Core minimization job queue
std::condition_variable m_core_min_cv;
scoped_ptr_vector<core_min_job> m_core_min_jobs;
bool m_ablate_backtracking = false;
// called from batch manager to cancel other workers if we've reached a verdict
void cancel_workers() {
IF_VERBOSE(1, verbose_stream() << "Canceling workers\n");
@ -137,22 +152,36 @@ namespace smt {
cancel_backbones_worker();
m_bb_cv.notify_all();
}
if (p.m_core_minimizer_worker) {
p.m_core_minimizer_worker->cancel();
m_core_min_cv.notify_all();
}
}
// to avoid deadlock
bool is_global_backbone_unlocked(ast_translation& l2g, expr* bb_cand) {
expr_ref cand(l2g(bb_cand), l2g.to());
return any_of(m_global_backbones, [&](expr *bb) { return bb == cand.get(); });
return m_global_backbones.contains(cand.get());
}
bool is_global_backbone_or_negation_unlocked(ast_translation& l2g, expr* bb_cand) {
expr_ref cand(l2g(bb_cand), l2g.to());
expr_ref neg_cand(mk_not(l2g.to(), cand), l2g.to());
return m_global_backbones.contains(cand.get()) || m_global_backbones.contains(neg_cand.get());
}
void backtrack_unlocked(ast_translation& l2g, unsigned worker_id, expr_ref_vector const& core,
node_lease const* lease = nullptr, vector<node_lease> const* targets = nullptr);
void collect_clause_unlocked(ast_translation &l2g, unsigned source_worker_id, expr *clause);
void release_lease_unlocked(unsigned worker_id, node* n, unsigned epoch);
void release_lease_unlocked(unsigned worker_id, node* n);
void cancel_closed_leases_unlocked(unsigned source_worker_id);
void collect_matching_targets_unlocked(node* source, expr* lit, vector<cube_config::literal> const& core,
vector<node_lease>& targets);
node* find_core_source_unlocked(ast_translation& l2g, node* source, expr_ref_vector const& core);
unsigned select_best_core_min_job_unlocked() const;
public:
batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_search_tree(expr_ref(m)), m_global_backbones(m) { }
batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_search_tree(expr_ref(m)) { }
void initialize(unsigned num_global_bb_threads, unsigned initial_max_thread_conflicts = 1000); // TODO: pass in from worker config
@ -163,12 +192,30 @@ namespace smt {
void collect_statistics(::statistics& st) const;
void collect_backbone_candidates(ast_translation& l2g, bb_candidates& bb_candidates);
bool collect_global_backbone(ast_translation& l2g, expr_ref const& backbone);
void collect_backbone_evidence(ast_translation& l2g, expr* lit, double delta);
bool collect_global_backbone(ast_translation& l2g, expr_ref const& backbone, unsigned source_worker_id = UINT_MAX);
bool wait_for_backbone_job(unsigned bb_thread_id, ast_translation& g2l, vector<parallel::bb_candidate>& out, reslimit& lim);
bb_candidates return_global_bb_candidates(ast_translation& g2l);
bool has_new_backbone_candidates(unsigned epoch) {
return m_bb_candidate_epoch.load(std::memory_order_acquire) != epoch;
}
unsigned get_bb_candidate_epoch() const {
return m_bb_candidate_epoch.load(std::memory_order_acquire);
}
expr_ref_vector get_global_backbones_snapshot(ast_translation& g2l) {
std::scoped_lock lock(mux);
expr_ref_vector snapshot(g2l.to());
for (expr* gb : m_global_backbones)
snapshot.push_back(g2l(gb));
return snapshot;
}
bool get_cube(ast_translation& g2l, unsigned id, expr_ref_vector& cube, bool is_first_run, node_lease& lease);
void backtrack(ast_translation& l2g, unsigned worker_id, expr_ref_vector const& core, node_lease const& lease);
void enqueue_core_minimization(ast_translation& l2g, node* source, expr_ref_vector const& core);
bool wait_for_core_min_job(ast_translation& g2l, node*& source,
expr_ref_vector& core, reslimit& lim);
void publish_minimized_core(ast_translation& l2g, expr_ref_vector const& asms, node* source,
unsigned original_core_size, expr_ref_vector const& minimized_core);
void try_split(ast_translation& l2g, unsigned worker_id, node_lease const& lease, expr* atom, unsigned effort);
void release_lease(unsigned worker_id, node_lease const& lease);
bool lease_canceled(node_lease const& lease);
@ -178,9 +225,9 @@ namespace smt {
lbool get_result() const;
bool is_global_backbone(ast_translation& l2g, expr* bb_cand) {
bool is_global_backbone_or_negation(ast_translation& l2g, expr* bb_cand) {
std::scoped_lock lock(mux);
return is_global_backbone_unlocked(l2g, bb_cand);
return is_global_backbone_or_negation_unlocked(l2g, bb_cand);
}
void cancel_current_backbone_batch() {
@ -207,14 +254,15 @@ namespace smt {
double m_max_conflict_mul = 1.5;
bool m_inprocessing = false;
bool m_global_backbones = false;
bool m_local_backbones = false;
bool m_sls = false;
unsigned m_inprocessing_delay = 1;
unsigned m_max_cube_depth = 20;
unsigned m_max_conflicts = UINT_MAX;
bool m_core_minimize = false;
bool m_ablate_backtracking = false;
};
using node = search_tree::node<cube_config>;
unsigned id; // unique identifier for the worker
parallel& p;
batch_manager& b;
@ -279,13 +327,42 @@ namespace smt {
}
};
class core_minimizer_worker {
batch_manager &b;
ast_manager m;
expr_ref_vector asms;
smt_params m_smt_params;
scoped_ptr<context> ctx;
ast_translation m_g2l, m_l2g;
unsigned m_num_core_minimize_calls = 0;
unsigned m_num_core_minimize_undef = 0;
unsigned m_num_core_minimize_refined = 0;
unsigned m_num_core_minimize_lits_removed = 0;
unsigned m_num_core_minimize_found_sat = 0;
unsigned m_core_minimize_conflict_budget = 5000;
unsigned m_shared_clause_limit = 0;
void minimize_unsat_core(expr_ref_vector& core);
void collect_shared_clauses();
public:
core_minimizer_worker(parallel& p, expr_ref_vector const& _asms);
void run();
void cancel();
void collect_statistics(::statistics& st) const;
reslimit& limit() { return m.limit(); }
};
class backbones_worker {
struct stats {
unsigned m_batches_total = 0;
unsigned m_candidates_total = 0;
unsigned m_singleton_backbones = 0;
unsigned m_backbones_detected = 0;
unsigned m_backbones_found = 0;
unsigned m_internal_backbones_found = 0;
unsigned m_retry_backbones_found = 0;
unsigned m_bb_retries = 0;
unsigned m_fallback_singleton_checks = 0;
unsigned m_fallback_reason_chunk_exhausted = 0;
unsigned m_fallback_reason_undef = 0;
@ -308,16 +385,17 @@ namespace smt {
ast_translation m_g2l, m_l2g;
unsigned m_bb_chunk_size = 20;
unsigned m_bb_conflicts_per_chunk = 1000;
uint_set m_known_units;
bool m_use_failed_literal_test;
stats m_stats;
bb_mode m_mode;
unsigned m_num_global_bb_threads = 1; // used to toggle behavior when testing bb candidates
unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share
bool check_backbone(expr* bb_candidate);
unsigned m_shared_units_prefix = 0;
unsigned m_num_initial_atoms = 0;
bool try_get_unit_backbone(expr* candidate, expr_ref& backbone);
void run_batch_mode();
void run_failed_literal_mode();
lbool check_sat(expr_ref_vector const &asms);
lbool probe_literal(bool_var v, uint_set& units, expr *e);
lbool probe_literal(bool_var v, expr *e, bool is_retry);
public:
backbones_worker(unsigned id, parallel &p, expr_ref_vector const &_asms);
void cancel();
@ -330,6 +408,7 @@ namespace smt {
batch_manager m_batch_manager;
scoped_ptr_vector<worker> m_workers;
scoped_ptr<sls_worker> m_sls_worker;
scoped_ptr<core_minimizer_worker> m_core_minimizer_worker;
scoped_ptr_vector<backbones_worker> m_global_backbones_workers;
public:

2
src/tactic/smtlogics/qflia_tactic.cpp
View file

@ -204,7 +204,7 @@ tactic * mk_preamble_tactic(ast_manager& m) {
using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
using_params(mk_simplify_tactic(m), pull_ite_p),
mk_solve_eqs_tactic(m),
mk_lia2card_tactic(m, lia2card_p),
using_params(mk_lia2card_tactic(m), lia2card_p),
mk_elim_uncnstr_tactic(m));
}

33
src/util/search_tree.h
View file

@ -50,7 +50,6 @@ namespace search_tree {
unsigned m_effort_spent = 0;
unsigned m_round_max_effort = 0;
unsigned m_active_workers = 0;
unsigned m_epoch = 0;
unsigned m_cancel_epoch = 0;
public:
@ -78,7 +77,6 @@ namespace search_tree {
SASSERT(!m_right);
m_left = alloc(node<Config>, a, this);
m_right = alloc(node<Config>, b, this);
inc_epoch();
}
node* left() const { return m_left; }
@ -150,12 +148,6 @@ namespace search_tree {
m_round_max_effort = effort;
m_effort_spent += m_round_max_effort;
}
unsigned epoch() const {
return m_epoch;
}
void inc_epoch() {
++m_epoch;
}
unsigned get_cancel_epoch() const {
return m_cancel_epoch;
}
@ -242,7 +234,7 @@ namespace search_tree {
count_active_nodes(cur->right());
}
// Find the shallowest leaf node that at least 1 worker has visited
// Find the depth of the shallowest leaf node that at least 1 worker has timed out on
// Used for tree expansion policy
void find_shallowest_timed_out_leaf_depth(node<Config>* cur, unsigned& best_depth) const {
if (!cur || cur->get_status() == status::closed)
@ -255,8 +247,8 @@ namespace search_tree {
find_shallowest_timed_out_leaf_depth(cur->right(), best_depth);
}
bool should_split(node<Config>* n, unsigned epoch) {
if (!is_lease_valid(n, epoch) || !n->is_leaf())
bool should_split(node<Config>* n) {
if (!n || n->get_status() != status::active || !n->is_leaf())
return false;
unsigned num_active_nodes = count_active_nodes(m_root.get());
@ -348,7 +340,6 @@ namespace search_tree {
void close(node<Config> *n, vector<literal> const &C) {
if (!n || n->get_status() == status::closed)
return;
n->inc_epoch();
n->inc_cancel_epoch();
n->set_status(status::closed);
n->set_core(C);
@ -373,8 +364,10 @@ namespace search_tree {
node<Config> *p = n->parent();
// The conflict does NOT depend on the decision literal at node n, so n’s split literal is irrelevant to this conflict
// thus the entire subtree under n is closed regardless of the split, so the conflict should be attached higher, at the nearest ancestor that does participate
// The conflict does NOT depend on the decision literal at node n, so n’s decision literal is irrelevant to this conflict
// thus the entire subtree under n is closed, so the conflict should be attached higher, at the nearest ancestor that does participate
// NOTE: I think this is dead code because the backtrack function already walks up to the nearest ancestor whose literal is in the conflict, which is the only place where this is called
// Keep for now since it does generalize this function to be used for arbitrary conflict attachment
if (p && all_of(C, [n](auto const &l) { return l != n->get_literal(); })) {
close_with_core(p, C);
return;
@ -451,7 +444,7 @@ namespace search_tree {
// On timeout, either expand the current leaf or reopen the node for a
// later revisit, depending on the tree-expansion heuristic.
bool try_split(node<Config> *n, unsigned epoch, unsigned cancel_epoch, literal const &a, literal const &b, unsigned effort) {
bool try_split(node<Config> *n, unsigned cancel_epoch, literal const &a, literal const &b, unsigned effort) {
if (is_lease_canceled(n, cancel_epoch))
return false;
@ -460,7 +453,7 @@ namespace search_tree {
n->update_round_max_effort(effort);
bool did_split = false;
if (should_split(n, epoch)) {
if (should_split(n)) {
n->split(a, b);
did_split = true;
}
@ -494,6 +487,8 @@ namespace search_tree {
// Walk upward to find the nearest ancestor whose decision participates in the conflict
while (n) {
// Does the UNSAT core contain the decision literal at node n?
// If yes, i.e. if the core contains n->literal, then the conflict depends on the decision made at node n.
if (any_of(conflict, [&](auto const &a) { return a == n->get_literal(); })) {
// close the subtree under n (preserves core attached to n), and attempt to resolve upwards
close_with_core(n, conflict);
@ -532,7 +527,6 @@ namespace search_tree {
find_nonclosed_nodes_with_literal_rec(m_root.get(), lit, out);
}
private:
void find_nonclosed_nodes_with_literal_rec(node<Config>* n, literal const& lit, ptr_vector<node<Config>>& out) {
if (!n)
return;
@ -544,17 +538,12 @@ namespace search_tree {
find_nonclosed_nodes_with_literal_rec(n->right(), lit, out);
}
public:
void dec_active_workers(node<Config>* n) {
if (!n)
return;
n->dec_active_workers();
}
bool is_lease_valid(node<Config>* n, unsigned epoch) const {
return n && n->get_status() == status::active && n->epoch() == epoch;
}
bool is_lease_canceled(node<Config>* n, unsigned cancel_epoch) const {
return !n || n->get_status() == status::closed || n->get_cancel_epoch() != cancel_epoch;
}