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