Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/floatingpoint_literal_symfpu.cpp	Lines:	101	120	84.2 %
Date:	2021-09-29	Branches:	61	300	20.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Martin Brain, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * SymFPU glue code for floating-point values.
 */
#include "util/floatingpoint_literal_symfpu.h"

#include "base/check.h"

#include "symfpu/core/add.h"
#include "symfpu/core/classify.h"
#include "symfpu/core/compare.h"
#include "symfpu/core/convert.h"
#include "symfpu/core/divide.h"
#include "symfpu/core/fma.h"
#include "symfpu/core/ite.h"
#include "symfpu/core/multiply.h"
#include "symfpu/core/packing.h"
#include "symfpu/core/remainder.h"
#include "symfpu/core/sign.h"
#include "symfpu/core/sqrt.h"
#include "symfpu/utils/numberOfRoundingModes.h"
#include "symfpu/utils/properties.h"

/* -------------------------------------------------------------------------- */

namespace symfpu {

#define CVC5_LIT_ITE_DFN(T)                                            \
  template <>                                                          \
  struct ite<::cvc5::symfpuLiteral::Cvc5Prop, T>                       \
  {                                                                    \
    static const T& iteOp(const ::cvc5::symfpuLiteral::Cvc5Prop& cond, \
                          const T& l,                                  \
                          const T& r)                                  \
    {                                                                  \
      return cond ? l : r;                                             \
    }                                                                  \
  }

CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::rm);
CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::prop);
CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::sbv);
CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::ubv);

#undef CVC5_LIT_ITE_DFN
}  // namespace symfpu

/* -------------------------------------------------------------------------- */

namespace cvc5 {

uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size)
{
  return SymFPUUnpackedFloatLiteral::exponentWidth(size);
}

uint32_t FloatingPointLiteral::getUnpackedSignificandWidth(
    FloatingPointSize& size)
{
  return SymFPUUnpackedFloatLiteral::significandWidth(size);
}

FloatingPointLiteral::FloatingPointLiteral(uint32_t exp_size,
                                           uint32_t sig_size,
                                           const BitVector& bv)
    : d_fp_size(exp_size, sig_size)
      ,
      d_symuf(symfpu::unpack<symfpuLiteral::traits>(
          symfpuLiteral::Cvc5FPSize(exp_size, sig_size), bv))
{
}

FloatingPointLiteral::FloatingPointLiteral(
    const FloatingPointSize& size, FloatingPointLiteral::SpecialConstKind kind)
    : d_fp_size(size)
      ,
      d_symuf(SymFPUUnpackedFloatLiteral::makeNaN(size))
{
  Assert(kind == FloatingPointLiteral::SpecialConstKind::FPNAN);
}

FloatingPointLiteral::FloatingPointLiteral(
    const FloatingPointSize& size,
    FloatingPointLiteral::SpecialConstKind kind,
    bool sign)
    : d_fp_size(size)
      ,
      d_symuf(kind == FloatingPointLiteral::SpecialConstKind::FPINF
                  ? SymFPUUnpackedFloatLiteral::makeInf(size, sign)
                  : SymFPUUnpackedFloatLiteral::makeZero(size, sign))
{
  Assert(kind == FloatingPointLiteral::SpecialConstKind::FPINF
         || kind == FloatingPointLiteral::SpecialConstKind::FPZERO);
}

FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
                                           const BitVector& bv)
    : d_fp_size(size)
      ,
      d_symuf(symfpu::unpack<symfpuLiteral::traits>(size, bv))
{
}

FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
                                           const RoundingMode& rm,
                                           const BitVector& bv,
                                           bool signedBV)
    : d_fp_size(size)
      ,
      d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>(
                  symfpuLiteral::Cvc5FPSize(size),
                  symfpuLiteral::Cvc5RM(rm),
                  symfpuLiteral::Cvc5SignedBitVector(bv))
                       : symfpu::convertUBVToFloat<symfpuLiteral::traits>(
                           symfpuLiteral::Cvc5FPSize(size),
                           symfpuLiteral::Cvc5RM(rm),
                           symfpuLiteral::Cvc5UnsignedBitVector(bv)))
{
}

BitVector FloatingPointLiteral::pack(void) const
{
  BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_symuf));
  return bv;
}

FloatingPointLiteral FloatingPointLiteral::absolute(void) const
{
  return FloatingPointLiteral(
      d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_symuf));
}

FloatingPointLiteral FloatingPointLiteral::negate(void) const
{
  return FloatingPointLiteral(
      d_fp_size, symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_symuf));
}

FloatingPointLiteral FloatingPointLiteral::add(
    const RoundingMode& rm, const FloatingPointLiteral& arg) const
{
  Assert(d_fp_size == arg.d_fp_size);
  return FloatingPointLiteral(d_fp_size,
                              symfpu::add<symfpuLiteral::traits>(
                                  d_fp_size, rm, d_symuf, arg.d_symuf, true));
}

FloatingPointLiteral FloatingPointLiteral::sub(
    const RoundingMode& rm, const FloatingPointLiteral& arg) const
{
  Assert(d_fp_size == arg.d_fp_size);
  return FloatingPointLiteral(d_fp_size,
                              symfpu::add<symfpuLiteral::traits>(
                                  d_fp_size, rm, d_symuf, arg.d_symuf, false));
}

