Quickstart Guide

First, create a cvc5 term manager instance:

tm = cvc5.TermManager()

Then, create a cvc5 solver instance:

solver = cvc5.Solver(tm)

We will ask the solver to produce models and unsat cores in the following, and for this we have to enable the following options.

solver.setOption("produce-models", "true")
solver.setOption("produce-unsat-cores", "true")

Next we set the logic. The simplest way to set a logic for the solver is to choose "ALL". This enables all logics in the solver. Alternatively, "QF_ALL" enables all logics without quantifiers. To optimize the solver’s behavior for a more specific logic, use the logic name, e.g. "QF_BV" or "QF_AUFBV".

solver.setLogic("ALL")

In the following, we will define constraints of reals and integers. For this, we first query the solver for the corresponding sorts.

realSort = tm.getRealSort()
intSort = tm.getIntegerSort()

Now, we create two constants x and y of sort Real, and two constants a and b of sort Integer. Notice that these are symbolic constants, but not actual values.

x = tm.mkConst(realSort, "x")
y = tm.mkConst(realSort, "y")
a = tm.mkConst(intSort, "a")
b = tm.mkConst(intSort, "b")

We define the following constraints regarding x and y:

\[(0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y)\]

We construct the required terms and assert them as follows:

# Formally, constraints are also terms. Their sort is Boolean.
# We will construct these constraints gradually,
# by defining each of their components.
# We start with the constant numerals 0 and 1:
zero = tm.mkReal(0)
one = tm.mkReal(1)

# Next, we construct the term x + y
xPlusY = tm.mkTerm(Kind.ADD, x, y)

# Now we can define the constraints.
# They use the operators +, <=, and <.
# In the API, these are denoted by Plus, Leq, and Lt.
constraint1 = tm.mkTerm(Kind.LT, zero, x)
constraint2 = tm.mkTerm(Kind.LT, zero, y)
constraint3 = tm.mkTerm(Kind.LT, xPlusY, one)
constraint4 = tm.mkTerm(Kind.LEQ, x, y)

# Now we assert the constraints to the solver.
solver.assertFormula(constraint1)
solver.assertFormula(constraint2)
solver.assertFormula(constraint3)
solver.assertFormula(constraint4)

Now we check if the asserted formula is satisfiable, that is, we check if there exist values of sort Real for x and y that satisfy all the constraints.

r1 = solver.checkSat()

The result we get from this satisfiability check is either sat, unsat or unknown. It’s status can be queried via isSat, isUnsat and isSatUnknown functions. Alternatively, it can also be printed.

print("expected: sat")
print("result: ", r1)

This will print:

expected: sat
result: sat

Now, we query the solver for the values for x and y that satisfy the constraints.

xVal = solver.getValue(x)
yVal = solver.getValue(y)

It is also possible to get values for terms that do not appear in the original formula.

xMinusY = tm.mkTerm(Kind.SUB, x, y)
xMinusYVal = solver.getValue(xMinusY)

We can retrieve the Python representation of these values as follows.

xPy = xVal.getRealValue()
yPy = yVal.getRealValue()
xMinusYPy = xMinusYVal.getRealValue()

print("value for x: ", xPy)
print("value for y: ", yPy)
print("value for x - y: ", xMinusYPy)

This will print the following:

value for x: 1/6
value for y: 1/6
value for x - y: 0

Another way to independently compute the value of x - y would be to use the Python minus operator instead of asking the solver. However, for more complex terms, it is easier to let the solver do the evaluation.

xMinusYComputed = xPy - yPy
if xMinusYComputed == xMinusYPy:
  print("computed correctly")
else:
  print("computed incorrectly")

This will print:

computed correctly

Further, we can convert these values to strings:

xStr = str(xPy)
yStr = str(yPy)
xMinusYStr = str(xMinusYPy)

Next, we will check satisfiability of the same formula, only this time over integer variables a and b. For this, we first reset the assertions added to the solver.

solver.resetAssertions()

Next, we assert the same assertions as above, but with integers. This time, we inline the construction of terms to the assertion command.

solver.assertFormula(tm.mkTerm(Kind.LT, tm.mkInteger(0), a))
solver.assertFormula(tm.mkTerm(Kind.LT, tm.mkInteger(0), b))
solver.assertFormula(
    tm.mkTerm(
        Kind.LT, tm.mkTerm(Kind.ADD, a, b), tm.mkInteger(1)))
