# 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:

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:

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:

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:

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.

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:

sat
[x = 5, y = 0]

### Defining variables

You can define singleton variables like:

p = Bool('p')
x = Int('x')
y = Real('y')

To define a list of variables at a time, use:

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:

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 `>, <, >=, <=, !=`:

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:

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`:

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`).

from cvc5.pythonic import * 

if __name__ == "__main__":
    solver = Solver()
    x, y = Ints('x y')
    solver.add( x + y == 5 )
    print(solver.check()) # Output: sat

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:

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:

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:

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:

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.