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
|
###############################################################################
# Top contributors (to current version):
# Alex Ozdemir, Anjiang-Wei
#
# 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.
# #############################################################################
#
# An example of solving floating-point problems with cvc5's Python API.
#
# This example shows to create floating-point types, variables and expressions,
# and how to create rounding mode constants by solving toy problems. The
# example also shows making special values (such as NaN and +oo) and converting
# an IEEE 754-2008 bit-vector to a floating-point number.
##
from cvc5.pythonic import *
if __name__ == "__main__":
x, y, z = FPs("x y z", Float32())
set_default_rounding_mode(RoundNearestTiesToEven())
# FP addition is *not* commutative. This finds a counterexample.
assert not is_tautology(fpEQ(x + y, y + x))
# Without NaN or infinities, it is commutative. This proof succeeds.
assert is_tautology(
Implies(
Not(Or(fpIsNaN(x), fpIsNaN(y), fpIsInf(x), fpIsInf(y))), fpEQ(x + y, y + x)
)
)
pi = FPVal(+3.14, Float32())
# FP addition is *not* associative in the range (-pi, pi).
assert not is_tautology(
Implies(
And(x >= -pi, x <= pi, y >= -pi, y <= pi, z >= -pi, z <= pi),
fpEQ((x + y) + z, x + (y + z)),
)
)
|
