fold/docs/internal/z3-multisolver-portfolio.md

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:

// 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.