Feat/cvc5 backend

[Riley-Kilgore]

Description

This PR adds initial cvc5 backend support to Blaster while preserving Z3 as the default SMT solver.

The change introduces solver selection through both tactic options and environment configuration, adds solver-specific process/version handling, updates counterexample/model retrieval to use a more portable SMT-LIB command, extends CI to exercise both supported solvers, and adds cvc5-focused tests and documentation.

Z3 remains the default backend for existing #blaster usage.

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

• Fixes #

Changes Made

• Added support for selecting the SMT backend via a new solver option: #blaster (solver: z3) or #blaster (solver: cvc5).
• Added support for selecting the default solver through the BLASTER_SOLVER environment variable.
• Introduced a solver abstraction for backend-specific behavior, including command candidates, version probing, minimum supported version checks, process arguments, and default SMT options.
• Added initial cvc5 process support with cvc5-specific command-line arguments and SMT options.
• Preserved Z3 as the default solver to avoid changing existing user behavior.
• Updated counterexample/model value retrieval from Z3-specific (eval ...) usage to SMT-LIB-style (get-value (...)) handling.
• Added response parsing support for get-value output.
• Added a solvercheck executable for validating local solver availability and supported versions.
• Added cvc5-oriented test coverage for solver selection, expected success cases, expected failure/counterexample cases, and known backend differences.
• Updated CI to run solver-specific test jobs for both Z3 and cvc5.
• Updated documentation with solver selection examples, cvc5 installation notes, BLASTER_SOLVER usage, solvercheck usage, and current backend limitations.

Testing

The intended validation for this PR is:

• lake build Blaster
• lake exe solvercheck z3
• lake exe solvercheck cvc5
• BLASTER_SOLVER=z3 lake test
• BLASTER_SOLVER=cvc5 BLASTER_TIMEOUT=30 lake test
• CI passes for the Z3 solver job
• CI passes for the cvc5 solver job
• Manual smoke test with explicit Z3 selection: #blaster (solver: z3) ...
• Manual smoke test with explicit cvc5 selection: #blaster (solver: cvc5) ...
• Manual smoke test with BLASTER_SOLVER unset, confirming Z3 remains the default

Remaining items before marking ready:

• Remove the leftover debug/compile-failure line from SolverCheck.lean: #eval thisIdentifierDoesNotExist
• Confirm whether the only-smt-lib path should emit the same default solver setup commands used by the normal solver path.
• Confirm version parsing behavior for supported solvers when the version banner cannot be parsed.
• Verify WSL fallback behavior for both Z3 and cvc5.
• Add direct unit coverage for get-value response parsing.
• Add direct unit coverage for solver version parsing and minimum-version checks.
• Review timeout-sensitive cvc5 tests for potential CI flakiness.
• Confirm that the selected cvc5 options are accepted across the documented minimum supported cvc5 version range.
• Decide how to track known cvc5 limitations around quantifiers, recursive definitions, model behavior, and timeout behavior.

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