FloatingPointLiteral FloatingPointLiteral::mult(
    const RoundingMode& rm, const FloatingPointLiteral& arg) const
{
  Assert(d_fp_size == arg.d_fp_size);
  return FloatingPointLiteral(d_fp_size,
                              symfpu::multiply<symfpuLiteral::traits>(
                                  d_fp_size, rm, d_symuf, arg.d_symuf));
}

FloatingPointLiteral FloatingPointLiteral::div(
    const RoundingMode& rm, const FloatingPointLiteral& arg) const
{
  Assert(d_fp_size == arg.d_fp_size);
  return FloatingPointLiteral(d_fp_size,
                              symfpu::divide<symfpuLiteral::traits>(
                                  d_fp_size, rm, d_symuf, arg.d_symuf));
}

FloatingPointLiteral FloatingPointLiteral::fma(
    const RoundingMode& rm,
    const FloatingPointLiteral& arg1,
    const FloatingPointLiteral& arg2) const
{
  Assert(d_fp_size == arg1.d_fp_size);
  Assert(d_fp_size == arg2.d_fp_size);
  return FloatingPointLiteral(
      d_fp_size,
      symfpu::fma<symfpuLiteral::traits>(
          d_fp_size, rm, d_symuf, arg1.d_symuf, arg2.d_symuf));
}

FloatingPointLiteral FloatingPointLiteral::sqrt(const RoundingMode& rm) const
{
  return FloatingPointLiteral(
      d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
}

FloatingPointLiteral FloatingPointLiteral::rti(const RoundingMode& rm) const
{
  return FloatingPointLiteral(
      d_fp_size,
      symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
}

FloatingPointLiteral FloatingPointLiteral::rem(
    const FloatingPointLiteral& arg) const
{
  Assert(d_fp_size == arg.d_fp_size);
  return FloatingPointLiteral(d_fp_size,
                              symfpu::remainder<symfpuLiteral::traits>(
                                  d_fp_size, d_symuf, arg.d_symuf));
}

FloatingPointLiteral FloatingPointLiteral::maxTotal(
    const FloatingPointLiteral& arg, bool zeroCaseLeft) const
{
  Assert(d_fp_size == arg.d_fp_size);
  return FloatingPointLiteral(
      d_fp_size,
      symfpu::max<symfpuLiteral::traits>(
          d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
}

FloatingPointLiteral FloatingPointLiteral::minTotal(
    const FloatingPointLiteral& arg, bool zeroCaseLeft) const
{
  Assert(d_fp_size == arg.d_fp_size);
  return FloatingPointLiteral(
      d_fp_size,
      symfpu::min<symfpuLiteral::traits>(
          d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
}

bool FloatingPointLiteral::operator==(const FloatingPointLiteral& fp) const
{
  return ((d_fp_size == fp.d_fp_size)
          && symfpu::smtlibEqual<symfpuLiteral::traits>(
              d_fp_size, d_symuf, fp.d_symuf));
}

bool FloatingPointLiteral::operator<=(const FloatingPointLiteral& arg) const
{
  Assert(d_fp_size == arg.d_fp_size);
  return symfpu::lessThanOrEqual<symfpuLiteral::traits>(
      d_fp_size, d_symuf, arg.d_symuf);
}

bool FloatingPointLiteral::operator<(const FloatingPointLiteral& arg) const
{
  Assert(d_fp_size == arg.d_fp_size);
  return symfpu::lessThan<symfpuLiteral::traits>(
      d_fp_size, d_symuf, arg.d_symuf);
}

BitVector FloatingPointLiteral::getExponent() const
{
  return d_symuf.exponent;
}

BitVector FloatingPointLiteral::getSignificand() const
{
  return d_symuf.significand;
}

bool FloatingPointLiteral::getSign() const
{
  return d_symuf.sign;
}

bool FloatingPointLiteral::isNormal(void) const
{
  return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
}

bool FloatingPointLiteral::isSubnormal(void) const
{
  return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
}

bool FloatingPointLiteral::isZero(void) const
{
  return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf);
}

bool FloatingPointLiteral::isInfinite(void) const
{
  return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf);
}

bool FloatingPointLiteral::isNaN(void) const
{
  return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf);
}

bool FloatingPointLiteral::isNegative(void) const
{
  return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf);
}

bool FloatingPointLiteral::isPositive(void) const
{
  return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_symuf);
}

FloatingPointLiteral FloatingPointLiteral::convert(
    const FloatingPointSize& target, const RoundingMode& rm) const
{
  return FloatingPointLiteral(
      target,
      symfpu::convertFloatToFloat<symfpuLiteral::traits>(
          d_fp_size, target, rm, d_symuf));
}

BitVector FloatingPointLiteral::convertToSBVTotal(BitVectorSize width,
                                                  const RoundingMode& rm,
                                                  BitVector undefinedCase) const
{
  return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
      d_fp_size, rm, d_symuf, width, undefinedCase);
}

BitVector FloatingPointLiteral::convertToUBVTotal(BitVectorSize width,
                                                  const RoundingMode& rm,
                                                  BitVector undefinedCase) const
{
  return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
      d_fp_size, rm, d_symuf, width, undefinedCase);
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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