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 (x86-64 variants of Linux and macOS)

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

pip install cvc5

Installation (ARM64 variants of Linux and macOS)

For ARM64-based machines (including Apple computers with M1 and M2 chips), the base and the pythonic Python API can be installed from source. Before building and installing, the following dependencies should be installed, using brew and pip:

brew install cmake python gmp java

Then cvc5 can be installed from source as follows:

git clone git@github.com:cvc5/cvc5.git
cd cvc5
./configure.sh --python-bindings --auto-download
cd build
make cvc5_python_api              # add -jN for parallel build using N threads
export PYTHONPATH="<path-to-local-cvc5-repo>/build/src/api/python/:$PYTHONPATH"

And to make sure that it works:

python3
import cvc5