Updates to param tuning (#8008)

ilanashapiro · dependabot[bot] · Copilot · web-flow · commit f1083647966d · 2025-10-31T00:10:44.000-07:00
* 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] <support@github.com> 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 <levnach@hotmail.com> * fixing the order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix the order of parameter evaluation Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove AI slop Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * param order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * param order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * param order evaluation * parameter eval order * parameter evaluation order * param eval * param eval order * parameter eval order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * parameter eval order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * parameter eval order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * parameter eval order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * parameter eval order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * parameter eval order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * parameter eval order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * 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] <support@github.com> 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 <nbjorner@microsoft.com> * trim parametric datatype test Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * restore single cell Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * restore the method behavior Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * 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 <nbjorner@microsoft.com> * 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 <nbjorner@microsoft.com> * build fixes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * 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 <nbjorner@microsoft.com> * 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] <support@github.com> 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 <levnach@hotmail.com> * throttle grobner method more actively Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * enable always add all coeffs in nlsat Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * 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] <support@github.com> Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> 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 <nbjorner@microsoft.com> Co-authored-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Nelson Elhage <nelhage@nelhage.com> Co-authored-by: hwisungi <hwisungi@users.noreply.github.com>
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
@@ -137,7 +137,7 @@ namespace smt {
         scoped_ptr<base_dependent_expr_state> m_fmls;
 
         svector<double> m_lit_scores[2];
-        vector<literal_vector> m_recorded_clauses;
+        vector<expr_ref_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
@@ -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
@@ -83,50 +83,51 @@ namespace smt {
         return r;
     }
 
-    unsigned parallel::param_generator::replay_proof_prefixes(vector<param_values> const& candidate_param_states, unsigned max_conflicts_epsilon=200) {
+    std::pair<parallel::param_generator::param_values, bool> 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];
-            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
+            // copy prefix solver context to a new probe_ctx for next replay with candidate mutation
+            scoped_ptr<context> 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);
+            }
 
-            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);
-                }
+            probe_ctx->get_fparams().m_max_conflicts = conflict_budget;
+            double score = 0.0;
 
-                // 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;
 
                 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 &param = 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<param_values> candidate_param_states;
-
-                // 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];
+                auto [best_param_state, found_better_params] = replay_proof_prefixes();
+
+                // 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
@@ -21,30 +21,12 @@ Revision History:
 #include "smt/smt_context.h"
 #include "util/search_tree.h"
 #include <variant>
-// #include "util/util.h"
 #include <thread>
 #include <mutex>
 
 
 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<unsigned_value>(v)) {
+                        unsigned_value uv = std::get<unsigned_value>(v);
+                        p.set_uint(k, uv.value);
+                    } else if (std::holds_alternative<bool>(v)) {
+                        bool bv = std::get<bool>(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<param_values> const& candidate_param_states, unsigned max_conflicts_epsilon);
+            std::pair<parallel::param_generator::param_values, bool> replay_proof_prefixes(unsigned max_conflicts_epsilon);
 
             reslimit &limit() {
                 return m.limit();
