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