Skip to content

Commit d0c86fe

Browse files
ilanashapiroNikolajBjornerhumnrdblenunoplopesCopilot
authored
Parallel solving (#7774)
* very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner <[email protected]> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <[email protected]> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <[email protected]> * remove verbose output Signed-off-by: Nikolaj Bjorner <[email protected]> * 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 <[email protected]> * 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 <[email protected]> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <[email protected]> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <[email protected]> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * 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 * fix #7603: race condition in Ctrl-C handling (#7755) * fix #7603: race condition in Ctrl-C handling * fix race in cancel_eh * fix build * add arithemtic saturation * add an option to register callback on quantifier instantiation Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation * missing new closure Signed-off-by: Nikolaj Bjorner <[email protected]> * add Z3_solver_propagate_on_binding to ml callback declarations Signed-off-by: Nikolaj Bjorner <[email protected]> * add python file Signed-off-by: Lev Nachmanson <[email protected]> * debug under defined calls Signed-off-by: Lev Nachmanson <[email protected]> * more untangle params Signed-off-by: Lev Nachmanson <[email protected]> * precalc parameters to define the eval order Signed-off-by: Lev Nachmanson <[email protected]> * remove a printout Signed-off-by: Lev Nachmanson <[email protected]> * rename a Python file Signed-off-by: Lev Nachmanson <[email protected]> * add on_binding callbacks across APIs update release notes, add to Java, .Net, C++ * use jboolean in Native interface Signed-off-by: Nikolaj Bjorner <[email protected]> * register on_binding attribute Signed-off-by: Nikolaj Bjorner <[email protected]> * fix java build for java bindings Signed-off-by: Nikolaj Bjorner <[email protected]> * avoid interferring side-effects in function calls Signed-off-by: Nikolaj Bjorner <[email protected]> * remove theory_str and classes that are only used by it * remove automata from python build Signed-off-by: Nikolaj Bjorner <[email protected]> * remove ref to theory_str Signed-off-by: Nikolaj Bjorner <[email protected]> * get the finest factorizations before project Signed-off-by: Lev Nachmanson <[email protected]> * rename add_lcs to add_lc Signed-off-by: Lev Nachmanson <[email protected]> * 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? * Update RELEASE_NOTES.md * resolve bug about not translating managers correctly for the second phase of the greedy cubing, and the frugal fallback * remove unused square-free check Signed-off-by: Lev Nachmanson <[email protected]> * add some debug prints and impelement internal polynomial fix * add some comments and debug m_assumptions_used * redo greedy->frugal strategy so we don't split on existing cubes in frugal at all (eliminate the incorrect/wasteful step by processing current batch first) * set up initial scaffolding for sharing clauses between threads and batch manager. needs some reworking/debug still --------- Signed-off-by: Nikolaj Bjorner <[email protected]> Signed-off-by: Lev Nachmanson <[email protected]> Signed-off-by: Lev Nachmanson <[email protected]> Co-authored-by: Nikolaj Bjorner <[email protected]> Co-authored-by: humnrdble <[email protected]> Co-authored-by: Nuno Lopes <[email protected]> Co-authored-by: Copilot <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> Co-authored-by: Lev Nachmanson <[email protected]>
1 parent bffefc5 commit d0c86fe

File tree

3 files changed

+120
-131
lines changed

3 files changed

+120
-131
lines changed

‎src/nlsat/nlsat_explain.cpp‎

Lines changed: 0 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -618,34 +618,6 @@ namespace nlsat {
618618
}
619619
}
620620

