Updates to param tuning #8008
Merged
Updates to param tuning #8008
+65
−89
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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>
…olve_upwards into once function
… different threads don't interfere (Z3Prover#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]>
Removed unused variable 'first' from the function.
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Nikolaj Bjorner <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Nikolaj Bjorner <[email protected]>
…as an assumption...
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.
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>
…h options to disable CFG. (Z3Prover#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.
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
…vant solver statistics fields from the statistics obj
…heir params according ly
ilanashapiro
commented
Oct 31, 2025
Comment on lines
+179
to
+182
| // 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 |
There was a problem hiding this comment.
see comment (I know this is likely not ideal and will need to be changed)
ilanashapiro
commented
Oct 31, 2025
| } | ||
|
|
||
| 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) { |
There was a problem hiding this comment.
see the other comment I left below about this
…directly from the context
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
debug some things
instead of saving many contexts in candidate_param_states, create a throwaway context for each tester on the fly
also create the mutation on the fly for each tester
in smt_internalizer, change m_recorded_clauses to m_recorded_cubes. m_recorded_cubes is of type vector<expr_ref_vector> (i.e. a vector of cubes, where each cube is an expr_ref_vector) since i couldn't figure out how to pass in an expr_ref to ctx->check