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 cvc5;
27
28int main()
29{
30 TermManager tm;
31 Solver solver(tm);
32 solver.setOption("incremental", "true");
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 // Rounding mode
43 Term rm = tm.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN);
44
45 std::cout << "Show that fused multiplication and addition `(fp.fma RM a b c)`"
46 << std::endl
47 << "is different from `(fp.add RM (fp.mul a b) c)`:" << std::endl;
48 solver.push(1);
49 Term fma = tm.mkTerm(Kind::FLOATINGPOINT_FMA, {rm, a, b, c});
50 Term mul = tm.mkTerm(Kind::FLOATINGPOINT_MULT, {rm, a, b});
51 Term add = tm.mkTerm(Kind::FLOATINGPOINT_ADD, {rm, mul, c});
52 solver.assertFormula(tm.mkTerm(Kind::DISTINCT, {fma, add}));
53 Result r = solver.checkSat(); // result is sat
54 std::cout << "Expect sat: " << r << std::endl;
55 std::cout << "Value of `a`: " << solver.getValue(a) << std::endl;
56 std::cout << "Value of `b`: " << solver.getValue(b) << std::endl;
57 std::cout << "Value of `c`: " << solver.getValue(c) << std::endl;
58 std::cout << "Value of `(fp.fma RNE a b c)`: " << solver.getValue(fma)
59 << std::endl;
60 std::cout << "Value of `(fp.add RNE (fp.mul a b) c)`: "
61 << solver.getValue(add) << std::endl;
62 std::cout << std::endl;
63 solver.pop(1);
64
65 std::cout << "Show that floating-point addition is not associative:"
66 << std::endl;
67 std::cout << "(a + (b + c)) != ((a + b) + c)" << std::endl;
68 solver.push(1);
69 solver.assertFormula(tm.mkTerm(
70 Kind::DISTINCT,
71 {tm.mkTerm(Kind::FLOATINGPOINT_ADD,
72 {rm, a, tm.mkTerm(Kind::FLOATINGPOINT_ADD, {rm, b, c})}),
73 tm.mkTerm(Kind::FLOATINGPOINT_ADD,
74 {rm, tm.mkTerm(Kind::FLOATINGPOINT_ADD, {rm, a, b}), c})}));
75
76 r = solver.checkSat(); // result is sat
77 std::cout << "Expect sat: " << r << std::endl;
78 assert (r.isSat());
79
80 std::cout << "Value of `a`: " << solver.getValue(a) << std::endl;
81 std::cout << "Value of `b`: " << solver.getValue(b) << std::endl;
82 std::cout << "Value of `c`: " << solver.getValue(c) << std::endl;
83 std::cout << std::endl;
84
85 std::cout << "Now, restrict `a` to be either NaN or positive infinity:"
86 << std::endl;
87 Term nan = tm.mkFloatingPointNaN(8, 24);
88 Term inf = tm.mkFloatingPointPosInf(8, 24);
89 solver.assertFormula(tm.mkTerm(
90 Kind::OR,
91 {tm.mkTerm(Kind::EQUAL, {a, inf}), tm.mkTerm(Kind::EQUAL, {a, nan})}));
92
93 r = solver.checkSat(); // result is sat
94 std::cout << "Expect sat: " << r << std::endl;
95 assert (r.isSat());
96
97 std::cout << "Value of `a`: " << solver.getValue(a) << std::endl;
98 std::cout << "Value of `b`: " << solver.getValue(b) << std::endl;
99 std::cout << "Value of `c`: " << solver.getValue(c) << std::endl;
100 std::cout << std::endl;
101 solver.pop(1);
102
103 std::cout << "Now, try to find a (normal) floating-point number that rounds"
104 << std::endl
105 << "to different integer values for different rounding modes:"
106 << std::endl;
107 solver.push(1);
108 Term rtp = tm.mkRoundingMode(RoundingMode::ROUND_TOWARD_POSITIVE);
109 Term rtn = tm.mkRoundingMode(RoundingMode::ROUND_TOWARD_NEGATIVE);
110 Op op = tm.mkOp(Kind::FLOATINGPOINT_TO_UBV, {16}); // (_ fp.to_ubv 16)
111 Term lhs = tm.mkTerm(op, {rtp, d});
112 Term rhs = tm.mkTerm(op, {rtn, d});
113 solver.assertFormula(tm.mkTerm(Kind::FLOATINGPOINT_IS_NORMAL, {d}));
114 solver.assertFormula(
115 tm.mkTerm(Kind::NOT, {tm.mkTerm(Kind::EQUAL, {lhs, rhs})}));
116
117 r = solver.checkSat(); // result is sat
118 std::cout << "Expect sat: " << r << std::endl;
119 assert (r.isSat());
120 std::cout << std::endl;
121
122 std::cout << "Get value of `d` as floating-point, bit-vector and real:"
123 << std::endl;
124 Term val = solver.getValue(d);
125 std::cout << "Value of `d`: " << val << std::endl;
126 std::cout << "Value of `((_ fp.to_ubv 16) RTP d)`: " << solver.getValue(lhs)
127 << std::endl;
128 std::cout << "Value of `((_ fp.to_ubv 16) RTN d)`: " << solver.getValue(rhs)
129 << std::endl;
130 std::cout << "Value of `(fp.to_real d)` "
131 << solver.getValue(tm.mkTerm(Kind::FLOATINGPOINT_TO_REAL, {val}))
132 << std::endl;
133 std::cout << std::endl;
134 solver.pop(1);
135
136 std::cout << "Finally, try to find a floating-point number between positive"
137 << std::endl
138 << "zero and the smallest positive floating-point number:"
139 << std::endl;
140 Term zero = tm.mkFloatingPointPosZero(8, 24);
141 Term smallest = tm.mkFloatingPoint(8, 24, tm.mkBitVector(32, 1));
142 solver.assertFormula(
143 tm.mkTerm(Kind::AND,
144 {tm.mkTerm(Kind::FLOATINGPOINT_LT, {zero, e}),
145 tm.mkTerm(Kind::FLOATINGPOINT_LT, {e, smallest})}));
146
147 r = solver.checkSat(); // result is unsat
148 std::cout << "Expect unsat: " << r << std::endl;
149 assert(r.isUnsat());
150}
examples/api/c/floating_point_arith.c
1/******************************************************************************
2 * Top contributors (to current version):
3 * 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 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 <assert.h>
22#include <cvc5/c/cvc5.h>
23#include <stdio.h>
24
25int main()
26{
27 Cvc5TermManager* tm = cvc5_term_manager_new();
28 Cvc5* slv = cvc5_new(tm);
29 cvc5_set_option(slv, "incremental", "true");
30 cvc5_set_option(slv, "produce-models", "true");
31
32 // Make single precision floating-point variables
33 Cvc5Sort fp32 = cvc5_mk_fp_sort(tm, 8, 24);
34 Cvc5Term a = cvc5_mk_const(tm, fp32, "a");
35 Cvc5Term b = cvc5_mk_const(tm, fp32, "b");
36 Cvc5Term c = cvc5_mk_const(tm, fp32, "c");
37 Cvc5Term d = cvc5_mk_const(tm, fp32, "d");
38 Cvc5Term e = cvc5_mk_const(tm, fp32, "e");
39
40 // Rounding mode
41 Cvc5Term rm = cvc5_mk_rm(tm, CVC5_RM_ROUND_NEAREST_TIES_TO_EVEN);
42
43 printf("Show that fused multiplication and addition `(fp.fma RM a b c)`\n");
44 printf("is different from `(fp.add RM (fp.mul a b) c)`:\n");
45 cvc5_push(slv, 1);
46
47 Cvc5Term args4[4] = {rm, a, b, c};
48 Cvc5Term fma = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_FMA, 4, args4);
49 Cvc5Term args3[3] = {rm, a, b};
50 Cvc5Term mul = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_MULT, 3, args3);
51 args3[0] = rm;
52 args3[1] = mul;
53 args3[2] = c;
54 Cvc5Term add = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_ADD, 3, args3);
55 Cvc5Term args2[2] = {fma, add};
56 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_DISTINCT, 2, args2));
57
58 Cvc5Result r = cvc5_check_sat(slv); // result is sat
59 assert(cvc5_result_is_sat(r));
60 printf("Expect sat: %s\n", cvc5_result_to_string(r));
61 printf("Value of `a`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, a)));
62 printf("Value of `b`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, b)));
63 printf("Value of `c`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, c)));
64 printf("Value of `(fp.fma RNE a b c)`: %s\n",
65 cvc5_term_to_string(cvc5_get_value(slv, fma)));
66 printf("Value of `(fp.add RNE (fp.mul a b) c)`: %s\n\n",
67 cvc5_term_to_string(cvc5_get_value(slv, add)));
68 cvc5_pop(slv, 1);
69
70 printf("Show that floating-point addition is not associative:\n");
71 printf("(a + (b + c)) != ((a + b) + c)\n");
72 cvc5_push(slv, 1);
73
74 args3[0] = rm;
75 args3[1] = b;
76 args3[2] = c;
77 Cvc5Term fp_add = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_ADD, 3, args3);
78 args3[0] = rm;
79 args3[1] = a;
80 args3[2] = fp_add;
81 Cvc5Term lhs = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_ADD, 3, args3);
82 args3[0] = rm;
83 args3[1] = a;
84 args3[2] = b;
85 cvc5_term_release(fp_add); // optional, not needed anymore so we can release
86 fp_add = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_ADD, 3, args3);
87 args3[0] = rm;
88 args3[1] = fp_add;
89 args3[2] = c;
90 Cvc5Term rhs = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_ADD, 3, args3);
91
92 args2[0] = lhs;
93 args2[1] = rhs;
94 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_DISTINCT, 2, args2));
95
96 cvc5_result_release(r); // optional, not needed anymore so we can release
97 r = cvc5_check_sat(slv); // result is sat
98 assert(cvc5_result_is_sat(r));
99 printf("Expect sat: %s\n", cvc5_result_to_string(r));
100 printf("Value of `a`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, a)));
101 printf("Value of `b`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, b)));
102 printf("Value of `c`: %s\n\n", cvc5_term_to_string(cvc5_get_value(slv, c)));
103
104 printf("Now, restrict `a` to be either NaN or positive infinity:\n");
105 Cvc5Term nan = cvc5_mk_fp_nan(tm, 8, 24);
106 Cvc5Term inf = cvc5_mk_fp_pos_inf(tm, 8, 24);
107 args2[0] = a;
108 args2[1] = inf;
109 Cvc5Term eq1 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
110 args2[0] = a;
111 args2[1] = nan;
112 Cvc5Term eq2 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
113 args2[0] = eq1;
114 args2[1] = eq2;
115 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_OR, 2, args2));
116
117 cvc5_result_release(r); // optional, not needed anymore so we can release
118 r = cvc5_check_sat(slv); // result is sat
119 assert(cvc5_result_is_sat(r));
120 printf("Expect sat: %s\n", cvc5_result_to_string(r));
121 printf("Value of `a`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, a)));
122 printf("Value of `b`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, b)));
123 printf("Value of `c`: %s\n\n", cvc5_term_to_string(cvc5_get_value(slv, c)));
124 cvc5_pop(slv, 1);
125
126 printf("Now, try to find a (normal) floating-point number that rounds\n");
127 printf("to different integer values for different rounding modes:\n");
128 cvc5_push(slv, 1);
129
130 Cvc5Term rtp = cvc5_mk_rm(tm, CVC5_RM_ROUND_TOWARD_POSITIVE);
131 Cvc5Term rtn = cvc5_mk_rm(tm, CVC5_RM_ROUND_TOWARD_NEGATIVE);
132 // (_ fp.to_ubv 16)
133 uint32_t idxs[1] = {16};
134 Cvc5Op op = cvc5_mk_op(tm, CVC5_KIND_FLOATINGPOINT_TO_UBV, 1, idxs);
135 args2[0] = rtp;
136 args2[1] = d;
137 cvc5_term_release(lhs); // optional, not needed anymore so we can release
138 lhs = cvc5_mk_term_from_op(tm, op, 2, args2);
139 args2[0] = rtn;
140 args2[1] = d;
141 cvc5_term_release(rhs); // optional, not needed anymore so we can release
142 rhs = cvc5_mk_term_from_op(tm, op, 2, args2);
143 Cvc5Term args1[1] = {d};
144 cvc5_assert_formula(
145 slv, cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_IS_NORMAL, 1, args1));
146 args2[0] = lhs;
147 args2[1] = rhs;
148 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_DISTINCT, 2, args2));
149
150 cvc5_result_release(r); // optional, not needed anymore so we can release
151 r = cvc5_check_sat(slv); // result is sat
152 assert(cvc5_result_is_sat(r));
153 printf("Expect sat: %s\n\n", cvc5_result_to_string(r));
154
155 printf("Get value of `d` as floating-point, bit-vector and real:\n");
156
157 Cvc5Term val = cvc5_get_value(slv, d);
158 printf("Value of `d`: %s\n", cvc5_term_to_string(val));
159 printf("Value of `((_ fp.to_ubv 16) RTP d)`: %s\n",
160 cvc5_term_to_string(cvc5_get_value(slv, lhs)));
161 printf("Value of `((_ fp.to_ubv 16) RTN d)`: %s\n",
162 cvc5_term_to_string(cvc5_get_value(slv, rhs)));
163 args1[0] = val;
164 Cvc5Term real_val = cvc5_get_value(
165 slv, cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_TO_REAL, 1, args1));
166 printf("Value of `(fp.to_real d)` %s\n\n", cvc5_term_to_string(real_val));
167 cvc5_pop(slv, 1);
168
169 printf("Finally, try to find a floating-point number between positive\n");
170 printf("zero and the smallest positive floating-point number:\n");
171 Cvc5Term zero = cvc5_mk_fp_pos_zero(tm, 8, 24);
172 Cvc5Term smallest = cvc5_mk_fp(tm, 8, 24, cvc5_mk_bv_uint64(tm, 32, 1));
173
174 args2[0] = zero;
175 args2[1] = e;
176 cvc5_term_release(lhs); // optional, not needed anymore so we can release
177 lhs = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_LT, 2, args2);
178 args2[0] = e;
179 args2[1] = smallest;
180 cvc5_term_release(rhs); // optional, not needed anymore so we can release
181 rhs = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_LT, 2, args2);
182 args2[0] = lhs;
183 args2[1] = rhs;
184 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_AND, 2, args2));
185
186 cvc5_result_release(r); // optional, not needed anymore so we can release
187 r = cvc5_check_sat(slv); // result is unsat
188 assert(cvc5_result_is_unsat(r));
189 printf("Expect unsat: %s\n", cvc5_result_to_string(r));
190
191 cvc5_delete(slv);
192 cvc5_term_manager_delete(tm);
193 return 0;
194}
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 TermManager tm = new TermManager();
30 Solver solver = new Solver(tm);
31 {
32 solver.setOption("incremental", "true");
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 // Rounding mode
43 Term rm = tm.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN);
44
45 System.out.println("Show that fused multiplication and addition `(fp.fma RM a b c)`");
46 System.out.println("is different from `(fp.add RM (fp.mul a b) c)`:");
47 solver.push(1);
48 Term fma = tm.mkTerm(Kind.FLOATINGPOINT_FMA, new Term[] {rm, a, b, c});
49 Term mul = tm.mkTerm(Kind.FLOATINGPOINT_MULT, rm, a, b);
50 Term add = tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, mul, c);
51 solver.assertFormula(tm.mkTerm(Kind.DISTINCT, fma, add));
52 Result r = solver.checkSat(); // result is sat
53 System.out.println("Expect sat: " + r);
54 System.out.println("Value of `a`: " + solver.getValue(a));
55 System.out.println("Value of `b`: " + solver.getValue(b));
56 System.out.println("Value of `c`: " + solver.getValue(c));
57 System.out.println("Value of `(fp.fma RNE a b c)`: " + solver.getValue(fma));
58 System.out.println("Value of `(fp.add RNE (fp.mul a b) c)`: " + solver.getValue(add));
59 System.out.println();
60 solver.pop(1);
61
62 System.out.println("Show that floating-point addition is not associative:");
63 System.out.println("(a + (b + c)) != ((a + b) + c)");
64 Term lhs =
65 tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, a, tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, b, c));
66 Term rhs =
67 tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, a, b), c);
68 solver.assertFormula(tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.EQUAL, a, b)));
69
70 r = solver.checkSat(); // result is sat
71 assert r.isSat();
72
73 System.out.println("Value of `a`: " + solver.getValue(a));
74 System.out.println("Value of `b`: " + solver.getValue(b));
75 System.out.println("Value of `c`: " + solver.getValue(c));
76
77 System.out.println("Now, restrict `a` to be either NaN or positive infinity:");
78 Term nan = tm.mkFloatingPointNaN(8, 24);
79 Term inf = tm.mkFloatingPointPosInf(8, 24);
80 solver.assertFormula(
81 tm.mkTerm(Kind.OR, tm.mkTerm(Kind.EQUAL, a, inf), tm.mkTerm(Kind.EQUAL, a, nan)));
82
83 r = solver.checkSat(); // result is sat
84 assert r.isSat();
85
86 System.out.println("Value of `a`: " + solver.getValue(a));
87 System.out.println("Value of `b`: " + solver.getValue(b));
88 System.out.println("Value of `c`: " + solver.getValue(c));
89
90 System.out.println("Now, try to find a (normal) floating-point number that rounds");
91 System.out.println("to different integer values for different rounding modes:");
92 Term rtp = tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE);
93 Term rtn = tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE);
94 Op op = tm.mkOp(Kind.FLOATINGPOINT_TO_UBV, 16); // (_ fp.to_ubv 16)
95 lhs = tm.mkTerm(op, rtp, d);
96 rhs = tm.mkTerm(op, rtn, d);
97 solver.assertFormula(tm.mkTerm(Kind.FLOATINGPOINT_IS_NORMAL, d));
98 solver.assertFormula(tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.EQUAL, lhs, rhs)));
99
100 r = solver.checkSat(); // result is sat
101 assert r.isSat();
102
103 System.out.println("Get value of `d` as floating-point, bit-vector and real:");
104 Term val = solver.getValue(d);
105 System.out.println("Value of `d`: " + val);
106 System.out.println("Value of `((_ fp.to_ubv 16) RTP d)`: " + solver.getValue(lhs));
107 System.out.println("Value of `((_ fp.to_ubv 16) RTN d)`: " + solver.getValue(rhs));
108 System.out.println("Value of `(fp.to_real d)`: "
109 + solver.getValue(tm.mkTerm(Kind.FLOATINGPOINT_TO_REAL, val)));
110
111 System.out.println("Finally, try to find a floating-point number between positive");
112 System.out.println("zero and the smallest positive floating-point number:");
113 Term zero = tm.mkFloatingPointPosZero(8, 24);
114 Term smallest = tm.mkFloatingPoint(8, 24, tm.mkBitVector(32, 0b001));
115 solver.assertFormula(tm.mkTerm(Kind.AND,
116 tm.mkTerm(Kind.FLOATINGPOINT_LT, zero, e),
117 tm.mkTerm(Kind.FLOATINGPOINT_LT, e, smallest)));
118
119 r = solver.checkSat(); // result is unsat
120 assert !r.isSat();
121 }
122 Context.deletePointers();
123 }
124}
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 # rounding mode
33 rm = tm.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN)
34
35 # create a few single-precision variables
36 a = tm.mkConst(fp32, 'a')
37 b = tm.mkConst(fp32, 'b')
38 c = tm.mkConst(fp32, 'c')
39 d = tm.mkConst(fp32, 'd')
40 e = tm.mkConst(fp32, 'e')
41
42 print("Show that fused multiplication and addition `(fp.fma RM a b c)`")
43 print("is different from `(fp.add RM (fp.mul a b) c)`:")
44 slv.push()
45 fma = tm.mkTerm(Kind.FLOATINGPOINT_FMA, rm, a, b, c)
46 mul = tm.mkTerm(Kind.FLOATINGPOINT_MULT, rm, a, b)
47 add = tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, mul, c)
48 slv.assertFormula(tm.mkTerm(Kind.DISTINCT, fma, add))
49 print("Expect SAT.")
50 print("cvc5:", slv.checkSat())
51 print(f'Value of `a`: {slv.getValue(a)}')
52 print(f'Value of `b`: {slv.getValue(b)}')
53 print(f'Value of `c`: {slv.getValue(c)}')
54 print(f'Value of `(fp.fma RNE a b c)`: {slv.getValue(fma)}')
55 print(f'Value of `(fp.add RNE (fp.mul a b) c)`: {slv.getValue(add)}')
56 print();
57 slv.pop();
58
59 print("Show that floating-point addition is not associative:")
60 print("(a + (b + c)) != ((a + b) + c)")
61 slv.push()
62 slv.assertFormula(tm.mkTerm(
63 Kind.DISTINCT,
64 tm.mkTerm(Kind.FLOATINGPOINT_ADD,
65 rm, a, tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, b, c)),
66 tm.mkTerm(Kind.FLOATINGPOINT_ADD,
67 rm, tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, a, b), c)))
68 print("Expect SAT.")
69 print("cvc5:", slv.checkSat())
70
71 print(f'Value of `a`: {slv.getValue(a)}')
72 print(f'Value of `b`: {slv.getValue(b)}')
73 print(f'Value of `c`: {slv.getValue(c)}')
74 print()
75
76 print("Now, restrict `a` to be either NaN or positive infinity:")
77 nan = tm.mkFloatingPointNaN(8, 24)
78 inf = tm.mkFloatingPointPosInf(8, 24)
79 slv.assertFormula(tm.mkTerm(
80 Kind.OR, tm.mkTerm(Kind.EQUAL, a, inf), tm.mkTerm(Kind.EQUAL, a, nan)))
81 print("Expect SAT.")
82 print("cvc5:", slv.checkSat())
83
84 print(f'Value of `a`: {slv.getValue(a)}')
85 print(f'Value of `b`: {slv.getValue(b)}')
86 print(f'Value of `c`: {slv.getValue(c)}')
87 print()
88 slv.pop(1)
89
90 print("Now, try to find a (normal) floating-point number that rounds")
91 print("to different integer values for different rounding modes:")
92 slv.push()
93 rtp = tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE)
94 rtn = tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE)
95 op = tm.mkOp(Kind.FLOATINGPOINT_TO_UBV, 16) # (_ fp.to_ubv 16)
96 lhs = tm.mkTerm(op, rtp, d)
97 rhs = tm.mkTerm(op, rtn, d)
98 slv.assertFormula(tm.mkTerm(Kind.FLOATINGPOINT_IS_NORMAL, d))
99 slv.assertFormula(tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.EQUAL, lhs, rhs)))
100
101 print("Expect SAT.")
102 print("cvc5:", slv.checkSat())
103
104 print("Get value of `d` as floating-point, bit-vector and real:")
105 val = slv.getValue(d)
106 print(f'Value of `d`: {val}')
107 print(f'Value of `((_ fp.to_ubv 16) RTP d)`: {slv.getValue(lhs)}')
108 print(f'Value of `((_ fp.to_ubv 16) RTN d)`: {slv.getValue(rhs)}')
109 print(f'Value of `(fp.to_real d)`: {slv.getValue(tm.mkTerm(Kind.FLOATINGPOINT_TO_REAL, val))}')
110 print()
111 slv.pop()
112
113 print("Finally, try to find a floating-point number between positive")
114 print("zero and the smallest positive floating-point number:")
115 zero = tm.mkFloatingPointPosZero(8, 24)
116 smallest = tm.mkFloatingPoint(8, 24, tm.mkBitVector(32, 0b001))
117 slv.assertFormula(tm.mkTerm(
118 Kind.AND, tm.mkTerm(Kind.FLOATINGPOINT_LT, zero, e),
119 tm.mkTerm(Kind.FLOATINGPOINT_LT, e, smallest)))
120 print("Expect UNSAT.")
121 print("cvc5:", slv.checkSat())
examples/api/smtlib/floating_point_arith.smt2
1(set-logic QF_FP)
2(set-option :incremental true)
3(set-option :produce-models true)
4
5(declare-const a Float32)
6(declare-const b Float32)
7(declare-const c Float32)
8(declare-const d Float32)
9(declare-const e Float32)
10
11(echo "Show that fused multiplication and addition (fp.fma RM a b c) is")
12(echo "different from (fp.add RM (fp.mul RM a b) c)")
13(push 1)
14(declare-const rm RoundingMode)
15(assert (distinct (fp.fma rm a b c) (fp.add rm (fp.mul rm a b) c)))
16(echo "Expect sat")
17(check-sat)
18(echo "Value of `a`:")
19(get-value (a))
20(echo "Value of `b`:")
21(get-value (b))
22(echo "Value of `c`:")
23(get-value (c))
24(echo "Value of `RM`:")
25(get-value (rm))
26(echo "Value of `(fp.fma RM a b c)`:")
27(get-value ((fp.fma rm a b c)))
28(echo "Value of `(fp.add RM (fp.mul RM a b) c))`:")
29(get-value ((fp.add rm (fp.mul rm a b) c)))
30(pop 1)
31
32(echo "Show that floating-point addition is not associative:")
33(echo "(a + (b + c)) != ((a + b) + c)")
34(push 1)
35(assert (distinct (fp.add RNE a (fp.add RNE b c)) (fp.add RNE (fp.add RNE a b) c)))
36(echo "Expect sat")
37(check-sat)
38(echo "Value of `a`:")
39(get-value (a))
40(echo "Value of `b`:")
41(get-value (b))
42(echo "Value of `c`:")
43(get-value (c))
44(pop 1)
45
46(echo "Restrict `a` to be either NaN or positive infinity:")
47(push 1)
48(assert (or (= a (_ +oo 8 24)) (= a (_ NaN 8 24))))
49(echo "Expect sat")
50(check-sat)
51(get-value (a b c))
52(pop 1)
53
54(echo "Find normal FP number that rounds to different integer values for different rounding modes:")
55(push 1)
56(assert (fp.isNormal d))
57(assert (distinct ((_ fp.to_ubv 16) RTP d) ((_ fp.to_ubv 16) RTN d)))
58(echo "Expect sat")
59(check-sat)
60
61(echo "Value of `d`:")
62(get-value (d))
63(echo "Value of `((_ fp.to_ubv 16) RTP d)`:")
64(get-value (((_ fp.to_ubv 16) RTP d)))
65(echo "Value of `((_ fp.to_ubv 16) RTN d)`:")
66(get-value (((_ fp.to_ubv 16) RTN d)))
67(echo "Value of `d` as a rational:")
68(get-value ((fp.to_real d)))
69(pop 1)
70
71(echo "Find FP number between +zero and the smallest positive FP number:")
72(push 1)
73(assert (and (fp.lt (_ +zero 8 24) e) (fp.lt e ((_ to_fp 8 24) (_ bv1 32)))))
74
75(echo "Expect unsat")
76(check-sat)
77(pop 1)