solver.assertFormula(tm.mkTerm(Kind.LEQ, a, b))

Now, we check whether the revised assertion is satisfiable.

r2 = solver.checkSat()
print("expected: unsat")
print("result:", r2)

This time the asserted formula is unsatisfiable:

expected: unsat
result: unsat

We can query the solver for an unsatisfiable core, that is, a subset of the assertions that is already unsatisfiable.

unsatCore = solver.getUnsatCore()
print("unsat core size:", len(unsatCore))
print("unsat core:", unsatCore)

This will print:

unsat core size: 3
unsat core: [(< 0 a), (< 0 b), (< (+ a b) 1)]

Example

examples/api/python/quickstart.py

  1#!/usr/bin/env python
  2###############################################################################
  3# Top contributors (to current version):
  4#   Yoni Zohar, Aina Niemetz, Alex Ozdemir
  5#
  6# This file is part of the cvc5 project.
  7#
  8# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
  9# in the top-level source directory and their institutional affiliations.
 10# All rights reserved.  See the file COPYING in the top-level source
 11# directory for licensing information.
 12# #############################################################################
 13#
 14# A simple demonstration of the api capabilities of cvc5, adapted from quickstart.cpp
 15##
 16
 17import cvc5
 18from cvc5 import Kind
 19
 20if __name__ == "__main__":
 21  # Create a term manager
 22  #! [docs-python-quickstart-0 start]
 23  tm = cvc5.TermManager()
 24  #! [docs-python-quickstart-0 end]
 25  # Create a solver
 26  #! [docs-python-quickstart-1 start]
 27  solver = cvc5.Solver(tm)
 28  #! [docs-python-quickstart-1 end]
 29
 30  # We will ask the solver to produce models and unsat cores,
 31  # hence these options should be turned on.
 32  #! [docs-python-quickstart-2 start]
 33  solver.setOption("produce-models", "true")
 34  solver.setOption("produce-unsat-cores", "true")
 35  #! [docs-python-quickstart-2 end]
 36
 37  # The simplest way to set a logic for the solver is to choose "ALL".
 38  # This enables all logics in the solver.
 39  # Alternatively, "QF_ALL" enables all logics without quantifiers.
 40  # To optimize the solver's behavior for a more specific logic,
 41  # use the logic name, e.g. "QF_BV" or "QF_AUFBV".
 42
 43  # Set the logic
 44  #! [docs-python-quickstart-3 start]
 45  solver.setLogic("ALL")
 46  #! [docs-python-quickstart-3 end]
 47
 48  # In this example, we will define constraints over reals and integers.
 49  # Hence, we first obtain the corresponding sorts.
 50  #! [docs-python-quickstart-4 start]
 51  realSort = tm.getRealSort()
 52  intSort = tm.getIntegerSort()
 53  #! [docs-python-quickstart-4 end]
 54
 55  # x and y will be real variables, while a and b will be integer variables.
 56  # Formally, their python type is Term,
 57  # and they are called "constants" in SMT jargon:
 58  #! [docs-python-quickstart-5 start]
 59  x = tm.mkConst(realSort, "x")
 60  y = tm.mkConst(realSort, "y")
 61  a = tm.mkConst(intSort, "a")
 62  b = tm.mkConst(intSort, "b")
 63  #! [docs-python-quickstart-5 end]
 64
 65  # Our constraints regarding x and y will be:
 66  #
 67  #   (1)  0 < x
 68  #   (2)  0 < y
 69  #   (3)  x + y < 1
 70  #   (4)  x <= y
 71  #
 72
 73  #! [docs-python-quickstart-6 start]
 74  # Formally, constraints are also terms. Their sort is Boolean.
 75  # We will construct these constraints gradually,
 76  # by defining each of their components.
 77  # We start with the constant numerals 0 and 1:
 78  zero = tm.mkReal(0)
 79  one = tm.mkReal(1)
 80
 81  # Next, we construct the term x + y
 82  xPlusY = tm.mkTerm(Kind.ADD, x, y)
 83
 84  # Now we can define the constraints.
 85  # They use the operators +, <=, and <.
 86  # In the API, these are denoted by Plus, Leq, and Lt.
 87  constraint1 = tm.mkTerm(Kind.LT, zero, x)
 88  constraint2 = tm.mkTerm(Kind.LT, zero, y)
 89  constraint3 = tm.mkTerm(Kind.LT, xPlusY, one)
 90  constraint4 = tm.mkTerm(Kind.LEQ, x, y)
 91
 92  # Now we assert the constraints to the solver.
 93  solver.assertFormula(constraint1)
 94  solver.assertFormula(constraint2)
 95  solver.assertFormula(constraint3)
 96  solver.assertFormula(constraint4)
 97  #! [docs-python-quickstart-6 end]
 98
 99  # Check if the formula is satisfiable, that is,
