cvc5 Python Bindings

1.3.3 verified Mon Apr 27 auth: no python

Python bindings for cvc5, an efficient automatic theorem prover for Satisfiability Modulo Theories (SMT). Current version 1.3.3. Release cadence: irregular, ~3 major versions per year.

pip install cvc5

Common errors

error ModuleNotFoundError: No module named 'cvc5' ↓

cause cvc5 package not installed or installed in wrong environment.

fix

Run: pip install cvc5

error ImportError: cannot import name 'Solver' from 'cvc5' ↓

cause Attempted to import Solver from the low-level C++ API (which does not expose it directly).

fix

Use: from cvc5.pythonic import Solver

error NameError: name 'Int' is not defined ↓

cause Forgot to import sort constructors like Int, Bool, etc. from cvc5.pythonic.

fix

Add: from cvc5.pythonic import * OR from cvc5.pythonic import Int, Bool, Solver, And, Or, ...

Warnings

breaking In cvc5 1.0, the Python API was completely redesigned away from the CVC4-style API. Code written for cvc5 < 1.0 will not work. Use the pythonic API (from cvc5.pythonic import *) for Z3-like syntax. ↓

fix Migrate to pythonic API: replace old 'from cvc5 import ...' with 'from cvc5.pythonic import Solver, Int, etc.'

deprecated mkString with std::wstring is deprecated in favor of std::u32string. Python bindings may be affected indirectly. ↓

fix Use Unicode strings (u32string) for string literals where applicable.

gotcha The pythonic API uses 'And', 'Or', 'Not' (capitalized) from cvc5.pythonic, but users may try lowercase from z3. This causes NameError. ↓

fix Use correct imports: from cvc5.pythonic import And, Or, Not, Implies, etc.

gotcha The Solver object from cvc5.pythonic does not have a 'model()' method that returns a Z3-like model. Instead, use s.model() after s.check() returns sat, but the model API is different. ↓

fix Use s.model() directly; it returns a cvc5 pythonic model object. Or use s.model().evaluate(term).

Imports

Solver
wrong
```
from cvc5 import Solver
```
correct
```
from cvc5.pythonic import Solver
```
cvc5 exposes two APIs: pythonic (Z3-like) and C++-style. The common mistake is using the low-level C++-style import incorrectly.

Quickstart

Minimal example using the pythonic (Z3-compatible) API.

from cvc5.pythonic import *
s = Solver()
s.add(Int('x') + Int('y') == 10)
print(s.check())