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