mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
66 lines
2.0 KiB
Python
66 lines
2.0 KiB
Python
###############################################################################
|
|
# Top contributors (to current version):
|
|
# Alex Ozdemir, Aina Niemetz
|
|
#
|
|
# This file is part of the cvc5 project.
|
|
#
|
|
# Copyright (c) 2009-2024 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]
|
|
|
|
|
|
|