A generic Python interface for evaluation and machine learning of
automated theorem provers (ATPs) and Satisfiability Modulo Theories solvers
(SMTs) — a single solverpy shell command driven by YAML experiment files,
a results database that caches every run, and a full Python API when you
need more control.
📖 Full documentation, install instructions, and step-by-step tutorials: https://cbboyan.github.io/solverpy/
This repository is a monorepo of three packages, each installable from PyPI independently:
| Package | Purpose |
|---|---|
solverpy (PyPI) |
Core solver interface, benchmark evaluation, and the results database. |
solverpy-learn (PyPI) |
Machine-learning guidance on top of solverpy: ENIGMA (E Prover clause selection) and cvc5ml. |
solverpy-grackle |
Configuration collection invention (algorithm configuration) for ATPs and SMT solvers. |
pip install solverpy
pip install solverpy-learn # optional, for ML guidanceSolver binaries (eprover, cvc5, z3, ...) are not bundled — see
Install.
solverpy init eprover
solverpy run eval-eprover.yamlor from Python:
from solverpy.solver.smt.cvc5 import Cvc5
cvc5 = Cvc5("T5") # time limit of 5 seconds
result = cvc5.solve("myproblem.smt2", "--enum-inst")
print(result["status"], result["runtime"])See Usage and Tutorials — including evaluating E, evaluating cvc5, training ENIGMA, and using the Python API directly — plus the full Commands reference.