Add Z3 with strategy V1 by The-Ray-Man · Pull Request #26 · viperproject/helium

The-Ray-Man · 2026-10-27T12:32:44Z

one Solver::new() per unit, facts synced incrementally, path condition and negated goal as assumptions of Solver::check_assumptions(...), at most 1 500 000 resource units per check.

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.

JonasAlaif · 2026-10-29T10:31:16Z

If you're looking for z3 settings/config to use, you can probably use the Viper ones as a baseline. Probably the silicon ones.

The-Ray-Man · 2026-10-29T10:50:06Z

Yes this was my plan. But Silicon afaik does it a bit more nuanced than my current setup does. It sets different limits for different kind of queries. I set it to a value that corresponds to about 2s of running Z3 (the mean time is 259ms at the moment). I set it because I prefer to have incompleteness than timeouts.

JonasAlaif · 2026-10-29T11:17:46Z

Yep, we definitely want to keep a tight bound on how long z3 can run. What I meant more is the config options that e.g. disable mbqi, select the aithmetic solver or whatever it's called (I think Viper uses number 2, although there's a new one, maybe 5?, that might be better and we might want to use), etc.

The-Ray-Man · 2026-10-29T11:26:22Z

Ah now I understand. Yes that makes a lot of sense to use the same config than Silicon. Thanks for the hint. I will mirror the configs of Silicon.

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>

The-Ray-Man · 2026-10-30T09:10:27Z

With the same configs as Silicon we have the following changes in runtime. The base for the speedup were the default z3 settings.

The non z3 related phases (typecheck, parse etc.) stayed within 0.98-1.02x. This is expected, since they are independent from z3.
Adding the assertions had a speedup of 1.11x
Solving the queries had a speedup of 1.18x
The other z3 phases stayed about the same (creating the solver was 0.98x)
the benchmark has with the new settings one more incompleteness than before. But this test case previously resulted in a time out, which is counted as "unknown" and not "rejected". So this is not an issue.

The-Ray-Man added 24 commits October 27, 2026 13:01

Add the z3 crate as a dependency

e0c9431

Uses the gh-release build of Z3 and the num feature for arbitrary-precision integer and real literals.

Translate VMIR types to Z3 sorts

950464e

Adds the verify::z3 module with a sort cache covering the builtin types, Option, field/predicate address sorts and ADTs.

Try Z3 as the last prover rung

d58da77

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.

Store FuncKind per id when minting it

12b9240

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.

Report Z3 rung build and solve time

359431d

VerifyStats gains a z3_timing trend (not gated), split into building the problem and Solver::check. verify --breakdown prints it and --json includes it.

fixup! Try Z3 as the last prover rung

2cbdae3

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.

promoted tests that are no longer failing

e1f666f

formatting & clippy

74085fa

if the class type can not be inferred, then the fact is dropped.

411596c

moved wrongly annotated test as failing to passing

5331e62

implement cache for class_types

2a1344a

add func_cache

dfcc8f6

wip: don't rebuild the whole z3 query every time

ffac45c

update egg to have the union log

584c169

use the union log to merge classes

cf672b6

actually use the solver that aggregates the facts

6aa5057

formatting

6e55c4f

The-Ray-Man changed the title ~~Ramon/add z3 ladder step~~ Add Z3 with strategy V1 with rlimit Oct 29, 2026

JonasAlaif added this pull request to stack #29 October 29, 2026 10:29

The-Ray-Man changed the title ~~Add Z3 with strategy V1 with rlimit~~ Add Z3 with strategy V1 Oct 29, 2026

The-Ray-Man mentioned this pull request Oct 29, 2026

Unsoundness in Helium #34

Open

Navigation Menu

Repository navigation

Add Z3 with strategy V1 - #26

Add Z3 with strategy V1#26
The-Ray-Man wants to merge 25 commits into
feature/z3-ladder-stepfrom
ramon/add-z3-ladder-step

The-Ray-Man commented Oct 27, 2026 •

edited

Loading

Uh oh!

JonasAlaif commented Oct 29, 2026

Uh oh!

The-Ray-Man commented Oct 29, 2026

Uh oh!

JonasAlaif commented Oct 29, 2026 •

edited

Loading

Uh oh!

The-Ray-Man commented Oct 29, 2026

Uh oh!

The-Ray-Man commented Oct 30, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

The-Ray-Man commented Oct 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JonasAlaif commented Oct 29, 2026

Uh oh!

The-Ray-Man commented Oct 29, 2026

Uh oh!

JonasAlaif commented Oct 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

The-Ray-Man commented Oct 29, 2026

Uh oh!

The-Ray-Man commented Oct 30, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

The-Ray-Man commented Oct 27, 2026 •

edited

Loading

JonasAlaif commented Oct 29, 2026 •

edited

Loading