Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/floatingpoint_literal_symfpu.cpp	Lines:	101	120	84.2 %
Date:	2021-05-24	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"

#ifdef CVC5_USE_SYMFPU
#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"
#endif

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

#ifdef CVC5_USE_SYMFPU
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
#endif

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

namespace cvc5 {

uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size)
{
#ifdef CVC5_USE_SYMFPU
  return SymFPUUnpackedFloatLiteral::exponentWidth(size);
#else
  unimplemented();
  return 2;
#endif
}

uint32_t FloatingPointLiteral::getUnpackedSignificandWidth(
    FloatingPointSize& size)
{
#ifdef CVC5_USE_SYMFPU
  return SymFPUUnpackedFloatLiteral::significandWidth(size);
#else
  unimplemented();
  return 2;
#endif
}

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

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

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

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

FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
                                           const RoundingMode& rm,
                                           const BitVector& bv,
                                           bool signedBV)
    : d_fp_size(size)
#ifdef CVC5_USE_SYMFPU
      ,
      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)))
#endif
{
}

BitVector FloatingPointLiteral::pack(void) const
{
#ifdef CVC5_USE_SYMFPU
  BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_symuf));
#else
  unimplemented();
  BitVector bv(4u, 0u);
#endif
  return bv;
}

FloatingPointLiteral FloatingPointLiteral::absolute(void) const
{
#ifdef CVC5_USE_SYMFPU
  return FloatingPointLiteral(
      d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_symuf));
#else
  unimplemented();
  return *this;
#endif
}

FloatingPointLiteral FloatingPointLiteral::negate(void) const
{
#ifdef CVC5_USE_SYMFPU
  return FloatingPointLiteral(
      d_fp_size, symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_symuf));
#else
  unimplemented();
  return *this;
#endif
}

FloatingPointLiteral FloatingPointLiteral::add(
    const RoundingMode& rm, const FloatingPointLiteral& arg) const
{
#ifdef CVC5_USE_SYMFPU
  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));
#else
  unimplemented();
  return *this;
#endif
}

FloatingPointLiteral FloatingPointLiteral::sub(
    const RoundingMode& rm, const FloatingPointLiteral& arg) const
{
#ifdef CVC5_USE_SYMFPU
  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));
#else
  unimplemented();
  return *this;
#endif
}

FloatingPointLiteral FloatingPointLiteral::mult(
    const RoundingMode& rm, const FloatingPointLiteral& arg) const
{
#ifdef CVC5_USE_SYMFPU
  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));
#else
  unimplemented();
  return *this;
#endif
}

FloatingPointLiteral FloatingPointLiteral::div(
    const RoundingMode& rm, const FloatingPointLiteral& arg) const
{
#ifdef CVC5_USE_SYMFPU
  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));
#else
  unimplemented();
  return *this;
#endif
}

FloatingPointLiteral FloatingPointLiteral::fma(
    const RoundingMode& rm,
    const FloatingPointLiteral& arg1,
    const FloatingPointLiteral& arg2) const
{
#ifdef CVC5_USE_SYMFPU
  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));
#else
  unimplemented();
  return *this;
#endif
}

FloatingPointLiteral FloatingPointLiteral::sqrt(const RoundingMode& rm) const
{
#ifdef CVC5_USE_SYMFPU
  return FloatingPointLiteral(
      d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
#else
  unimplemented();
  return *this;
#endif
}

FloatingPointLiteral FloatingPointLiteral::rti(const RoundingMode& rm) const
{
#ifdef CVC5_USE_SYMFPU
  return FloatingPointLiteral(
      d_fp_size,
      symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
#else
  unimplemented();
  return *this;
#endif
}

FloatingPointLiteral FloatingPointLiteral::rem(
    const FloatingPointLiteral& arg) const
{
#ifdef CVC5_USE_SYMFPU
  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));
#else
  unimplemented();
  return *this;
#endif
}

FloatingPointLiteral FloatingPointLiteral::maxTotal(
    const FloatingPointLiteral& arg, bool zeroCaseLeft) const
{
#ifdef CVC5_USE_SYMFPU
  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));
#else
  unimplemented();
  return *this;
