From f1083647966d61f07bd08fa9b9ad11f53f508830 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Fri, 31 Oct 2025 00:10:44 -0700 Subject: [PATCH] Updates to param tuning (#8008) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 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](https://github.com/actions/checkout/compare/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] 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 <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> * Remove unused variable 'first' in mpz.cpp Removed unused variable 'first' from the function. * fixing the order Signed-off-by: Lev Nachmanson * fixing the order Signed-off-by: Lev Nachmanson * fix the order of parameter evaluation Signed-off-by: Lev Nachmanson * remove AI slop Signed-off-by: Nikolaj Bjorner * param order Signed-off-by: Lev Nachmanson * param order Signed-off-by: Lev Nachmanson * param order evaluation * parameter eval order * parameter evaluation order * param eval * param eval order * parameter eval order Signed-off-by: Lev Nachmanson * parameter eval order Signed-off-by: Lev Nachmanson * parameter eval order Signed-off-by: Lev Nachmanson * parameter eval order Signed-off-by: Lev Nachmanson * parameter eval order Signed-off-by: Lev Nachmanson * parameter eval order Signed-off-by: Lev Nachmanson * parameter eval order Signed-off-by: Lev Nachmanson * 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](https://github.com/github/codeql-action/compare/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] 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 <3085284+NikolajBjorner@users.noreply.github.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> * 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 <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> Co-authored-by: Nikolaj Bjorner * trim parametric datatype test Signed-off-by: Nikolaj Bjorner * restore single cell Signed-off-by: Lev Nachmanson * restore the method behavior Signed-off-by: Lev Nachmanson * 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 <3085284+NikolajBjorner@users.noreply.github.com> * Remove unused dl_decl_plugin variable and include Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> * 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 <3085284+NikolajBjorner@users.noreply.github.com> * 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] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner * Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985) This reverts commit 05ffc0a77be2c565d09c9bc12bc0a35fd61bbe80. * 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 * build fixes Signed-off-by: Nikolaj Bjorner * 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 * 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](https://github.com/actions/setup-node/compare/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] 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 * throttle grobner method more actively Signed-off-by: Lev Nachmanson * enable always add all coeffs in nlsat Signed-off-by: Lev Nachmanson * 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 --------- Signed-off-by: dependabot[bot] Signed-off-by: Lev Nachmanson Signed-off-by: Nikolaj Bjorner Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner Co-authored-by: Lev Nachmanson Co-authored-by: Nelson Elhage Co-authored-by: hwisungi --- src/smt/smt_context.h | 4 +- src/smt/smt_internalizer.cpp | 20 +++++--- src/smt/smt_parallel.cpp | 95 ++++++++++++++---------------------- src/smt/smt_parallel.h | 33 +++++-------- 4 files changed, 64 insertions(+), 88 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 198c099a0..63df29d29 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -137,7 +137,7 @@ namespace smt { scoped_ptr m_fmls; svector m_lit_scores[2]; - vector m_recorded_clauses; + vector m_recorded_cubes; // ----------------------------------- @@ -1302,7 +1302,7 @@ namespace smt { void add_scores(unsigned n, literal const *lits); - void record_clause(unsigned n, literal const * lits); + void record_cube(unsigned n, literal const * lits); // ----------------------------------- diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 1b2b7a65d..6aa17d0b9 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -966,10 +966,17 @@ namespace smt { } // following the pattern of solver::persist_clause in src/sat/smt/user_solver.cpp - void context::record_clause(unsigned num_lits, literal const *lits) { - literal_vector clause; - clause.append(num_lits, lits); - m_recorded_clauses.push_back(clause); + void context::record_cube(unsigned num_lits, literal const *lits) { + expr_ref_vector cube(m); + for (unsigned i = 0; i < num_lits; ++i) { + literal lit = lits[i]; + expr* e = bool_var2expr(lit.var()); + if (!e) continue; + if (!lit.sign()) + e = m.mk_not(e); // only negate positive literal + cube.push_back(e); + } + m_recorded_cubes.push_back(cube); } void context::add_scores(unsigned n, literal const *lits) { @@ -981,7 +988,8 @@ namespace smt { void context::undo_mk_bool_var() { - SASSERT(!m_b_internalized_stack.empty()); + SASSERT(!m_b_internalized_stack.empty(ue key per literal + m_lit_scores[lit.sign()][v] += 1.)); m_stats.m_num_del_bool_var++; expr * n = m_b_internalized_stack.back(); unsigned n_id = n->get_id(); @@ -1439,7 +1447,7 @@ namespace smt { case CLS_LEARNED: dump_lemma(num_lits, lits); add_scores(num_lits, lits); - record_clause(num_lits, lits); + record_cube(num_lits, lits); break; default: break; diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 96de76217..59c01a30d 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -83,36 +83,34 @@ namespace smt { return r; } - unsigned parallel::param_generator::replay_proof_prefixes(vector const& candidate_param_states, unsigned max_conflicts_epsilon=200) { + std::pair parallel::param_generator::replay_proof_prefixes(unsigned max_conflicts_epsilon=200) { unsigned conflict_budget = m_max_prefix_conflicts + max_conflicts_epsilon; - unsigned best_param_state_idx; + param_values best_param_state; double best_score; + bool found_better_params = false; - for (unsigned i = 0; i < m_param_probe_contexts.size(); ++i) { + for (unsigned i = 0; i < N; ++i) { IF_VERBOSE(1, verbose_stream() << " PARAM TUNER: replaying proof prefix in param probe context " << i << "\n"); - context *probe_ctx = m_param_probe_contexts[i]; + + // copy prefix solver context to a new probe_ctx for next replay with candidate mutation + scoped_ptr probe_ctx = alloc(context, m, ctx->get_fparams(), m_p); + context::copy(*ctx, *probe_ctx, true); + + // apply a candidate (mutated) param state to probe_ctx + // (except for the first iteration, use the current param state) + param_values mutated_param_state = m_param_state; + if (i > 0) { + mutated_param_state = mutate_param_state(); + params_ref p = apply_param_values(mutated_param_state); + probe_ctx->updt_params(p); + } + probe_ctx->get_fparams().m_max_conflicts = conflict_budget; double score = 0.0; - // apply the ith param state to probe_ctx - params_ref p = apply_param_values(candidate_param_states[i]); - probe_ctx->updt_params(p); - - // todo: m_recorded_cubes as a expr_ref_vector - - for (auto const& clause : probe_ctx->m_recorded_clauses) { - expr_ref_vector negated_lits(probe_ctx->m); - for (literal lit : clause) { - expr* e = probe_ctx->bool_var2expr(lit.var()); - if (!e) continue; // skip if var not yet mapped - if (!lit.sign()) - e = probe_ctx->m.mk_not(e); // since bool_var2expr discards sign - negated_lits.push_back(e); - } - - // Replay the negated clause - - lbool r = probe_ctx->check(negated_lits.size(), negated_lits.data()); + // replay the cube (negation of the clause) + for (expr_ref_vector const& cube : probe_ctx->m_recorded_cubes) { + lbool r = probe_ctx->check(cube.size(), cube.data()); unsigned conflicts = probe_ctx->m_stats.m_num_conflicts; unsigned decisions = probe_ctx->m_stats.m_num_decisions; @@ -120,13 +118,16 @@ namespace smt { score += conflicts + decisions; } - if (i == 0 || score < best_score) { + if (i > 0 && score < best_score) { + found_better_params = true; + best_param_state = mutated_param_state; + best_score = score; + } else { best_score = score; - best_param_state_idx = i; } } - return best_param_state_idx; + return {best_param_state, found_better_params}; } void parallel::param_generator::init_param_state() { @@ -147,7 +148,6 @@ namespace smt { }; parallel::param_generator::param_values parallel::param_generator::mutate_param_state() { - param_values new_param_values(m_param_state); unsigned index = ctx->get_random_value() % new_param_values.size(); auto ¶m = new_param_values[index]; @@ -168,41 +168,23 @@ namespace smt { void parallel::param_generator::protocol_iteration() { IF_VERBOSE(1, verbose_stream() << " PARAM TUNER running protocol iteration\n"); - ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts; - - // copy current param state to all param probe contexts, before running the next prefix step - // this ensures that each param probe context replays the prefix from the same configuration - - // instead just one one context and reset it each time before copy. - for (unsigned i = 0; i < m_param_probe_contexts.size(); ++i) { - context::copy(*ctx, *m_param_probe_contexts[i], true); - } + ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts; lbool r = run_prefix_step(); switch (r) { case l_undef: { - // TODO, change from smt_params to a generic param state representation based on params_ref - // only params_ref have effect on updates. - param_values best_param_state = m_param_state; - vector candidate_param_states; + auto [best_param_state, found_better_params] = replay_proof_prefixes(); - // you can create the mutations on the fly and get the scores - // you don't have to copy all over each tester. - - - candidate_param_states.push_back(best_param_state); // first candidate param state is current best - while (candidate_param_states.size() <= N) { - candidate_param_states.push_back(mutate_param_state()); - } - - unsigned best_param_state_idx = replay_proof_prefixes(candidate_param_states); - - if (best_param_state_idx != 0) { - m_param_state = candidate_param_states[best_param_state_idx]; + // NOTE: we either need to return a pair from replay_proof_prefixes so we can return a boolean flag indicating whether better params were found. + // or, we have to implement a comparison operator for param_values + // or, we update the param state every single time even if it hasn't changed + // for now, I went with option 1 + if (found_better_params) { + m_param_state = best_param_state; auto p = apply_param_values(m_param_state); b.set_param_state(p); - IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found better param state at index " << best_param_state_idx << "\n"); + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found better param state\n"); } else { IF_VERBOSE(1, verbose_stream() << " PARAM TUNER retained current param state\n"); } @@ -315,11 +297,6 @@ namespace smt { : p(p), b(p.m_batch_manager), m_p(p.ctx.get_params()), m_l2g(m, p.ctx.m) { ctx = alloc(context, m, p.ctx.get_fparams(), m_p); context::copy(p.ctx, *ctx, true); - - for (unsigned i = 0; i < N; ++i) { - m_param_probe_contexts.push_back(alloc(context, m, ctx->get_fparams(), m_p)); - } - // don't share initial units ctx->pop_to_base_lvl(); init_param_state(); diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 1e9c6cdaf..fab6029ab 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -21,30 +21,12 @@ Revision History: #include "smt/smt_context.h" #include "util/search_tree.h" #include -// #include "util/util.h" #include #include namespace smt { - inline bool operator==(const smt_params& a, const smt_params& b) { - return a.m_nl_arith_branching == b.m_nl_arith_branching && - a.m_nl_arith_cross_nested == b.m_nl_arith_cross_nested && - a.m_nl_arith_delay == b.m_nl_arith_delay && - a.m_nl_arith_expensive_patching == b.m_nl_arith_expensive_patching && - a.m_nl_arith_gb == b.m_nl_arith_gb && - a.m_nl_arith_horner == b.m_nl_arith_horner && - a.m_nl_arith_horner_frequency == b.m_nl_arith_horner_frequency && - a.m_nl_arith_optimize_bounds == b.m_nl_arith_optimize_bounds && - a.m_nl_arith_propagate_linear_monomials == b.m_nl_arith_propagate_linear_monomials && - a.m_nl_arith_tangents == b.m_nl_arith_tangents; - } - - inline bool operator!=(const smt_params& a, const smt_params& b) { - return !(a == b); - } - struct cube_config { using literal = expr_ref; static bool literal_is_null(expr_ref const& l) { return l == nullptr; } @@ -151,9 +133,18 @@ namespace smt { param_values m_param_state; params_ref apply_param_values(param_values const &pv) { - return m_p; + params_ref p = m_p; + for (auto const& [k, v] : pv) { + if (std::holds_alternative(v)) { + unsigned_value uv = std::get(v); + p.set_uint(k, uv.value); + } else if (std::holds_alternative(v)) { + bool bv = std::get(v); + p.set_bool(k, bv); + } + } + return p; } - // todo private: void init_param_state(); @@ -164,7 +155,7 @@ namespace smt { param_generator(parallel &p); lbool run_prefix_step(); void protocol_iteration(); - unsigned replay_proof_prefixes(vector const& candidate_param_states, unsigned max_conflicts_epsilon); + std::pair replay_proof_prefixes(unsigned max_conflicts_epsilon); reslimit &limit() { return m.limit();