Merged
Conversation
…#7743 Signed-off-by: Nikolaj Bjorner <[email protected]>
Signed-off-by: Nikolaj Bjorner <[email protected]>
…pressions Signed-off-by: Nikolaj Bjorner <[email protected]>
Signed-off-by: Nikolaj Bjorner <[email protected]>
axioms for len(substr(...)) escaped due to nested rewriting
add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification.
Signed-off-by: Nikolaj Bjorner <[email protected]>
add pre-processing simplification
fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop.
…digm, need to debug as I am getting segfault still
…collecting shared lits" This reverts commit bba1111.
Signed-off-by: Nikolaj Bjorner <[email protected]>
…7782) * Initial plan * Fix Z3_solver_translate to use solver factory translate method Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]>
This reverts commit c8e866f.
Signed-off-by: Nikolaj Bjorner <[email protected]>
…tement (Z3Prover#7785) * Initial plan * Fix compilation warning: add missing is_passive_eq case to switch statement Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]>
* Initial plan * Remove NugetPublishNightly stage from nightly.yaml Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]>
Signed-off-by: Nikolaj Bjorner <[email protected]>
…3Prover#7790) * Initial plan * Fix nullptr dereference in pp_symbol with null symbol names Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]>
Z3Prover#7791 reports on using model values during lex optimization that break soft constraints. This is an artifact of using optimization where optimal values can be arbitrarily close to a rational. In a way it is by design, but we give the user now an option to control the starting point for epsilon when converting infinitesimals into rationals.
add missing revert operations
Signed-off-by: Nikolaj Bjorner <[email protected]>
Signed-off-by: Nikolaj Bjorner <[email protected]>
* Initial plan * Create VERSION.txt and update CMakeLists.txt to read version from file Co-authored-by: NikolajBjorner <[email protected]> * Complete centralized version management system Co-authored-by: NikolajBjorner <[email protected]> * Fix version update script and finalize implementation Co-authored-by: NikolajBjorner <[email protected]> * Create centralized version management with VERSION.txt Co-authored-by: NikolajBjorner <[email protected]> --------- Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: NikolajBjorner <[email protected]>
Signed-off-by: Nikolaj Bjorner <[email protected]>
Signed-off-by: Nikolaj Bjorner <[email protected]>
Signed-off-by: Nikolaj Bjorner <[email protected]>
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
add a simple python experiment for param tuning