Python API

cvc5 offers two separate APIs for Python users. The base Python API is an almost exact copy of the C++ API. Alternatively, the pythonic API is a more pythonic API that aims to be fully compatible with Z3s Python API while adding functionality that Z3 does not support.

Which Python API should I use?

If you are a new user, or already have an application that uses Z3’s python API, use the pythonic API. If you would like a more feature-complete—yet verbose—python API, with the ability to do almost everything that the cpp API allows, use the base Python API.

You can compare examples using the two APIs by visiting the examples page.

Installation (from PyPi)

The base and pythonic Python API can be installed via pip as follows:

pip install cvc5

Installation (from source)

The base and pythonic Python API can also be installed from source following these steps:

git clone https://github.com/cvc5/cvc5.git
cd cvc5
./configure.sh --python-bindings --auto-download
cd build
make # add -jN for parallel build using N threads
make install

The last step installs both the cvc5 binary and the Python bindings. If you want to install only the Python bindings, run the following command instead of make install:

cmake --install . --component python-api

For Windows, the steps above must be executed on a MINGW64 environment (see the installation instructions).

Finally, you can make sure that it works by running:

python3
import cvc5