From 5700e3dfe4f9e25f66b734c1d73e9e8335d74a55 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Wed, 6 Aug 2025 01:27:54 -0700 Subject: [PATCH 1/3] Parallel solving (#7759) * very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner * remove verbose output Signed-off-by: Nikolaj Bjorner * 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 * 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 --------- Signed-off-by: Nikolaj Bjorner Co-authored-by: Nikolaj Bjorner Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/smt_parallel.cpp | 258 +++++++++++++++++---------------------- src/smt/smt_parallel.h | 4 +- 2 files changed, 117 insertions(+), 145 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index ab100775e..065958a08 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -52,31 +52,43 @@ namespace smt { if (!m.inc()) return; // stop if the main context is cancelled switch (check_cube(cube)) { - case l_undef: { - vector returned_cubes; - returned_cubes.push_back(cube); - auto split_atoms = get_split_atoms(); - b.return_cubes(l2g, returned_cubes, split_atoms); - break; - } - case l_true: { - model_ref mdl; - ctx->get_model(mdl); - b.set_sat(l2g, *mdl); - return; - } - case l_false: { - auto const& unsat_core = ctx->unsat_core(); - // If the unsat core only contains assumptions, - // unsatisfiability does not depend on the current cube and the entire problem is unsat. - if (any_of(unsat_core, [&](expr* e) { return asms.contains(e); })) { - b.set_unsat(l2g, ctx->unsat_core()); + case l_undef: { + // return unprocessed cubes to the batch manager + // add a split literal to the batch manager. + // optionally process other cubes and delay sending back unprocessed cubes to batch manager. + vector returned_cubes; + returned_cubes.push_back(cube); + auto split_atoms = get_split_atoms(); + b.return_cubes(l2g, returned_cubes, split_atoms); + break; + } + case l_true: { + std::cout << "Worker " << id << " found sat cube: " << mk_pp(mk_and(cube), m) << "\n"; + model_ref mdl; + ctx->get_model(mdl); + b.set_sat(l2g, *mdl); return; } - // TODO: can share lemmas here, such as new units and not(and(unsat_core)), binary clauses, etc. - // TODO: remember assumptions used in core so that they get used for the final core. - break; - } + case l_false: { + // if unsat core only contains (external) assumptions (i.e. all the unsat core are asms), then unsat and return as this does NOT depend on cubes + // otherwise, extract lemmas that can be shared (units (and unsat core?)). + // share with batch manager. + // process next cube. + expr_ref_vector const& unsat_core = ctx->unsat_core(); + // If the unsat core only contains assumptions, + // unsatisfiability does not depend on the current cube and the entire problem is unsat. + if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) { + std::cout << "Worker " << id << " determined formula unsat"; + b.set_unsat(l2g, unsat_core); + return; + } + // TODO: can share lemmas here, such as new units and not(and(unsat_core)), binary clauses, etc. + // TODO: remember assumptions used in core so that they get used for the final core. + std::cout << "Worker " << id << " found unsat cube: " << mk_pp(mk_and(cube), m) << "\n"; + b.share_lemma(l2g, mk_not(mk_and(unsat_core))); + // share_units(); + break; + } } } } @@ -92,7 +104,61 @@ namespace smt { ctx->set_random_seed(id + m_smt_params.m_random_seed); } + void parallel::worker::share_units() { + // obj_hashtable unit_set; + // expr_ref_vector unit_trail(ctx.m); + // unsigned_vector unit_lim; + // for (unsigned i = 0; i < num_threads; ++i) unit_lim.push_back(0); + // // we just want to share lemmas and have a way of remembering how they are shared -- this is the next step + // // (this needs to be reworked) + // std::function collect_units = [&,this]() { + // //return; -- has overhead + // for (unsigned i = 0; i < num_threads; ++i) { + // context& pctx = *pctxs[i]; + // pctx.pop_to_base_lvl(); + // ast_translation tr(pctx.m, ctx.m); + // unsigned sz = pctx.assigned_literals().size(); + // for (unsigned j = unit_lim[i]; j < sz; ++j) { + // literal lit = pctx.assigned_literals()[j]; + // //IF_VERBOSE(0, verbose_stream() << "(smt.thread " << i << " :unit " << lit << " " << pctx.is_relevant(lit.var()) << ")\n";); + // if (!pctx.is_relevant(lit.var())) + // continue; + // expr_ref e(pctx.bool_var2expr(lit.var()), pctx.m); + // if (lit.sign()) e = pctx.m.mk_not(e); + // expr_ref ce(tr(e.get()), ctx.m); + // if (!unit_set.contains(ce)) { + // unit_set.insert(ce); + // unit_trail.push_back(ce); + // } + // } + // } + + // unsigned sz = unit_trail.size(); + // for (unsigned i = 0; i < num_threads; ++i) { + // context& pctx = *pctxs[i]; + // ast_translation tr(ctx.m, pctx.m); + // for (unsigned j = unit_lim[i]; j < sz; ++j) { + // expr_ref src(ctx.m), dst(pctx.m); + // dst = tr(unit_trail.get(j)); + // pctx.assert_expr(dst); // Assert that the conjunction of the assumptions in this unsat core is not satisfiable — prune it from future search + // } + // unit_lim[i] = pctx.assigned_literals().size(); + // } + // IF_VERBOSE(1, verbose_stream() << "(smt.thread :units " << sz << ")\n"); + // }; + } + + void parallel::batch_manager::share_lemma(ast_translation& l2g, expr* lemma) { + std::scoped_lock lock(mux); + 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? + } + + + // PUT THE LOGIC FOR LEARNING FROM UNSAT CORE HERE IF THE CUBE INTERSECTS WITH IT!!! + // 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 + // 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 lbool parallel::worker::check_cube(expr_ref_vector const& cube) { for (auto& atom : cube) asms.push_back(atom); @@ -145,10 +211,7 @@ namespace smt { std::scoped_lock lock(mux); if (l_false == m_result) return; - m_result = l_false; - expr_ref_vector g_core(l2g.to()); - for (auto& e : unsat_core) - g_core.push_back(l2g(e)); + m_result = l_false; p.ctx.m_unsat_core.reset(); for (expr* e : unsat_core) p.ctx.m_unsat_core.push_back(l2g(e)); @@ -197,31 +260,43 @@ namespace smt { std::scoped_lock lock(mux); for (auto & c : cubes) { expr_ref_vector g_cube(l2g.to()); - for (auto& e : c) { - g_cube.push_back(l2g(e)); + for (auto& atom : c) { + g_cube.push_back(l2g(atom)); + } + + m_cubes.push_back(g_cube); // base cube + expr_ref_vector& base = m_cubes.back(); + + for (auto& atom : m_split_atoms) { + if (g_cube.contains(atom) || g_cube.contains(m.mk_not(atom))) + continue; + + // Split base: one copy with ¬atom, one with atom + m_cubes.push_back(base); // push new copy of base cube + m_cubes.back().push_back(m.mk_not(atom)); // add ¬atom to new copy + base.push_back(atom); // add atom to base cube } - // TODO: split this g_cube on m_split_atoms that are not already in g_cube as literals. - m_cubes.push_back(g_cube); } // TODO: avoid making m_cubes too large. + // QUESTION: do we need to check if any split_atoms are already in the cubes in m_cubes?? for (auto& atom : split_atoms) { - expr_ref g_atom(l2g.from()); + expr_ref g_atom(l2g.to()); g_atom = l2g(atom); if (m_split_atoms.contains(g_atom)) continue; m_split_atoms.push_back(g_atom); unsigned sz = m_cubes.size(); for (unsigned i = 0; i < sz; ++i) { - m_cubes.push_back(m_cubes[i]); // copy the existing cubes - m_cubes.back().push_back(m.mk_not(g_atom)); // add the negation of the split atom to each cube - m_cubes[i].push_back(g_atom); + m_cubes.push_back(m_cubes[i]); // push copy of m_cubes[i] + m_cubes.back().push_back(m.mk_not(g_atom)); // add ¬p to the copy + m_cubes[i].push_back(g_atom); // add p to the original } } } expr_ref_vector parallel::worker::get_split_atoms() { - unsigned k = 1; + unsigned k = 2; auto candidates = ctx->m_pq_scores.get_heap(); std::sort(candidates.begin(), candidates.end(), @@ -244,7 +319,6 @@ namespace smt { } lbool parallel::new_check(expr_ref_vector const& asms) { - ast_manager& m = ctx.m; if (m.has_trace_stream()) @@ -255,7 +329,7 @@ namespace smt { unsigned num_threads = std::min((unsigned)std::thread::hardware_concurrency(), ctx.get_fparams().m_threads); SASSERT(num_threads > 1); for (unsigned i = 0; i < num_threads; ++i) - m_workers.push_back(alloc(worker, i, *this, asms)); + m_workers.push_back(alloc(worker, i, *this, asms)); // i.e. "new worker(i, *this, asms)" // THIS WILL ALLOW YOU TO CANCEL ALL THE CHILD THREADS // within the lexical scope of the code block, creates a data structure that allows you to push children @@ -284,113 +358,9 @@ namespace smt { } lbool parallel::operator()(expr_ref_vector const& asms) { - - lbool result = l_undef; - unsigned num_threads = std::min((unsigned) std::thread::hardware_concurrency(), ctx.get_fparams().m_threads); + std::cout << "Parallel solving with " << asms.size() << " assumptions." << std::endl; flet _nt(ctx.m_fparams.m_threads, 1); - unsigned thread_max_conflicts = ctx.get_fparams().m_threads_max_conflicts; - unsigned max_conflicts = ctx.get_fparams().m_max_conflicts; - - // try first sequential with a low conflict budget to make super easy problems cheap - // GET RID OF THIS, AND IMMEDIATELY SEND TO THE MULTITHREADED CHECKER - // THE FIRST BATCH OF CUBES IS EMPTY, AND WE WILL SET ALL THREADS TO WORK ON THE ORIGINAL FORMULA - - enum par_exception_kind { - DEFAULT_EX, - ERROR_EX - }; - - // MOVE ALL OF THIS INSIDE THE WORKER THREAD AND CREATE/MANAGE LOCALLY - // SO THEN WE REMOVE THE ENCAPSULATING scoped_ptr_vector ETC, SMT_PARAMS BECOMES SMT_ - vector smt_params; - scoped_ptr_vector pms; - scoped_ptr_vector pctxs; - vector pasms; - - ast_manager& m = ctx.m; - scoped_limits sl(m.limit()); - unsigned finished_id = UINT_MAX; - std::string ex_msg; - par_exception_kind ex_kind = DEFAULT_EX; - unsigned error_code = 0; - bool done = false; - unsigned num_rounds = 0; - if (m.has_trace_stream()) - throw default_exception("trace streams have to be off in parallel mode"); - - - params_ref params = ctx.get_params(); - for (unsigned i = 0; i < num_threads; ++i) { - smt_params.push_back(ctx.get_fparams()); - smt_params.back().m_preprocess = false; - } - - for (unsigned i = 0; i < num_threads; ++i) { - ast_manager* new_m = alloc(ast_manager, m, true); - pms.push_back(new_m); - pctxs.push_back(alloc(context, *new_m, smt_params[i], params)); - context& new_ctx = *pctxs.back(); - context::copy(ctx, new_ctx, true); - new_ctx.set_random_seed(i + ctx.get_fparams().m_random_seed); - ast_translation tr(m, *new_m); - pasms.push_back(tr(asms)); - sl.push_child(&(new_m->limit())); - } - - obj_hashtable unit_set; - expr_ref_vector unit_trail(ctx.m); - unsigned_vector unit_lim; - for (unsigned i = 0; i < num_threads; ++i) unit_lim.push_back(0); - - std::function collect_units = [&,this]() { - //return; -- has overhead - for (unsigned i = 0; i < num_threads; ++i) { - context& pctx = *pctxs[i]; - pctx.pop_to_base_lvl(); - ast_translation tr(pctx.m, ctx.m); - unsigned sz = pctx.assigned_literals().size(); - for (unsigned j = unit_lim[i]; j < sz; ++j) { - literal lit = pctx.assigned_literals()[j]; - //IF_VERBOSE(0, verbose_stream() << "(smt.thread " << i << " :unit " << lit << " " << pctx.is_relevant(lit.var()) << ")\n";); - if (!pctx.is_relevant(lit.var())) - continue; - expr_ref e(pctx.bool_var2expr(lit.var()), pctx.m); - if (lit.sign()) e = pctx.m.mk_not(e); - expr_ref ce(tr(e.get()), ctx.m); - if (!unit_set.contains(ce)) { - unit_set.insert(ce); - unit_trail.push_back(ce); - } - } - } - - unsigned sz = unit_trail.size(); - for (unsigned i = 0; i < num_threads; ++i) { - context& pctx = *pctxs[i]; - ast_translation tr(ctx.m, pctx.m); - for (unsigned j = unit_lim[i]; j < sz; ++j) { - expr_ref src(ctx.m), dst(pctx.m); - dst = tr(unit_trail.get(j)); - pctx.assert_expr(dst); // Assert that the conjunction of the assumptions in this unsat core is not satisfiable — prune it from future search - } - unit_lim[i] = pctx.assigned_literals().size(); - } - IF_VERBOSE(1, verbose_stream() << "(smt.thread :units " << sz << ")\n"); - }; - - // Gather statistics from all solver contexts - for (context* c : pctxs) { - c->collect_statistics(ctx.m_aux_stats); - } - - // If no thread finished successfully, throw recorded error - if (finished_id == UINT_MAX) { - switch (ex_kind) { - case ERROR_EX: throw z3_error(error_code); - default: throw default_exception(std::move(ex_msg)); - } - } - + return new_check(asms); } } diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 9db32a53e..0892d81e1 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -19,6 +19,7 @@ Revision History: #pragma once #include "smt/smt_context.h" +#include namespace smt { @@ -38,12 +39,13 @@ namespace smt { std::mutex mux; expr_ref_vector m_split_atoms; // atoms to split on vector m_cubes; - lbool m_result = l_false; + lbool m_result = l_false; // want states: init/undef, canceled/exception, sat, unsat unsigned m_max_batch_size = 10; exception_kind m_exception_kind = NO_EX; unsigned m_exception_code = 0; std::string m_exception_msg; + // called from batch manager to cancel other workers if we've reached a verdict void cancel_workers() { for (auto& w : p.m_workers) w->cancel(); From 9dd8221f2c61ec3a45c622bbb812be2b0f509d13 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Aug 2025 10:05:38 -0700 Subject: [PATCH 2/3] updates Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 149 ++++++++++++++++++++++++++------------- src/smt/smt_parallel.h | 21 +++--- 2 files changed, 111 insertions(+), 59 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 065958a08..db33cda14 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -49,8 +49,10 @@ namespace smt { if (cubes.empty()) return; for (auto& cube : cubes) { - if (!m.inc()) + if (!m.inc()) { + b.set_exception("context cancelled"); return; // stop if the main context is cancelled + } switch (check_cube(cube)) { case l_undef: { // return unprocessed cubes to the batch manager @@ -78,13 +80,13 @@ namespace smt { // If the unsat core only contains assumptions, // unsatisfiability does not depend on the current cube and the entire problem is unsat. if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) { - std::cout << "Worker " << id << " determined formula unsat"; + IF_VERBOSE(0, verbose_stream() << "Worker " << id << " determined formula unsat"); b.set_unsat(l2g, unsat_core); return; } // TODO: can share lemmas here, such as new units and not(and(unsat_core)), binary clauses, etc. // TODO: remember assumptions used in core so that they get used for the final core. - std::cout << "Worker " << id << " found unsat cube: " << mk_pp(mk_and(cube), m) << "\n"; + IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found unsat cube: " << mk_pp(mk_and(cube), m) << "\n"); b.share_lemma(l2g, mk_not(mk_and(unsat_core))); // share_units(); break; @@ -200,18 +202,18 @@ namespace smt { void parallel::batch_manager::set_sat(ast_translation& l2g, model& m) { std::scoped_lock lock(mux); - if (l_true == m_result) + if (m_state != state::is_running) return; - m_result = l_true; + m_state = state::is_sat; p.ctx.set_model(m.translate(l2g)); cancel_workers(); } void parallel::batch_manager::set_unsat(ast_translation& l2g, expr_ref_vector const& unsat_core) { std::scoped_lock lock(mux); - if (l_false == m_result) + if (m_state != state::is_running) return; - m_result = l_false; + m_state = state::is_unsat; p.ctx.m_unsat_core.reset(); for (expr* e : unsat_core) p.ctx.m_unsat_core.push_back(l2g(e)); @@ -220,43 +222,94 @@ namespace smt { void parallel::batch_manager::set_exception(unsigned error_code) { std::scoped_lock lock(mux); - if (m_exception_kind != NO_EX) - return; // already set - m_exception_kind = ERROR_CODE_EX; + if (m_state != state::is_running) + return; + m_state = state::is_exception_code; m_exception_code = error_code; cancel_workers(); } void parallel::batch_manager::set_exception(std::string const& msg) { std::scoped_lock lock(mux); - if (m_exception_kind != NO_EX) - return; // already set - m_exception_kind = ERROR_MSG_EX; + if (m_state != state::is_running || m.limit().is_canceled()) + return; + m_state = state::is_exception_msg; m_exception_msg = msg; cancel_workers(); } lbool parallel::batch_manager::get_result() const { - if (m_exception_kind == ERROR_MSG_EX) - throw default_exception(m_exception_msg.c_str()); - if (m_exception_kind == ERROR_CODE_EX) - throw z3_error(m_exception_code); if (m.limit().is_canceled()) return l_undef; // the main context was cancelled, so we return undef. - return m_result; + switch (m_state) { + case state::is_running: + if (!m_cubes.empty()) + throw default_exception("inconsistent end state"); + // TODO collect unsat core from assumptions, if any. + return l_false; + case state::is_unsat: + return l_false; + case state::is_sat: + return l_true; + case state::is_exception_msg: + throw default_exception(m_exception_msg.c_str()); + case state::is_exception_code: + throw z3_error(m_exception_code); + default: + UNREACHABLE(); + } } -#if 0 - for (auto& c : m_cubes) { - expr_ref_vector g_cube(l2g.to()); - for (auto& e : c) { - g_cube.push_back(l2g(e)); - } - share_lemma(l2g, mk_and(g_cube)); - } -#endif - - void parallel::batch_manager::return_cubes(ast_translation& l2g, vectorconst& cubes, expr_ref_vector const& split_atoms) { + // + // Batch manager maintains C_batch, A_batch. + // C_batch - set of cubes + // A_batch - set of split atoms. + // return_cubes is called with C_batch A_batch C A. + // C_worker - one or more cubes + // A_worker - split atoms form the worker thread. + // + // Assumption: A_worker does not occur in C_worker. + // + // Greedy strategy: + // + // return_cubes C_batch A_batch C_worker A_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 } + // = + // let C_batch' = C_batch u { cube * 2^(A_batch \ atoms(cube)) | cube in C_worker } + // { cube * 2^(A_worker \ A_batch) | cube in C_batch' } + // A_batch <- A_batch u A_worker + // + // Frugal strategy: + // + // 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 + // + // return_cubes C_batch A_batch C_worker A_worker: + // C_batch <- C_batch u { cube * 2^A_worker | cube in C_worker }. + // 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 } + // A_batch <- A_batch u A_worker + // + // Or: use greedy strategy by a policy when C_batch, A_batch, A_worker are "small". + // + void parallel::batch_manager::return_cubes(ast_translation& l2g, vectorconst& cubes, expr_ref_vector const& a_worker) { + 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); }); + }; + + auto add_split_atom = [&](expr* atom, unsigned start) { + unsigned stop = m_cubes.size(); + for (unsigned i = start; i < stop; ++i) { + m_cubes.push_back(m_cubes[i]); // push copy of m_cubes[i] + m_cubes.back().push_back(m.mk_not(atom)); // add ¬atom to the copy + m_cubes[i].push_back(atom); // add atom to the original + } + }; + std::scoped_lock lock(mux); for (auto & c : cubes) { expr_ref_vector g_cube(l2g.to()); @@ -264,34 +317,25 @@ namespace smt { g_cube.push_back(l2g(atom)); } + unsigned start = m_cubes.size(); m_cubes.push_back(g_cube); // base cube - expr_ref_vector& base = m_cubes.back(); for (auto& atom : m_split_atoms) { - if (g_cube.contains(atom) || g_cube.contains(m.mk_not(atom))) + if (atom_in_cube(g_cube, atom)) continue; - - // Split base: one copy with ¬atom, one with atom - m_cubes.push_back(base); // push new copy of base cube - m_cubes.back().push_back(m.mk_not(atom)); // add ¬atom to new copy - base.push_back(atom); // add atom to base cube + add_split_atom(atom, start); } } // TODO: avoid making m_cubes too large. // QUESTION: do we need to check if any split_atoms are already in the cubes in m_cubes?? - for (auto& atom : split_atoms) { + for (auto& atom : a_worker) { expr_ref g_atom(l2g.to()); g_atom = l2g(atom); if (m_split_atoms.contains(g_atom)) continue; m_split_atoms.push_back(g_atom); - unsigned sz = m_cubes.size(); - for (unsigned i = 0; i < sz; ++i) { - m_cubes.push_back(m_cubes[i]); // push copy of m_cubes[i] - m_cubes.back().push_back(m.mk_not(g_atom)); // add ¬p to the copy - m_cubes[i].push_back(g_atom); // add p to the original - } + add_split_atom(g_atom, 0); // add ¬p to all cubes in m_cubes } } @@ -318,15 +362,25 @@ namespace smt { return top_lits; } - lbool parallel::new_check(expr_ref_vector const& asms) { + void parallel::batch_manager::initialize() { + m_state = state::is_running; + m_cubes.reset(); + m_cubes.push_back(expr_ref_vector(m)); // push empty cube + m_split_atoms.reset(); + } + + lbool parallel::operator()(expr_ref_vector const& asms) { ast_manager& m = ctx.m; if (m.has_trace_stream()) throw default_exception("trace streams have to be off in parallel mode"); { + m_batch_manager.initialize(); + m_workers.reset(); scoped_limits sl(m.limit()); unsigned num_threads = std::min((unsigned)std::thread::hardware_concurrency(), ctx.get_fparams().m_threads); + flet _nt(ctx.m_fparams.m_threads, 1); SASSERT(num_threads > 1); for (unsigned i = 0; i < num_threads; ++i) m_workers.push_back(alloc(worker, i, *this, asms)); // i.e. "new worker(i, *this, asms)" @@ -356,12 +410,7 @@ namespace smt { m_workers.clear(); return m_batch_manager.get_result(); } - - lbool parallel::operator()(expr_ref_vector const& asms) { - std::cout << "Parallel solving with " << asms.size() << " assumptions." << std::endl; - flet _nt(ctx.m_fparams.m_threads, 1); - return new_check(asms); - } + } #endif diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 0892d81e1..44dc1400e 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -29,19 +29,21 @@ namespace smt { class batch_manager { - enum exception_kind { - NO_EX, - ERROR_CODE_EX, - ERROR_MSG_EX + enum state { + is_running, + is_sat, + is_unsat, + is_exception_msg, + is_exception_code }; + ast_manager& m; parallel& p; std::mutex mux; + state m_state = state::is_running; expr_ref_vector m_split_atoms; // atoms to split on vector m_cubes; - lbool m_result = l_false; // want states: init/undef, canceled/exception, sat, unsat unsigned m_max_batch_size = 10; - exception_kind m_exception_kind = NO_EX; unsigned m_exception_code = 0; std::string m_exception_msg; @@ -52,7 +54,10 @@ namespace smt { } public: - batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_split_atoms(m) { m_cubes.push_back(expr_ref_vector(m)); } + batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_split_atoms(m) { } + + void initialize(); + void set_unsat(ast_translation& l2g, expr_ref_vector const& unsat_core); void set_sat(ast_translation& l2g, model& m); void set_exception(std::string const& msg); @@ -104,8 +109,6 @@ namespace smt { batch_manager m_batch_manager; ptr_vector m_workers; - lbool new_check(expr_ref_vector const& asms); - public: parallel(context& ctx) : ctx(ctx), From 4bb139435a340ee45e54b6cc87199da776d1a57d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Aug 2025 10:51:45 -0700 Subject: [PATCH 3/3] simplify output Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index db33cda14..73ff58a2a 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -65,7 +65,7 @@ namespace smt { break; } case l_true: { - std::cout << "Worker " << id << " found sat cube: " << mk_pp(mk_and(cube), m) << "\n"; + std::cout << "Worker " << id << " found sat cube: " << mk_and(cube) << "\n"; model_ref mdl; ctx->get_model(mdl); b.set_sat(l2g, *mdl);