Python Interface for Automated Solvers

SolverPy provides a uniform Python interface for several automated ATP and SMT solvers.

Currently supported solvers are E, Vampire, Prover9, Lash, cvc5, Z3, and Bitwuzla.

The interface can be used for:

💡 Solving a single problem instance with compatible results.
🔧 Benchmark parallel evaluation with database storage.
🧠 Machine learning of models and strategies for solver guidance.

Installation

Install the Python package using pip:

$ pip install solverpy

Or clone our GitHub repository:

$ git clone https://github.com/cbboyan/solverpy.git

🗒️ Note: The solver binaries/libraries are not part of this Python package and must be installed separately. The binaries must be (by default) in PATH or specified using binary parameter in Setup, if you wish to use them from solverpy.

Overview

💡 Single problem solving

Single problem solving involves creating a solver object and calling its solve method.

from solverpy.solver.smt.cvc5 import Cvc5

cvc5 = Cvc5("T5")  # time limit of 5 seconds
result = cvc5.solve("myproblem.smt2", "--enum-inst") # problem and strategy

Strategies are solver-specific, typically command line options as a string.

☕ The result is a dictionary guaranteed to contain at least two keys: status as a string and runtime in seconds, apart from solver-specific keys.

😎 For more details, see the solver module.

🔧 Benchmark evaluation

SolverPy provides dataclass Setup that describes the evaluation configuration. It auromatically connects to database DB to store results, by default, using the Jsons provider.

To evaluate a set of strategies on a set of benchmark problems, you just need to provide your experiment description as a Python dict.

💡 Use typed version Setup to avoid typos and type errors.

Functions from the setups module are used to fill in the required keys and values. To run the evaluation you setup a solver for an evaluation, then launch it.

🤞 Before launching the evaluation, you need to setup the SolverPy database by creating directories solverpy_db/strats in the current directory. This directory stores the strategy files. For the above example, there should be an empty file solverpy_db/strats/default (default cvc5 strategy). The problem files should be in problems/ directory.

from solverpy import setups

mysetup = setups.Setup(
    cores=4,
    bidlist=["problems"],
    sidlist=["default"],
    limit='T10',
)

setups.cvc5(mysetup)
setups.evaluation(mysetup)

setups.launch(mysetup)

☕ After the evaluation, you can inspect the results in the database directory solverpy_db/results.

😎 For more details, see the benchmark module.

🧠 Machine learning

Similarly, you can use the enigma and cvc5ml from setups module. to setup several loops of interleaved evaluation and model training.

😎 For more details, see the builder module.