#endif
}

FloatingPointLiteral FloatingPointLiteral::minTotal(
    const FloatingPointLiteral& arg, bool zeroCaseLeft) const
{
#ifdef CVC5_USE_SYMFPU
  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));
#else
  unimplemented();
  return *this;
#endif
}

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

bool FloatingPointLiteral::operator<=(const FloatingPointLiteral& arg) const
{
#ifdef CVC5_USE_SYMFPU
  Assert(d_fp_size == arg.d_fp_size);
  return symfpu::lessThanOrEqual<symfpuLiteral::traits>(
      d_fp_size, d_symuf, arg.d_symuf);
#else
  unimplemented();
  return false;
#endif
}

bool FloatingPointLiteral::operator<(const FloatingPointLiteral& arg) const
{
#ifdef CVC5_USE_SYMFPU
  Assert(d_fp_size == arg.d_fp_size);
  return symfpu::lessThan<symfpuLiteral::traits>(
      d_fp_size, d_symuf, arg.d_symuf);
#else
  unimplemented();
  return false;
#endif
}

BitVector FloatingPointLiteral::getExponent() const
{
#ifdef CVC5_USE_SYMFPU
  return d_symuf.exponent;
#else
  unimplemented();
  Unreachable() << "no concrete implementation of FloatingPointLiteral";
  return BitVector();
#endif
}

BitVector FloatingPointLiteral::getSignificand() const
{
#ifdef CVC5_USE_SYMFPU
  return d_symuf.significand;
#else
  unimplemented();
  Unreachable() << "no concrete implementation of FloatingPointLiteral";
  return BitVector();
#endif
}

bool FloatingPointLiteral::getSign() const
{
#ifdef CVC5_USE_SYMFPU
  return d_symuf.sign;
#else
  unimplemented();
  Unreachable() << "no concrete implementation of FloatingPointLiteral";
  return false;
#endif
}

bool FloatingPointLiteral::isNormal(void) const
{
#ifdef CVC5_USE_SYMFPU
  return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
#else
  unimplemented();
  return false;
#endif
}

bool FloatingPointLiteral::isSubnormal(void) const
{
#ifdef CVC5_USE_SYMFPU
  return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
#else
  unimplemented();
  return false;
#endif
}

bool FloatingPointLiteral::isZero(void) const
{
#ifdef CVC5_USE_SYMFPU
  return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf);
#else
  unimplemented();
  return false;
#endif
}

bool FloatingPointLiteral::isInfinite(void) const
{
#ifdef CVC5_USE_SYMFPU
  return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf);
#else
  unimplemented();
  return false;
#endif
}

bool FloatingPointLiteral::isNaN(void) const
{
#ifdef CVC5_USE_SYMFPU
  return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf);
#else
  unimplemented();
  return false;
#endif
}

bool FloatingPointLiteral::isNegative(void) const
{
#ifdef CVC5_USE_SYMFPU
  return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf);
#else
  unimplemented();
  return false;
#endif
}

bool FloatingPointLiteral::isPositive(void) const
{
#ifdef CVC5_USE_SYMFPU
  return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_symuf);
#else
  unimplemented();
  return false;
#endif
}

FloatingPointLiteral FloatingPointLiteral::convert(
    const FloatingPointSize& target, const RoundingMode& rm) const
{
#ifdef CVC5_USE_SYMFPU
  return FloatingPointLiteral(
      target,
      symfpu::convertFloatToFloat<symfpuLiteral::traits>(
          d_fp_size, target, rm, d_symuf));
#else
  unimplemented();
  return *this;
#endif
}

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

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

#ifndef CVC5_USE_SYMFPU
void FloatingPointLiteral::unimplemented(void)
{
  Unimplemented() << "no concrete implementation of FloatingPointLiteral";
}

