Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Mathias Preiner, Martin Brain
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * SymFPU glue code for floating-point values.
14 : : */
15 : : #include "util/floatingpoint_literal_symfpu.h"
16 : :
17 : : #include "base/check.h"
18 : :
19 : : #include "symfpu/core/add.h"
20 : : #include "symfpu/core/classify.h"
21 : : #include "symfpu/core/compare.h"
22 : : #include "symfpu/core/convert.h"
23 : : #include "symfpu/core/divide.h"
24 : : #include "symfpu/core/fma.h"
25 : : #include "symfpu/core/ite.h"
26 : : #include "symfpu/core/multiply.h"
27 : : #include "symfpu/core/packing.h"
28 : : #include "symfpu/core/remainder.h"
29 : : #include "symfpu/core/sign.h"
30 : : #include "symfpu/core/sqrt.h"
31 : : #include "symfpu/utils/numberOfRoundingModes.h"
32 : : #include "symfpu/utils/properties.h"
33 : :
34 : : /* -------------------------------------------------------------------------- */
35 : :
36 : : namespace symfpu {
37 : :
38 : : #define CVC5_LIT_ITE_DFN(T) \
39 : : template <> \
40 : : struct ite<cvc5::internal::symfpuLiteral::Cvc5Prop, T> \
41 : : { \
42 : : static const T& iteOp(const cvc5::internal::symfpuLiteral::Cvc5Prop& cond, \
43 : : const T& l, \
44 : : const T& r) \
45 : : { \
46 : : return cond ? l : r; \
47 : : } \
48 : : }
49 : :
50 : : CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::rm);
51 [ + + ]: 733718 : CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::prop);
52 [ + + ]: 466982 : CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::sbv);
53 [ + + ]: 548057 : CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::ubv);
54 : :
55 : : #undef CVC5_LIT_ITE_DFN
56 : : } // namespace symfpu
57 : :
58 : : /* -------------------------------------------------------------------------- */
59 : :
60 : : namespace cvc5::internal {
61 : :
62 : 233 : uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size)
63 : : {
64 : 233 : return SymFPUUnpackedFloatLiteral::exponentWidth(size);
65 : : }
66 : :
67 : 172 : uint32_t FloatingPointLiteral::getUnpackedSignificandWidth(
68 : : FloatingPointSize& size)
69 : : {
70 : 172 : return SymFPUUnpackedFloatLiteral::significandWidth(size);
71 : : }
72 : :
73 : 6174 : FloatingPointLiteral::FloatingPointLiteral(uint32_t exp_size,
74 : : uint32_t sig_size,
75 : 6174 : const BitVector& bv)
76 : : : d_fp_size(exp_size, sig_size)
77 : : ,
78 : : d_symuf(symfpu::unpack<symfpuLiteral::traits>(
79 : 6174 : symfpuLiteral::Cvc5FPSize(exp_size, sig_size), bv))
80 : : {
81 : 6174 : }
82 : :
83 : 224 : FloatingPointLiteral::FloatingPointLiteral(
84 : 224 : const FloatingPointSize& size, FloatingPointLiteral::SpecialConstKind kind)
85 : : : d_fp_size(size)
86 : : ,
87 : 224 : d_symuf(SymFPUUnpackedFloatLiteral::makeNaN(size))
88 : : {
89 [ - + ][ - + ]: 224 : Assert(kind == FloatingPointLiteral::SpecialConstKind::FPNAN);
[ - - ]
90 : 224 : }
91 : :
92 : 818 : FloatingPointLiteral::FloatingPointLiteral(
93 : : const FloatingPointSize& size,
94 : : FloatingPointLiteral::SpecialConstKind kind,
95 : 818 : bool sign)
96 : : : d_fp_size(size)
97 : : ,
98 : : d_symuf(kind == FloatingPointLiteral::SpecialConstKind::FPINF
99 : : ? SymFPUUnpackedFloatLiteral::makeInf(size, sign)
100 [ + + ]: 818 : : SymFPUUnpackedFloatLiteral::makeZero(size, sign))
101 : : {
102 [ + + ][ - + ]: 818 : Assert(kind == FloatingPointLiteral::SpecialConstKind::FPINF
[ - + ][ - - ]
103 : : || kind == FloatingPointLiteral::SpecialConstKind::FPZERO);
104 : 818 : }
105 : :
106 : 32 : FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
107 : 32 : const BitVector& bv)
108 : : : d_fp_size(size)
109 : : ,
110 : 32 : d_symuf(symfpu::unpack<symfpuLiteral::traits>(size, bv))
111 : : {
112 : 32 : }
113 : :
114 : 160 : FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
115 : : const RoundingMode& rm,
116 : : const BitVector& bv,
117 : 160 : bool signedBV)
118 : : : d_fp_size(size)
119 : : ,
120 : : d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>(
121 : 0 : symfpuLiteral::Cvc5FPSize(size),
122 : 0 : symfpuLiteral::Cvc5RM(rm),
123 [ - - ]: 10 : symfpuLiteral::Cvc5SignedBitVector(bv))
124 : : : symfpu::convertUBVToFloat<symfpuLiteral::traits>(
125 : 0 : symfpuLiteral::Cvc5FPSize(size),
126 : 0 : symfpuLiteral::Cvc5RM(rm),
127 [ + + ][ + + ]: 160 : symfpuLiteral::Cvc5UnsignedBitVector(bv)))
[ + + ][ - - ]
128 : : {
129 : 160 : }
130 : :
131 : 40643 : BitVector FloatingPointLiteral::pack(void) const
132 : : {
133 : 40643 : BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_symuf));
134 : 40643 : return bv;
135 : : }
136 : :
137 : 258 : FloatingPointLiteral FloatingPointLiteral::absolute(void) const
138 : : {
139 : : return FloatingPointLiteral(
140 : 516 : d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_symuf));
141 : : }
142 : :
143 : 641 : FloatingPointLiteral FloatingPointLiteral::negate(void) const
144 : : {
145 : : return FloatingPointLiteral(
146 : 1282 : d_fp_size, symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_symuf));
147 : : }
148 : :
149 : 5125 : FloatingPointLiteral FloatingPointLiteral::add(
150 : : const RoundingMode& rm, const FloatingPointLiteral& arg) const
151 : : {
152 [ - + ][ - + ]: 5125 : Assert(d_fp_size == arg.d_fp_size);
[ - - ]
153 : 5125 : return FloatingPointLiteral(d_fp_size,
154 : 5125 : symfpu::add<symfpuLiteral::traits>(
155 : 10250 : d_fp_size, rm, d_symuf, arg.d_symuf, true));
156 : : }
157 : :
158 : 0 : FloatingPointLiteral FloatingPointLiteral::sub(
159 : : const RoundingMode& rm, const FloatingPointLiteral& arg) const
160 : : {
161 : 0 : Assert(d_fp_size == arg.d_fp_size);
162 : 0 : return FloatingPointLiteral(d_fp_size,
163 : 0 : symfpu::add<symfpuLiteral::traits>(
164 : 0 : d_fp_size, rm, d_symuf, arg.d_symuf, false));
165 : : }
166 : :
167 : 2526 : FloatingPointLiteral FloatingPointLiteral::mult(
168 : : const RoundingMode& rm, const FloatingPointLiteral& arg) const
169 : : {
170 [ - + ][ - + ]: 2526 : Assert(d_fp_size == arg.d_fp_size);
[ - - ]
171 : 2526 : return FloatingPointLiteral(d_fp_size,
172 : 2526 : symfpu::multiply<symfpuLiteral::traits>(
173 : 5052 : d_fp_size, rm, d_symuf, arg.d_symuf));
174 : : }
175 : :
176 : 2890 : FloatingPointLiteral FloatingPointLiteral::div(
177 : : const RoundingMode& rm, const FloatingPointLiteral& arg) const
178 : : {
179 [ - + ][ - + ]: 2890 : Assert(d_fp_size == arg.d_fp_size);
[ - - ]
180 : 2890 : return FloatingPointLiteral(d_fp_size,
181 : 2890 : symfpu::divide<symfpuLiteral::traits>(
182 : 5780 : d_fp_size, rm, d_symuf, arg.d_symuf));
183 : : }
184 : :
185 : 0 : FloatingPointLiteral FloatingPointLiteral::fma(
186 : : const RoundingMode& rm,
187 : : const FloatingPointLiteral& arg1,
188 : : const FloatingPointLiteral& arg2) const
189 : : {
190 : 0 : Assert(d_fp_size == arg1.d_fp_size);
191 : 0 : Assert(d_fp_size == arg2.d_fp_size);
192 : : return FloatingPointLiteral(
193 : 0 : d_fp_size,
194 : 0 : symfpu::fma<symfpuLiteral::traits>(
195 : 0 : d_fp_size, rm, d_symuf, arg1.d_symuf, arg2.d_symuf));
196 : : }
197 : :
198 : 1280 : FloatingPointLiteral FloatingPointLiteral::sqrt(const RoundingMode& rm) const
199 : : {
200 : : return FloatingPointLiteral(
201 : 2560 : d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
202 : : }
203 : :
204 : 210 : FloatingPointLiteral FloatingPointLiteral::rti(const RoundingMode& rm) const
205 : : {
206 : : return FloatingPointLiteral(
207 : 210 : d_fp_size,
208 : 420 : symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
209 : : }
210 : :
211 : 544 : FloatingPointLiteral FloatingPointLiteral::rem(
212 : : const FloatingPointLiteral& arg) const
213 : : {
214 [ - + ][ - + ]: 544 : Assert(d_fp_size == arg.d_fp_size);
[ - - ]
215 : 544 : return FloatingPointLiteral(d_fp_size,
216 : 544 : symfpu::remainder<symfpuLiteral::traits>(
217 : 1088 : d_fp_size, d_symuf, arg.d_symuf));
218 : : }
219 : :
220 : 424 : FloatingPointLiteral FloatingPointLiteral::maxTotal(
221 : : const FloatingPointLiteral& arg, bool zeroCaseLeft) const
222 : : {
223 [ - + ][ - + ]: 424 : Assert(d_fp_size == arg.d_fp_size);
[ - - ]
224 : : return FloatingPointLiteral(
225 : 424 : d_fp_size,
226 : 424 : symfpu::max<symfpuLiteral::traits>(
227 : 848 : d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
228 : : }
229 : :
230 : 18 : FloatingPointLiteral FloatingPointLiteral::minTotal(
231 : : const FloatingPointLiteral& arg, bool zeroCaseLeft) const
232 : : {
233 [ - + ][ - + ]: 18 : Assert(d_fp_size == arg.d_fp_size);
[ - - ]
234 : : return FloatingPointLiteral(
235 : 18 : d_fp_size,
236 : 18 : symfpu::min<symfpuLiteral::traits>(
237 : 36 : d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
238 : : }
239 : :
240 : 26532 : bool FloatingPointLiteral::operator==(const FloatingPointLiteral& fp) const
241 : : {
242 : 26532 : return ((d_fp_size == fp.d_fp_size)
243 [ + - ][ + + ]: 53064 : && symfpu::smtlibEqual<symfpuLiteral::traits>(
244 : 53064 : d_fp_size, d_symuf, fp.d_symuf));
245 : : }
246 : :
247 : 40 : bool FloatingPointLiteral::operator<=(const FloatingPointLiteral& arg) const
248 : : {
249 [ - + ][ - + ]: 40 : Assert(d_fp_size == arg.d_fp_size);
[ - - ]
250 : 80 : return symfpu::lessThanOrEqual<symfpuLiteral::traits>(
251 : 40 : d_fp_size, d_symuf, arg.d_symuf);
252 : : }
253 : :
254 : 2 : bool FloatingPointLiteral::operator<(const FloatingPointLiteral& arg) const
255 : : {
256 [ - + ][ - + ]: 2 : Assert(d_fp_size == arg.d_fp_size);
[ - - ]
257 : 4 : return symfpu::lessThan<symfpuLiteral::traits>(
258 : 2 : d_fp_size, d_symuf, arg.d_symuf);
259 : : }
260 : :
261 : 46 : BitVector FloatingPointLiteral::getExponent() const
262 : : {
263 : 46 : return d_symuf.exponent;
264 : : }
265 : :
266 : 46 : BitVector FloatingPointLiteral::getSignificand() const
267 : : {
268 : 46 : return d_symuf.significand;
269 : : }
270 : :
271 : 46 : bool FloatingPointLiteral::getSign() const
272 : : {
273 : 46 : return d_symuf.sign;
274 : : }
275 : :
276 : 32 : bool FloatingPointLiteral::isNormal(void) const
277 : : {
278 : 32 : return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
279 : : }
280 : :
281 : 35 : bool FloatingPointLiteral::isSubnormal(void) const
282 : : {
283 : 35 : return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
284 : : }
285 : :
286 : 500 : bool FloatingPointLiteral::isZero(void) const
287 : : {
288 : 500 : return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf);
289 : : }
290 : :
291 : 273 : bool FloatingPointLiteral::isInfinite(void) const
292 : : {
293 : 273 : return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf);
294 : : }
295 : :
296 : 258 : bool FloatingPointLiteral::isNaN(void) const
297 : : {
298 : 258 : return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf);
299 : : }
300 : :
301 : 116 : bool FloatingPointLiteral::isNegative(void) const
302 : : {
303 : 116 : return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf);
304 : : }
305 : :
306 : 109 : bool FloatingPointLiteral::isPositive(void) const
307 : : {
308 : 109 : return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_symuf);
309 : : }
310 : :
311 : 82 : FloatingPointLiteral FloatingPointLiteral::convert(
312 : : const FloatingPointSize& target, const RoundingMode& rm) const
313 : : {
314 : : return FloatingPointLiteral(
315 : : target,
316 : 82 : symfpu::convertFloatToFloat<symfpuLiteral::traits>(
317 : 164 : d_fp_size, target, rm, d_symuf));
318 : : }
319 : :
320 : 4 : BitVector FloatingPointLiteral::convertToSBVTotal(BitVectorSize width,
321 : : const RoundingMode& rm,
322 : : BitVector undefinedCase) const
323 : : {
324 : 12 : return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
325 : 12 : d_fp_size, rm, d_symuf, width, undefinedCase);
326 : : }
327 : :
328 : 8 : BitVector FloatingPointLiteral::convertToUBVTotal(BitVectorSize width,
329 : : const RoundingMode& rm,
330 : : BitVector undefinedCase) const
331 : : {
332 : 24 : return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
333 : 24 : d_fp_size, rm, d_symuf, width, undefinedCase);
334 : : }
335 : :
336 : : } // namespace cvc5::internal
|
