Repository navigation
Add Z3 with strategy V5 - #31
Draft
The-Ray-Man wants to merge 26 commits into
Draft
The-Ray-Man wants to merge 26 commits into
The-Ray-Man wants to merge 26 commits into
Conversation
Uses the gh-release build of Z3 and the num feature for arbitrary-precision integer and real literals.
Adds the verify::z3 module with a sort cache covering the builtin types, Option, field/predicate address sorts and ADTs.
FuncRegistry::kind tells whether a FuncId is a declared function, an ADT constructor/projection/tester, a limited twin or a precondition token, so the Z3 translation knows how to encode each application. This first version recovers the kind by searching the registry's maps.
Every e-class becomes a Z3 constant of its exact type and every e-node one equation c_class == [node], covering literals (including big integers and reals), arithmetic, ite, casts and function applications. The translation is a set of free functions over VerifyContext, whose new z3translator field holds the sort and datatype caches, so the e-graph and the caches are never borrowed at the same time.
prove_by_z3 asserts the e-graph facts and the full path condition (block cube plus the instruction's literals) and checks the negated goal; unsat proves it. It runs only after every e-graph tier has failed, and only when SILVER_OXIDE_Z3 is set.
Datatypes are declared on first use, together with every undeclared datatype reachable through their fields in a single create_datatypes call, so recursive and mutually recursive datatypes resolve by name. Constructors and projections translate to the datatype's own constructor and accessor functions, and the per-kind function translation moves into translate_function.
FuncRegistry now records each id's kind as it mints it, so kind() is a map lookup instead of a search over every registry map. FuncRegistry::new now builds on empty(), so the builtin Option ids, names and rules are defined once.
VerifyStats gains a z3_timing trend (not gated), split into building the problem and Solver::check. verify --breakdown prints it and --json includes it.
prove_by_z3 asserts the e-graph facts and the full path condition (block cube plus the instruction's literals) and checks the negated goal; unsat proves it. It runs only after every e-graph tier has failed, and only when SILVER_OXIDE_Z3 is set.
The Z3 rung reported only build and solve wall time. Benchmarking the solver lifecycle needs more: how often the rung runs, what Z3 answers, how many facts it is given, and how much of the time is creating the solver and the FFI assert calls alone. `Z3Timing` gains `init`, `assert`, `calls`, `unsat`, `sat`, `unknown` and `facts`; `build` and `solve` keep their meaning, so older logs stay comparable. All of it is a non-gated trend, like the existing timing fields.
`with_scratch_graph` runs code on a clone of the live e-graph and then restores the live graph. The clone hands out ids past the live graph's, and after the restore those ids are handed out again, for different terms. The persistent solver kept the clone's facts about them, its watermarks pointed past the restored graph (so new nodes below them were never synced), and the class-sort cache kept the clone's sorts. The scratch extent is now a solver scope: `enter_scratch` pushes and saves the watermarks and the sort cache, `leave_scratch` pops and restores them. `z3_timing.scratch_scopes` counts the scopes in which something had to be discarded.
The persistent incremental solver answers most queries in milliseconds but can spend minutes on one (enum_v5_p1 never finished). The solver parameter `timeout` ends such a check as `unknown`, which the rung already treats as "not proven", so it can only lose a proof, never add one. `SILVER_OXIDE_Z3_TIMEOUT_MS` overrides the 2000 ms default.
Replace the 2 s timeout with rlimit 1,500,000 (SILVER_OXIDE_Z3_RLIMIT), the value that best matched 2 s over 2,680 traced checks. The most expensive proof on the benchmark suite used 39,864 units, so no proof is lost, and the verdict no longer depends on machine speed or load.
The same persistent plain solver, but each query's path condition and negated goal are asserted between push and pop instead of passed to check_assumptions. Compared against ramon/add-z3-ladder-step it isolates the effect of the query form on the plain incremental solver.
Set, once per process and before the first context exists, the options from Silicon's z3config.smt2 that change how Z3 solves: auto_config off, MBQI off, the simplex arithmetic solver (smt.arith.solver 2), case_split 3, delay_units, qi.eager_threshold 100 and qi.max_multi_patterns 1000. The options that only concern Silicon's SMT-LIB pipe or how output is printed are left out. A test checks that Z3 accepted every one, since it only warns about an unknown parameter. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This branch has not been deployed
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.
prove_by_z3opens a scope, asserts the path-condition literals and the negated goal, callsSolver::checkand pops the scope.