# Basic cvc5 tutorial (pythonic API)
This is a gentle beginner's guide on how to use the pythonic API for cvc5. A more advanced programmer may prefer to consult the [cvc5 documentation](https://cvc5.github.io/docs/cvc5-1.0.2/api/python/pythonic/pythonic.html) directly.
I also recommend checking out [z3](https://z3prover.github.io/papers/programmingz3.html) and seeing how it compares to cvc5 for your desired application. The python API is mostly identical, and sometimes z3 outperforms cvc5.
## What is cvc5?
[cvc5](https://cvc5.github.io/) is a **SMT solver**. SMT stands for "satisfiability modulo theories". In short, this means that cvc5 can determine whether certain kinds of simple mathematical constraints are satisfiable or unsatisfiable.
**Satisfiable** means there exist values you can set your variables to make all of the provided constraints true. For example, $x+y+z = 5$ and $x-y-z = 1$ are satisfiable by $x=3, y=2, z=0$ (but there are many other solutions).
* Accordingly, if it is impossible to set your variables to make all of the provided constraints simultaneously true, then your constraints are *unsatisfiable*. For example, $x^2 + 2x + 3 < 0$ is unsatisfiable.
* (Note that SMT solvers can also be used to show that a statement always holds: just show that $\texttt{Not}(\text{statement})$ is unsatisfiable.)
**Modulo theories** is a fancy way of saying "SMT solvers only know certain simple parts of math". In logic, a (first-order) [*theory*](https://en.wikipedia.org/wiki/Theory_(mathematical_logic)) is roughly speaking a collection of true statements using certain mathematical notation. For example, $\forall x, y, z,\ x \leq y \wedge y \leq z \implies x \leq z$ is true in the theory of orders: no matter what kinds of items you compare, this statement always holds.
* cvc5 can handle the theories of basic logic and arithmetic, [and a few more things](https://cvc5.github.io/docs/cvc5-1.0.2/api/python/pythonic/pythonic.html), but certainly not everything (in part due to [the undecidability of many theories](https://en.wikipedia.org/wiki/Decidability_(logic))).
The **cvc5 pythonic API** lets you input your constraints into the solver using Python. This is nice because by default, cvc5 input files must be written in specialized languages such as SMT-LIBv2. With the pythonic API, you sacrifice a bit of functionality (see [here](https://cvc5.github.io/docs/cvc5-1.0.2/api/python/pythonic/pythonic.html) for details), but for quick applications it is often easier to use. (To compare the pythonic API with raw SMT-LIBv2, see [this examples page](https://cvc5.github.io/docs/cvc5-1.0.2/examples/quickstart.html).)
### Starter example
For example, suppose you want to determine whether you want to solve the following puzzle:
> Find distinct 0-9 digit values for each letter in the following equation to make it true: $SEND + MORE = MONEY$. (Also $M \neq 0$.)
In cvc5.pythonic you can solve the puzzle using this code:
```python=
from cvc5.pythonic import *
def to_num(vars : list) -> int:
"""
Given list of vars, returns a number using the vars as digits.
Example: [s,e,n,d] -> 1000*s + 100*e + 10*n + 1*d
"""
pows = [10**i for i in range(len(vars)-1, -1, -1)]
return sum([vars[i] * pows[i] for i in range(len(vars))])
if __name__ == "__main__":
vars = Ints('s e n d m o r y')
s, e, n, d, m, o, r, y = vars
solver = Solver()
for var in vars:
solver.add(var >= 0, var <= 9)
solver.add(Distinct(vars))
solver.add( m != 0 )
solver.add( to_num([s,e,n,d]) + to_num([m,o,r,e]) == to_num([m,o,n,e,y]) )
print(solver.check())
if solver.check() == sat:
m = solver.model()
print(m)
```
which outputs:
```python
sat
[d = 7, e = 5, m = 1, n = 6, o = 0, r = 8, s = 9, y = 2]
```
### Should you use cvc5 or another tool?
Use cvc5 (or another SMT solver like z3) if:
* You want to determine whether some constraints are *satisfiable* or *unsatisfiable*.
* Your constraints can be expressed using simple logic, arithmetic, set operations, and [other theories implemented by cvc5](https://cvc5.github.io/docs/cvc5-1.0.2/api/python/pythonic/pythonic.html). (See [the limitations of cvc5 section](#Quirks-and-limitations-of-cvc5) for more information.)
Situations where cvc5 is not suitable:
* Have a pure boolean logic formula like $(x_1 \wedge x_2) \vee (\neg x_3 \vee x_4) \vee \dots$? Use a [SAT solver](https://en.wikipedia.org/wiki/SAT_solver).
* Have a LP, MIP, or MINLP? Use a solver like [SCIP](https://scipopt.org/).
* Have complicated mathematical operations? Use tools like [SageMath](https://www.sagemath.org/), [Lean's mathlib](https://github.com/leanprover-community/mathlib), or [Mathematica](https://www.wolfram.com/mathematica/).
## Installing cvc5 (pythonic API)
To install the pythonic API of cvc5, run the following command:
```
pip install cvc5
```
To test that cvc5 is working, create a file `sendmoremoney.py`, write inside it the contents of the $SEND+MORE=MONEY$ program above, and run
```
python3 sendmoremoney.py
```
### (if applicable) fixing a bug with `pythonic_printer.py`
:::warning
Do you get an error `Exception: Cannot print: Kind.CONST_INTEGER`? Here is how to fix that:
1. Open the file `cd ~/.local/lib/python3.10/site-packages/cvc5/pythonic/pythonic_printer.py`
2. There should be a function `_op_name(a)` which looks like:
```python=
def _op_name(a):
k = a.kind()
n = _cvc5_kinds_to_str.get(k, None)
if n is None:
if k in [Kind.CONSTANT, Kind.CONST_FLOATINGPOINT, Kind.CONST_ROUNDINGMODE, Kind.VARIABLE, Kind.UNINTERPRETED_SORT_VALUE, Kind.PI]:
return str(a.ast)
if k == Kind.INTERNAL_KIND:
# Hack to handle DT selectors and constructors
return str(a.ast)
if isinstance(a, cvc.FuncDeclRef):
f = a
else:
raise Exception("Cannot print: " + str(k))
return f.name()
else:
return n
```
Replace it with this code instead:
```python=
def _op_name(a):
k = a.kind()
n = _cvc5_kinds_to_str.get(k, None)
if n is None:
if k in [Kind.CONSTANT, Kind.CONST_FLOATINGPOINT, Kind.CONST_ROUNDINGMODE, Kind.VARIABLE, Kind.UNINTERPRETED_SORT_VALUE, Kind.PI]:
return str(a.ast)
if k == Kind.INTERNAL_KIND:
# Hack to handle DT selectors and constructors
return str(a.ast)
if isinstance(a, cvc.FuncDeclRef):
f = a
if k == Kind.CONST_INTEGER: # Added line to fix bug
return str(a.ast) # Added line to fix bug
else:
raise Exception("Cannot print: " + str(k))
return f.name()
else:
return n
```
This may display the integer `1` like `1()` instead. If you figure out how to fix this I would be delighted to hear about it.
:::
## Basic cvc5 pythonic API commands
### Setting up a solver
Here is some boilerplate code to get you started.
```python=
from cvc5.pythonic import *
if __name__ == "__main__":
# Set up a "solver" object.
solver = Solver()
# Define variables and put constraints in solver object.
x, y = Ints('x y')
solver.add(x + y == 5)
# Check whether the constraints supplied are sat or unsat.
print(solver.check())
# If the constraints are sat, display concrete values which
# make them satisfiable.
if solver.check() == sat:
m = solver.model()
print(m)
```
Output:
```python
sat
[x = 5, y = 0]
```
### Defining variables
You can define singleton variables like:
```python=
p = Bool('p')
x = Int('x')
y = Real('y')
```
To define a list of variables at a time, use:
```python=
p1, p2 = Bools('p1 p2')
x1, x2 = Ints('x1 x2')
some_reals = Reals('r1 r2 r3 r4')
# some_reals is a list [r1, r2, r3, r4]
```
You can use Python data structures to get $n$ variables at a time. For example:
```python=
n = 5
nums = []
for i in range(n):
nums.append(Int(f"x[{i}]"))
# nums is a list [x[1], ..., x[n]] of Ints
```
### Including constraints
Each `solver.add()` line specifies a constraint that must be satisfied.
Write equations with `==` and inequalities with `>, <, >=, <=, !=`:
```python=
x, y, z = Ints('x y z')
solver.add(x + y == z)
solver.add(x >= y, y < 2) # this requires that x >= y AND y < 2 hold.
```
You can also specify `And`s, `Or`s, and `Not`s of expressions:
```python=
solver.add( Not( x + y == 3 ) )
solver.add( Or(x >= y, y < 2) ) # This requires that x >= y OR y < 2 hold.
```
If you want a list of variables to be distinct, use `Distinct`:
```python=
a, b = Ints('a b')
nums = Ints('x y z')
solver.add(Distinct(a, b)) # a != b
solver.add(Distinct(nums)) # All elements in nums are distinct
```
You can also include constraints involving [bit-vectors](https://cvc5.github.io/docs/cvc5-1.0.2/api/python/pythonic/bitvec.html), [arrays](https://cvc5.github.io/docs/cvc5-1.0.2/api/python/pythonic/array.html), and [sets](https://cvc5.github.io/docs/cvc5-1.0.2/api/python/pythonic/set.html).
### Determining satisfiability
Once you have run all of your `solver.add()` commands, you can run `solver.check()` to determine satisfiability. This should output `sat` or `unsat` (or if you are unlucky, `unknown`).
```python=
from cvc5.pythonic import *
if __name__ == "__main__":
solver = Solver()
x, y = Ints('x y')
solver.add( x + y == 5 )
print(solver.check()) # Output: sat
```
```python=
from cvc5.pythonic import *
if __name__ == "__main__":
solver = Solver()
x, y = Ints('x y')
solver.add( x + y == 5 )
solver.add( x == y )
print(solver.check()) # Output: unsat
```
### Finding values which satisfy constraints
In cvc5, any concrete values which satisfy the constraints inputted into the solver are called a *model*. When `solver.check()` returns `sat`, then you can call `solver.model()` to determine values which satisfy the constraints:
```python=
from cvc5.pythonic import *
if __name__ == "__main__":
solver = Solver()
x, y = Ints('x y')
solver.add(x + y == 5)
print(solver.check())
if solver.check() == sat:
m = solver.model()
print(m)
```
Output:
```python
sat
[x = 5, y = 0]
```
In addition to storing values for the variables in the constraints, the model `m = solver.model()` is also able to compute related quantities:
```python=
print(f"Whole model: {m}")
print(f"x = {m[x]}")
print(f"x + y = {m[x+y]}")
print(f"2*x + 3*y = {m[2*x + 3*y]}")
```
Output:
```python=
Whole model: [x = 5, y = 0]
x = 5
x + y = 5
2*x + 3*y = 10
```
## Quirks and limitations of cvc5
### The word `Sort` in cvc5
In cvc5, the word `Sort` means what `type` means in Python. For example, `IntVal("1").sort()` returns `Int`, and `ArraySort()` specifies the types of elements contained in your cvc5 array.
### `Ints` only knows very basic facts about the integers
When `x, y = Ints('x y')`, cvc5 knows that `2*x == 2*y + 1` is `unsat` (makes sense: no even integer can be equal to an odd integer).
Here's another true fact: the sum of two perfect squares can never be 3 mod 4. (This is because perfect squares can only be 0 or 1 mod 4, so the sum of *two* squares can only be 0, 1, or 2 mod 4.) However, cvc5 does not seem to know this. On my computer, checking satisfiability of `x*x + y*y == 4*z + 3` for `x, y, z = Ints('x y z')` hangs.
### `Reals` less reliable than `Ints`
On my computer, `x**2 + 2*x + 1 < 0` returns `unsat` when `x = Int('x')`, but when `x = Real('x')`, the solver hangs. ([z3](https://z3prover.github.io/papers/programmingz3.html) works fine for both.)
## Conclusion
This was a very quick overview of how to get started with the pythonic API for cvc5. To dive deeper, I recommend you consult [the documentation](https://cvc5.github.io/docs/cvc5-1.0.2/api/python/pythonic/pythonic.html). Unfortunately these is limited information online about cvc5 (e.g. tiny Stack Overflow footprint). As a substitute, large language models such as ChatGPT can be useful to help you find where to look in the documentation, or elaborate on what a particular function does.

or

By clicking below, you agree to our terms of service.

Sign in via Facebook
Sign in via Twitter
Sign in via GitHub
Sign in via Dropbox
Sign in with Wallet

Wallet
(
)

Connect another wallet
New to HackMD? Sign up