Skip to content

Commit 2e74175

Browse files
ilanashapirodependabot[bot]CopilotNikolajBjornerlevnach
authored
Debugging param tuning (I think it runs now) (#8012)
* draft attempt at optimizing cube tree with resolvents. have not tested/ran yet * adding comments * fix bug about needing to bubble resolvent upwards to highest ancestor * fix bug where we need to cover the whole resolvent in the path when bubbling up * clean up comments * Bump actions/checkout from 4 to 5 (#7954) Bumps [actions/checkout](https://github.com/actions/checkout) from 4 to 5. - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md) - [Commits](actions/checkout@v4...v5) --- updated-dependencies: - dependency-name: actions/checkout dependency-version: '5' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <[email protected]> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> * close entire tree when sibling resolvent is empty * integrate asms directly into cube tree, remove separate tracking * try to fix bug about redundant resolutions, merging close and try_resolve_upwards into once function * separate the logic again to avoid mutual recursion * [WIP] Add a mutex to warning.cpp to ensure that warning messages from different threads don't interfere (#7963) * Initial plan * Add mutex to warning.cpp for thread safety Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> * Remove unused variable 'first' in mpz.cpp Removed unused variable 'first' from the function. * fixing the order Signed-off-by: Lev Nachmanson <[email protected]> * fixing the order Signed-off-by: Lev Nachmanson <[email protected]> * fix the order of parameter evaluation Signed-off-by: Lev Nachmanson <[email protected]> * remove AI slop Signed-off-by: Nikolaj Bjorner <[email protected]> * param order Signed-off-by: Lev Nachmanson <[email protected]> * param order Signed-off-by: Lev Nachmanson <[email protected]> * param order evaluation * parameter eval order * parameter evaluation order * param eval * param eval order * parameter eval order Signed-off-by: Lev Nachmanson <[email protected]> * parameter eval order Signed-off-by: Lev Nachmanson <[email protected]> * parameter eval order Signed-off-by: Lev Nachmanson <[email protected]> * parameter eval order Signed-off-by: Lev Nachmanson <[email protected]> * parameter eval order Signed-off-by: Lev Nachmanson <[email protected]> * parameter eval order Signed-off-by: Lev Nachmanson <[email protected]> * parameter eval order Signed-off-by: Lev Nachmanson <[email protected]> * Bump github/codeql-action from 3 to 4 (#7971) Bumps [github/codeql-action](https://github.com/github/codeql-action) from 3 to 4. - [Release notes](https://github.com/github/codeql-action/releases) - [Changelog](https://github.com/github/codeql-action/blob/main/CHANGELOG.md) - [Commits](github/codeql-action@v3...v4) --- updated-dependencies: - dependency-name: github/codeql-action dependency-version: '4' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <[email protected]> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> * Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype (#7966) * Initial plan * Update Z3_mk_datatype_sort API to accept array of parameters Co-authored-by: NikolajBjorner <[email protected]> * Update language bindings for parametric datatype sort API - Python: Updated DatatypeSort() to accept optional params list - OCaml: Added mk_sort_ref_p/mk_sort_ref_ps for parametric datatypes - .NET: Added MkDatatypeSortRef() methods with optional params - Java: Added mkDatatypeSortRef() methods with optional params - All changes maintain backward compatibility Co-authored-by: NikolajBjorner <[email protected]> * Fix .NET build error - rename params to parameters The 'params' keyword is reserved in C#, causing compilation errors. Renamed parameter from 'params' to 'parameters' in MkDatatypeSortRef methods. Co-authored-by: NikolajBjorner <[email protected]> * Add unit test for parametric datatypes Added test_parametric_datatype.cpp to demonstrate polymorphic datatypes. The test creates two concrete instantiations of a generic pair concept: - pair_int_real with fields (first:Int, second:Real) - pair_real_int with fields (first:Real, second:Int) Then verifies that accessors work correctly and type checking is enforced. Co-authored-by: NikolajBjorner <[email protected]> * Implement polymorphic type variables support for parametric datatypes - Modified datatype_decl_plugin to allow type variables as parameters - Updated mk_datatype_decl to extract type variables from field sorts - Type variables are collected in order of first appearance - Revised unit test to use Z3_mk_type_variable for polymorphic datatypes - Test creates pair datatype with type variables alpha and beta - Successfully instantiates with concrete types (pair Int Real) and (pair Real Int) - Verifies accessor types match and equality terms are well-typed - All tests pass Co-authored-by: NikolajBjorner <[email protected]> * Add Z3_mk_polymorphic_datatype API and refactor datatype creation - Added new API Z3_mk_polymorphic_datatype to z3_api.h - Renamed static mk_datatype_decl to api_datatype_decl in api_datatype.cpp - Modified api_datatype_decl to accept explicit type parameters - Updated all callers to use renamed function - Added test_polymorphic_datatype_api demonstrating new API usage - Both tests pass successfully Co-authored-by: NikolajBjorner <[email protected]> * Remove type variable collection logic from constructors Removed the logic for collecting type variables from field sorts based on constructors. * Update comments on parameter handling in api_datatype.cpp Clarify usage of parameters in API documentation. * Fix OCaml build error - use list instead of array for mk_datatype_sort Changed mk_sort_ref to pass empty list [] instead of empty array [||]. Changed mk_sort_ref_p to pass params list directly instead of converting to array. Z3native.mk_datatype_sort expects a list, not an array. Co-authored-by: NikolajBjorner <[email protected]> * Add polymorphic datatype example to C++ examples Added polymorphic_datatype_example() demonstrating: - Creating type variables alpha and beta with Z3_mk_type_variable - Defining parametric Pair datatype with fields of type alpha and beta - Instantiating with concrete types (Pair Int Real) and (Pair Real Int) - Getting constructors and accessors from instantiated datatypes - Creating constants and expressions using the polymorphic types - Verifying type correctness with equality (= (first p1) (second p2)) Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> Co-authored-by: Nikolaj Bjorner <[email protected]> * trim parametric datatype test Signed-off-by: Nikolaj Bjorner <[email protected]> * restore single cell Signed-off-by: Lev Nachmanson <[email protected]> * restore the method behavior Signed-off-by: Lev Nachmanson <[email protected]> * setting up python tuning experiment, not done * Add finite_set_value_factory for creating finite set values in model generation (#7981) * Initial plan * Add finite_set_value_factory implementation Co-authored-by: NikolajBjorner <[email protected]> * Remove unused dl_decl_plugin variable and include Co-authored-by: NikolajBjorner <[email protected]> * Update copyright and add TODOs in finite_set_value_factory Updated copyright information and added TODO comments for handling in finite_set_value_factory methods. * Update copyright information in finite_set_value_factory.h Updated copyright year from 2006 to 2025. * Implement finite_set_value_factory using array_util to create singleton sets Co-authored-by: NikolajBjorner <[email protected]> * Simplify empty set creation in finite_set_value_factory Refactor finite_set_value_factory to simplify empty set handling and remove array-specific logic. * Change family ID for finite_set_value_factory * Fix build error by restoring array_decl_plugin include and implementation Co-authored-by: NikolajBjorner <[email protected]> * Update finite_set_value_factory.h * Add SASSERT for finite set check in factory Added assertion to check if the sort is a finite set. * Rename member variable from m_util to u * Refactor finite_set_value_factory for value handling * Use register_value instead of direct set insertion Replaced direct insertion into set with register_value calls. * Update finite_set_value_factory.cpp --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> Co-authored-by: Nikolaj Bjorner <[email protected]> * Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985) This reverts commit 05ffc0a. * Update arith_rewriter.cpp fix memory leak introduced by update to ensure determinism * update pythonnn prototyping experiment, need to add a couple more things * add explicit constructors for nightly mac build failure Signed-off-by: Nikolaj Bjorner <[email protected]> * build fixes Signed-off-by: Nikolaj Bjorner <[email protected]> * fixes * fix some more things but now it hangs * change multithread to multiprocess seems to have resolved current deadlock * fix some bugs, it seems to run now * fix logic about checking clauses individually, and add proof prefix clause selection (naively) via the OnClause hook * disable manylinux until segfault is resolved Signed-off-by: Nikolaj Bjorner <[email protected]> * add the "noexcept" keyword to value_score=(value_score&&) declaration * expose a status flag for clauses but every single one is being coded as an assumption... * Add a fast-path to _coerce_exprs. (#7995) When the inputs are already the same sort, we can skip most of the coercion logic and just return. Currently, `_coerce_exprs` is by far the most expensive part of building up many common Z3 ASTs, so this fast-path is a substantial speedup for many use-cases. * Bump actions/setup-node from 5 to 6 (#7994) Bumps [actions/setup-node](https://github.com/actions/setup-node) from 5 to 6. - [Release notes](https://github.com/actions/setup-node/releases) - [Commits](actions/setup-node@v5...v6) --- updated-dependencies: - dependency-name: actions/setup-node dependency-version: '6' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <[email protected]> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> * Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988) * Enabling Control Flow Guard by default for MSVC on Windows, with options to disable it. * Fix configuration error for non-MSVC compilers. * Reviewed and updated configuration for Python build and added comment for CFG. * try exponential delay in grobner Signed-off-by: Lev Nachmanson <[email protected]> * throttle grobner method more actively Signed-off-by: Lev Nachmanson <[email protected]> * enable always add all coeffs in nlsat Signed-off-by: Lev Nachmanson <[email protected]> * initial parameter probe thread setup in C++ * more param tuning setup * setting up the param probe solvers and mutation generator * adding the learned clauses from the internalizer * fix some things for clause replay * score the param probes, but i can't figure out how to access the relevant solver statistics fields from the statistics obj * set up pattern to notify batch manager so worker threads can update their params according ly * add a getter for solver stats. it compiles but still everything is untested * bugfix * updates to param tuning * remove the getter for solver statistics since we're getting the vals directly from the context * merge * patch fix for default manager construction so it can be used to create the param tuning context without segfault * still debugging threading issues where we can't create nested param tuners or it spins infinitely. added flag for this. but now there is segfault on the probe_ctx.check() call * make param tuning singlethreaded to resolve segfault when spawning subprocesses ffor nested ctx checks --------- Signed-off-by: dependabot[bot] <[email protected]> Signed-off-by: Lev Nachmanson <[email protected]> Signed-off-by: Nikolaj Bjorner <[email protected]> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> Co-authored-by: Copilot <[email protected]> Co-authored-by: NikolajBjorner <[email protected]> Co-authored-by: Nikolaj Bjorner <[email protected]> Co-authored-by: Lev Nachmanson <[email protected]> Co-authored-by: Nelson Elhage <[email protected]> Co-authored-by: hwisungi <[email protected]>
1 parent 863d0e3 commit 2e74175

File tree

5 files changed

+78
-36
lines changed

5 files changed

+78
-36
lines changed

‎src/smt/smt_context.cpp‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3617,15 +3617,15 @@ namespace smt {
36173617
\remark A logical context can only be configured at scope level 0,
36183618
and before internalizing any formulas.
36193619
*/
3620-
lbool context::setup_and_check(bool reset_cancel) {
3620+
lbool context::setup_and_check(bool reset_cancel, bool enable_parallel_param_tuning) {
36213621
if (!check_preamble(reset_cancel)) return l_undef;
36223622
SASSERT(m_scope_lvl == 0);
36233623
SASSERT(!m_setup.already_configured());
36243624
setup_context(m_fparams.m_auto_config);
36253625

36263626
if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {
3627-
parallel p(*this);
36283627
expr_ref_vector asms(m);
3628+
parallel p(*this, enable_parallel_param_tuning);
36293629
return p(asms);
36303630
}
36313631

@@ -3685,14 +3685,15 @@ namespace smt {
36853685
}
36863686
}
36873687

3688-
lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel) {
3688+
lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel, bool enable_parallel_param_tuning) {
36893689
if (!check_preamble(reset_cancel)) return l_undef;
36903690
SASSERT(at_base_level());
36913691
setup_context(false);
36923692
search_completion sc(*this);
36933693
if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {
36943694
expr_ref_vector asms(m, num_assumptions, assumptions);
3695-
parallel p(*this);
3695+
IF_VERBOSE(1, verbose_stream() << "Starting parallel check with " << asms.size() << " assumptions and param tuning enabled: " << enable_parallel_param_tuning << "\n");
3696+
parallel p(*this, enable_parallel_param_tuning);
36963697
return p(asms);
36973698
}
36983699
lbool r = l_undef;

‎src/smt/smt_context.h‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -132,6 +132,7 @@ namespace smt {
132132
unsigned m_par_index = 0;
133133
bool m_internalizing_assertions = false;
134134
lbool m_internal_completed = l_undef;
135+
bool m_in_parallel = false;
135136

136137
scoped_ptr<dependent_expr_simplifier> m_simplifier;
137138
scoped_ptr<base_dependent_expr_state> m_fmls;
@@ -1689,7 +1690,7 @@ namespace smt {
16891690

16901691
void pop(unsigned num_scopes);
16911692

1692-
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true);
1693+
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true, bool enable_parallel_param_tuning = true);
16931694

16941695
lbool check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses);
16951696

@@ -1699,7 +1700,7 @@ namespace smt {
16991700

17001701
lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
17011702

1702-
lbool setup_and_check(bool reset_cancel = true);
1703+
lbool setup_and_check(bool reset_cancel = true, bool enable_parallel_param_tuning = true);
17031704

17041705
void reduce_assertions();
17051706

‎src/smt/smt_internalizer.cpp‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -990,7 +990,8 @@ namespace smt {
990990

991991

992992
void context::undo_mk_bool_var() {
993-
SASSERT(!m_b_internalized_stack.empty());
993+
SASSERT(!m_b_internalized_stack.empty(ue key per literal
994+
m_lit_scores[lit.sign()][v] += 1.));
994995
m_stats.m_num_del_bool_var++;
995996
expr * n = m_b_internalized_stack.back();
996997
unsigned n_id = n->get_id();

‎src/smt/smt_parallel.cpp‎

Lines changed: 47 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -66,13 +66,18 @@ namespace smt {
6666
namespace smt {
6767

6868
lbool parallel::param_generator::run_prefix_step() {
69-
IF_VERBOSE(1, verbose_stream() << " Param generator running prefix step\n");
69+
if (m.limit().is_canceled())
70+
return l_undef;
71+
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER running prefix step\n");
7072
ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts;
73+
ctx->get_fparams().m_threads = 1;
74+
7175
m_recorded_cubes.reset();
7276
ctx->m_recorded_cubes = &m_recorded_cubes;
7377
lbool r = l_undef;
7478
try {
75-
r = ctx->check();
79+
r = ctx->check(0, nullptr, true, false);
80+
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER: prefix step result " << r << "\n");
7681
}
7782
catch (z3_error &err) {
7883
b.set_exception(err.error_code());
@@ -93,8 +98,11 @@ namespace smt {
9398
bool found_better_params = false;
9499

95100
for (unsigned i = 0; i <= N; ++i) {
96-
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER: replaying proof prefix in param probe context " << i << "\n");
101+
if (m.limit().is_canceled())
102+
return;
97103

104+
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER: replaying proof prefix in param probe context " << i << "\n");
105+
98106
// copy prefix solver context to a new probe_ctx for next replay with candidate mutation
99107
smt_params smtp(m_p);
100108
scoped_ptr<context> probe_ctx = alloc(context, m, smtp, m_p);
@@ -110,11 +118,16 @@ namespace smt {
110118
}
111119

112120
probe_ctx->get_fparams().m_max_conflicts = conflict_budget;
121+
probe_ctx->get_fparams().m_threads = 1;
113122

114123
// replay the cube (negation of the clause)
124+
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER: begin replay of " << m_recorded_cubes.size() << " cubes\n");
115125
for (expr_ref_vector const& cube : m_recorded_cubes) {
116-
lbool r = probe_ctx->check(cube.size(), cube.data());
117-
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER " << i << ": cube replay result " << r << "\n");
126+
if (m.limit().is_canceled())
127+
return;
128+
// the conflicts and decisions are cumulative over all cube replays inside the probe_ctx
129+
lbool r = probe_ctx->check(cube.size(), cube.data(), true, false);
130+
IF_VERBOSE(2, verbose_stream() << " PARAM TUNER " << i << ": cube replay result " << r << "\n");
118131
}
119132
unsigned conflicts = probe_ctx->m_stats.m_num_conflicts;
120133
unsigned decisions = probe_ctx->m_stats.m_num_decisions;
@@ -130,10 +143,7 @@ namespace smt {
130143
best_score = score;
131144
}
132145
}
133-
// NOTE: we either need to apply the best params found that are better than base line
134-
// or, we have to implement a comparison operator for param_values (what would this do?)
135-
// or, we update the param state every single time even if it hasn't changed (what would this do?)
136-
// for now, I went with option 1
146+
137147
if (found_better_params) {
138148
m_param_state = best_param_state;
139149
auto p = apply_param_values(m_param_state);
@@ -192,7 +202,8 @@ namespace smt {
192202
}
193203
std::get<unsigned_value>(param.second).value = new_value;
194204
}
195-
IF_VERBOSE(0,
205+
IF_VERBOSE(1,
206+
verbose_stream() << "Mutating param: ";
196207
for (auto const &[name, val] : new_param_values) {
197208
if (std::holds_alternative<bool>(val)) {
198209
verbose_stream() << name << " = " << std::get<bool>(val) << "\n";
@@ -211,6 +222,9 @@ namespace smt {
211222
ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts;
212223
lbool r = run_prefix_step();
213224

225+
if (m.limit().is_canceled())
226+
return;
227+
214228
switch (r) {
215229
case l_undef: {
216230
replay_proof_prefixes();
@@ -234,6 +248,11 @@ namespace smt {
234248
}
235249
}
236250

251+
void parallel::param_generator::cancel() {
252+
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER cancelling\n");
253+
m.limit().cancel();
254+
}
255+
237256
void parallel::worker::run() {
238257
search_tree::node<cube_config> *node = nullptr;
239258
expr_ref_vector cube(m);
@@ -255,7 +274,7 @@ namespace smt {
255274

256275
lbool r = check_cube(cube);
257276

258-
if (!m.inc()) {
277+
if (m.limit().is_canceled()) {
259278
b.set_exception("context cancelled");
260279
return;
261280
}
@@ -320,7 +339,11 @@ namespace smt {
320339
}
321340

322341
parallel::param_generator::param_generator(parallel& p)
323-
: p(p), b(p.m_batch_manager), m_p(p.ctx.get_params()), m_l2g(m, p.ctx.m) {
342+
: b(p.m_batch_manager), m_p(p.ctx.get_params()), m_l2g(m, p.ctx.m) {
343+
// patch fix so that ctx = alloc(context, m, p.ctx.get_fparams(), m_p); doesn't crash due to some issue with default construction of m
344+
ast_translation m_g2l(p.ctx.m, m);
345+
m_g2l(p.ctx.m.mk_true());
346+
324347
ctx = alloc(context, m, p.ctx.get_fparams(), m_p);
325348
context::copy(p.ctx, *ctx, true);
326349
// don't share initial units
@@ -450,7 +473,7 @@ namespace smt {
450473
IF_VERBOSE(1, m_search_tree.display(verbose_stream() << bounded_pp_exprs(core) << "\n"););
451474
if (m_search_tree.is_closed()) {
452475
m_state = state::is_unsat;
453-
cancel_workers();
476+
cancel_background_threads();
454477
}
455478
}
456479

@@ -516,7 +539,7 @@ namespace smt {
516539
<< bounded_pp_exprs(cube)
517540
<< "with max_conflicts: " << ctx->get_fparams().m_max_conflicts << "\n";);
518541
try {
519-
r = ctx->check(asms.size(), asms.data());
542+
r = ctx->check(asms.size(), asms.data(), true, false);
520543
} catch (z3_error &err) {
521544
b.set_exception(err.error_code());
522545
} catch (z3_exception &ex) {
@@ -561,7 +584,7 @@ namespace smt {
561584
return;
562585
m_state = state::is_sat;
563586
p.ctx.set_model(m.translate(l2g));
564-
cancel_workers();
587+
cancel_background_threads();
565588
}
566589

567590
void parallel::batch_manager::set_unsat(ast_translation &l2g, expr_ref_vector const &unsat_core) {
@@ -575,7 +598,7 @@ namespace smt {
575598
SASSERT(p.ctx.m_unsat_core.empty());
576599
for (expr *e : unsat_core)
577600
p.ctx.m_unsat_core.push_back(l2g(e));
578-
cancel_workers();
601+
cancel_background_threads();
579602
}
580603

581604
void parallel::batch_manager::set_exception(unsigned error_code) {
@@ -585,7 +608,7 @@ namespace smt {
585608
return;
586609
m_state = state::is_exception_code;
587610
m_exception_code = error_code;
588-
cancel_workers();
611+
cancel_background_threads();
589612
}
590613

591614
void parallel::batch_manager::set_exception(std::string const &msg) {
@@ -595,7 +618,7 @@ namespace smt {
595618
return;
596619
m_state = state::is_exception_msg;
597620
m_exception_msg = msg;
598-
cancel_workers();
621+
cancel_background_threads();
599622
}
600623

601624
lbool parallel::batch_manager::get_result() const {
@@ -675,6 +698,7 @@ namespace smt {
675698

676699
m_batch_manager.initialize();
677700
m_workers.reset();
701+
678702
scoped_limits sl(m.limit());
679703
flet<unsigned> _nt(ctx.m_fparams.m_threads, 1);
680704
SASSERT(num_threads > 1);
@@ -684,15 +708,16 @@ namespace smt {
684708
for (auto w : m_workers)
685709
sl.push_child(&(w->limit()));
686710

687-
sl.push_child(&(m_param_generator.limit()));
711+
sl.push_child(&(m_param_generator->limit()));
688712

689713
// Launch threads
690-
vector<std::thread> threads(num_threads + 1); // +1 for parameter generator
691-
for (unsigned i = 0; i < num_threads - 1; ++i) {
714+
vector<std::thread> threads(m_enable_param_tuner ? num_threads + 1 : num_threads); // +1 for param generator
715+
for (unsigned i = 0; i < num_threads; ++i) {
692716
threads[i] = std::thread([&, i]() { m_workers[i]->run(); });
693717
}
694718
// the final thread runs the parameter generator
695-
threads[num_threads - 1] = std::thread([&]() { m_param_generator.protocol_iteration(); });
719+
if (m_enable_param_tuner)
720+
threads[num_threads] = std::thread([&]() { m_param_generator->protocol_iteration(); });
696721

697722
// Wait for all threads to finish
698723
for (auto &th : threads)

‎src/smt/smt_parallel.h‎

Lines changed: 21 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ namespace smt {
3636
class parallel {
3737
context& ctx;
3838
unsigned num_threads;
39+
bool m_enable_param_tuner;
3940

4041
struct shared_clause {
4142
unsigned source_worker_id;
@@ -57,7 +58,6 @@ namespace smt {
5758
unsigned m_num_cubes = 0;
5859
};
5960

60-
6161
ast_manager& m;
6262
parallel& p;
6363
std::mutex mux;
@@ -72,13 +72,23 @@ namespace smt {
7272
vector<shared_clause> shared_clause_trail; // store all shared clauses with worker IDs
7373
obj_hashtable<expr> shared_clause_set; // for duplicate filtering on per-thread clause expressions
7474

75+
void cancel_background_threads() {
76+
cancel_workers();
77+
cancel_param_generator();
78+
}
79+
7580
// called from batch manager to cancel other workers if we've reached a verdict
7681
void cancel_workers() {
7782
IF_VERBOSE(1, verbose_stream() << "Canceling workers\n");
7883
for (auto& w : p.m_workers)
7984
w->cancel();
8085
}
8186

87+
void cancel_param_generator() {
88+
IF_VERBOSE(1, verbose_stream() << "Canceling param generator\n");
89+
p.m_param_generator->cancel();
90+
}
91+
8292
public:
8393
batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_search_tree(expr_ref(m)) { }
8494

@@ -88,7 +98,10 @@ namespace smt {
8898
void set_sat(ast_translation& l2g, model& m);
8999
void set_exception(std::string const& msg);
90100
void set_exception(unsigned error_code);
91-
void set_param_state(params_ref const& p) { m_param_state.copy(p); }
101+
void set_param_state(params_ref const& p) {
102+
m_param_state.copy(p);
103+
IF_VERBOSE(1, verbose_stream() << "Batch manager updated param state\n");
104+
}
92105
void get_param_state(params_ref &p);
93106
void collect_statistics(::statistics& st) const;
94107

@@ -118,11 +131,9 @@ namespace smt {
118131
using param_value = std::variant<unsigned_value, bool>;
119132
using param_values = vector<std::pair<symbol, param_value>>;
120133

121-
parallel &p;
122134
batch_manager &b;
123135
ast_manager m;
124136
scoped_ptr<context> ctx;
125-
ast_translation m_l2g;
126137

127138
unsigned N = 4; // number of prefix permutations to test (including current)
128139
unsigned m_max_prefix_conflicts = 1000;
@@ -131,6 +142,7 @@ namespace smt {
131142
vector<expr_ref_vector> m_recorded_cubes;
132143
params_ref m_p;
133144
param_values m_param_state;
145+
ast_translation m_l2g;
134146

135147
params_ref apply_param_values(param_values const &pv);
136148
void init_param_state();
@@ -141,6 +153,7 @@ namespace smt {
141153
lbool run_prefix_step();
142154
void protocol_iteration();
143155
void replay_proof_prefixes(unsigned max_conflicts_epsilon);
156+
void cancel();
144157

145158
reslimit &limit() {
146159
return m.limit();
@@ -206,16 +219,17 @@ namespace smt {
206219

207220
batch_manager m_batch_manager;
208221
scoped_ptr_vector<worker> m_workers;
209-
param_generator m_param_generator;
222+
scoped_ptr<param_generator> m_param_generator;
210223

211224
public:
212-
parallel(context& ctx) :
225+
parallel(context& ctx, bool enable_param_tuner = true) :
213226
ctx(ctx),
214227
num_threads(std::min(
215228
(unsigned)std::thread::hardware_concurrency(),
216229
ctx.get_fparams().m_threads)),
230+
m_enable_param_tuner(enable_param_tuner),
217231
m_batch_manager(ctx.m, *this),
218-
m_param_generator(*this) {}
232+
m_param_generator(enable_param_tuner ? alloc(param_generator, *this) : nullptr) {}
219233

220234
lbool operator()(expr_ref_vector const& asms);
221235
};

0 commit comments

Comments
 (0)