Feat/cvc5 concurrency

[Riley-Kilgore]

Description

Type of Change

• Bug fix (non-breaking change fixing an issue)
• New feature (non-breaking change adding functionality)
• Breaking change (fix or feature causing existing functionality to change)
• Documentation update
• Performance improvement
• Code refactoring
• Test updates

Related Issue

Use any of the following for our ticket management to know which tickets to move to Done when PR is merged:

• Fixes #(issue number)
• Closes #(issue number)

Changes Made

Testing

Test Coverage

• Added new tests for new functionality
• Updated existing tests
• All tests pass locally
• For bug fixes: Added example to Tests/Issues/ folder

Documentation

• README updated (if applicable)
• Code comments added/updated
• Doc comments added for new optimization/rewritting rules

• My code follows the project's style guidelines
• I have performed a self-review of my code
• I have commented my code, particularly in hard-to-understand areas
• I have made corresponding changes to the documentation
• I have added tests that prove my fix is effective or that my feature works
• New and existing unit tests pass locally with my changes using make check_all
• For bug fixes: Original failing example added to Tests/Issues/ folder with reference to issue number

Additional Notes

[Copilot]

Pull request overview

This PR adds concurrent SMT solving to Blaster. It introduces a new solver-mode option with three policies — single (existing behavior), first (race Z3 and cvc5, first decisive verdict wins), and agree (run both and require compatible verdicts) — and rewrites the SMT process lifecycle to own multiple independent solver sessions, with structured verdict/status/evidence separation, a Blaster-side timeout with a fixed response-drain grace, cancellation handling, and .blaster/agreement-* diagnostic artifacts. It fits into the core translate/solve path (Blaster/Smt/Translate.lean, Blaster/Smt/Env.lean) and the state-machine strategies (BMC/KInduction), replacing the single smtProc model with sessions/solverRecords/configuredSolvers/singleSolver.

Changes:

• New SolverMode option (parser, syntax, docs) and validation rejecting solver + concurrent mode and only-smt-lib + concurrent mode.
• Multi-session engine: withSmtSessionOwner, per-session command broadcast, first/agree/single check drivers, timeout/cancellation/agreement aggregation, and canonical-query replay for retired sessions.
• Extensive new tests (ConcurrentSolvers, ConcurrentDump, CrashLifecycle, SolverOutcomePolicy, SolverModeConfiguration, CounterexampleSpike) plus README/spike documentation, Makefile/CI/script updates for artifacts and module exclusion.

Reviewed changes

Copilot reviewed 30 out of 31 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
Blaster/Smt/Env.lean	Core rewrite: sessions, records, verdict/outcome types, aggregateAgreement, timeout/cancellation, artifacts, setup transcript
Blaster/Smt/Translate.lean	Translate.main wrapped in session owner; concurrent start, validation, deferred logSmtQuery
Blaster/Optimize/Env.lean	SmtEnv fields for sessions/records; idempotent throwEnvError cleanup
Blaster/Smt/EmitCommand.lean	Emission target switched to emitProc; removed getProcStdOut
Blaster/Command/Options.lean	SolverMode enum + solverMode field
Blaster/Command/Syntax.lean / Tactic.lean	solver-mode syntax, parser, and docs
Blaster/Logging/Basic.lean	Per-backend labeled SMT transcript output at dump/verbose-3
Blaster/StateMachine/{BMC,KInduction,StateMachine}.lean	Session-owner wrapping; logSmtQuery after check; singleSolver for policy
Tests/Smt/*	New concurrency, outcome-policy, lifecycle, dump, and spike tests; timeout tweaks
Tests/FixedIssues/Issue{17,24,25}.lean	Bound polymorphic-string regressions independently of solver timing
README.md / COUNTEREXAMPLE_SPIKE.md	Concurrent-mode and diagnostics documentation
Makefile / scripts/check_lean_project_compilation.sh / .github/workflows/ci-linux.yaml / .gitignore	Artifact cleanup/upload, module exclusion, .blaster/ ignore

I reviewed the option plumbing, the multi-session engine (first/agree/single drivers, timeout grace, cancellation, agreement aggregation and evidence selection), the state-machine integration, and the test/documentation updates. The design is internally consistent with its tests, references to the renamed helpers are updated, BLASTER_TIMEOUT ?= 30 backs the Makefile change, and the excluded spike module is correctly whitelisted in the compilation check. I did not identify an objective, within-diff defect meeting the bar for a change-blocking comment. However, this is a very large, high-risk rewrite of solver process ownership, concurrency, cancellation, and timeout semantics, where subtle race/lifecycle behavior is hard to fully verify from diffs alone, so it warrants final human review.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.