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 directly.

I also recommend checking out z3 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 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
  $\mathtt{\text{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 is roughly speaking a collection of true statements using certain mathematical notation. For example,

$\mathrm{\forall }x,y,z,x\le y\wedge y\le z⟹x\le 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, but certainly not everything (in part due to the undecidability of many theories).

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

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\ne 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. (See the limitations of cvc5 section for more information.)

Situations where cvc5 is not suitable:

• Have a pure boolean logic formula like
  $(x_1\wedge x_2)\vee (\mathrm{\neg }{x}_3\vee x_4)\vee \dots$? Use a SAT solver.
• Have a LP, MIP, or MINLP? Use a solver like SCIP.
• Have complicated mathematical operations? Use tools like SageMath, Lean's mathlib, or 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

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 Ands, Ors, and Nots 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, arrays, and sets.

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