Theory of Floating-Points
examples/api/cpp/floating_point_arith.cpp
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * An example of solving floating-point problems with cvc5's cpp API.
11 *
12 * This example shows to create floating-point types, variables and expressions,
13 * and how to create rounding mode constants by solving toy problems. The
14 * example also shows making special values (such as NaN and +oo) and converting
15 * an IEEE 754-2008 bit-vector to a floating-point number.
16 */
17
18#include <cvc5/cvc5.h>
19
20#include <iostream>
21#include <cassert>
22
23using namespace cvc5;
24
25int main()
26{
27 TermManager tm;
28 Solver solver(tm);
29 solver.setOption("incremental", "true");
30 solver.setOption("produce-models", "true");
31
32 // Make single precision floating-point variables
33 Sort fpt32 = tm.mkFloatingPointSort(8, 24);
34 Term a = tm.mkConst(fpt32, "a");
35 Term b = tm.mkConst(fpt32, "b");
36 Term c = tm.mkConst(fpt32, "c");
37 Term d = tm.mkConst(fpt32, "d");
38 Term e = tm.mkConst(fpt32, "e");
39 // Rounding mode
40 Term rm = tm.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN);
41
42 std::cout << "Show that fused multiplication and addition `(fp.fma RM a b c)`"
43 << std::endl
44 << "is different from `(fp.add RM (fp.mul a b) c)`:" << std::endl;
45 solver.push(1);
46 Term fma = tm.mkTerm(Kind::FLOATINGPOINT_FMA, {rm, a, b, c});
47 Term mul = tm.mkTerm(Kind::FLOATINGPOINT_MULT, {rm, a, b});
48 Term add = tm.mkTerm(Kind::FLOATINGPOINT_ADD, {rm, mul, c});
49 solver.assertFormula(tm.mkTerm(Kind::DISTINCT, {fma, add}));
50 Result r = solver.checkSat(); // result is sat
51 std::cout << "Expect sat: " << r << std::endl;
52 std::cout << "Value of `a`: " << solver.getValue(a) << std::endl;
53 std::cout << "Value of `b`: " << solver.getValue(b) << std::endl;
54 std::cout << "Value of `c`: " << solver.getValue(c) << std::endl;
55 std::cout << "Value of `(fp.fma RNE a b c)`: " << solver.getValue(fma)
56 << std::endl;
57 std::cout << "Value of `(fp.add RNE (fp.mul a b) c)`: "
58 << solver.getValue(add) << std::endl;
59 std::cout << std::endl;
60 solver.pop(1);
61
62 std::cout << "Show that floating-point addition is not associative:"
63 << std::endl;
64 std::cout << "(a + (b + c)) != ((a + b) + c)" << std::endl;
65 solver.push(1);
66 solver.assertFormula(tm.mkTerm(
67 Kind::DISTINCT,
68 {tm.mkTerm(Kind::FLOATINGPOINT_ADD,
69 {rm, a, tm.mkTerm(Kind::FLOATINGPOINT_ADD, {rm, b, c})}),
70 tm.mkTerm(Kind::FLOATINGPOINT_ADD,
71 {rm, tm.mkTerm(Kind::FLOATINGPOINT_ADD, {rm, a, b}), c})}));
72
73 r = solver.checkSat(); // result is sat
74 std::cout << "Expect sat: " << r << std::endl;
75 assert (r.isSat());
76
77 std::cout << "Value of `a`: " << solver.getValue(a) << std::endl;
78 std::cout << "Value of `b`: " << solver.getValue(b) << std::endl;
79 std::cout << "Value of `c`: " << solver.getValue(c) << std::endl;
80 std::cout << std::endl;
81
82 std::cout << "Now, restrict `a` to be either NaN or positive infinity:"
83 << std::endl;
84 Term nan = tm.mkFloatingPointNaN(8, 24);
85 Term inf = tm.mkFloatingPointPosInf(8, 24);
86 solver.assertFormula(tm.mkTerm(
87 Kind::OR,
88 {tm.mkTerm(Kind::EQUAL, {a, inf}), tm.mkTerm(Kind::EQUAL, {a, nan})}));
89
90 r = solver.checkSat(); // result is sat
91 std::cout << "Expect sat: " << r << std::endl;
92 assert (r.isSat());
93
94 std::cout << "Value of `a`: " << solver.getValue(a) << std::endl;
95 std::cout << "Value of `b`: " << solver.getValue(b) << std::endl;
96 std::cout << "Value of `c`: " << solver.getValue(c) << std::endl;
97 std::cout << std::endl;
98 solver.pop(1);
99
100 std::cout << "Now, try to find a (normal) floating-point number that rounds"
101 << std::endl
102 << "to different integer values for different rounding modes:"
103 << std::endl;
104 solver.push(1);
105 Term rtp = tm.mkRoundingMode(RoundingMode::ROUND_TOWARD_POSITIVE);
106 Term rtn = tm.mkRoundingMode(RoundingMode::ROUND_TOWARD_NEGATIVE);
107 Op op = tm.mkOp(Kind::FLOATINGPOINT_TO_UBV, {16}); // (_ fp.to_ubv 16)
108 Term lhs = tm.mkTerm(op, {rtp, d});
109 Term rhs = tm.mkTerm(op, {rtn, d});
110 solver.assertFormula(tm.mkTerm(Kind::FLOATINGPOINT_IS_NORMAL, {d}));
111 solver.assertFormula(
112 tm.mkTerm(Kind::NOT, {tm.mkTerm(Kind::EQUAL, {lhs, rhs})}));
113
114 r = solver.checkSat(); // result is sat
115 std::cout << "Expect sat: " << r << std::endl;
116 assert (r.isSat());
117 std::cout << std::endl;
118
119 std::cout << "Get value of `d` as floating-point, bit-vector and real:"
120 << std::endl;
121 Term val = solver.getValue(d);
122 std::cout << "Value of `d`: " << val << std::endl;
123 std::cout << "Value of `((_ fp.to_ubv 16) RTP d)`: " << solver.getValue(lhs)
124 << std::endl;
125 std::cout << "Value of `((_ fp.to_ubv 16) RTN d)`: " << solver.getValue(rhs)
126 << std::endl;
127 std::cout << "Value of `(fp.to_real d)` "
128 << solver.getValue(tm.mkTerm(Kind::FLOATINGPOINT_TO_REAL, {val}))
129 << std::endl;
130 std::cout << std::endl;
131 solver.pop(1);
132
133 std::cout << "Finally, try to find a floating-point number between positive"
134 << std::endl
135 << "zero and the smallest positive floating-point number:"
136 << std::endl;
137 Term zero = tm.mkFloatingPointPosZero(8, 24);
138 Term smallest = tm.mkFloatingPoint(8, 24, tm.mkBitVector(32, 1));
139 solver.assertFormula(
140 tm.mkTerm(Kind::AND,
141 {tm.mkTerm(Kind::FLOATINGPOINT_LT, {zero, e}),
142 tm.mkTerm(Kind::FLOATINGPOINT_LT, {e, smallest})}));
143
144 r = solver.checkSat(); // result is unsat
145 std::cout << "Expect unsat: " << r << std::endl;
146 assert(r.isUnsat());
147}
examples/api/c/floating_point_arith.c
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * An example of solving floating-point problems with cvc5's cpp API.
11 *
12 * This example shows to create floating-point types, variables and expressions,
13 * and how to create rounding mode constants by solving toy problems. The
14 * example also shows making special values (such as NaN and +oo) and converting
15 * an IEEE 754-2008 bit-vector to a floating-point number.
16 */
17
18#include <assert.h>
19#include <cvc5/c/cvc5.h>
20#include <stdio.h>
21
22int main()
23{
24 Cvc5TermManager* tm = cvc5_term_manager_new();
25 Cvc5* slv = cvc5_new(tm);
26 cvc5_set_option(slv, "incremental", "true");
27 cvc5_set_option(slv, "produce-models", "true");
28
29 // Make single precision floating-point variables
30 Cvc5Sort fp32 = cvc5_mk_fp_sort(tm, 8, 24);
31 Cvc5Term a = cvc5_mk_const(tm, fp32, "a");
32 Cvc5Term b = cvc5_mk_const(tm, fp32, "b");
33 Cvc5Term c = cvc5_mk_const(tm, fp32, "c");
34 Cvc5Term d = cvc5_mk_const(tm, fp32, "d");
35 Cvc5Term e = cvc5_mk_const(tm, fp32, "e");
36
37 // Rounding mode
38 Cvc5Term rm = cvc5_mk_rm(tm, CVC5_RM_ROUND_NEAREST_TIES_TO_EVEN);
39
40 printf("Show that fused multiplication and addition `(fp.fma RM a b c)`\n");
41 printf("is different from `(fp.add RM (fp.mul a b) c)`:\n");
42 cvc5_push(slv, 1);
43
44 Cvc5Term args4[4] = {rm, a, b, c};
45 Cvc5Term fma = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_FMA, 4, args4);
46 Cvc5Term args3[3] = {rm, a, b};
47 Cvc5Term mul = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_MULT, 3, args3);
48 args3[0] = rm;
49 args3[1] = mul;
50 args3[2] = c;
51 Cvc5Term add = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_ADD, 3, args3);
52 Cvc5Term args2[2] = {fma, add};
53 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_DISTINCT, 2, args2));
54
55 Cvc5Result r = cvc5_check_sat(slv); // result is sat
56 assert(cvc5_result_is_sat(r));
57 printf("Expect sat: %s\n", cvc5_result_to_string(r));
58 printf("Value of `a`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, a)));
59 printf("Value of `b`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, b)));
60 printf("Value of `c`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, c)));
61 printf("Value of `(fp.fma RNE a b c)`: %s\n",
62 cvc5_term_to_string(cvc5_get_value(slv, fma)));
63 printf("Value of `(fp.add RNE (fp.mul a b) c)`: %s\n\n",
64 cvc5_term_to_string(cvc5_get_value(slv, add)));
65 cvc5_pop(slv, 1);
66
67 printf("Show that floating-point addition is not associative:\n");
68 printf("(a + (b + c)) != ((a + b) + c)\n");
69 cvc5_push(slv, 1);
70
71 args3[0] = rm;
72 args3[1] = b;
73 args3[2] = c;
74 Cvc5Term fp_add = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_ADD, 3, args3);
75 args3[0] = rm;
76 args3[1] = a;
77 args3[2] = fp_add;
78 Cvc5Term lhs = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_ADD, 3, args3);
79 args3[0] = rm;
80 args3[1] = a;
81 args3[2] = b;
82 cvc5_term_release(fp_add); // optional, not needed anymore so we can release
83 fp_add = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_ADD, 3, args3);
84 args3[0] = rm;
85 args3[1] = fp_add;
86 args3[2] = c;
87 Cvc5Term rhs = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_ADD, 3, args3);
88
89 args2[0] = lhs;
90 args2[1] = rhs;
91 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_DISTINCT, 2, args2));
92
93 cvc5_result_release(r); // optional, not needed anymore so we can release
94 r = cvc5_check_sat(slv); // result is sat
95 assert(cvc5_result_is_sat(r));
96 printf("Expect sat: %s\n", cvc5_result_to_string(r));
97 printf("Value of `a`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, a)));
98 printf("Value of `b`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, b)));
99 printf("Value of `c`: %s\n\n", cvc5_term_to_string(cvc5_get_value(slv, c)));
100
101 printf("Now, restrict `a` to be either NaN or positive infinity:\n");
102 Cvc5Term nan = cvc5_mk_fp_nan(tm, 8, 24);
103 Cvc5Term inf = cvc5_mk_fp_pos_inf(tm, 8, 24);
104 args2[0] = a;
105 args2[1] = inf;
106 Cvc5Term eq1 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
107 args2[0] = a;
108 args2[1] = nan;
109 Cvc5Term eq2 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
110 args2[0] = eq1;
111 args2[1] = eq2;
112 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_OR, 2, args2));
113
114 cvc5_result_release(r); // optional, not needed anymore so we can release
115 r = cvc5_check_sat(slv); // result is sat
116 assert(cvc5_result_is_sat(r));
117 printf("Expect sat: %s\n", cvc5_result_to_string(r));
118 printf("Value of `a`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, a)));
119 printf("Value of `b`: %s\n", cvc5_term_to_string(cvc5_get_value(slv, b)));
120 printf("Value of `c`: %s\n\n", cvc5_term_to_string(cvc5_get_value(slv, c)));
121 cvc5_pop(slv, 1);
122
123 printf("Now, try to find a (normal) floating-point number that rounds\n");
124 printf("to different integer values for different rounding modes:\n");
125 cvc5_push(slv, 1);
126
127 Cvc5Term rtp = cvc5_mk_rm(tm, CVC5_RM_ROUND_TOWARD_POSITIVE);
128 Cvc5Term rtn = cvc5_mk_rm(tm, CVC5_RM_ROUND_TOWARD_NEGATIVE);
129 // (_ fp.to_ubv 16)
130 uint32_t idxs[1] = {16};
131 Cvc5Op op = cvc5_mk_op(tm, CVC5_KIND_FLOATINGPOINT_TO_UBV, 1, idxs);
132 args2[0] = rtp;
133 args2[1] = d;
134 cvc5_term_release(lhs); // optional, not needed anymore so we can release
135 lhs = cvc5_mk_term_from_op(tm, op, 2, args2);
136 args2[0] = rtn;
137 args2[1] = d;
138 cvc5_term_release(rhs); // optional, not needed anymore so we can release
139 rhs = cvc5_mk_term_from_op(tm, op, 2, args2);
140 Cvc5Term args1[1] = {d};
141 cvc5_assert_formula(
142 slv, cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_IS_NORMAL, 1, args1));
143 args2[0] = lhs;
144 args2[1] = rhs;
145 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_DISTINCT, 2, args2));
146
147 cvc5_result_release(r); // optional, not needed anymore so we can release
148 r = cvc5_check_sat(slv); // result is sat
149 assert(cvc5_result_is_sat(r));
150 printf("Expect sat: %s\n\n", cvc5_result_to_string(r));
151
152 printf("Get value of `d` as floating-point, bit-vector and real:\n");
153
154 Cvc5Term val = cvc5_get_value(slv, d);
155 printf("Value of `d`: %s\n", cvc5_term_to_string(val));
156 printf("Value of `((_ fp.to_ubv 16) RTP d)`: %s\n",
157 cvc5_term_to_string(cvc5_get_value(slv, lhs)));
158 printf("Value of `((_ fp.to_ubv 16) RTN d)`: %s\n",
159 cvc5_term_to_string(cvc5_get_value(slv, rhs)));
160 args1[0] = val;
161 Cvc5Term real_val = cvc5_get_value(
162 slv, cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_TO_REAL, 1, args1));
163 printf("Value of `(fp.to_real d)` %s\n\n", cvc5_term_to_string(real_val));
164 cvc5_pop(slv, 1);
165
166 printf("Finally, try to find a floating-point number between positive\n");
167 printf("zero and the smallest positive floating-point number:\n");
168 Cvc5Term zero = cvc5_mk_fp_pos_zero(tm, 8, 24);
169 Cvc5Term smallest = cvc5_mk_fp(tm, 8, 24, cvc5_mk_bv_uint64(tm, 32, 1));
170
171 args2[0] = zero;
172 args2[1] = e;
173 cvc5_term_release(lhs); // optional, not needed anymore so we can release
174 lhs = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_LT, 2, args2);
175 args2[0] = e;
176 args2[1] = smallest;
177 cvc5_term_release(rhs); // optional, not needed anymore so we can release
178 rhs = cvc5_mk_term(tm, CVC5_KIND_FLOATINGPOINT_LT, 2, args2);
179 args2[0] = lhs;
180 args2[1] = rhs;
181 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_AND, 2, args2));
182
183 cvc5_result_release(r); // optional, not needed anymore so we can release
184 r = cvc5_check_sat(slv); // result is unsat
185 assert(cvc5_result_is_unsat(r));
186 printf("Expect unsat: %s\n", cvc5_result_to_string(r));
187
188 cvc5_delete(slv);
189 cvc5_term_manager_delete(tm);
190 return 0;
191}
examples/api/java/FloatingPointArith.java
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * An example of solving floating-point problems with cvc5's Java API
11 *
12 * This example shows to create floating-point types, variables and expressions,
13 * and how to create rounding mode constants by solving toy problems. The
14 * example also shows making special values (such as NaN and +oo) and converting
15 * an IEEE 754-2008 bit-vector to a floating-point number.
16 */
17
18import static io.github.cvc5.Kind.*;
19
20import io.github.cvc5.*;
21
22public class FloatingPointArith
23{
24 public static void main(String[] args) throws CVC5ApiException
25 {
26 TermManager tm = new TermManager();
27 Solver solver = new Solver(tm);
28 {
29 solver.setOption("incremental", "true");
30 solver.setOption("produce-models", "true");
31
32 // Make single precision floating-point variables
33 Sort fpt32 = tm.mkFloatingPointSort(8, 24);
34 Term a = tm.mkConst(fpt32, "a");
35 Term b = tm.mkConst(fpt32, "b");
36 Term c = tm.mkConst(fpt32, "c");
37 Term d = tm.mkConst(fpt32, "d");
38 Term e = tm.mkConst(fpt32, "e");
39 // Rounding mode
40 Term rm = tm.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN);
41
42 System.out.println("Show that fused multiplication and addition `(fp.fma RM a b c)`");
43 System.out.println("is different from `(fp.add RM (fp.mul a b) c)`:");
44 solver.push(1);
45 Term fma = tm.mkTerm(Kind.FLOATINGPOINT_FMA, new Term[] {rm, a, b, c});
46 Term mul = tm.mkTerm(Kind.FLOATINGPOINT_MULT, rm, a, b);
47 Term add = tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, mul, c);
48 solver.assertFormula(tm.mkTerm(Kind.DISTINCT, fma, add));
49 Result r = solver.checkSat(); // result is sat
50 System.out.println("Expect sat: " + r);
51 System.out.println("Value of `a`: " + solver.getValue(a));
52 System.out.println("Value of `b`: " + solver.getValue(b));
53 System.out.println("Value of `c`: " + solver.getValue(c));
54 System.out.println("Value of `(fp.fma RNE a b c)`: " + solver.getValue(fma));
55 System.out.println("Value of `(fp.add RNE (fp.mul a b) c)`: " + solver.getValue(add));
56 System.out.println();
57 solver.pop(1);
58
59 System.out.println("Show that floating-point addition is not associative:");
60 System.out.println("(a + (b + c)) != ((a + b) + c)");
61 Term lhs =
62 tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, a, tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, b, c));
63 Term rhs =
64 tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, a, b), c);
65 solver.assertFormula(tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.EQUAL, a, b)));
66
67 r = solver.checkSat(); // result is sat
68 assert r.isSat();
69
70 System.out.println("Value of `a`: " + solver.getValue(a));
71 System.out.println("Value of `b`: " + solver.getValue(b));
72 System.out.println("Value of `c`: " + solver.getValue(c));
73
74 System.out.println("Now, restrict `a` to be either NaN or positive infinity:");
75 Term nan = tm.mkFloatingPointNaN(8, 24);
76 Term inf = tm.mkFloatingPointPosInf(8, 24);
77 solver.assertFormula(
78 tm.mkTerm(Kind.OR, tm.mkTerm(Kind.EQUAL, a, inf), tm.mkTerm(Kind.EQUAL, a, nan)));
79
80 r = solver.checkSat(); // result is sat
81 assert r.isSat();
82
83 System.out.println("Value of `a`: " + solver.getValue(a));
84 System.out.println("Value of `b`: " + solver.getValue(b));
85 System.out.println("Value of `c`: " + solver.getValue(c));
86
87 System.out.println("Now, try to find a (normal) floating-point number that rounds");
88 System.out.println("to different integer values for different rounding modes:");
89 Term rtp = tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE);
90 Term rtn = tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE);
91 Op op = tm.mkOp(Kind.FLOATINGPOINT_TO_UBV, 16); // (_ fp.to_ubv 16)
92 lhs = tm.mkTerm(op, rtp, d);
93 rhs = tm.mkTerm(op, rtn, d);
94 solver.assertFormula(tm.mkTerm(Kind.FLOATINGPOINT_IS_NORMAL, d));
95 solver.assertFormula(tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.EQUAL, lhs, rhs)));
96
97 r = solver.checkSat(); // result is sat
98 assert r.isSat();
99
100 System.out.println("Get value of `d` as floating-point, bit-vector and real:");
101 Term val = solver.getValue(d);
102 System.out.println("Value of `d`: " + val);
103 System.out.println("Value of `((_ fp.to_ubv 16) RTP d)`: " + solver.getValue(lhs));
104 System.out.println("Value of `((_ fp.to_ubv 16) RTN d)`: " + solver.getValue(rhs));
105 System.out.println("Value of `(fp.to_real d)`: "
106 + solver.getValue(tm.mkTerm(Kind.FLOATINGPOINT_TO_REAL, val)));
107
108 System.out.println("Finally, try to find a floating-point number between positive");
109 System.out.println("zero and the smallest positive floating-point number:");
110 Term zero = tm.mkFloatingPointPosZero(8, 24);
111 Term smallest = tm.mkFloatingPoint(8, 24, tm.mkBitVector(32, 0b001));
112 solver.assertFormula(tm.mkTerm(Kind.AND,
113 tm.mkTerm(Kind.FLOATINGPOINT_LT, zero, e),
114 tm.mkTerm(Kind.FLOATINGPOINT_LT, e, smallest)));
115
116 r = solver.checkSat(); // result is unsat
117 assert !r.isSat();
118 }
119 Context.deletePointers();
120 }
121}
examples/api/python/pythonic/floating_point.py
1###############################################################################
2# This file is part of the cvc5 project.
3#
4# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5# in the top-level source directory and their institutional affiliations.
6# All rights reserved. See the file COPYING in the top-level source
7# directory for licensing information.
8# #############################################################################
9#
10# An example of solving floating-point problems with cvc5's Python API.
11#
12# This example shows to create floating-point types, variables and expressions,
13# and how to create rounding mode constants by solving toy problems. The
14# example also shows making special values (such as NaN and +oo) and converting
15# an IEEE 754-2008 bit-vector to a floating-point number.
16##
17from cvc5.pythonic import *
18
19if __name__ == "__main__":
20 x, y, z = FPs("x y z", Float32())
21 set_default_rounding_mode(RoundNearestTiesToEven())
22
23 # FP addition is *not* commutative. This finds a counterexample.
24 assert not is_tautology(fpEQ(x + y, y + x))
25
26 # Without NaN or infinities, it is commutative. This proof succeeds.
27 assert is_tautology(
28 Implies(
29 Not(Or(fpIsNaN(x), fpIsNaN(y), fpIsInf(x), fpIsInf(y))), fpEQ(x + y, y + x)
30 )
31 )
32
33 pi = FPVal(+3.14, Float32())
34
35 # FP addition is *not* associative in the range (-pi, pi).
36 assert not is_tautology(
37 Implies(
38 And(x >= -pi, x <= pi, y >= -pi, y <= pi, z >= -pi, z <= pi),
39 fpEQ((x + y) + z, x + (y + z)),
40 )
41 )
examples/api/python/floating_point.py
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# A simple demonstration of the solving capabilities of the cvc5
12# floating point solver through the Python API contributed by Eva
13# Darulova. This requires building cvc5 with symfpu.
14##
15
16import cvc5
17from cvc5 import Kind, RoundingMode
18
19if __name__ == "__main__":
20 tm = cvc5.TermManager()
21 slv = cvc5.Solver(tm)
22
23 slv.setOption("produce-models", "true")
24 slv.setLogic("QF_FP")
25
26 # single 32-bit precision
27 fp32 = tm.mkFloatingPointSort(8, 24)
28
29 # rounding mode
30 rm = tm.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN)
31
32 # create a few single-precision variables
33 a = tm.mkConst(fp32, 'a')
34 b = tm.mkConst(fp32, 'b')
35 c = tm.mkConst(fp32, 'c')
36 d = tm.mkConst(fp32, 'd')
37 e = tm.mkConst(fp32, 'e')
38
39 print("Show that fused multiplication and addition `(fp.fma RM a b c)`")
40 print("is different from `(fp.add RM (fp.mul a b) c)`:")
41 slv.push()
42 fma = tm.mkTerm(Kind.FLOATINGPOINT_FMA, rm, a, b, c)
43 mul = tm.mkTerm(Kind.FLOATINGPOINT_MULT, rm, a, b)
44 add = tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, mul, c)
45 slv.assertFormula(tm.mkTerm(Kind.DISTINCT, fma, add))
46 print("Expect SAT.")
47 print("cvc5:", slv.checkSat())
48 print(f'Value of `a`: {slv.getValue(a)}')
49 print(f'Value of `b`: {slv.getValue(b)}')
50 print(f'Value of `c`: {slv.getValue(c)}')
51 print(f'Value of `(fp.fma RNE a b c)`: {slv.getValue(fma)}')
52 print(f'Value of `(fp.add RNE (fp.mul a b) c)`: {slv.getValue(add)}')
53 print();
54 slv.pop();
55
56 print("Show that floating-point addition is not associative:")
57 print("(a + (b + c)) != ((a + b) + c)")
58 slv.push()
59 slv.assertFormula(tm.mkTerm(
60 Kind.DISTINCT,
61 tm.mkTerm(Kind.FLOATINGPOINT_ADD,
62 rm, a, tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, b, c)),
63 tm.mkTerm(Kind.FLOATINGPOINT_ADD,
64 rm, tm.mkTerm(Kind.FLOATINGPOINT_ADD, rm, a, b), c)))
65 print("Expect SAT.")
66 print("cvc5:", slv.checkSat())
67
68 print(f'Value of `a`: {slv.getValue(a)}')
69 print(f'Value of `b`: {slv.getValue(b)}')
70 print(f'Value of `c`: {slv.getValue(c)}')
71 print()
72
73 print("Now, restrict `a` to be either NaN or positive infinity:")
74 nan = tm.mkFloatingPointNaN(8, 24)
75 inf = tm.mkFloatingPointPosInf(8, 24)
76 slv.assertFormula(tm.mkTerm(
77 Kind.OR, tm.mkTerm(Kind.EQUAL, a, inf), tm.mkTerm(Kind.EQUAL, a, nan)))
78 print("Expect SAT.")
79 print("cvc5:", slv.checkSat())
80
81 print(f'Value of `a`: {slv.getValue(a)}')
82 print(f'Value of `b`: {slv.getValue(b)}')
83 print(f'Value of `c`: {slv.getValue(c)}')
84 print()
85 slv.pop(1)
86
87 print("Now, try to find a (normal) floating-point number that rounds")
88 print("to different integer values for different rounding modes:")
89 slv.push()
90 rtp = tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE)
91 rtn = tm.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE)
92 op = tm.mkOp(Kind.FLOATINGPOINT_TO_UBV, 16) # (_ fp.to_ubv 16)
93 lhs = tm.mkTerm(op, rtp, d)
94 rhs = tm.mkTerm(op, rtn, d)
95 slv.assertFormula(tm.mkTerm(Kind.FLOATINGPOINT_IS_NORMAL, d))
96 slv.assertFormula(tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.EQUAL, lhs, rhs)))
97
98 print("Expect SAT.")
99 print("cvc5:", slv.checkSat())
100
101 print("Get value of `d` as floating-point, bit-vector and real:")
102 val = slv.getValue(d)
103 print(f'Value of `d`: {val}')
104 print(f'Value of `((_ fp.to_ubv 16) RTP d)`: {slv.getValue(lhs)}')
105 print(f'Value of `((_ fp.to_ubv 16) RTN d)`: {slv.getValue(rhs)}')
106 print(f'Value of `(fp.to_real d)`: {slv.getValue(tm.mkTerm(Kind.FLOATINGPOINT_TO_REAL, val))}')
107 print()
108 slv.pop()
109
110 print("Finally, try to find a floating-point number between positive")
111 print("zero and the smallest positive floating-point number:")
112 zero = tm.mkFloatingPointPosZero(8, 24)
113 smallest = tm.mkFloatingPoint(8, 24, tm.mkBitVector(32, 0b001))
114 slv.assertFormula(tm.mkTerm(
115 Kind.AND, tm.mkTerm(Kind.FLOATINGPOINT_LT, zero, e),
116 tm.mkTerm(Kind.FLOATINGPOINT_LT, e, smallest)))
117 print("Expect UNSAT.")
118 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)