size_t FloatingPointLiteral::hash(void) const
{
  unimplemented();
  return 23;
}
#endif

}  // 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		#ifdef CVC5_USE_SYMFPU
20		#include "symfpu/core/add.h"
21		#include "symfpu/core/classify.h"
22		#include "symfpu/core/compare.h"
23		#include "symfpu/core/convert.h"
24		#include "symfpu/core/divide.h"
25		#include "symfpu/core/fma.h"
26		#include "symfpu/core/ite.h"
27		#include "symfpu/core/multiply.h"
28		#include "symfpu/core/packing.h"
29		#include "symfpu/core/remainder.h"
30		#include "symfpu/core/sign.h"
31		#include "symfpu/core/sqrt.h"
32		#include "symfpu/utils/numberOfRoundingModes.h"
33		#include "symfpu/utils/properties.h"
34		#endif
35
36		/* -------------------------------------------------------------------------- */
37
38		#ifdef CVC5_USE_SYMFPU
39		namespace symfpu {
40
41		#define CVC5_LIT_ITE_DFN(T) \
42		template <> \
43		struct ite<::cvc5::symfpuLiteral::Cvc5Prop, T> \
44		{ \
45		static const T& iteOp(const ::cvc5::symfpuLiteral::Cvc5Prop& cond, \
46		const T& l, \
47		const T& r) \
48		{ \
49		return cond ? l : r; \
50		} \
51		}
52
53		CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::rm);
54	60629	CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::prop);
55	39292	CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::sbv);
56	48566	CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::ubv);
57
58		#undef CVC5_LIT_ITE_DFN
59		} // namespace symfpu
60		#endif
61
62		/* -------------------------------------------------------------------------- */
63
64		namespace cvc5 {
65
66	117	uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size)
67		{
68		#ifdef CVC5_USE_SYMFPU
69	117	return SymFPUUnpackedFloatLiteral::exponentWidth(size);
70		#else
71		unimplemented();
72		return 2;
73		#endif
74		}
75
76	89	uint32_t FloatingPointLiteral::getUnpackedSignificandWidth(
77		FloatingPointSize& size)
78		{
79		#ifdef CVC5_USE_SYMFPU
80	89	return SymFPUUnpackedFloatLiteral::significandWidth(size);
81		#else
82		unimplemented();
83		return 2;
84		#endif
85		}
86
87	261	FloatingPointLiteral::FloatingPointLiteral(uint32_t exp_size,
88		uint32_t sig_size,
89	261	const BitVector& bv)
90		: d_fp_size(exp_size, sig_size)
91		#ifdef CVC5_USE_SYMFPU
92		,
93		d_symuf(symfpu::unpack<symfpuLiteral::traits>(
94	261	symfpuLiteral::Cvc5FPSize(exp_size, sig_size), bv))
95		#endif
96		{
97	261	}
98
99	28	FloatingPointLiteral::FloatingPointLiteral(
100	28	const FloatingPointSize& size, FloatingPointLiteral::SpecialConstKind kind)
101		: d_fp_size(size)
102		#ifdef CVC5_USE_SYMFPU
103		,
104	28	d_symuf(SymFPUUnpackedFloatLiteral::makeNaN(size))
105		#endif
106		{
107	28	Assert(kind == FloatingPointLiteral::SpecialConstKind::FPNAN);
108	28	}
109
110	113	FloatingPointLiteral::FloatingPointLiteral(
111		const FloatingPointSize& size,
112		FloatingPointLiteral::SpecialConstKind kind,
113	113	bool sign)
114		: d_fp_size(size)
115		#ifdef CVC5_USE_SYMFPU
116		,
117		d_symuf(kind == FloatingPointLiteral::SpecialConstKind::FPINF
118		? SymFPUUnpackedFloatLiteral::makeInf(size, sign)
119	113	: SymFPUUnpackedFloatLiteral::makeZero(size, sign))
120		#endif
121		{
122	113	Assert(kind == FloatingPointLiteral::SpecialConstKind::FPINF
123		\|\| kind == FloatingPointLiteral::SpecialConstKind::FPZERO);
124	113	}
125
126	64	FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
127	64	const BitVector& bv)
128		: d_fp_size(size)
129		#ifdef CVC5_USE_SYMFPU
130		,
131	64	d_symuf(symfpu::unpack<symfpuLiteral::traits>(size, bv))
132		#endif
133		{
134	64	}
135
136	68	FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
137		const RoundingMode& rm,
138		const BitVector& bv,
139	68	bool signedBV)
140		: d_fp_size(size)
141		#ifdef CVC5_USE_SYMFPU
142		,
143		d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>(
144	76	symfpuLiteral::Cvc5FPSize(size),
145	76	symfpuLiteral::Cvc5RM(rm),
146	76	symfpuLiteral::Cvc5SignedBitVector(bv))
147		: symfpu::convertUBVToFloat<symfpuLiteral::traits>(
148	128	symfpuLiteral::Cvc5FPSize(size),
149	128	symfpuLiteral::Cvc5RM(rm),
150	280	symfpuLiteral::Cvc5UnsignedBitVector(bv)))
151		#endif
152		{
153	68	}
154
155	3123	BitVector FloatingPointLiteral::pack(void) const
156		{
157		#ifdef CVC5_USE_SYMFPU
158	3123	BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_symuf));
159		#else
160		unimplemented();
161		BitVector bv(4u, 0u);
162		#endif
163	3123	return bv;
164		}
165
166	9	FloatingPointLiteral FloatingPointLiteral::absolute(void) const
167		{
168		#ifdef CVC5_USE_SYMFPU
169		return FloatingPointLiteral(
170	9	d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_symuf));
171		#else
172		unimplemented();
173		return *this;
174		#endif
175		}
176
177	127	FloatingPointLiteral FloatingPointLiteral::negate(void) const
178		{
179		#ifdef CVC5_USE_SYMFPU
180		return FloatingPointLiteral(
181	127	d_fp_size, symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_symuf));
182		#else
183		unimplemented();
184		return *this;
185		#endif
186		}
187
188	451	FloatingPointLiteral FloatingPointLiteral::add(
189		const RoundingMode& rm, const FloatingPointLiteral& arg) const
190		{
191		#ifdef CVC5_USE_SYMFPU
192	451	Assert(d_fp_size == arg.d_fp_size);
193		return FloatingPointLiteral(d_fp_size,
194	902	symfpu::add<symfpuLiteral::traits>(
195	902	d_fp_size, rm, d_symuf, arg.d_symuf, true));
196		#else
197		unimplemented();
198		return *this;
199		#endif
200		}
201
202		FloatingPointLiteral FloatingPointLiteral::sub(
203		const RoundingMode& rm, const FloatingPointLiteral& arg) const
204		{
205		#ifdef CVC5_USE_SYMFPU
206		Assert(d_fp_size == arg.d_fp_size);
207		return FloatingPointLiteral(d_fp_size,
208		symfpu::add<symfpuLiteral::traits>(
209		d_fp_size, rm, d_symuf, arg.d_symuf, false));
210		#else
211		unimplemented();
212		return *this;
213		#endif
214		}
215
216	132	FloatingPointLiteral FloatingPointLiteral::mult(
217		const RoundingMode& rm, const FloatingPointLiteral& arg) const
218		{
219		#ifdef CVC5_USE_SYMFPU
220	132	Assert(d_fp_size == arg.d_fp_size);
221		return FloatingPointLiteral(d_fp_size,
222	264	symfpu::multiply<symfpuLiteral::traits>(
223	264	d_fp_size, rm, d_symuf, arg.d_symuf));
224		#else
225		unimplemented();
226		return *this;
227		#endif
228		}
229
230	189	FloatingPointLiteral FloatingPointLiteral::div(
231		const RoundingMode& rm, const FloatingPointLiteral& arg) const
232		{
233		#ifdef CVC5_USE_SYMFPU
234	189	Assert(d_fp_size == arg.d_fp_size);
235		return FloatingPointLiteral(d_fp_size,
236	378	symfpu::divide<symfpuLiteral::traits>(
237	378	d_fp_size, rm, d_symuf, arg.d_symuf));
238		#else
239		unimplemented();
240		return *this;
241		#endif
242		}
243
244		FloatingPointLiteral FloatingPointLiteral::fma(
245		const RoundingMode& rm,
246		const FloatingPointLiteral& arg1,
247		const FloatingPointLiteral& arg2) const
248		{
249		#ifdef CVC5_USE_SYMFPU
250		Assert(d_fp_size == arg1.d_fp_size);
251		Assert(d_fp_size == arg2.d_fp_size);
252		return FloatingPointLiteral(
253		d_fp_size,
254		symfpu::fma<symfpuLiteral::traits>(
255		d_fp_size, rm, d_symuf, arg1.d_symuf, arg2.d_symuf));
256		#else
257		unimplemented();
258		return *this;
259		#endif
260		}
261
262	27	FloatingPointLiteral FloatingPointLiteral::sqrt(const RoundingMode& rm) const
263		{
264		#ifdef CVC5_USE_SYMFPU
265		return FloatingPointLiteral(
266	27	d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
267		#else
268		unimplemented();
269		return *this;
270		#endif
271		}
272
273	140	FloatingPointLiteral FloatingPointLiteral::rti(const RoundingMode& rm) const
274		{
275		#ifdef CVC5_USE_SYMFPU
276		return FloatingPointLiteral(
277		d_fp_size,
278	140	symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
279		#else
280		unimplemented();
281		return *this;
282		#endif
283		}
284
285	99	FloatingPointLiteral FloatingPointLiteral::rem(
286		const FloatingPointLiteral& arg) const
287		{
288		#ifdef CVC5_USE_SYMFPU
289	99	Assert(d_fp_size == arg.d_fp_size);
290		return FloatingPointLiteral(d_fp_size,
291	198	symfpu::remainder<symfpuLiteral::traits>(
292	198	d_fp_size, d_symuf, arg.d_symuf));
293		#else
294		unimplemented();
295		return *this;
296		#endif
297		}
298
299	216	FloatingPointLiteral FloatingPointLiteral::maxTotal(
300		const FloatingPointLiteral& arg, bool zeroCaseLeft) const
301		{
302		#ifdef CVC5_USE_SYMFPU
303	216	Assert(d_fp_size == arg.d_fp_size);
304		return FloatingPointLiteral(
305		d_fp_size,
306	432	symfpu::max<symfpuLiteral::traits>(
307	432	d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
308		#else
309		unimplemented();
310		return *this;
311		#endif
312		}
313
314		FloatingPointLiteral FloatingPointLiteral::minTotal(
315		const FloatingPointLiteral& arg, bool zeroCaseLeft) const
316		{
317		#ifdef CVC5_USE_SYMFPU
318		Assert(d_fp_size == arg.d_fp_size);
319		return FloatingPointLiteral(
320		d_fp_size,
321		symfpu::min<symfpuLiteral::traits>(
322		d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
323		#else
324		unimplemented();
325		return *this;
326		#endif
327		}
328
329	2311	bool FloatingPointLiteral::operator==(const FloatingPointLiteral& fp) const
330		{
331		#ifdef CVC5_USE_SYMFPU
332	2311	return ((d_fp_size == fp.d_fp_size)
333	2311	&& symfpu::smtlibEqual<symfpuLiteral::traits>(
334	2311	d_fp_size, d_symuf, fp.d_symuf));
335		#else
336		unimplemented();
337		return ((d_fp_size == fp.d_fp_size));
338		#endif
339		}
340
341	26	bool FloatingPointLiteral::operator<=(const FloatingPointLiteral& arg) const
342		{
343		#ifdef CVC5_USE_SYMFPU
344	26	Assert(d_fp_size == arg.d_fp_size);
345	26	return symfpu::lessThanOrEqual<symfpuLiteral::traits>(
346	26	d_fp_size, d_symuf, arg.d_symuf);
347		#else
348		unimplemented();
349		return false;
350		#endif
351		}
352
353	2	bool FloatingPointLiteral::operator<(const FloatingPointLiteral& arg) const
354		{
355		#ifdef CVC5_USE_SYMFPU
356	2	Assert(d_fp_size == arg.d_fp_size);
357	2	return symfpu::lessThan<symfpuLiteral::traits>(
358	2	d_fp_size, d_symuf, arg.d_symuf);
359		#else
360		unimplemented();
361		return false;
362		#endif
363		}
364
365	9	BitVector FloatingPointLiteral::getExponent() const
366		{
367		#ifdef CVC5_USE_SYMFPU
368	9	return d_symuf.exponent;
369		#else
370		unimplemented();
371		Unreachable() << "no concrete implementation of FloatingPointLiteral";
372		return BitVector();
373		#endif
374		}
375
376	9	BitVector FloatingPointLiteral::getSignificand() const
377		{
378		#ifdef CVC5_USE_SYMFPU
379	9	return d_symuf.significand;
380		#else
381		unimplemented();
382		Unreachable() << "no concrete implementation of FloatingPointLiteral";
383		return BitVector();
384		#endif
385		}
386
387	9	bool FloatingPointLiteral::getSign() const
388		{
389		#ifdef CVC5_USE_SYMFPU
390	9	return d_symuf.sign;
391		#else
392		unimplemented();
393		Unreachable() << "no concrete implementation of FloatingPointLiteral";
394		return false;
395		#endif
396		}
397
398	43	bool FloatingPointLiteral::isNormal(void) const
399		{
400		#ifdef CVC5_USE_SYMFPU
401	43	return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
402		#else
403		unimplemented();
404		return false;
405		#endif
406		}
407
408	41	bool FloatingPointLiteral::isSubnormal(void) const
409		{
410		#ifdef CVC5_USE_SYMFPU
411	41	return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
412		#else
413		unimplemented();
414		return false;
415		#endif
416		}
417
418	161	bool FloatingPointLiteral::isZero(void) const
419		{
420		#ifdef CVC5_USE_SYMFPU
421	161	return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf);
422		#else
423		unimplemented();
424		return false;
425		#endif
426		}
427
428	28	bool FloatingPointLiteral::isInfinite(void) const
429		{
430		#ifdef CVC5_USE_SYMFPU
431	28	return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf);
432		#else
433		unimplemented();
434		return false;
435		#endif
436		}
437
438	41	bool FloatingPointLiteral::isNaN(void) const
439		{
440		#ifdef CVC5_USE_SYMFPU
441	41	return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf);
442		#else
443		unimplemented();
444		return false;
445		#endif
446		}
447
448	14	bool FloatingPointLiteral::isNegative(void) const
449		{
450		#ifdef CVC5_USE_SYMFPU
451	14	return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf);
452		#else
453		unimplemented();
454		return false;
455		#endif
456		}
457
458	11	bool FloatingPointLiteral::isPositive(void) const
459		{
460		#ifdef CVC5_USE_SYMFPU
461	11	return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_symuf);
462		#else
463		unimplemented();
464		return false;
465		#endif
466		}
467
468	47	FloatingPointLiteral FloatingPointLiteral::convert(
469		const FloatingPointSize& target, const RoundingMode& rm) const
470		{
471		#ifdef CVC5_USE_SYMFPU
472		return FloatingPointLiteral(
473		target,
474	94	symfpu::convertFloatToFloat<symfpuLiteral::traits>(
475	94	d_fp_size, target, rm, d_symuf));
476		#else
477		unimplemented();
478		return *this;
479		#endif
480		}
481
482		BitVector FloatingPointLiteral::convertToSBVTotal(BitVectorSize width,
483		const RoundingMode& rm,
484		BitVector undefinedCase) const
485		{
486		#ifdef CVC5_USE_SYMFPU
487		return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
488		d_fp_size, rm, d_symuf, width, undefinedCase);
489		#else
490		unimplemented();
491		return undefinedCase;
492		#endif
493		}
494
495		BitVector FloatingPointLiteral::convertToUBVTotal(BitVectorSize width,
496		const RoundingMode& rm,
497		BitVector undefinedCase) const
498		{
499		#ifdef CVC5_USE_SYMFPU
500		return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
501		d_fp_size, rm, d_symuf, width, undefinedCase);
502		#else
503		unimplemented();
504		return undefinedCase;
505		#endif
506		}
507
508		#ifndef CVC5_USE_SYMFPU
509		void FloatingPointLiteral::unimplemented(void)
510		{
511		Unimplemented() << "no concrete implementation of FloatingPointLiteral";
512		}
513
514		size_t FloatingPointLiteral::hash(void) const
515		{
516		unimplemented();
517		return 23;
518		}
519		#endif
520
521	28191	} // namespace cvc5