From fd86c779ad5e2c7a67217d5aa678304f8aaeccf7 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Tue, 28 Oct 2025 17:23:51 -0700 Subject: [PATCH] initial parameter probe thread setup in C++ --- src/params/theory_arith_params.cpp | 10 +++++++ src/params/theory_arith_params.h | 5 ++++ src/smt/smt_parallel.cpp | 24 ++++++++++++++--- src/smt/smt_parallel.h | 43 +++++++++++++++++++++++++----- 4 files changed, 72 insertions(+), 10 deletions(-) diff --git a/src/params/theory_arith_params.cpp b/src/params/theory_arith_params.cpp index 27a8949b0..39e520287 100644 --- a/src/params/theory_arith_params.cpp +++ b/src/params/theory_arith_params.cpp @@ -22,6 +22,11 @@ Revision History: void theory_arith_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); + m_nl_arith_delay = p.arith_nl_delay(); + m_nl_arith_expensive_patching = p.arith_nl_expensive_patching(); + m_nl_arith_horner = p.arith_nl_horner(); + m_nl_arith_horner_frequency = p.arith_nl_horner_frequency(); + m_nl_arith_tangents = p.arith_nl_tangents(); m_arith_random_initial_value = p.arith_random_initial_value(); m_arith_random_seed = p.random_seed(); m_arith_mode = static_cast(p.arith_solver()); @@ -102,4 +107,9 @@ void theory_arith_params::display(std::ostream & out) const { DISPLAY_PARAM(m_arith_validate); DISPLAY_PARAM(m_arith_dump_lemmas); DISPLAY_PARAM(m_arith_epsilon); + DISPLAY_PARAM(m_nl_arith_delay); + DISPLAY_PARAM(m_nl_arith_expensive_patching); + DISPLAY_PARAM(m_nl_arith_horner); + DISPLAY_PARAM(m_nl_arith_horner_frequency); + DISPLAY_PARAM(m_nl_arith_tangents); } diff --git a/src/params/theory_arith_params.h b/src/params/theory_arith_params.h index 8329ae1fd..9b2b60b95 100644 --- a/src/params/theory_arith_params.h +++ b/src/params/theory_arith_params.h @@ -112,6 +112,11 @@ struct theory_arith_params { bool m_nl_arith_propagate_linear_monomials = true; bool m_nl_arith_optimize_bounds = true; bool m_nl_arith_cross_nested = true; + unsigned m_nl_arith_delay = 10; + bool m_nl_arith_expensive_patching = false; + bool m_nl_arith_horner = true; + unsigned m_nl_arith_horner_frequency = 4; + bool m_nl_arith_tangents = true; theory_arith_params(params_ref const & p = params_ref()) { updt_params(p); diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index b711394d9..95d3b34b7 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -64,6 +64,10 @@ namespace smt { namespace smt { + void parallel::param_generator::run() { + + } + void parallel::worker::run() { search_tree::node *node = nullptr; expr_ref_vector cube(m); @@ -143,6 +147,16 @@ namespace smt { m_num_initial_atoms = ctx->get_num_bool_vars(); } + parallel::param_generator::param_generator(parallel& p) + : p(p), b(p.m_batch_manager), m_params(p.ctx.get_fparams()), m_p(p.ctx.get_params()) { + ctx = alloc(context, m, m_params, m_p); + context::copy(p.ctx, *ctx, true); + // don't share initial units + ctx->pop_to_base_lvl(); + init_param_state(); + IF_VERBOSE(1, verbose_stream() << "Initialized parameter generator\n"); + } + void parallel::worker::share_units() { // Collect new units learned locally by this worker and send to batch manager ctx->pop_to_base_lvl(); @@ -489,15 +503,19 @@ namespace smt { SASSERT(num_threads > 1); for (unsigned i = 0; i < num_threads; ++i) m_workers.push_back(alloc(worker, i, *this, asms)); - + for (auto w : m_workers) sl.push_child(&(w->limit())); + + sl.push_child(&(m_param_generator.limit())); // Launch threads - vector threads(num_threads); - for (unsigned i = 0; i < num_threads; ++i) { + vector threads(num_threads + 1); // +1 for parameter generator + for (unsigned i = 0; i < num_threads - 1; ++i) { threads[i] = std::thread([&, i]() { m_workers[i]->run(); }); } + // the final thread runs the parameter generator + threads[num_threads - 1] = std::thread([&]() { m_param_generator.run(); }); // Wait for all threads to finish for (auto &th : threads) diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index f3fa7371b..106d413db 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -77,8 +77,6 @@ namespace smt { w->cancel(); } - void init_parameters_state(); - public: batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_search_tree(expr_ref(m)) { } @@ -107,11 +105,40 @@ namespace smt { // 3. pick winner configuration if any are better than current. // 4. update current configuration with the winner - class parameter_generator_thread { - unsigned N; // number of prefix permutation testers - scoped_ptr prefix_solver; - scoped_ptr_vector testers; // N testers + class param_generator { + parallel& p; + batch_manager& b; + ast_manager m; + unsigned N = 4; // number of prefix permutation testers + scoped_ptr m_prefix_solver; + scoped_ptr_vector m_testers; // N testers + smt_params m_params; + params_ref m_p; + scoped_ptr ctx; + + private: + void init_param_state() { + m_params.m_nl_arith_branching = true; + m_params.m_nl_arith_cross_nested = true; + m_params.m_nl_arith_delay = 10; + m_params.m_nl_arith_expensive_patching = false; + m_params.m_nl_arith_gb = true; + m_params.m_nl_arith_horner = true; + m_params.m_nl_arith_horner_frequency = 4; + m_params.m_nl_arith_optimize_bounds = true; + m_params.m_nl_arith_propagate_linear_monomials = true; + m_params.m_nl_arith_tangents = true; + m_params.updt_params(m_p); + ctx->updt_params(m_p); + }; + public: + param_generator(parallel& p); + void run(); + + reslimit& limit() { + return m.limit(); + } }; class worker { @@ -173,6 +200,7 @@ namespace smt { batch_manager m_batch_manager; scoped_ptr_vector m_workers; + param_generator m_param_generator; public: parallel(context& ctx) : @@ -180,7 +208,8 @@ namespace smt { num_threads(std::min( (unsigned)std::thread::hardware_concurrency(), ctx.get_fparams().m_threads)), - m_batch_manager(ctx.m, *this) {} + m_batch_manager(ctx.m, *this), + m_param_generator(*this) {} lbool operator()(expr_ref_vector const& asms); };