mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 13:06:05 +00:00
Code Activity

Parallel solving (#7769)

Browse source 
* very basic setup

* ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* respect smt configuration parameter in elim_unconstrained simplifier

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* indentation

* add bash files for test runs

* add option to selectively disable variable solving for only ground expressions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove verbose output

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #7745

axioms for len(substr(...)) escaped due to nested rewriting

* ensure atomic constraints are processed by arithmetic solver

* #7739 optimization

add simplification rule for at(x, offset) = ""

Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions.
The example highlights some opportunities for simplification, noteworthy at(..) = "".
The example is solved in both versions after adding this simplification.

* fix unsound len(substr) axiom

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* FreshConst is_sort (#7748)

* #7750

add pre-processing simplification

* Add parameter validation for selected API functions

* updates to ac-plugin

fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop.

* enable passive, add check for bloom up-to-date

* add top-k fixed-sized min-heap priority queue for top scoring literals

* set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still

* fix bug in parallel solving batch setup

* fix bug

* allow for internalize implies

* disable pre-processing during cubing

* debugging

* remove default constructor

* remove a bunch of string copies

* Update euf_ac_plugin.cpp

include reduction rules in forward simplification

* Update euf_completion.cpp

try out restricting scope of equalities added by instantation

* Update smt_parallel.cpp

Drop non-relevant units from shared structures.

* process cubes as lists of individual lits

* merge

* Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734)

* Initial plan

* Add datatype type definitions to types.ts (work in progress)

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Complete datatype type definitions with working TypeScript compilation

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Implement core datatype functionality with TypeScript compilation success

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Complete datatype implementation with full Context integration and tests

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* chipping away at the new code structure

* comments

* debug infinite recursion and split cubes on existing split atoms that aren't in the cube

* share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing

* merge

* resolve bad bug about l2g and g2l translators using wrong global context. add some debug prints

* initial attempt at dynamically switching from greedy to frugal splitting strategy in return_cubes. need to test. also there is some bug where the threads take forever to cancel?

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com>
Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Ilana Shapiro 2025-08-10 13:32:40 -07:00 • committed by GitHub
parent 4bb139435a
commit 2169364b6d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 136 additions and 83 deletions
Download patch file Download diff file Expand all files Collapse all files

180
src/smt/smt_parallel.cpp
View file

@ -41,8 +41,8 @@ namespace smt {
namespace smt { namespace smt {
void parallel::worker::run() { void parallel::worker::run() {
ast_translation g2l(ctx->m, m); ast_translation g2l(p.ctx.m, m); // global to local context -- MUST USE p.ctx.m, not ctx->m, AS GLOBAL MANAGER!!!
ast_translation l2g(m, ctx->m); ast_translation l2g(m, p.ctx.m); // local to global context
while (m.inc()) { while (m.inc()) {
vector<expr_ref_vector> cubes; vector<expr_ref_vector> cubes;
b.get_cubes(g2l, cubes); b.get_cubes(g2l, cubes);
@ -51,7 +51,7 @@ namespace smt {
for (auto& cube : cubes) { for (auto& cube : cubes) {
if (!m.inc()) { if (!m.inc()) {
b.set_exception("context cancelled"); b.set_exception("context cancelled");
return; // stop if the main context is cancelled return; // stop if the main context (i.e. parent thread) is cancelled
} }
switch (check_cube(cube)) { switch (check_cube(cube)) {
case l_undef: { case l_undef: {
@ -65,7 +65,7 @@ namespace smt {
break; break;
} }
case l_true: { case l_true: {
std::cout << "Worker " << id << " found sat cube: " << mk_and(cube) << "\n"; IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found sat cube: " << mk_and(cube) << "\n");
model_ref mdl; model_ref mdl;
ctx->get_model(mdl); ctx->get_model(mdl);
b.set_sat(l2g, *mdl); b.set_sat(l2g, *mdl);
@ -100,6 +100,7 @@ namespace smt {
ast_translation g2l(p.ctx.m, m); ast_translation g2l(p.ctx.m, m);
for (auto e : _asms) for (auto e : _asms)
asms.push_back(g2l(e)); asms.push_back(g2l(e));
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " created with " << asms.size() << " assumptions\n");
m_smt_params.m_preprocess = false; m_smt_params.m_preprocess = false;
ctx = alloc(context, m, m_smt_params, p.ctx.get_params()); ctx = alloc(context, m, m_smt_params, p.ctx.get_params());
context::copy(p.ctx, *ctx, true); context::copy(p.ctx, *ctx, true);
@ -154,7 +155,7 @@ namespace smt {
void parallel::batch_manager::share_lemma(ast_translation& l2g, expr* lemma) { void parallel::batch_manager::share_lemma(ast_translation& l2g, expr* lemma) {
std::scoped_lock lock(mux); std::scoped_lock lock(mux);
expr_ref g_lemma(l2g(lemma), l2g.to()); expr_ref g_lemma(l2g(lemma), l2g.to());
p.ctx.assert_expr(g_lemma); // QUESTION: where does this get shared with the local thread contexts? p.ctx.assert_expr(g_lemma); // QUESTION: where does this get shared with the local thread contexts? -- doesn't right now, we will build the scaffolding for this later!
} }
@ -242,10 +243,10 @@ namespace smt {
if (m.limit().is_canceled()) if (m.limit().is_canceled())
return l_undef; // the main context was cancelled, so we return undef. return l_undef; // the main context was cancelled, so we return undef.
switch (m_state) { switch (m_state) {
case state::is_running: case state::is_running: // batch manager is still running, but all threads have processed their cubes, which means all cubes were unsat
if (!m_cubes.empty()) if (!m_cubes.empty())
throw default_exception("inconsistent end state"); throw default_exception("inconsistent end state");
// TODO collect unsat core from assumptions, if any. // TODO collect unsat core from assumptions, if any. -- this is for the version where asms are passed in (currently, asms are empty)
return l_false; return l_false;
case state::is_unsat: case state::is_unsat:
return l_false; return l_false;
@ -257,46 +258,64 @@ namespace smt {
throw z3_error(m_exception_code); throw z3_error(m_exception_code);
default: default:
UNREACHABLE(); UNREACHABLE();
return l_undef;
} }
} }
// /*
// Batch manager maintains C_batch, A_batch. Batch manager maintains C_batch, A_batch.
// C_batch - set of cubes C_batch - set of cubes
// A_batch - set of split atoms. A_batch - set of split atoms.
// return_cubes is called with C_batch A_batch C A. return_cubes is called with C_batch A_batch C A.
// C_worker - one or more cubes C_worker - one or more cubes
// A_worker - split atoms form the worker thread. A_worker - split atoms form the worker thread.
//
// Assumption: A_worker does not occur in C_worker. Assumption: A_worker does not occur in C_worker.
//
// Greedy strategy: ------------------------------------------------------------------------------------------------------------------------------------------------------------
// Greedy strategy:
// return_cubes C_batch A_batch C_worker A_worker: For each returned cube c from the worker, you split it on all split atoms not in it (i.e., A_batch \ atoms(c)), plus any new atoms from A_worker.
// C_batch <- { cube * 2^(A_worker u (A_batch \ atoms(cube)) | cube in C_worker } u For each existing cube in the batch, you also split it on the new atoms from A_worker.
// { cube * 2^(A_worker \ A_batch) | cube in C_batch }
// = return_cubes C_batch A_batch C_worker A_worker:
// let C_batch' = C_batch u { cube * 2^(A_batch \ atoms(cube)) | cube in C_worker } C_batch <- { cube * 2^(A_worker u (A_batch \ atoms(cube)) | cube in C_worker } u
// { cube * 2^(A_worker \ A_batch) | cube in C_batch' } { cube * 2^(A_worker \ A_batch) | cube in C_batch }
// A_batch <- A_batch u A_worker =
// let C_batch' = C_batch u { cube * 2^(A_batch \ atoms(cube)) | cube in C_worker }
// Frugal strategy: in { cube * 2^(A_worker \ A_batch) | cube in C_batch' }
// A_batch <- A_batch u A_worker
// return_cubes C_batch A_batch [[]] A_worker:
// C_batch <- C_batch u 2^(A_worker u A_batch), ------------------------------------------------------------------------------------------------------------------------------------------------------------
// A_batch <- A_batch u A_worker Frugal strategy: only split on worker cubes
//
// return_cubes C_batch A_batch C_worker A_worker: case 1: thread returns no cubes, just atoms: just create 2^k cubes from all combinations of atoms so far.
// C_batch <- C_batch u { cube * 2^A_worker | cube in C_worker }. return_cubes C_batch A_batch [[]] A_worker:
// A_batch <- A_batch u A_worker C_batch <- C_batch u 2^(A_worker u A_batch),
// A_batch <- A_batch u A_worker
// Between Frugal and Greedy: (generalizes the first case of empty cube returned by worker)
// C_batch <- C_batch u { cube * 2^(A_worker u (A_batch \ atoms(cube)) | cube in C_worker } case 2: thread returns both cubes and atoms
// A_batch <- A_batch u A_worker Only the returned cubes get split by the newly discovered atoms (A_worker). Existing cubes are not touched.
// return_cubes C_batch A_batch C_worker A_worker:
// Or: use greedy strategy by a policy when C_batch, A_batch, A_worker are "small". C_batch <- C_batch u { cube * 2^A_worker | cube in C_worker }.
// A_batch <- A_batch u A_worker
void parallel::batch_manager::return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& cubes, expr_ref_vector const& a_worker) {
This means:
Only the returned cubes get split by the newly discovered atoms (A_worker).
Existing cubes are not touched.
------------------------------------------------------------------------------------------------------------------------------------------------------------
Hybrid: Between Frugal and Greedy: (generalizes the first case of empty cube returned by worker) -- don't focus on this approach
i.e. Expand only the returned cubes, but allow them to be split on both new and old atoms not already in them.
C_batch <- C_batch u { cube * 2^(A_worker u (A_batch \ atoms(cube)) | cube in C_worker }
A_batch <- A_batch u A_worker
------------------------------------------------------------------------------------------------------------------------------------------------------------
Final thought (do this!): use greedy strategy by a policy when C_batch, A_batch, A_worker are "small". -- want to do this. switch to frugal strategy after reaching size limit
*/
// currenly, the code just implements the greedy strategy
void parallel::batch_manager::return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& C_worker, expr_ref_vector const& A_worker) {
auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) { auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) {
return any_of(cube, [&](expr* e) { return e == atom || (m.is_not(e, e) && e == atom); }); return any_of(cube, [&](expr* e) { return e == atom || (m.is_not(e, e) && e == atom); });
}; };
@ -304,38 +323,69 @@ namespace smt {
auto add_split_atom = [&](expr* atom, unsigned start) { auto add_split_atom = [&](expr* atom, unsigned start) {
unsigned stop = m_cubes.size(); unsigned stop = m_cubes.size();
for (unsigned i = start; i < stop; ++i) { for (unsigned i = start; i < stop; ++i) {
m_cubes.push_back(m_cubes[i]); // push copy of m_cubes[i] m_cubes.push_back(m_cubes[i]);
m_cubes.back().push_back(m.mk_not(atom)); // add ¬atom to the copy m_cubes.back().push_back(m.mk_not(atom));
m_cubes[i].push_back(atom); // add atom to the original m_cubes[i].push_back(atom);
} }
}; };
std::scoped_lock lock(mux); std::scoped_lock lock(mux);
for (auto & c : cubes) { unsigned max_cubes = 1000;
bool greedy_mode = (m_cubes.size() <= max_cubes);
unsigned initial_m_cubes_size = m_cubes.size(); // cubes present before processing this batch
// --- Phase 1: Add worker cubes from C_worker and split each new cube on the existing atoms in A_batch (m_split_atoms) that aren't already in the new cube ---
for (auto& c : C_worker) {
expr_ref_vector g_cube(l2g.to()); expr_ref_vector g_cube(l2g.to());
for (auto& atom : c) { for (auto& atom : c)
g_cube.push_back(l2g(atom)); g_cube.push_back(l2g(atom));
}
unsigned start = m_cubes.size(); unsigned start = m_cubes.size();
m_cubes.push_back(g_cube); // base cube m_cubes.push_back(g_cube); // continuously update the start idx so we're just processing the single most recent cube
for (auto& atom : m_split_atoms) { if (greedy_mode) {
if (atom_in_cube(g_cube, atom)) // Split new cube all existing m_split_atoms (i.e. A_batch) that aren't already in the cube
continue; for (auto g_atom : m_split_atoms) {
add_split_atom(atom, start); if (!atom_in_cube(g_cube, g_atom)) {
add_split_atom(g_atom, start);
if (m_cubes.size() > max_cubes) {
greedy_mode = false;
break; // stop splitting on older atoms, switch to frugal mode
}
}
}
} }
} }
// TODO: avoid making m_cubes too large. unsigned a_worker_start_idx = 0;
// QUESTION: do we need to check if any split_atoms are already in the cubes in m_cubes??
for (auto& atom : a_worker) { // --- Phase 2: Process split atoms from A_worker ---
expr_ref g_atom(l2g.to()); if (greedy_mode) {
g_atom = l2g(atom); // Start as greedy: split all cubes on new atoms
for (; a_worker_start_idx < A_worker.size(); ++a_worker_start_idx) {
expr_ref g_atom(A_worker[a_worker_start_idx], l2g.to());
if (m_split_atoms.contains(g_atom)) if (m_split_atoms.contains(g_atom))
continue; continue;
m_split_atoms.push_back(g_atom); m_split_atoms.push_back(g_atom);
add_split_atom(g_atom, 0); // add ¬p to all cubes in m_cubes
add_split_atom(g_atom, 0);
if (m_cubes.size() > max_cubes) {
greedy_mode = false;
++a_worker_start_idx; // Record where to start processing the remaining atoms for frugal processing, so there's no redundant splitting
break;
}
}
}
// --- Phase 3: Frugal fallback ---
if (!greedy_mode) {
// Split only cubes added in *this call* on the new A_worker atoms (starting where we left off from the initial greedy phase)
for (unsigned i = a_worker_start_idx; i < A_worker.size(); ++i) {
expr_ref g_atom(A_worker[i], l2g.to());
if (!m_split_atoms.contains(g_atom))
m_split_atoms.push_back(g_atom);
add_split_atom(g_atom, initial_m_cubes_size); // start from the initial size of m_cubes to ONLY split the NEW worker cubes
}
} }
} }
@ -343,6 +393,7 @@ namespace smt {
unsigned k = 2; unsigned k = 2;
auto candidates = ctx->m_pq_scores.get_heap(); auto candidates = ctx->m_pq_scores.get_heap();
std::sort(candidates.begin(), candidates.end(), std::sort(candidates.begin(), candidates.end(),
[](const auto& a, const auto& b) { return a.priority > b.priority; }); [](const auto& a, const auto& b) { return a.priority > b.priority; });
@ -379,7 +430,6 @@ namespace smt {
m_batch_manager.initialize(); m_batch_manager.initialize();
m_workers.reset(); m_workers.reset();
scoped_limits sl(m.limit()); scoped_limits sl(m.limit());
unsigned num_threads = std::min((unsigned)std::thread::hardware_concurrency(), ctx.get_fparams().m_threads);
flet<unsigned> _nt(ctx.m_fparams.m_threads, 1); flet<unsigned> _nt(ctx.m_fparams.m_threads, 1);
SASSERT(num_threads > 1); SASSERT(num_threads > 1);
for (unsigned i = 0; i < num_threads; ++i) for (unsigned i = 0; i < num_threads; ++i)
@ -407,10 +457,10 @@ namespace smt {
for (auto w : m_workers) for (auto w : m_workers)
w->collect_statistics(ctx.m_aux_stats); w->collect_statistics(ctx.m_aux_stats);
} }
m_workers.clear();
return m_batch_manager.get_result();
}
m_workers.clear();
return m_batch_manager.get_result(); // i.e. all threads have finished all of their cubes -- so if state::is_running is still true, means the entire formula is unsat (otherwise a thread would have returned l_undef)
}
} }
#endif #endif

3
src/smt/smt_parallel.h
View file

@ -49,6 +49,7 @@ namespace smt {
// called from batch manager to cancel other workers if we've reached a verdict // called from batch manager to cancel other workers if we've reached a verdict
void cancel_workers() { void cancel_workers() {
IF_VERBOSE(0, verbose_stream() << "Canceling workers\n");
for (auto& w : p.m_workers) for (auto& w : p.m_workers)
w->cancel(); w->cancel();
} }
@ -96,9 +97,11 @@ namespace smt {
void run(); void run();
expr_ref_vector get_split_atoms(); expr_ref_vector get_split_atoms();
void cancel() { void cancel() {
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " canceling\n");
m.limit().cancel(); m.limit().cancel();
} }
void collect_statistics(::statistics& st) const { void collect_statistics(::statistics& st) const {
IF_VERBOSE(0, verbose_stream() << "Collecting statistics for worker " << id << "\n");
ctx->collect_statistics(st); ctx->collect_statistics(st);
} }
reslimit& limit() { reslimit& limit() {