Z3alpha synthesizes efficient Z3 strategies tailored to your problem set! See our IJCAI'24 paper Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis for technical details.

Our tool is built on top of the Z3 SMT solver.

Setup

python -m venv venv
source venv/bin/activate  # Unix/macOS
pip install z3-solver
pip3 install -e .

Z3alpha requires a Z3 binary and runs benchmarks in parallel workers. Before running any synthesis or evaluation, specify machine-specific settings in env_config.json at the repo root — these control which Z3 binary is used and how many parallel workers are launched:

• z3_path — path to the Z3 binary (default: z3 on PATH)
• z3_version — if set, the binary version is verified at startup
• workers — parallel benchmark evaluations per simulation (default: 4)
• machine_name — informational label for result logs

All fields are optional; missing fields use defaults.

A Synthesis Example

A smoke-test configuration for QF_NIA is provided at data/smoke/configs/synthesis.json, with benchmarks in data/smoke/benchmarks/QF_NIA/. Run it with:

python -m z3alpha.synthesize data/smoke/configs/synthesis.json

This runs Z3alpha on 10 QF_NIA benchmarks with 10 stage-1 MCTS simulations, 50 stage-2 simulations, and a 2-second per-benchmark timeout.

Output files (in experiments/synthesis/out-<timestamp>/):

• linear_strategy_summary.csv — per-strategy: simulation id, strategy string, n_solved, par2_avg, par10_avg
• linear_strategy_per_benchmark.csv — per-instance outcomes (sat/unsat/timeout/error, solve time)
• linear_selected_strategies.csv — shortlist of strategies passed to stage 2
• synthesized_strategy.txt — synthesized strategy string

Tactic and Parameter Configuration

The tactic action space and the asscociated parameter search grids are defined in z3alpha/tactics/logic_configs/, one JSON file per SMT-LIB logic (e.g. QF_NIA.json). Each top-level key is a Z3 tactic name:

"simplify": {
  "solver": false,
  "params": {
    "elim_and": { "default": "false", "values": ["true", "false"] },
    "hoist_mul": { "default": "false", "values": ["true", "false"] }
  }
},
"smt": { "solver": true }

• Tactics with "solver": true terminate a strategy (leaf nodes); others are preprocessing steps.
• "params" defines the parameter search grid: "default" is Z3's own default for that parameter (omitted from the synthesized strategy string if selected); "values" is the candidate set to explore.

To add a new logic or extend an existing one, create or edit the corresponding file and run the validator to check tactic names, parameter names, and defaults against your Z3 binary:

python scripts/validate_logic_configs.py        # check
python scripts/validate_logic_configs.py --fix  # auto-correct defaults

IJCAI-24 Reproduction

Benchmarks

The scripts in data/ijcai24/benchmarks/download_scripts/ will download all benchmark sets used in the paper into the data/ijcai24/benchmarks/ directory. For example, to download the original FastSMT benchmarks for the experiments in Section 5.3, run:

./data/ijcai24/benchmarks/download_scripts/download_fastsmt_benchmarks.sh

Z3alpha Strategy Synthesis

We provide configuration JSON files for the experiments in data/ijcai24/configs/synthesis/. When under the repository root, run the following command with the corresponding configuration file.

For example, to synthesize a strategy for leipzig, run:

python -m z3alpha.synthesize data/ijcai24/configs/synthesis/leipzig.json

Before running the script, ensure to adjust the JSON configuration file to match your computer's specifications.

Evaluation

We provide the script scripts/eval_solvers.py for evaluating solvers and strategies. Sample configuration files for evaluating our synthesized strategies are provided in data/ijcai24/configs/eval. For example, to evaluate all solvers on the leipzig test, run:

python scripts/eval_solvers.py data/ijcai24/configs/eval/leipzig.json

The evaluation outcomes are saved in the directory specified by the res_dir entry in the configuration JSON file.

SMT-COMP'24

As a derived solver, Z3alpha participated in SMT-COMP 2024 (Single Query Track) and won some awards.

License

Z3alpha is licensed under the Apache 2.0 License.

Citing this Work

IJCAI'24 (conference):

@inproceedings{z3alpha_ijcai2024,
  title     = {Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis},
  author    = {Lu, Zhengyang and Siemer, Stefan and Jha, Piyush and Day, Joel and Manea, Florin and Ganesh, Vijay},
  booktitle = {Proceedings of the Thirty-Third International Joint Conference on
               Artificial Intelligence, {IJCAI-24}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Kate Larson},
  pages     = {1907--1915},
  year      = {2024},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2024/211},
  url       = {https://doi.org/10.24963/ijcai.2024/211},
}

Acta Informatica (journal, 2025):

@article{z3alpha_acta_informatica_2025,
  title   = {Novel tree-search method for synthesizing SMT strategies},
  author  = {Lu, Zhengyang John and Day, Joel and Jha, Piyush and Sarnighausen-Cahn, Paul and Siemer, Stefan and Manea, Florin and Ganesh, Vijay},
  journal = {Acta Informatica},
  volume  = {62},
  number  = {3},
  pages   = {28},
  year    = {2025},
  doi     = {10.1007/s00236-025-00495-x},
  url     = {https://doi.org/10.1007/s00236-025-00495-x},
}