Theory of Floating-Points ¶
examples/api/cpp/floating_point_arith.cpp
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Mathias Preiner, Andres Noetzli
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 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 * An example of solving floating-point problems with cvc5's cpp API
14 *
15 * This example shows to create floating-point types, variables and expressions,
16 * and how to create rounding mode constants by solving toy problems. The
17 * example also shows making special values (such as NaN and +oo) and converting
18 * an IEEE 754-2008 bit-vector to a floating-point number.
19 */
20
21 #include <cvc5/cvc5.h>
22
23 #include <iostream>
24 #include <cassert>
25
26 using namespace std;
27 using namespace cvc5;
28
29 int main()
30 {
31 Solver solver;
32 solver.setOption("produce-models", "true");
33
34 // Make single precision floating-point variables
35 Sort fpt32 = solver.mkFloatingPointSort(8, 24);
36 Term a = solver.mkConst(fpt32, "a");
37 Term b = solver.mkConst(fpt32, "b");
38 Term c = solver.mkConst(fpt32, "c");
39 Term d = solver.mkConst(fpt32, "d");
40 Term e = solver.mkConst(fpt32, "e");
41
42 // Assert that floating-point addition is not associative:
43 // (a + (b + c)) != ((a + b) + c)
44 Term rm = solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN);
45 Term lhs = solver.mkTerm(
46 FLOATINGPOINT_ADD, {rm, a, solver.mkTerm(FLOATINGPOINT_ADD, {rm, b, c})});
47 Term rhs = solver.mkTerm(
48 FLOATINGPOINT_ADD, {rm, solver.mkTerm(FLOATINGPOINT_ADD, {rm, a, b}), c});
49 solver.assertFormula(solver.mkTerm(NOT, {solver.mkTerm(EQUAL, {a, b})}));
50
51 Result r = solver.checkSat(); // result is sat
52 assert (r.isSat());
53
54 cout << "a = " << solver.getValue(a) << endl;
55 cout << "b = " << solver.getValue(b) << endl;
56 cout << "c = " << solver.getValue(c) << endl;
57
58 // Now, let's restrict `a` to be either NaN or positive infinity
59 Term nan = solver.mkFloatingPointNaN(8, 24);
60 Term inf = solver.mkFloatingPointPosInf(8, 24);
61 solver.assertFormula(solver.mkTerm(
62 OR, {solver.mkTerm(EQUAL, {a, inf}), solver.mkTerm(EQUAL, {a, nan})}));
63
64 r = solver.checkSat(); // result is sat
65 assert (r.isSat());
66
67 cout << "a = " << solver.getValue(a) << endl;
68 cout << "b = " << solver.getValue(b) << endl;
69 cout << "c = " << solver.getValue(c) << endl;
70
71 // And now for something completely different. Let's try to find a (normal)
72 // floating-point number that rounds to different integer values for
73 // different rounding modes.
74 Term rtp = solver.mkRoundingMode(ROUND_TOWARD_POSITIVE);
75 Term rtn = solver.mkRoundingMode(ROUND_TOWARD_NEGATIVE);
76 Op op = solver.mkOp(FLOATINGPOINT_TO_SBV, {16}); // (_ fp.to_sbv 16)
77 lhs = solver.mkTerm(op, {rtp, d});
78 rhs = solver.mkTerm(op, {rtn, d});
79 solver.assertFormula(solver.mkTerm(FLOATINGPOINT_IS_NORMAL, {d}));
80 solver.assertFormula(solver.mkTerm(NOT, {solver.mkTerm(EQUAL, {lhs, rhs})}));
81
82 r = solver.checkSat(); // result is sat
83 assert (r.isSat());
84
85 // Convert the result to a rational and print it
86 Term val = solver.getValue(d);
87 Term realVal = solver.getValue(solver.mkTerm(FLOATINGPOINT_TO_REAL, {val}));
88 cout << "d = " << val << " = " << realVal << endl;
89 cout << "((_ fp.to_sbv 16) RTP d) = " << solver.getValue(lhs) << endl;
90 cout << "((_ fp.to_sbv 16) RTN d) = " << solver.getValue(rhs) << endl;
91
92 // For our final trick, let's try to find a floating-point number between
93 // positive zero and the smallest positive floating-point number
94 Term zero = solver.mkFloatingPointPosZero(8, 24);
95 Term smallest = solver.mkFloatingPoint(8, 24, solver.mkBitVector(32, 0b001));
96 solver.assertFormula(
97 solver.mkTerm(AND,
98 {solver.mkTerm(FLOATINGPOINT_LT, {zero, e}),
99 solver.mkTerm(FLOATINGPOINT_LT, {e, smallest})}));
100
101 r = solver.checkSat(); // result is unsat
102 assert (!r.isSat());
103 }
examples/api/java/FloatingPointArith.java
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Andres Noetzli, Aina Niemetz
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 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 * An example of solving floating-point problems with cvc5's Java API
14 *
15 * This example shows to create floating-point types, variables and expressions,
16 * and how to create rounding mode constants by solving toy problems. The
17 * example also shows making special values (such as NaN and +oo) and converting
18 * an IEEE 754-2008 bit-vector to a floating-point number.
19 */
20
21 import static io.github.cvc5.Kind.*;
22
23 import io.github.cvc5.*;
24
25 public class FloatingPointArith
26 {
27 public static void main(String[] args) throws CVC5ApiException
28 {
29 try (Solver solver = new Solver())
30 {
31 solver.setOption("produce-models", "true");
32
33 // Make single precision floating-point variables
34 Sort fpt32 = solver.mkFloatingPointSort(8, 24);
35 Term a = solver.mkConst(fpt32, "a");
36 Term b = solver.mkConst(fpt32, "b");
37 Term c = solver.mkConst(fpt32, "c");
38 Term d = solver.mkConst(fpt32, "d");
39 Term e = solver.mkConst(fpt32, "e");
40
41 // Assert that floating-point addition is not associative:
42 // (a + (b + c)) != ((a + b) + c)
43 Term rm = solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN);
44 Term lhs = solver.mkTerm(
45 Kind.FLOATINGPOINT_ADD, rm, a, solver.mkTerm(Kind.FLOATINGPOINT_ADD, rm, b, c));
46 Term rhs = solver.mkTerm(
47 Kind.FLOATINGPOINT_ADD, rm, solver.mkTerm(Kind.FLOATINGPOINT_ADD, rm, a, b), c);
48 solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, a, b)));
49
50 Result r = solver.checkSat(); // result is sat
51 assert r.isSat();
52
53 System.out.println("a = " + solver.getValue(a));
54 System.out.println("b = " + solver.getValue(b));
55 System.out.println("c = " + solver.getValue(c));
56
57 // Now, let's restrict `a` to be either NaN or positive infinity
58 Term nan = solver.mkFloatingPointNaN(8, 24);
59 Term inf = solver.mkFloatingPointPosInf(8, 24);
60 solver.assertFormula(solver.mkTerm(
61 Kind.OR, solver.mkTerm(Kind.EQUAL, a, inf), solver.mkTerm(Kind.EQUAL, a, nan)));
62
63 r = solver.checkSat(); // result is sat
64 assert r.isSat();
65
66 System.out.println("a = " + solver.getValue(a));
67 System.out.println("b = " + solver.getValue(b));
68 System.out.println("c = " + solver.getValue(c));
69
70 // And now for something completely different. Let's try to find a (normal)
71 // floating-point number that rounds to different integer values for
72 // different rounding modes.
73 Term rtp = solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE);
74 Term rtn = solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE);
75 Op op = solver.mkOp(Kind.FLOATINGPOINT_TO_SBV, 16); // (_ fp.to_sbv 16)
76 lhs = solver.mkTerm(op, rtp, d);
77 rhs = solver.mkTerm(op, rtn, d);
78 solver.assertFormula(solver.mkTerm(Kind.FLOATINGPOINT_IS_NORMAL, d));
79 solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, lhs, rhs)));
80
81 r = solver.checkSat(); // result is sat
82 assert r.isSat();
83
84 // Convert the result to a rational and print it
85 Term val = solver.getValue(d);
86 Term realVal = solver.getValue(solver.mkTerm(FLOATINGPOINT_TO_REAL, val));
87 System.out.println("d = " + val + " = " + realVal);
88 System.out.println("((_ fp.to_sbv 16) RTP d) = " + solver.getValue(lhs));
89 System.out.println("((_ fp.to_sbv 16) RTN d) = " + solver.getValue(rhs));
90
91 // For our final trick, let's try to find a floating-point number between
92 // positive zero and the smallest positive floating-point number
93 Term zero = solver.mkFloatingPointPosZero(8, 24);
94 Term smallest = solver.mkFloatingPoint(8, 24, solver.mkBitVector(32, 0b001));
95 solver.assertFormula(solver.mkTerm(Kind.AND,
96 solver.mkTerm(Kind.FLOATINGPOINT_LT, zero, e),
97 solver.mkTerm(Kind.FLOATINGPOINT_LT, e, smallest)));
98
99 r = solver.checkSat(); // result is unsat
100 assert !r.isSat();
101 }
102 }
103 }
examples/api/python/pythonic/floating_point.py
1 from cvc5.pythonic import *
2
3 if __name__ == "__main__":
4 x, y, z = FPs("x y z", Float32())
5 set_default_rounding_mode(RoundNearestTiesToEven())
6
7 # FP addition is *not* commutative. This finds a counterexample.
8 assert not is_tautology(fpEQ(x + y, y + x))
9
10 # Without NaN or infinities, is is commutative. This proof succeeds.
11 assert is_tautology(
12 Implies(
13 Not(Or(fpIsNaN(x), fpIsNaN(y), fpIsInf(x), fpIsInf(y))), fpEQ(x + y, y + x)
14 )
15 )
16
17 pi = FPVal(+3.14, Float32())
18
19 # FP addition is *not* associative in the range (-pi, pi).
20 assert not is_tautology(
21 Implies(
22 And(x >= -pi, x <= pi, y >= -pi, y <= pi, z >= -pi, z <= pi),
23 fpEQ((x + y) + z, x + (y + z)),
24 )
25 )
examples/api/python/floating_point.py
1 #!/usr/bin/env python
2 ###############################################################################
3 # Top contributors (to current version):
4 # Aina Niemetz, Makai Mann, Mathias Preiner
5 #
6 # This file is part of the cvc5 project.
7 #
8 # Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
9 # in the top-level source directory and their institutional affiliations.
10 # All rights reserved. See the file COPYING in the top-level source
11 # directory for licensing information.
12 # #############################################################################
13 #
14 # A simple demonstration of the solving capabilities of the cvc5
15 # floating point solver through the Python API contributed by Eva
16 # Darulova. This requires building cvc5 with symfpu.
17 ##
18
19 import cvc5
20 from cvc5 import Kind, RoundingMode
21
22 if __name__ == "__main__":
23 slv = cvc5.Solver()
24
25 slv.setOption("produce-models", "true")
26 slv.setLogic("QF_FP")
27
28 # single 32-bit precision
29 fp32 = slv.mkFloatingPointSort(8, 24)
30
31 # the standard rounding mode
32 rm = slv.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN)
33
34 # create a few single-precision variables
35 x = slv.mkConst(fp32, 'x')
36 y = slv.mkConst(fp32, 'y')
37 z = slv.mkConst(fp32, 'z')
38
39 # check floating-point arithmetic is commutative, i.e. x + y == y + x
40 commutative = slv.mkTerm(
41 Kind.FLOATINGPOINT_EQ,
42 slv.mkTerm(Kind.FLOATINGPOINT_ADD, rm, x, y),
43 slv.mkTerm(Kind.FLOATINGPOINT_ADD, rm, y, x))
44
45 slv.push()
46 slv.assertFormula(slv.mkTerm(Kind.NOT, commutative))
47 print("Checking floating-point commutativity")
48 print("Expect SAT (property does not hold for NaN and Infinities).")
49 print("cvc5:", slv.checkSat())
50 print("Model for x:", slv.getValue(x))
51 print("Model for y:", slv.getValue(y))
52
53 # disallow NaNs and Infinities
54 slv.assertFormula(slv.mkTerm(
55 Kind.NOT, slv.mkTerm(Kind.FLOATINGPOINT_IS_NAN, x)))
56 slv.assertFormula(slv.mkTerm(
57 Kind.NOT, slv.mkTerm(Kind.FLOATINGPOINT_IS_INF, x)))
58 slv.assertFormula(slv.mkTerm(
59 Kind.NOT, slv.mkTerm(Kind.FLOATINGPOINT_IS_NAN, y)))
60 slv.assertFormula(slv.mkTerm(
61 Kind.NOT, slv.mkTerm(Kind.FLOATINGPOINT_IS_INF, y)))
62
63 print("Checking floating-point commutativity assuming x and y are not NaN or Infinity")
64 print("Expect UNSAT.")
65 print("cvc5:", slv.checkSat())
66
67 # check floating-point arithmetic is not associative
68 slv.pop()
69
70 # constrain x, y, z between -3.14 and 3.14 (also disallows NaN and infinity)
71 a = slv.mkFloatingPoint(
72 8,
73 24,
74 slv.mkBitVector(32, "11000000010010001111010111000011", 2)) # -3.14
75 b = slv.mkFloatingPoint(
76 8,
77 24,
78 slv.mkBitVector(32, "01000000010010001111010111000011", 2)) # 3.14
79
80 bounds_x = slv.mkTerm(
81 Kind.AND,
82 slv.mkTerm(Kind.FLOATINGPOINT_LEQ, a, x),
83 slv.mkTerm(Kind.FLOATINGPOINT_LEQ, x, b))
84 bounds_y = slv.mkTerm(
85 Kind.AND,
86 slv.mkTerm(Kind.FLOATINGPOINT_LEQ, a, y),
87 slv.mkTerm(Kind.FLOATINGPOINT_LEQ, y, b))
88 bounds_z = slv.mkTerm(
89 Kind.AND,
90 slv.mkTerm(Kind.FLOATINGPOINT_LEQ, a, z),
91 slv.mkTerm(Kind.FLOATINGPOINT_LEQ, z, b))
92 slv.assertFormula(slv.mkTerm(
93 Kind.AND, slv.mkTerm(Kind.AND, bounds_x, bounds_y), bounds_z))
94
95 # (x + y) + z == x + (y + z)
96 lhs = slv.mkTerm(
97 Kind.FLOATINGPOINT_ADD,
98 rm,
99 slv.mkTerm(Kind.FLOATINGPOINT_ADD, rm, x, y),
100 z)
101 rhs = slv.mkTerm(
102 Kind.FLOATINGPOINT_ADD,
103 rm,
104 x,
105 slv.mkTerm(Kind.FLOATINGPOINT_ADD, rm, y, z))
106 associative = slv.mkTerm(
107 Kind.NOT,
108 slv.mkTerm(Kind.FLOATINGPOINT_EQ, lhs, rhs))
109
110 slv.assertFormula(associative)
111
112 print("Checking floating-point associativity")
113 print("Expect SAT.")
114 print("cvc5:", slv.checkSat())
115 print("Model for x:", slv.getValue(x))
116 print("Model for y:", slv.getValue(y))
117 print("Model for z:", slv.getValue(z))