[DNM] Native solver experiment - #16526
Draft
figtracer wants to merge 5 commits into
Draft
Conversation
Contributor
✅ Changelog foundThe deterministic check will validate the changed entry. |
Raises native corpus coverage from 92.28% to 95.59% and lowers isolated corpus wall time by 25.48%. The five-suite native mean sum falls by 6.21%, with identical semantic projections.
Assert the explicit unknown result from an unsupported native-only query rather than requiring a heuristic witness. Retain incomplete status, solver identity, zero SMT traffic, and no replay assertions. AI-assisted CI fix by Centaur. Co-authored-by: Derek Cofausper <256792747+decofe@users.noreply.github.com>
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
2 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.
This draft pins V51 of the native solver and tries it before Foundry's configured SMT backend. It reads the interned expression DAG directly, validates every SAT model against the original expression, and returns
Unknownfor unsupported queries so the existing solver can take over. Native-only mode is available to test the no-Z3 path.Results
On the same Forge binary, the five-suite mean is 22.621s with persistent Z3 and 3.485s with native solving: 6.49x faster, with identical pass/fail/incomplete/path outcomes and all 1,143 SAT models replaying. This remains a do-not-merge experiment rather than a complete Z3 replacement because 76 captured queries are still unsupported.
Built with Codex assistance.