Quickstart Guide

First, 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, y = Reals('x y')
a, b = Ints('a b')

We define the following constraints regarding x and y :

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

We check whether there is a solution to these constraints:

solve(0 < x, 0 < y, x + y < 1, x <= y)

In this case, there is, so we get output:

[x = 1/6, y = 1/6]

We can also get an explicit model (assignment) for the constraints.

s = Solver()
s.add(0 < x, 0 < y, x + y < 1, x <= y)
assert sat == s.check()
m = s.model()

With the model, we can evaluate variables and terms:

print('x:', m[x])
print('y:', m[y])
print('x - y:', m[x - y])

This will print:

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

We can also get these values in other forms:

print('string x:', str(m[x]))
print('decimal x:', m[x].as_decimal(4))
print('fraction x:', m[x].as_fraction())
print('float x:', float(m[x].as_fraction()))

Next, we assert the same assertions as above, but with integers. This time, there is no solution, so “no solution” is printed.

solve(0 < a, 0 < b, a + b < 1, a <= b)

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