621-
// The monomials have to be square free according to
622-
//"An improved projection operation for cylindrical algebraic decomposition of three-dimensional space", by McCallum, Scott
623-
624-
bool is_square_free_at_sample(polynomial_ref_vector &ps, var x) {
625-
polynomial_ref p(m_pm);
626-
polynomial_ref lc_poly(m_pm);
627-
polynomial_ref disc_poly(m_pm);
628-
629-
for (unsigned i = 0; i < ps.size(); i++) {
630-
p = ps.get(i);
631-
unsigned k_deg = m_pm.degree(p, x);
632-
if (k_deg == 0)
633-
continue;
634-
// p depends on x
635-
disc_poly = discriminant(p, x); // Use global helper
636-
if (sign(disc_poly) == 0) { // Discriminant is zero
637-
TRACE(nlsat_explain, tout << "p is not square free:\n ";
638-
display(tout, p); tout << "\ndiscriminant: "; display(tout, disc_poly) << "\n";
639-
m_solver.display_assignment(tout) << '\n';
640-
m_solver.display_var(tout << "x:", x) << '\n';
641-
);
642-
643-
return false;
644-
}
645-
}
646-
return true;
647-
}
648-
649621
// For each p in ps add the leading coefficent to the projection,
650622
void add_lc(polynomial_ref_vector &ps, var x) {
651623
polynomial_ref p(m_pm);

‎src/smt/smt_parallel.cpp‎

Lines changed: 105 additions & 97 deletions
Original file line numberDiff line numberDiff line change
@@ -43,19 +43,25 @@ namespace smt {
4343
void parallel::worker::run() {
4444
ast_translation g2l(p.ctx.m, m); // global to local context -- MUST USE p.ctx.m, not ctx->m, AS GLOBAL MANAGER!!!
4545
ast_translation l2g(m, p.ctx.m); // local to global context
46-
while (m.inc()) {
47-
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " checking cubes\n");
46+
while (m.inc()) { // inc: increase the limit and check if it is canceled, vs m.limit().is_canceled() is readonly. the .limit() is also not necessary (m.inc() etc provides a convenience wrapper)
4847
vector<expr_ref_vector> cubes;
4948
b.get_cubes(g2l, cubes);
5049
if (cubes.empty())
5150
return;
5251
for (auto& cube : cubes) {
5352
if (!m.inc()) {
5453
b.set_exception("context cancelled");
55-
return; // stop if the main context (i.e. parent thread) is cancelled
54+
return;
5655
}
57-
switch (check_cube(cube)) {
56+
IF_VERBOSE(0, verbose_stream() << "Processing cube: " << mk_bounded_pp(mk_and(cube), m, 3) << "\n");
57+
lbool r = check_cube(cube);
58+
if (m.limit().is_canceled()) {
59+
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " context cancelled\n");
60+
return;
61+
}
62+
switch (r) {
5863
case l_undef: {
64+
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found undef cube\n");
5965
// return unprocessed cubes to the batch manager
6066
// add a split literal to the batch manager.
6167
// optionally process other cubes and delay sending back unprocessed cubes to batch manager.
@@ -66,7 +72,7 @@ namespace smt {
6672
break;
6773
}
6874
case l_true: {
69-
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found sat cube: " << mk_and(cube) << "\n");
75+
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found sat cube\n");
7076
model_ref mdl;
7177
ctx->get_model(mdl);
7278
b.set_sat(l2g, *mdl);
@@ -85,14 +91,15 @@ namespace smt {
8591
b.set_unsat(l2g, unsat_core);
8692
return;
8793
}
88-
for (expr * e : unsat_core)
94+
for (expr* e : unsat_core)
8995
if (asms.contains(e))
9096
b.report_assumption_used(l2g, e); // report assumptions used in unsat core, so they can be used in final core
9197

9298
// TODO: can share lemmas here, such as new units and not(and(unsat_core)), binary clauses, etc.
93-
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found unsat cube: " << mk_pp(mk_and(cube), m) << "\n");
94-
b.share_lemma(l2g, mk_not(mk_and(unsat_core)));
95-
// share_units();
99+
// TODO: remember assumptions used in core so that they get used for the final core.
100+
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found unsat cube\n");
101+
b.collect_clause(l2g, id, mk_not(mk_and(unsat_core)));
102+
share_units(l2g);
96103
break;
97104
}
98105
}
@@ -111,62 +118,57 @@ namespace smt {
111118
ctx->set_random_seed(id + m_smt_params.m_random_seed);
112119
}
113120

114-
void parallel::worker::share_units() {
115-
// obj_hashtable<expr> unit_set;
116-
// expr_ref_vector unit_trail(ctx.m);
117-
// unsigned_vector unit_lim;
118-
// for (unsigned i = 0; i < num_threads; ++i) unit_lim.push_back(0);
119-
120-
// // we just want to share lemmas and have a way of remembering how they are shared -- this is the next step
121-
// // (this needs to be reworked)
122-
// std::function<void(void)> collect_units = [&,this]() {
123-
// //return; -- has overhead
124-
// for (unsigned i = 0; i < num_threads; ++i) {
125-
// context& pctx = *pctxs[i];
126-
// pctx.pop_to_base_lvl();
127-
// ast_translation tr(pctx.m, ctx.m);
128-
// unsigned sz = pctx.assigned_literals().size();
129-
// for (unsigned j = unit_lim[i]; j < sz; ++j) {
130-
// literal lit = pctx.assigned_literals()[j];
131-
// //IF_VERBOSE(0, verbose_stream() << "(smt.thread " << i << " :unit " << lit << " " << pctx.is_relevant(lit.var()) << ")\n";);
132-
// if (!pctx.is_relevant(lit.var()))
133-
// continue;
134-
// expr_ref e(pctx.bool_var2expr(lit.var()), pctx.m);
135-
// if (lit.sign()) e = pctx.m.mk_not(e);
136-
// expr_ref ce(tr(e.get()), ctx.m);
137-
// if (!unit_set.contains(ce)) {
138-
// unit_set.insert(ce);
139-
// unit_trail.push_back(ce);
140-
// }
141-
// }
142-
// }
143-
144-
// unsigned sz = unit_trail.size();
145-
// for (unsigned i = 0; i < num_threads; ++i) {
146-
// context& pctx = *pctxs[i];
147-
// ast_translation tr(ctx.m, pctx.m);
148-
// for (unsigned j = unit_lim[i]; j < sz; ++j) {
149-
// expr_ref src(ctx.m), dst(pctx.m);
150-
// dst = tr(unit_trail.get(j));
151-
// pctx.assert_expr(dst); // Assert that the conjunction of the assumptions in this unsat core is not satisfiable — prune it from future search
152-
// }
153-
// unit_lim[i] = pctx.assigned_literals().size();
154-
// }
155-
// IF_VERBOSE(1, verbose_stream() << "(smt.thread :units " << sz << ")\n");
156-
// };
121+
void parallel::worker::share_units(ast_translation& l2g) {
122+
// Collect new units learned locally by this worker and send to batch manager
123+
unsigned sz = ctx->assigned_literals().size();
124+
for (unsigned j = shared_clause_limit; j < sz; ++j) { // iterate only over new literals since last sync -- QUESTION: I THINK THIS IS BUGGY BECAUSE THE SHARED CLAUSE LIMIT IS ONLY UPDATED (FOR ALL CLAUSE TYPES) WHEN WE GATHER NEW SHARED UNITS
125+
literal lit = ctx->assigned_literals()[j];
126+
expr_ref e(ctx->bool_var2expr(lit.var()), ctx->m); // turn literal into a Boolean expression
127+
if (lit.sign())
128+
e = ctx->m.mk_not(e); // negate if literal is negative
129+
b.collect_clause(l2g, id, e);
130+
}
157131
}
158132

159-
void parallel::batch_manager::share_lemma(ast_translation& l2g, expr* lemma) {
133+
void parallel::batch_manager::collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* clause) {
160134
std::scoped_lock lock(mux);
161-
expr_ref g_lemma(l2g(lemma), l2g.to());
162-
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!
135+
expr* g_clause = l2g(clause);
136+
if (!shared_clause_set.contains(g_clause)) {
137+
shared_clause_set.insert(g_clause);
138+
SharedClause sc{source_worker_id, g_clause};
139+
shared_clause_trail.push_back(sc);
140+
}
141+
}
142+
143+
// QUESTION -- WHERE SHOULD WE CALL THIS?
144+
void parallel::worker::collect_shared_clauses(ast_translation& g2l) {
145+
expr_ref_vector new_clauses = b.return_shared_clauses(g2l, shared_clause_limit, id); // get new clauses from the batch manager
146+
// iterate over new clauses and assert them in the local context
147+
for (expr* e : new_clauses) {
148+
expr_ref local_clause(e, g2l.to()); // e was already translated to the local context in the batch manager!!
149+
ctx->assert_expr(local_clause); // assert the clause in the local context
150+
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " asserting shared clause: " << mk_bounded_pp(local_clause, m, 3) << "\n");
151+
}
163152
}
164153

154+
// get new clauses from the batch manager and assert them in the local context
155+
expr_ref_vector parallel::batch_manager::return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id) {
156+
expr_ref_vector result(g2l.to());
157+
{
158+
std::scoped_lock lock(mux);
159+
for (unsigned i = worker_limit; i < shared_clause_trail.size(); ++i) {
160+
if (shared_clause_trail[i].source_worker_id == worker_id)
161+
continue; // skip clauses from the requesting worker
162+
expr_ref local_clause(g2l(shared_clause_trail[i].clause), g2l.to());
163+
result.push_back(local_clause);
164+
}
165+
worker_limit = shared_clause_trail.size(); // update the worker limit to the end of the current trail
166+
}
167+
return result;
168+
}
165169

166-
// PUT THE LOGIC FOR LEARNING FROM UNSAT CORE HERE IF THE CUBE INTERSECTS WITH IT!!!
167-
// THERE IS AN EDGE CASE: IF ALL THE CUBES ARE UNSAT, BUT DEPEND ON NONEMPTY ASSUMPTIONS, NEED TO TAKE THE UNION OF THESE ASMS WHEN LEARNING FROM UNSAT CORE
168-
// DON'T CODE THIS CASE YET: WE ARE JUST TESTING WITH EMPTY ASMS FOR NOW (I.E. WE ARE NOT PASSING IN ASMS). THIS DOES NOT APPLY TO THE INTERNAL "LEARNED" UNSAT CORE
169170
lbool parallel::worker::check_cube(expr_ref_vector const& cube) {
171+
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " checking cube\n";);
170172
for (auto& atom : cube)
171173
asms.push_back(atom);
172174
lbool r = l_undef;
@@ -183,6 +185,7 @@ namespace smt {
183185
b.set_exception("unknown exception");
184186
}
185187
asms.shrink(asms.size() - cube.size());
188+
IF_VERBOSE(0, verbose_stream() << "Worker " << id << " DONE checking cube\n";);
186189
return r;
187190
}
188191

@@ -219,6 +222,10 @@ namespace smt {
219222
if (m_state != state::is_running)
220223
return;
221224
m_state = state::is_unsat;
225+
226+
// every time we do a check_sat call, don't want to have old info coming from a prev check_sat call
227+
// the unsat core gets reset internally in the context after each check_sat, so we assert this property here
228+
// takeaway: each call to check_sat needs to have a fresh unsat core
222229
SASSERT(p.ctx.m_unsat_core.empty());
223230
for (expr* e : unsat_core)
224231
p.ctx.m_unsat_core.push_back(l2g(e));
@@ -245,7 +252,7 @@ namespace smt {
245252

246253
void parallel::batch_manager::report_assumption_used(ast_translation& l2g, expr* assumption) {
247254
std::scoped_lock lock(mux);
248-
m_used_assumptions.insert(l2g(assumption))
255+
p.m_assumptions_used.insert(l2g(assumption));
249256
}
250257

251258
lbool parallel::batch_manager::get_result() const {
@@ -255,10 +262,10 @@ namespace smt {
255262
case state::is_running: // batch manager is still running, but all threads have processed their cubes, which means all cubes were unsat
256263
if (!m_cubes.empty())
257264
throw default_exception("inconsistent end state");
258-
if (!m_assumptions_used.empty()) {
259-
// collect unsat core from assumptions used, if any.
265+
if (!p.m_assumptions_used.empty()) {
266+
// collect unsat core from assumptions used, if any --> case when all cubes were unsat, but depend on nonempty asms, so we need to add these asms to final unsat core
260267
SASSERT(p.ctx.m_unsat_core.empty());
261-
for (auto a : m_assumptions_used)
268+
for (auto a : p.m_assumptions_used)
262269
p.ctx.m_unsat_core.push_back(a);
263270
}
264271
return l_false;
@@ -346,59 +353,59 @@ namespace smt {
346353
std::scoped_lock lock(mux);
347354
unsigned max_cubes = 1000;
348355
bool greedy_mode = (m_cubes.size() <= max_cubes);
349-
unsigned initial_m_cubes_size = m_cubes.size(); // cubes present before processing this batch
356+
unsigned a_worker_start_idx = 0;
350357

351-
// --- 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 ---
358+
//
359+
// --- Phase 1: Greedy split of *existing* cubes on new A_worker atoms (greedy) ---
360+
//
361+
if (greedy_mode) {
362+
for (; a_worker_start_idx < A_worker.size(); ++a_worker_start_idx) {
363+
expr_ref g_atom(l2g(A_worker[a_worker_start_idx]), l2g.to());
364+
if (m_split_atoms.contains(g_atom))
365+
continue;
366+
m_split_atoms.push_back(g_atom);
367+
368+
add_split_atom(g_atom, 0); // split all *existing* cubes
369+
if (m_cubes.size() > max_cubes) {
370+
greedy_mode = false;
371+
++a_worker_start_idx; // start frugal from here
372+
break;
373+
}
374+
}
375+
}
376+
377+
unsigned initial_m_cubes_size = m_cubes.size(); // where to start processing the worker cubes after splitting the EXISTING cubes on the new worker atoms
378+
379+
// --- Phase 2: Process worker cubes (greedy) ---
352380
for (auto& c : C_worker) {
353381
expr_ref_vector g_cube(l2g.to());
354382
for (auto& atom : c)
355383
g_cube.push_back(l2g(atom));
356384

357-
unsigned start = m_cubes.size();
358-
m_cubes.push_back(g_cube); // continuously update the start idx so we're just processing the single most recent cube
385+
unsigned start = m_cubes.size(); // update start after adding each cube so we only process the current cube being added
386+
m_cubes.push_back(g_cube);
359387

360388
if (greedy_mode) {
361-
// Split new cube all existing m_split_atoms (i.e. A_batch) that aren't already in the cube
389+
// Split new cube on all existing m_split_atoms not in it
362390
for (auto g_atom : m_split_atoms) {
363391
if (!atom_in_cube(g_cube, g_atom)) {
364392
add_split_atom(g_atom, start);
365393
if (m_cubes.size() > max_cubes) {
366394
greedy_mode = false;
367-
break; // stop splitting on older atoms, switch to frugal mode
395+
break;
368396
}
369397
}
370398
}
371399
}
372-
}
373-
374-
unsigned a_worker_start_idx = 0;
375-
376-
// --- Phase 2: Process split atoms from A_worker ---
377-
if (greedy_mode) {
378-
// Start as greedy: split all cubes on new atoms
379-
for (; a_worker_start_idx < A_worker.size(); ++a_worker_start_idx) {
380-
expr_ref g_atom(l2g(A_worker[a_worker_start_idx]), l2g.to());
381-
if (m_split_atoms.contains(g_atom))
382-
continue;
383-
m_split_atoms.push_back(g_atom);
384-
385-
add_split_atom(g_atom, 0);
386-
if (m_cubes.size() > max_cubes) {
387-
greedy_mode = false;
388-
++a_worker_start_idx; // Record where to start processing the remaining atoms for frugal processing, so there's no redundant splitting
389-
break;
390-
}
391-
}
392400
}
393401

394-
// --- Phase 3: Frugal fallback ---
402+
// --- Phase 3: Frugal fallback: only process NEW worker cubes with NEW atoms ---
395403
if (!greedy_mode) {
396-
// Split only cubes added in *this call* on the new A_worker atoms (starting where we left off from the initial greedy phase)
397404
for (unsigned i = a_worker_start_idx; i < A_worker.size(); ++i) {
398405
expr_ref g_atom(l2g(A_worker[i]), l2g.to());
399406
if (!m_split_atoms.contains(g_atom))
400407
m_split_atoms.push_back(g_atom);
401-
add_split_atom(g_atom, initial_m_cubes_size); // start from the initial size of m_cubes
408+
add_split_atom(g_atom, initial_m_cubes_size);
402409
}
403410
}
404411
}
@@ -439,13 +446,13 @@ namespace smt {
439446

440447
if (m.has_trace_stream())
441448
throw default_exception("trace streams have to be off in parallel mode");
442-
449+
443450
struct scoped_clear_table {
444-
obj_hashtable& ht;
445-
scoped_clear(obj_hashtable& ht) : ht(ht) {}
446-
~scoped_clear() { ht.reset(); }
451+
obj_hashtable<expr>& ht;
452+
scoped_clear_table(obj_hashtable<expr>& ht) : ht(ht) {} // Constructor: Takes a reference to a hash table when the object is created and saves it.
453+
~scoped_clear_table() { ht.reset(); } // Destructor: When the scoped_clear_table object goes out of scope, it automatically calls reset() on that hash table, clearing it
447454
};
448-
scoped_clear_table clear(m_batch_manager.m_used_assumptions);
455+
scoped_clear_table clear(m_assumptions_used); // creates a scoped_clear_table named clear, bound to m_assumptions_used
449456

450457
{
451458
m_batch_manager.initialize();
@@ -460,6 +467,7 @@ namespace smt {
460467
// within the lexical scope of the code block, creates a data structure that allows you to push children
461468
// objects to the limit object, so if someone cancels the parent object, the cancellation propagates to the children
462469
// and that cancellation has the lifetime of the scope
470+
// even if this code doesn't expliclty kill the main thread, still applies bc if you e.g. Ctrl+C the main thread, the children threads need to be cancelled
463471
for (auto w : m_workers)
464472
sl.push_child(&(w->limit()));
465473

@@ -475,7 +483,7 @@ namespace smt {
475483
for (auto& th : threads)
476484
th.join();
477485

478-
for (auto w : m_workers)
486+
for (auto w : m_workers)
479487
w->collect_statistics(ctx.m_aux_stats);
480488
}
481489

0 commit comments

Comments
 (0)