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