[WIP] CVC 5 integration - #140
Draft
RSoulatIOHK wants to merge 20 commits into
Draft
Conversation
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
cvc5 1.3.4 reserves @/.-prefixed symbols in default parsing mode, but Blaster emits qualifiers like @isnat; spawn with --parsing-mode=lenient. Bump minVersion to 1.3.4 (local + CI pin), add end-to-end cvc5 tests (valid/falsified/gen-cex/timeout/seed/tactic) on goals the pre-SMT optimizer cannot fold away. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Script-generated: 497 siblings across 45 files. Skips invocations that never reach a solver (only-smt-lib/only-optimize), #guard_msgs-wrapped blocks (Z3 baselines, handled separately), and invocations already carrying a solver option. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
:finite-model-find + :fmf-fun (suggested by JFE) let cvc5 produce counterexample models for falsified goals over recursively-defined functions. :tlimit-per 30000 caps every check by default so no cvc5 invocation can run forever; explicit (timeout: n) still overrides. Spec documents the qualifier bridge-axiom limitation and the proven define-fun follow-up fix. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…outs Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
SolverChoice (one/all/any) replaces the single-solver option. all/any spawn every supported solver (Z3+cvc5), each with its own startup options, all receiving the identical command stream via a broadcast submission layer over an smtProcs array. any: first definitive answer wins; losing processes are killed and the run narrows to the winner (BMC/K-Induction rounds after the first decided check are single-solver). all: answers are cross-checked each round — sat vs unsat is a hard soundness error; definitive vs unknown raises a warning listing per-solver verdicts (tracking signal for goals not discharged by every solver). Model values are queried only on the answering process using that solver's query style. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…suggestion all mode logs per-solver verdicts with wall-clock answer times (⏱ Z3 → unsat (12ms), cvc5 → unsat (24ms)) for benchmarking; any mode announces the winning solver and its time (🏁), and offers a 'Try this' code action replacing (solver: any) with the winner so the result can be reproduced deterministically — on both the #blaster command and the blaster tactic. (verbose: 1) additionally reports the total wall-clock of the whole call. Per-solver timings and the any-winner are recorded in SmtEnv (solverPerf/anyWinner). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The all-mode cross-check now records the fastest solver whose answer matches the adopted result; the Try-this code action offers replacing (solver: all) with it, same as for any-mode races. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The builtin tryThisProvider reads TryThisInfo from the command info tree, which async-elaborated commands like #blaster never expose to the server — leaving only the InfoView link. This code-action provider reconstructs the quick fix from the reported 'Try this:' diagnostic itself (its range is the invocation to replace; its rendered message carries the replacement) and links the action to the diagnostic, so editors offer it from the diagnostic hover box and the quick-fix menu. Verified with a headless LSP probe: quickfix returned, preferred, with the correct text edit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
497 command pairs and 19 tactic-theorem pairs collapse into one (solver: all) call each: both solvers now run in parallel per test with a sat/unsat soundness cross-check, definitive-vs-unknown divergences surface as tracking warnings, and the suite shrinks by ~650 lines. Differing pair expectations resolve to the definitive solve-result; cvc5-side timeouts are kept. #guard_msgs-baselined blocks and the deliberate per-solver coverage in SmtSolverSelection stay unchanged. Side effect: the previously failing cvc5-only tactic siblings in Issue26/27 are fixed — all-mode adopts Z3's unsat when cvc5 gives up. Co-Authored-By: Claude Fable 5 <noreply@anthropic.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
1 participant
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.
I used the short time we got Fable 5 to try to have it do the CVC 5 integration.
This has not been reviewed. Done with Fable 5 everything maxed.