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/pythonic/quickstart.py

 1###############################################################################
 2# This file is part of the cvc5 project.
 3#
 4# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
 5# in the top-level source directory and their institutional affiliations.
 6# All rights reserved.  See the file COPYING in the top-level source
 7# directory for licensing information.
 8# #############################################################################
 9#
10# A simple demonstration of the API capabilities of cvc5.
11##
12from cvc5.pythonic import *
13
14if __name__ == '__main__':
15
16    # Let's introduce some variables
17    #! [docs-pythonic-quickstart-1 start]
18    x, y = Reals('x y')
19    a, b = Ints('a b')
20    #! [docs-pythonic-quickstart-1 end]
21
22    # We will confirm that
23    #  * 0 < x
24    #  * 0 < y
25    #  * x + y < 1
26    #  * x <= y
27    # are satisfiable
28    #! [docs-pythonic-quickstart-2 start]
29    solve(0 < x, 0 < y, x + y < 1, x <= y)
30    #! [docs-pythonic-quickstart-2 end]
31
32    # If we get the model (the satisfying assignment) explicitly, we can
33    # evaluate terms under it.
34    #! [docs-pythonic-quickstart-3 start]
35    s = Solver()
36    s.add(0 < x, 0 < y, x + y < 1, x <= y)
37    assert sat == s.check()
38    m = s.model()
39    #! [docs-pythonic-quickstart-3 end]
40
41    #! [docs-pythonic-quickstart-4 start]
42    print('x:', m[x])
43    print('y:', m[y])
44    print('x - y:', m[x - y])
45    #! [docs-pythonic-quickstart-4 end]
46
47    # We can also get these values in other forms:
48    #! [docs-pythonic-quickstart-5 start]
49    print('string x:', str(m[x]))
50    print('decimal x:', m[x].as_decimal(4))
51    print('fraction x:', m[x].as_fraction())
52    print('float x:', float(m[x].as_fraction()))
53    #! [docs-pythonic-quickstart-5 end]
54
55    # The above constraints are *UNSAT* for integer variables.
56    # This reports "no solution"
57    #! [docs-pythonic-quickstart-6 start]
58    solve(0 < a, 0 < b, a + b < 1, a <= b)
59    #! [docs-pythonic-quickstart-6 end]
60
61
62