d7258c4021
- Bitwuzla BV solver is 5.1x faster than Z3 (SMT-COMP 2023) - ESBMC pattern: dispatch to 6 solvers, race for first result - Proposal: add --solver bitwuzla | z3 | portfolio-all flag - Expected 2-5x speedup on fold's BV-64 queries
45 lines
2 KiB
Markdown
45 lines
2 KiB
Markdown
# Z3 Parallel Solving + Multi-Solver Portfolio for fold
|
|
|
|
> Generated 2026-05-29. Research on accelerating fold's Z3 solving.
|
|
|
|
## Current State
|
|
|
|
fold uses `z3::solver` with `QF_BV` logic. The `--portfolio` flag runs Z3 tactics in parallel threads (bit-blast + SAT). Default per-query timeout is 2000ms.
|
|
|
|
## Multi-Solver Portfolio Opportunity
|
|
|
|
| Solver | BV perf vs Z3 | Language | Integration |
|
|
|--------|--------------|----------|-------------|
|
|
| **Bitwuzla** | 5.1x faster | C/C++ | C API, drop-in for Z3 |
|
|
| CVC5 | ~3x slower | C++ | C API, broader theory support |
|
|
| MathSAT | Similar | C | C API, optimization (OMT) |
|
|
|
|
**Recommended**: Add `--solver bitwuzla` flag to fold. On BV-only queries (which fold uses exclusively), Bitwuzla is 5x faster. Keep Z3 as default for its mature tactics engine, but offer Bitwuzla for large codebases.
|
|
|
|
## Incremental Solving
|
|
|
|
fold already uses `solver.push()`/`solver.pop()` in the security walker for branch-local constraints. Z3's incremental mode reuses learned clauses across queries — fold leverages this implicitly.
|
|
|
|
## Parallel Portfolio (ESBMC Pattern)
|
|
|
|
ESBMC dispatches to 6 solvers simultaneously and returns the first result. fold's current `checkWithPortfolio` uses Z3 tactics only. Could extend to:
|
|
|
|
```cpp
|
|
// Dispatch to Z3, Bitwuzla, and CVC5 in parallel
|
|
auto result = race({
|
|
z3_solver.check(assumptions),
|
|
bitwuzla_solver.check(assumptions),
|
|
cvc5_solver.check(assumptions)
|
|
});
|
|
```
|
|
|
|
This trades memory for speed — 3 solvers running simultaneously on different cores.
|
|
|
|
## Bitwuzla Integration Plan
|
|
|
|
1. Add `--solver` flag to ScanOptions (choices: z3, bitwuzla, portfolio-all)
|
|
2. Add Bitwuzla C API wrapper in `src/symbolic/bitwuzla_solver.cpp`
|
|
3. Extend `checkWithPortfolio` in `tactics.cpp` to optionally dispatch to Bitwuzla
|
|
4. Benchmark on fold's own codebase to measure speedup
|
|
|
|
**Expected impact**: 2-5x speedup on BV-heavy queries. Most fold queries are simple null-equality checks — Bitwuzla's BV specialization is ideal for this workload.
|