100  # are there real values for x and y that satisfy all the constraints?
101  #! [docs-python-quickstart-7 start]
102  r1 = solver.checkSat()
103  #! [docs-python-quickstart-7 end]
104
105  # The result is either SAT, UNSAT, or UNKNOWN.
106  # In this case, it is SAT.
107  #! [docs-python-quickstart-8 start]
108  print("expected: sat")
109  print("result: ", r1)
110  #! [docs-python-quickstart-8 end]
111
112  # We can get the values for x and y that satisfy the constraints.
113  #! [docs-python-quickstart-9 start]
114  xVal = solver.getValue(x)
115  yVal = solver.getValue(y)
116  #! [docs-python-quickstart-9 end]
117
118  # It is also possible to get values for compound terms,
119  # even if those did not appear in the original formula.
120  #! [docs-python-quickstart-10 start]
121  xMinusY = tm.mkTerm(Kind.SUB, x, y)
122  xMinusYVal = solver.getValue(xMinusY)
123  #! [docs-python-quickstart-10 end]
124
125  # We can now obtain the values as python values
126  #! [docs-python-quickstart-11 start]
127  xPy = xVal.getRealValue()
128  yPy = yVal.getRealValue()
129  xMinusYPy = xMinusYVal.getRealValue()
130
131  print("value for x: ", xPy)
132  print("value for y: ", yPy)
133  print("value for x - y: ", xMinusYPy)
134  #! [docs-python-quickstart-11 end]
135
136  # Another way to independently compute the value of x - y would be
137  # to use the python minus operator instead of asking the solver.
138  # However, for more complex terms,
139  # it is easier to let the solver do the evaluation.
140  #! [docs-python-quickstart-12 start]
141  xMinusYComputed = xPy - yPy
142  if xMinusYComputed == xMinusYPy:
143    print("computed correctly")
144  else:
145    print("computed incorrectly")
146  #! [docs-python-quickstart-12 end]
147
148  # Further, we can convert the values to strings
149  #! [docs-python-quickstart-13 start]
150  xStr = str(xPy)
151  yStr = str(yPy)
152  xMinusYStr = str(xMinusYPy)
153  #! [docs-python-quickstart-13 end]
154
155  # Next, we will check satisfiability of the same formula,
156  # only this time over integer variables a and b.
157
158  # We start by resetting assertions added to the solver.
159  #! [docs-python-quickstart-14 start]
160  solver.resetAssertions()
161  #! [docs-python-quickstart-14 end]
162
163  # Next, we assert the same assertions above with integers.
164  # This time, we inline the construction of terms
165  # to the assertion command.
166  #! [docs-python-quickstart-15 start]
167  solver.assertFormula(tm.mkTerm(Kind.LT, tm.mkInteger(0), a))
168  solver.assertFormula(tm.mkTerm(Kind.LT, tm.mkInteger(0), b))
169  solver.assertFormula(
170      tm.mkTerm(
171          Kind.LT, tm.mkTerm(Kind.ADD, a, b), tm.mkInteger(1)))
172  solver.assertFormula(tm.mkTerm(Kind.LEQ, a, b))
173  #! [docs-python-quickstart-15 end]
174
175  # We check whether the revised assertion is satisfiable.
176  #! [docs-python-quickstart-16 start]
177  r2 = solver.checkSat()
178  #! [docs-python-quickstart-16 end]
179
180  # This time the formula is unsatisfiable
181  #! [docs-python-quickstart-17 start]
182  print("expected: unsat")
183  print("result:", r2)
184  #! [docs-python-quickstart-17 end]
185
186  # We can query the solver for an unsatisfiable core, i.e., a subset
187  # of the assertions that is already unsatisfiable.
188  #! [docs-python-quickstart-18 start]
189  unsatCore = solver.getUnsatCore()
190  print("unsat core size:", len(unsatCore))
191  print("unsat core:", unsatCore)
192  #! [docs-python-quickstart-18 end]