{
CVC4::FloatingPointToFPIEEEBitVector ext =
d_node->getConst<FloatingPointToFPIEEEBitVector>();
- indices = std::make_pair(ext.d_fp_size.exponentWidth(),
- ext.d_fp_size.significandWidth());
+ indices = std::make_pair(ext.getSize().exponentWidth(),
+ ext.getSize().significandWidth());
}
else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT)
{
CVC4::FloatingPointToFPFloatingPoint ext =
d_node->getConst<FloatingPointToFPFloatingPoint>();
- indices = std::make_pair(ext.d_fp_size.exponentWidth(),
- ext.d_fp_size.significandWidth());
+ indices = std::make_pair(ext.getSize().exponentWidth(),
+ ext.getSize().significandWidth());
}
else if (k == FLOATINGPOINT_TO_FP_REAL)
{
CVC4::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>();
- indices = std::make_pair(ext.d_fp_size.exponentWidth(),
- ext.d_fp_size.significandWidth());
+ indices = std::make_pair(ext.getSize().exponentWidth(),
+ ext.getSize().significandWidth());
}
else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR)
{
CVC4::FloatingPointToFPSignedBitVector ext =
d_node->getConst<FloatingPointToFPSignedBitVector>();
- indices = std::make_pair(ext.d_fp_size.exponentWidth(),
- ext.d_fp_size.significandWidth());
+ indices = std::make_pair(ext.getSize().exponentWidth(),
+ ext.getSize().significandWidth());
}
else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR)
{
CVC4::FloatingPointToFPUnsignedBitVector ext =
d_node->getConst<FloatingPointToFPUnsignedBitVector>();
- indices = std::make_pair(ext.d_fp_size.exponentWidth(),
- ext.d_fp_size.significandWidth());
+ indices = std::make_pair(ext.getSize().exponentWidth(),
+ ext.getSize().significandWidth());
}
else if (k == FLOATINGPOINT_TO_FP_GENERIC)
{
CVC4::FloatingPointToFPGeneric ext =
d_node->getConst<FloatingPointToFPGeneric>();
- indices = std::make_pair(ext.d_fp_size.exponentWidth(),
- ext.d_fp_size.significandWidth());
+ indices = std::make_pair(ext.getSize().exponentWidth(),
+ ext.getSize().significandWidth());
}
else if (k == REGEXP_LOOP)
{
case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
out << "(_ to_fp "
<< n.getConst<FloatingPointToFPIEEEBitVector>()
- .d_fp_size.exponentWidth()
+ .getSize()
+ .exponentWidth()
<< ' '
<< n.getConst<FloatingPointToFPIEEEBitVector>()
- .d_fp_size.significandWidth()
+ .getSize()
+ .significandWidth()
<< ")";
break;
case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
out << "(_ to_fp "
<< n.getConst<FloatingPointToFPFloatingPoint>()
- .d_fp_size.exponentWidth()
+ .getSize()
+ .exponentWidth()
<< ' '
<< n.getConst<FloatingPointToFPFloatingPoint>()
- .d_fp_size.significandWidth()
+ .getSize()
+ .significandWidth()
<< ")";
break;
case kind::FLOATINGPOINT_TO_FP_REAL_OP:
out << "(_ to_fp "
- << n.getConst<FloatingPointToFPReal>().d_fp_size.exponentWidth()
+ << n.getConst<FloatingPointToFPReal>().getSize().exponentWidth()
<< ' '
- << n.getConst<FloatingPointToFPReal>().d_fp_size.significandWidth()
+ << n.getConst<FloatingPointToFPReal>().getSize().significandWidth()
<< ")";
break;
case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
out << "(_ to_fp "
<< n.getConst<FloatingPointToFPSignedBitVector>()
- .d_fp_size.exponentWidth()
+ .getSize()
+ .exponentWidth()
<< ' '
<< n.getConst<FloatingPointToFPSignedBitVector>()
- .d_fp_size.significandWidth()
+ .getSize()
+ .significandWidth()
<< ")";
break;
case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
out << "(_ to_fp_unsigned "
<< n.getConst<FloatingPointToFPUnsignedBitVector>()
- .d_fp_size.exponentWidth()
+ .getSize()
+ .exponentWidth()
<< ' '
<< n.getConst<FloatingPointToFPUnsignedBitVector>()
- .d_fp_size.significandWidth()
+ .getSize()
+ .significandWidth()
<< ")";
break;
case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
out << "(_ to_fp "
- << n.getConst<FloatingPointToFPGeneric>().d_fp_size.exponentWidth()
+ << n.getConst<FloatingPointToFPGeneric>().getSize().exponentWidth()
<< ' '
- << n.getConst<FloatingPointToFPGeneric>().d_fp_size.significandWidth()
+ << n.getConst<FloatingPointToFPGeneric>().getSize().significandWidth()
<< ")";
break;
case kind::FLOATINGPOINT_TO_UBV_OP:
FloatingPoint arg1(node[1].getConst<FloatingPoint>());
FloatingPoint arg2(node[2].getConst<FloatingPoint>());
- Assert(arg1.d_fp_size == arg2.d_fp_size);
+ Assert(arg1.getSize() == arg2.getSize());
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.plus(rm, arg2)));
}
FloatingPoint arg1(node[1].getConst<FloatingPoint>());
FloatingPoint arg2(node[2].getConst<FloatingPoint>());
- Assert(arg1.d_fp_size == arg2.d_fp_size);
+ Assert(arg1.getSize() == arg2.getSize());
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.mult(rm, arg2)));
}
FloatingPoint arg2(node[2].getConst<FloatingPoint>());
FloatingPoint arg3(node[3].getConst<FloatingPoint>());
- Assert(arg1.d_fp_size == arg2.d_fp_size);
- Assert(arg1.d_fp_size == arg3.d_fp_size);
+ Assert(arg1.getSize() == arg2.getSize());
+ Assert(arg1.getSize() == arg3.getSize());
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.fma(rm, arg2, arg3)));
}
FloatingPoint arg1(node[1].getConst<FloatingPoint>());
FloatingPoint arg2(node[2].getConst<FloatingPoint>());
- Assert(arg1.d_fp_size == arg2.d_fp_size);
+ Assert(arg1.getSize() == arg2.getSize());
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.div(rm, arg2)));
}
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.d_fp_size == arg2.d_fp_size);
+ Assert(arg1.getSize() == arg2.getSize());
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.rem(arg2)));
}
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.d_fp_size == arg2.d_fp_size);
+ Assert(arg1.getSize() == arg2.getSize());
FloatingPoint::PartialFloatingPoint res(arg1.min(arg2));
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.d_fp_size == arg2.d_fp_size);
+ Assert(arg1.getSize() == arg2.getSize());
FloatingPoint::PartialFloatingPoint res(arg1.max(arg2));
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.d_fp_size == arg2.d_fp_size);
+ Assert(arg1.getSize() == arg2.getSize());
// Can be called with the third argument non-constant
if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.d_fp_size == arg2.d_fp_size);
+ Assert(arg1.getSize() == arg2.getSize());
// Can be called with the third argument non-constant
if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.d_fp_size == arg2.d_fp_size);
+ Assert(arg1.getSize() == arg2.getSize());
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 == arg2));
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.d_fp_size == arg2.d_fp_size);
+ Assert(arg1.getSize() == arg2.getSize());
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 <= arg2));
}
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.d_fp_size == arg2.d_fp_size);
+ Assert(arg1.getSize() == arg2.getSize());
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 < arg2));
}
const BitVector &bv = node[0].getConst<BitVector>();
Node lit = NodeManager::currentNM()->mkConst(
- FloatingPoint(param.d_fp_size.exponentWidth(),
- param.d_fp_size.significandWidth(),
+ FloatingPoint(param.getSize().exponentWidth(),
+ param.getSize().significandWidth(),
bv));
return RewriteResponse(REWRITE_DONE, lit);
return RewriteResponse(
REWRITE_DONE,
- NodeManager::currentNM()->mkConst(arg1.convert(info.d_fp_size, rm)));
+ NodeManager::currentNM()->mkConst(arg1.convert(info.getSize(), rm)));
}
RewriteResponse convertFromRealLiteral (TNode node, bool) {
RoundingMode rm(node[0].getConst<RoundingMode>());
Rational arg(node[1].getConst<Rational>());
- FloatingPoint res(param.d_fp_size, rm, arg);
+ FloatingPoint res(param.getSize(), rm, arg);
Node lit = NodeManager::currentNM()->mkConst(res);
RoundingMode rm(node[0].getConst<RoundingMode>());
BitVector arg(node[1].getConst<BitVector>());
- FloatingPoint res(param.d_fp_size, rm, arg, true);
+ FloatingPoint res(param.getSize(), rm, arg, true);
Node lit = NodeManager::currentNM()->mkConst(res);
RoundingMode rm(node[0].getConst<RoundingMode>());
BitVector arg(node[1].getConst<BitVector>());
- FloatingPoint res(param.d_fp_size, rm, arg, false);
+ FloatingPoint res(param.getSize(), rm, arg, false);
Node lit = NodeManager::currentNM()->mkConst(res);
if (check)
{
- if (!(validExponentSize(f.d_fp_size.exponentWidth())))
+ if (!(validExponentSize(f.getSize().exponentWidth())))
{
throw TypeCheckingExceptionPrivate(
n, "constant with invalid exponent size");
}
- if (!(validSignificandSize(f.d_fp_size.significandWidth())))
+ if (!(validSignificandSize(f.getSize().significandWidth())))
{
throw TypeCheckingExceptionPrivate(
n, "constant with invalid significand size");
}
}
- return nodeManager->mkFloatingPointType(f.d_fp_size);
+ return nodeManager->mkFloatingPointType(f.getSize());
}
};
}
};
-class FloatingPointToFPIEEEBitVectorTypeRule {
+class FloatingPointToFPIEEEBitVectorTypeRule
+{
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
bool check) {
"than bit vector");
}
else if (!(operandType.getBitVectorSize()
- == info.d_fp_size.exponentWidth()
- + info.d_fp_size.significandWidth()))
+ == info.getSize().exponentWidth()
+ + info.getSize().significandWidth()))
{
throw TypeCheckingExceptionPrivate(
n,
}
}
- return nodeManager->mkFloatingPointType(info.d_fp_size);
+ return nodeManager->mkFloatingPointType(info.getSize());
}
};
-class FloatingPointToFPFloatingPointTypeRule {
+class FloatingPointToFPFloatingPointTypeRule
+{
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
bool check) {
}
}
- return nodeManager->mkFloatingPointType(info.d_fp_size);
+ return nodeManager->mkFloatingPointType(info.getSize());
}
};
-class FloatingPointToFPRealTypeRule {
+class FloatingPointToFPRealTypeRule
+{
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
bool check) {
}
}
- return nodeManager->mkFloatingPointType(info.d_fp_size);
+ return nodeManager->mkFloatingPointType(info.getSize());
}
};
-class FloatingPointToFPSignedBitVectorTypeRule {
+class FloatingPointToFPSignedBitVectorTypeRule
+{
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
bool check) {
}
}
- return nodeManager->mkFloatingPointType(info.d_fp_size);
+ return nodeManager->mkFloatingPointType(info.getSize());
}
};
-class FloatingPointToFPUnsignedBitVectorTypeRule {
+class FloatingPointToFPUnsignedBitVectorTypeRule
+{
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
bool check) {
}
}
- return nodeManager->mkFloatingPointType(info.d_fp_size);
+ return nodeManager->mkFloatingPointType(info.getSize());
}
};
-class FloatingPointToFPGenericTypeRule {
+class FloatingPointToFPGenericTypeRule
+{
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
bool check) {
}
}
- return nodeManager->mkFloatingPointType(info.d_fp_size);
+ return nodeManager->mkFloatingPointType(info.getSize());
}
};
#include "util/floatingpoint_literal_symfpu.h"
#include "util/integer.h"
-#ifdef CVC4_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 CVC4_USE_SYMFPU
-namespace symfpu {
-
-#define CVC4_LIT_ITE_DFN(T) \
- template <> \
- struct ite<::CVC4::symfpuLiteral::CVC4Prop, T> \
- { \
- static const T& iteOp(const ::CVC4::symfpuLiteral::CVC4Prop& cond, \
- const T& l, \
- const T& r) \
- { \
- return cond ? l : r; \
- } \
- }
-
-CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::rm);
-CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::prop);
-CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::sbv);
-CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv);
-
-#undef CVC4_LIT_ITE_DFN
-}
-#endif
-
/* -------------------------------------------------------------------------- */
namespace CVC4 {
uint32_t FloatingPoint::getUnpackedExponentWidth(FloatingPointSize& size)
{
-#ifdef CVC4_USE_SYMFPU
- return SymFPUUnpackedFloatLiteral::exponentWidth(size);
-#else
- Unreachable() << "no concrete implementation of FloatingPointLiteral";
- return 2;
-#endif
+ return FloatingPointLiteral::getUnpackedExponentWidth(size);
}
uint32_t FloatingPoint::getUnpackedSignificandWidth(FloatingPointSize& size)
{
-#ifdef CVC4_USE_SYMFPU
- return SymFPUUnpackedFloatLiteral::significandWidth(size);
-#else
- Unreachable() << "no concrete implementation of FloatingPointLiteral";
- return 2;
-#endif
+ return FloatingPointLiteral::getUnpackedSignificandWidth(size);
}
FloatingPoint::FloatingPoint(uint32_t d_exp_size,
uint32_t d_sig_size,
const BitVector& bv)
- : d_fp_size(d_exp_size, d_sig_size),
-#ifdef CVC4_USE_SYMFPU
- d_fpl(new FloatingPointLiteral(symfpu::unpack<symfpuLiteral::traits>(
- symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv)))
-#else
- d_fpl(new FloatingPointLiteral(d_exp_size, d_sig_size, 0.0))
-#endif
+ : d_fpl(new FloatingPointLiteral(d_exp_size, d_sig_size, bv))
{
}
FloatingPoint::FloatingPoint(const FloatingPointSize& size, const BitVector& bv)
- : d_fp_size(size),
-#ifdef CVC4_USE_SYMFPU
- d_fpl(new FloatingPointLiteral(
- symfpu::unpack<symfpuLiteral::traits>(size, bv)))
-#else
- d_fpl(new FloatingPointLiteral(
- size.exponentWidth(), size.significandWidth(), 0.0))
-#endif
+ : d_fpl(new FloatingPointLiteral(size, bv))
{
}
const RoundingMode& rm,
const BitVector& bv,
bool signedBV)
- : d_fp_size(size)
+ : d_fpl(new FloatingPointLiteral(size, rm, bv, signedBV))
{
-#ifdef CVC4_USE_SYMFPU
- if (signedBV)
- {
- d_fpl.reset(new FloatingPointLiteral(
- symfpu::convertSBVToFloat<symfpuLiteral::traits>(
- symfpuLiteral::CVC4FPSize(size),
- symfpuLiteral::CVC4RM(rm),
- symfpuLiteral::CVC4SignedBitVector(bv))));
- }
- else
- {
- d_fpl.reset(new FloatingPointLiteral(
- symfpu::convertUBVToFloat<symfpuLiteral::traits>(
- symfpuLiteral::CVC4FPSize(size),
- symfpuLiteral::CVC4RM(rm),
- symfpuLiteral::CVC4UnsignedBitVector(bv))));
- }
-#else
- d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0));
-#endif
}
-FloatingPoint::FloatingPoint(const FloatingPointSize& fp_size,
- FloatingPointLiteral* fpl)
- : d_fp_size(fp_size)
-{
- d_fpl.reset(fpl);
-}
+FloatingPoint::FloatingPoint(FloatingPointLiteral* fpl) { d_fpl.reset(fpl); }
-FloatingPoint::FloatingPoint(const FloatingPoint& fp) : d_fp_size(fp.d_fp_size)
+FloatingPoint::FloatingPoint(const FloatingPoint& fp)
{
d_fpl.reset(new FloatingPointLiteral(*fp.d_fpl));
}
FloatingPoint::FloatingPoint(const FloatingPointSize& size,
const RoundingMode& rm,
const Rational& r)
- : d_fp_size(size)
{
Rational two(2, 1);
if (r.isZero())
{
-#ifdef CVC4_USE_SYMFPU
// In keeping with the SMT-LIB standard
- d_fpl.reset(new FloatingPointLiteral(
- SymFPUUnpackedFloatLiteral::makeZero(size, false)));
-#else
- d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0));
-#endif
+ d_fpl.reset(
+ new FloatingPointLiteral(FloatingPointLiteral::makeZero(size, false)));
}
else
{
-#ifdef CVC4_USE_SYMFPU
uint32_t negative = (r.sgn() < 0) ? 1 : 0;
-#endif
Rational rabs(r.abs());
// Compute the exponent
// A small subtlety... if the format has expBits the unpacked format
// may have more to allow subnormals to be normalised.
// Thus...
-#ifdef CVC4_USE_SYMFPU
uint32_t extension =
- SymFPUUnpackedFloatLiteral::exponentWidth(exactFormat) - expBits;
+ FloatingPointLiteral::getUnpackedExponentWidth(exactFormat) - expBits;
FloatingPointLiteral exactFloat(
- negative, exactExp.signExtend(extension), sig);
+ exactFormat, negative, exactExp.signExtend(extension), sig);
// Then cast...
- d_fpl.reset(new FloatingPointLiteral(symfpu::convertFloatToFloat(
- exactFormat, size, rm, exactFloat.d_symuf)));
-#else
- Unreachable() << "no concrete implementation of FloatingPointLiteral";
-#endif
+ d_fpl.reset(new FloatingPointLiteral(exactFloat.convert(size, rm)));
}
}
{
}
+const FloatingPointSize& FloatingPoint::getSize() const
+{
+ return d_fpl->getSize();
+}
+
FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size)
{
-#ifdef CVC4_USE_SYMFPU
return FloatingPoint(
- size,
- new FloatingPointLiteral(SymFPUUnpackedFloatLiteral::makeNaN(size)));
-#else
- return FloatingPoint(2, 2, BitVector(4U, 0U));
-#endif
+ new FloatingPointLiteral(FloatingPointLiteral::makeNaN(size)));
}
FloatingPoint FloatingPoint::makeInf(const FloatingPointSize& size, bool sign)
{
-#ifdef CVC4_USE_SYMFPU
- return FloatingPoint(size,
- new FloatingPointLiteral(
- SymFPUUnpackedFloatLiteral::makeInf(size, sign)));
-#else
- return FloatingPoint(2, 2, BitVector(4U, 0U));
-#endif
+ return FloatingPoint(
+ new FloatingPointLiteral(FloatingPointLiteral::makeInf(size, sign)));
}
FloatingPoint FloatingPoint::makeZero(const FloatingPointSize& size, bool sign)
{
-#ifdef CVC4_USE_SYMFPU
- return FloatingPoint(size,
- new FloatingPointLiteral(
- SymFPUUnpackedFloatLiteral::makeZero(size, sign)));
-#else
- return FloatingPoint(2, 2, BitVector(4U, 0U));
-#endif
+ return FloatingPoint(
+ new FloatingPointLiteral(FloatingPointLiteral::makeZero(size, sign)));
}
FloatingPoint FloatingPoint::makeMinSubnormal(const FloatingPointSize& size,
return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
}
-/* Operations implemented using symfpu */
FloatingPoint FloatingPoint::absolute(void) const
{
-#ifdef CVC4_USE_SYMFPU
- return FloatingPoint(
- d_fp_size,
- new FloatingPointLiteral(
- symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf)));
-#else
- return *this;
-#endif
+ return FloatingPoint(new FloatingPointLiteral(d_fpl->absolute()));
}
FloatingPoint FloatingPoint::negate(void) const
{
-#ifdef CVC4_USE_SYMFPU
- return FloatingPoint(
- d_fp_size,
- new FloatingPointLiteral(
- symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf)));
-#else
- return *this;
-#endif
+ return FloatingPoint(new FloatingPointLiteral(d_fpl->negate()));
}
FloatingPoint FloatingPoint::plus(const RoundingMode& rm,
const FloatingPoint& arg) const
{
-#ifdef CVC4_USE_SYMFPU
- Assert(d_fp_size == arg.d_fp_size);
- return FloatingPoint(
- d_fp_size,
- new FloatingPointLiteral(symfpu::add<symfpuLiteral::traits>(
- d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf, true)));
-#else
- return *this;
-#endif
+ return FloatingPoint(new FloatingPointLiteral(d_fpl->add(rm, *arg.d_fpl)));
}
FloatingPoint FloatingPoint::sub(const RoundingMode& rm,
const FloatingPoint& arg) const
{
-#ifdef CVC4_USE_SYMFPU
- Assert(d_fp_size == arg.d_fp_size);
- return FloatingPoint(
- d_fp_size,
- new FloatingPointLiteral(symfpu::add<symfpuLiteral::traits>(
- d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf, false)));
-#else
- return *this;
-#endif
+ return FloatingPoint(new FloatingPointLiteral(d_fpl->sub(rm, *arg.d_fpl)));
}
FloatingPoint FloatingPoint::mult(const RoundingMode& rm,
const FloatingPoint& arg) const
{
-#ifdef CVC4_USE_SYMFPU
- Assert(d_fp_size == arg.d_fp_size);
- return FloatingPoint(
- d_fp_size,
- new FloatingPointLiteral(symfpu::multiply<symfpuLiteral::traits>(
- d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf)));
-#else
- return *this;
-#endif
+ return FloatingPoint(new FloatingPointLiteral(d_fpl->mult(rm, *arg.d_fpl)));
}
FloatingPoint FloatingPoint::fma(const RoundingMode& rm,
const FloatingPoint& arg1,
const FloatingPoint& arg2) const
{
-#ifdef CVC4_USE_SYMFPU
- Assert(d_fp_size == arg1.d_fp_size);
- Assert(d_fp_size == arg2.d_fp_size);
return FloatingPoint(
- d_fp_size,
- new FloatingPointLiteral(
- symfpu::fma<symfpuLiteral::traits>(d_fp_size,
- rm,
- d_fpl->d_symuf,
- arg1.d_fpl->d_symuf,
- arg2.d_fpl->d_symuf)));
-#else
- return *this;
-#endif
+ new FloatingPointLiteral(d_fpl->fma(rm, *arg1.d_fpl, *arg2.d_fpl)));
}
FloatingPoint FloatingPoint::div(const RoundingMode& rm,
const FloatingPoint& arg) const
{
-#ifdef CVC4_USE_SYMFPU
- Assert(d_fp_size == arg.d_fp_size);
- return FloatingPoint(
- d_fp_size,
- new FloatingPointLiteral(symfpu::divide<symfpuLiteral::traits>(
- d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf)));
-#else
- return *this;
-#endif
+ return FloatingPoint(new FloatingPointLiteral(d_fpl->div(rm, *arg.d_fpl)));
}
FloatingPoint FloatingPoint::sqrt(const RoundingMode& rm) const
{
-#ifdef CVC4_USE_SYMFPU
- return FloatingPoint(
- d_fp_size,
- new FloatingPointLiteral(
- symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_fpl->d_symuf)));
-#else
- return *this;
-#endif
+ return FloatingPoint(new FloatingPointLiteral(d_fpl->sqrt(rm)));
}
FloatingPoint FloatingPoint::rti(const RoundingMode& rm) const
{
-#ifdef CVC4_USE_SYMFPU
- return FloatingPoint(
- d_fp_size,
- new FloatingPointLiteral(symfpu::roundToIntegral<symfpuLiteral::traits>(
- d_fp_size, rm, d_fpl->d_symuf)));
-#else
- return *this;
-#endif
+ return FloatingPoint(new FloatingPointLiteral(d_fpl->rti(rm)));
}
FloatingPoint FloatingPoint::rem(const FloatingPoint& arg) const
{
-#ifdef CVC4_USE_SYMFPU
- Assert(d_fp_size == arg.d_fp_size);
- return FloatingPoint(
- d_fp_size,
- new FloatingPointLiteral(symfpu::remainder<symfpuLiteral::traits>(
- d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf)));
-#else
- return *this;
-#endif
+ return FloatingPoint(new FloatingPointLiteral(d_fpl->rem(*arg.d_fpl)));
}
FloatingPoint FloatingPoint::maxTotal(const FloatingPoint& arg,
bool zeroCaseLeft) const
{
-#ifdef CVC4_USE_SYMFPU
- Assert(d_fp_size == arg.d_fp_size);
return FloatingPoint(
- d_fp_size,
- new FloatingPointLiteral(symfpu::max<symfpuLiteral::traits>(
- d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf, zeroCaseLeft)));
-#else
- return *this;
-#endif
+ new FloatingPointLiteral(d_fpl->maxTotal(*arg.d_fpl, zeroCaseLeft)));
}
FloatingPoint FloatingPoint::minTotal(const FloatingPoint& arg,
bool zeroCaseLeft) const
{
-#ifdef CVC4_USE_SYMFPU
- Assert(d_fp_size == arg.d_fp_size);
return FloatingPoint(
- d_fp_size,
- new FloatingPointLiteral(symfpu::min<symfpuLiteral::traits>(
- d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf, zeroCaseLeft)));
-#else
- return *this;
-#endif
+ new FloatingPointLiteral(d_fpl->minTotal(*arg.d_fpl, zeroCaseLeft)));
}
FloatingPoint::PartialFloatingPoint FloatingPoint::max(
bool FloatingPoint::operator==(const FloatingPoint& fp) const
{
-#ifdef CVC4_USE_SYMFPU
- return ((d_fp_size == fp.d_fp_size)
- && symfpu::smtlibEqual<symfpuLiteral::traits>(
- d_fp_size, d_fpl->d_symuf, fp.d_fpl->d_symuf));
-#else
- return ((d_fp_size == fp.d_fp_size));
-#endif
+ return *d_fpl == *fp.d_fpl;
}
-bool FloatingPoint::operator<=(const FloatingPoint& arg) const
+bool FloatingPoint::operator<=(const FloatingPoint& fp) const
{
-#ifdef CVC4_USE_SYMFPU
- Assert(d_fp_size == arg.d_fp_size);
- return symfpu::lessThanOrEqual<symfpuLiteral::traits>(
- d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf);
-#else
- return false;
-#endif
+ return *d_fpl <= *fp.d_fpl;
}
-bool FloatingPoint::operator<(const FloatingPoint& arg) const
+bool FloatingPoint::operator<(const FloatingPoint& fp) const
{
-#ifdef CVC4_USE_SYMFPU
- Assert(d_fp_size == arg.d_fp_size);
- return symfpu::lessThan<symfpuLiteral::traits>(
- d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf);
-#else
- return false;
-#endif
+ return *d_fpl < *fp.d_fpl;
}
-BitVector FloatingPoint::getExponent() const
-{
-#ifdef CVC4_USE_SYMFPU
- return d_fpl->d_symuf.exponent;
-#else
- Unreachable() << "no concrete implementation of FloatingPointLiteral";
- return BitVector();
-#endif
-}
+BitVector FloatingPoint::getExponent() const { return d_fpl->getExponent(); }
BitVector FloatingPoint::getSignificand() const
{
-#ifdef CVC4_USE_SYMFPU
- return d_fpl->d_symuf.significand;
-#else
- Unreachable() << "no concrete implementation of FloatingPointLiteral";
- return BitVector();
-#endif
+ return d_fpl->getSignificand();
}
-bool FloatingPoint::getSign() const
-{
-#ifdef CVC4_USE_SYMFPU
- return d_fpl->d_symuf.sign;
-#else
- Unreachable() << "no concrete implementation of FloatingPointLiteral";
- return false;
-#endif
-}
+bool FloatingPoint::getSign() const { return d_fpl->getSign(); }
-bool FloatingPoint::isNormal(void) const
-{
-#ifdef CVC4_USE_SYMFPU
- return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
- return false;
-#endif
-}
+bool FloatingPoint::isNormal(void) const { return d_fpl->isNormal(); }
-bool FloatingPoint::isSubnormal(void) const
-{
-#ifdef CVC4_USE_SYMFPU
- return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
- return false;
-#endif
-}
+bool FloatingPoint::isSubnormal(void) const { return d_fpl->isSubnormal(); }
-bool FloatingPoint::isZero(void) const
-{
-#ifdef CVC4_USE_SYMFPU
- return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
- return false;
-#endif
-}
+bool FloatingPoint::isZero(void) const { return d_fpl->isZero(); }
-bool FloatingPoint::isInfinite(void) const
-{
-#ifdef CVC4_USE_SYMFPU
- return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
- return false;
-#endif
-}
+bool FloatingPoint::isInfinite(void) const { return d_fpl->isInfinite(); }
-bool FloatingPoint::isNaN(void) const
-{
-#ifdef CVC4_USE_SYMFPU
- return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
- return false;
-#endif
-}
+bool FloatingPoint::isNaN(void) const { return d_fpl->isNaN(); }
-bool FloatingPoint::isNegative(void) const
-{
-#ifdef CVC4_USE_SYMFPU
- return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
- return false;
-#endif
-}
+bool FloatingPoint::isNegative(void) const { return d_fpl->isNegative(); }
-bool FloatingPoint::isPositive(void) const
-{
-#ifdef CVC4_USE_SYMFPU
- return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
- return false;
-#endif
-}
+bool FloatingPoint::isPositive(void) const { return d_fpl->isPositive(); }
FloatingPoint FloatingPoint::convert(const FloatingPointSize& target,
const RoundingMode& rm) const
{
-#ifdef CVC4_USE_SYMFPU
- return FloatingPoint(target,
- new FloatingPointLiteral(
- symfpu::convertFloatToFloat<symfpuLiteral::traits>(
- d_fp_size, target, rm, d_fpl->d_symuf)));
-#else
- return *this;
-#endif
+ return FloatingPoint(new FloatingPointLiteral(d_fpl->convert(target, rm)));
}
BitVector FloatingPoint::convertToBVTotal(BitVectorSize width,
bool signedBV,
BitVector undefinedCase) const
{
-#ifdef CVC4_USE_SYMFPU
- if (signedBV)
- return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
- d_fp_size, rm, d_fpl->d_symuf, width, undefinedCase);
- else
- return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
- d_fp_size, rm, d_fpl->d_symuf, width, undefinedCase);
-#else
- return undefinedCase;
-#endif
+ if (signedBV)
+ {
+ return d_fpl->convertToSBVTotal(width, rm, undefinedCase);
+ }
+ return d_fpl->convertToUBVTotal(width, rm, undefinedCase);
}
Rational FloatingPoint::convertToRationalTotal(Rational undefinedCase) const
{
return PartialRational(Rational(0U, 1U), true);
}
- else
- {
-#ifdef CVC4_USE_SYMFPU
- Integer sign((d_fpl->d_symuf.getSign()) ? -1 : 1);
- Integer exp(
- d_fpl->d_symuf.getExponent().toSignedInteger()
- - (Integer(d_fp_size.significandWidth()
- - 1))); // -1 as forcibly normalised into the [1,2) range
- Integer significand(d_fpl->d_symuf.getSignificand().toInteger());
-#else
- Integer sign(0);
- Integer exp(0);
- Integer significand(0);
-#endif
- Integer signedSignificand(sign * significand);
-
- // We only have multiplyByPow(uint32_t) so we can't convert all numbers.
- // As we convert Integer -> unsigned int -> uint32_t we need that
- // unsigned int is not smaller than uint32_t
- static_assert(sizeof(unsigned int) >= sizeof(uint32_t),
- "Conversion float -> real could loose data");
+ Integer sign((d_fpl->getSign()) ? -1 : 1);
+ Integer exp(
+ d_fpl->getExponent().toSignedInteger()
+ - (Integer(d_fpl->getSize().significandWidth()
+ - 1))); // -1 as forcibly normalised into the [1,2) range
+ Integer significand(d_fpl->getSignificand().toInteger());
+ Integer signedSignificand(sign * significand);
+
+ // We only have multiplyByPow(uint32_t) so we can't convert all numbers.
+ // As we convert Integer -> unsigned int -> uint32_t we need that
+ // unsigned int is not smaller than uint32_t
+ static_assert(sizeof(unsigned int) >= sizeof(uint32_t),
+ "Conversion float -> real could loose data");
#ifdef CVC4_ASSERTIONS
- // Note that multipling by 2^n requires n bits of space (worst case)
- // so, in effect, these tests limit us to cases where the resultant
- // number requires up to 2^32 bits = 512 megabyte to represent.
- Integer shiftLimit(std::numeric_limits<uint32_t>::max());
+ // Note that multipling by 2^n requires n bits of space (worst case)
+ // so, in effect, these tests limit us to cases where the resultant
+ // number requires up to 2^32 bits = 512 megabyte to represent.
+ Integer shiftLimit(std::numeric_limits<uint32_t>::max());
#endif
- if (!(exp.strictlyNegative())) {
- Assert(exp <= shiftLimit);
- Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt()));
- return PartialRational(Rational(r), true);
- } else {
- Integer one(1U);
- Assert((-exp) <= shiftLimit);
- Integer q(one.multiplyByPow2((-exp).toUnsignedInt()));
- Rational r(signedSignificand, q);
- return PartialRational(r, true);
- }
+ if (!(exp.strictlyNegative()))
+ {
+ Assert(exp <= shiftLimit);
+ Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt()));
+ return PartialRational(Rational(r), true);
}
-
- Unreachable() << "Convert float literal to real broken.";
+ Integer one(1U);
+ Assert((-exp) <= shiftLimit);
+ Integer q(one.multiplyByPow2((-exp).toUnsignedInt()));
+ Rational r(signedSignificand, q);
+ return PartialRational(r, true);
}
-BitVector FloatingPoint::pack(void) const
-{
-#ifdef CVC4_USE_SYMFPU
- BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf));
-#else
- BitVector bv(4u, 0u);
-#endif
- return bv;
-}
+BitVector FloatingPoint::pack(void) const { return d_fpl->pack(); }
std::string FloatingPoint::toString(bool printAsIndexed) const
{
// retrive BV value
BitVector bv(pack());
uint32_t largestSignificandBit =
- d_fp_size.significandWidth() - 2; // -1 for -inclusive, -1 for hidden
+ getSize().significandWidth() - 2; // -1 for -inclusive, -1 for hidden
uint32_t largestExponentBit =
- (d_fp_size.exponentWidth() - 1) + (largestSignificandBit + 1);
+ (getSize().exponentWidth() - 1) + (largestSignificandBit + 1);
BitVector v[3];
v[0] = bv.extract(largestExponentBit + 1, largestExponentBit + 1);
v[1] = bv.extract(largestExponentBit, largestSignificandBit + 1);
std::ostream& operator<<(std::ostream& os, const FloatingPointConvertSort& fpcs)
{
- return os << "(_ to_fp " << fpcs.d_fp_size.exponentWidth() << " "
- << fpcs.d_fp_size.significandWidth() << ")";
+ return os << "(_ to_fp " << fpcs.getSize().exponentWidth() << " "
+ << fpcs.getSize().significandWidth() << ")";
}
}/* CVC4 namespace */
/**
* Get the number of exponent bits in the unpacked format corresponding to a
- * given packed format. These is the unpacked counter-parts of
+ * given packed format. This is the unpacked counter-part of
* FloatingPointSize::exponentWidth().
*/
static uint32_t getUnpackedExponentWidth(FloatingPointSize& size);
/**
* Get the number of exponent bits in the unpacked format corresponding to a
- * given packed format. These is the unpacked counter-parts of
+ * given packed format. This is the unpacked counter-part of
* FloatingPointSize::significandWidth().
*/
static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size);
/** Constructors. */
+
+ /** Create a FP value from its IEEE bit-vector representation. */
FloatingPoint(uint32_t e, uint32_t s, const BitVector& bv);
FloatingPoint(const FloatingPointSize& size, const BitVector& bv);
- FloatingPoint(const FloatingPoint& fp);
+
+ /**
+ * Create a FP value from a signed or unsigned bit-vector value with
+ * respect to given rounding mode.
+ */
FloatingPoint(const FloatingPointSize& size,
const RoundingMode& rm,
const BitVector& bv,
bool signedBV);
+
+ /**
+ * Create a FP value from a rational value with respect to given rounding
+ * mode.
+ */
FloatingPoint(const FloatingPointSize& size,
const RoundingMode& rm,
const Rational& r);
+
+ /** Copy constructor. */
+ FloatingPoint(const FloatingPoint& fp);
+
/** Destructor. */
~FloatingPoint();
*/
static FloatingPoint makeMaxNormal(const FloatingPointSize& size, bool sign);
+ /** Return the size of this FP value. */
+ const FloatingPointSize& getSize() const;
+
/** Get the wrapped floating-point value. */
const FloatingPointLiteral* getLiteral(void) const { return d_fpl.get(); }
*/
PartialRational convertToRational(void) const;
- /** The floating-point size of this floating-point value. */
- FloatingPointSize d_fp_size;
-
private:
/**
* Constructor.
* Note: This constructor takes ownership of 'fpl' and is not intended for
* public use.
*/
- FloatingPoint(const FloatingPointSize& fp_size, FloatingPointLiteral* fpl);
+ FloatingPoint(FloatingPointLiteral* fpl);
/** The floating-point literal of this floating-point value. */
std::unique_ptr<FloatingPointLiteral> d_fpl;
FloatingPointSizeHashFunction fpshf;
BitVectorHashFunction bvhf;
- return fpshf(fp.d_fp_size) ^ bvhf(fp.pack());
+ return fpshf(fp.getSize()) ^ bvhf(fp.pack());
}
}; /* struct FloatingPointHashFunction */
return d_fp_size == fpcs.d_fp_size;
}
+ /** Return the size of this FP convert sort. */
+ FloatingPointSize getSize() const { return d_fp_size; }
+
+ private:
/** The floating-point size of this sort. */
FloatingPointSize d_fp_size;
};
inline size_t operator()(const FloatingPointConvertSort& fpcs) const
{
FloatingPointSizeHashFunction f;
- return f(fpcs.d_fp_size) ^ (0x00005300 | (key << 24));
+ return f(fpcs.getSize()) ^ (0x00005300 | (key << 24));
}
}; /* struct FloatingPointConvertSortHashFunction */
#include "base/check.h"
+#ifdef CVC4_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 CVC4_USE_SYMFPU
+namespace symfpu {
+
+#define CVC4_LIT_ITE_DFN(T) \
+ template <> \
+ struct ite<::CVC4::symfpuLiteral::CVC4Prop, T> \
+ { \
+ static const T& iteOp(const ::CVC4::symfpuLiteral::CVC4Prop& cond, \
+ const T& l, \
+ const T& r) \
+ { \
+ return cond ? l : r; \
+ } \
+ }
+
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::rm);
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::prop);
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::sbv);
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv);
+
+#undef CVC4_LIT_ITE_DFN
+} // namespace symfpu
+#endif
+
+/* -------------------------------------------------------------------------- */
+
namespace CVC4 {
-#ifndef CVC4_USE_SYMFPU
-void FloatingPointLiteral::unfinished(void) const
+uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size)
+{
+#ifdef CVC4_USE_SYMFPU
+ return SymFPUUnpackedFloatLiteral::exponentWidth(size);
+#else
+ unimplemented();
+ return 2;
+#endif
+}
+
+uint32_t FloatingPointLiteral::getUnpackedSignificandWidth(
+ FloatingPointSize& size)
+{
+#ifdef CVC4_USE_SYMFPU
+ return SymFPUUnpackedFloatLiteral::significandWidth(size);
+#else
+ unimplemented();
+ return 2;
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::makeNaN(
+ const FloatingPointSize& size)
+{
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPointLiteral(size, SymFPUUnpackedFloatLiteral::makeNaN(size));
+#else
+ unimplemented();
+ return FloatingPointLiteral(size, BitVector(4u, 0u));
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::makeInf(
+ const FloatingPointSize& size, bool sign)
+{
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPointLiteral(size,
+ SymFPUUnpackedFloatLiteral::makeInf(size, sign));
+#else
+ unimplemented();
+ return FloatingPointLiteral(size, BitVector(4u, 0u));
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::makeZero(
+ const FloatingPointSize& size, bool sign)
+{
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPointLiteral(size,
+ SymFPUUnpackedFloatLiteral::makeZero(size, sign));
+#else
+ unimplemented();
+ return FloatingPointLiteral(size, BitVector(4u, 0u));
+#endif
+}
+
+FloatingPointLiteral::FloatingPointLiteral(uint32_t d_exp_size,
+ uint32_t d_sig_size,
+ const BitVector& bv)
+ : d_fp_size(d_exp_size, d_sig_size)
+#ifdef CVC4_USE_SYMFPU
+ ,
+ d_symuf(symfpu::unpack<symfpuLiteral::traits>(
+ symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv))
+#endif
+{
+}
+
+FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
+ const BitVector& bv)
+ : d_fp_size(size)
+#ifdef CVC4_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 CVC4_USE_SYMFPU
+ ,
+ d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>(
+ symfpuLiteral::CVC4FPSize(size),
+ symfpuLiteral::CVC4RM(rm),
+ symfpuLiteral::CVC4SignedBitVector(bv))
+ : symfpu::convertUBVToFloat<symfpuLiteral::traits>(
+ symfpuLiteral::CVC4FPSize(size),
+ symfpuLiteral::CVC4RM(rm),
+ symfpuLiteral::CVC4UnsignedBitVector(bv)))
+#endif
+{
+}
+
+BitVector FloatingPointLiteral::pack(void) const
{
- Unimplemented() << "Floating-point literals not yet implemented.";
+#ifdef CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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
}
-bool FloatingPointLiteral::operator==(const FloatingPointLiteral& other) const
+FloatingPointLiteral FloatingPointLiteral::div(
+ const RoundingMode& rm, const FloatingPointLiteral& arg) const
{
- unfinished();
+#ifdef CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_USE_SYMFPU
+ return d_symuf.exponent;
+#else
+ unimplemented();
+ Unreachable() << "no concrete implementation of FloatingPointLiteral";
+ return BitVector();
+#endif
+}
+
+BitVector FloatingPointLiteral::getSignificand() const
+{
+#ifdef CVC4_USE_SYMFPU
+ return d_symuf.significand;
+#else
+ unimplemented();
+ Unreachable() << "no concrete implementation of FloatingPointLiteral";
+ return BitVector();
+#endif
+}
+
+bool FloatingPointLiteral::getSign() const
+{
+#ifdef CVC4_USE_SYMFPU
+ return d_symuf.sign;
+#else
+ unimplemented();
+ Unreachable() << "no concrete implementation of FloatingPointLiteral";
+ return false;
+#endif
+}
+
+bool FloatingPointLiteral::isNormal(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
+#else
+ unimplemented();
+ return false;
+#endif
+}
+
+bool FloatingPointLiteral::isSubnormal(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
+#else
+ unimplemented();
+ return false;
+#endif
+}
+
+bool FloatingPointLiteral::isZero(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf);
+#else
+ unimplemented();
+ return false;
+#endif
+}
+
+bool FloatingPointLiteral::isInfinite(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf);
+#else
+ unimplemented();
+ return false;
+#endif
+}
+
+bool FloatingPointLiteral::isNaN(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf);
+#else
+ unimplemented();
+ return false;
+#endif
+}
+
+bool FloatingPointLiteral::isNegative(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf);
+#else
+ unimplemented();
+ return false;
+#endif
+}
+
+bool FloatingPointLiteral::isPositive(void) const
+{
+#ifdef CVC4_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 CVC4_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 CVC4_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 CVC4_USE_SYMFPU
+ return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
+ d_fp_size, rm, d_symuf, width, undefinedCase);
+#else
+ unimplemented();
+ return undefinedCase;
+#endif
+}
+
+#ifndef CVC4_USE_SYMFPU
+void FloatingPointLiteral::unimplemented(void)
+{
+ Unimplemented() << "no concrete implementation of FloatingPointLiteral";
}
size_t FloatingPointLiteral::hash(void) const
{
- unfinished();
+ unimplemented();
return 23;
}
#endif
#define CVC4__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
#include "util/bitvector.h"
+#include "util/floatingpoint_size.h"
#include "util/roundingmode.h"
// clang-format off
namespace CVC4 {
class FloatingPointSize;
-class FloatingPoint;
+class FloatingPointLiteral;
/* -------------------------------------------------------------------------- */
// clang-format off
#if @CVC4_USE_SYMFPU@
// clang-format on
-using SymFPUUnpackedFloatLiteral = ::symfpu::unpackedFloat<symfpuLiteral::traits>;
+using SymFPUUnpackedFloatLiteral =
+ ::symfpu::unpackedFloat<symfpuLiteral::traits>;
#endif
class FloatingPointLiteral
{
friend class FloatingPoint;
+
public:
- /** Constructors. */
+ /**
+ * Get the number of exponent bits in the unpacked format corresponding to a
+ * given packed format. This is the unpacked counter-part of
+ * FloatingPointSize::exponentWidth().
+ */
+ static uint32_t getUnpackedExponentWidth(FloatingPointSize& size);
+ /**
+ * Get the number of exponent bits in the unpacked format corresponding to a
+ * given packed format. This is the unpacked counter-part of
+ * FloatingPointSize::significandWidth().
+ */
+ static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size);
- /** Create an FP literal from a FloatingPoint. */
- FloatingPointLiteral(FloatingPoint& other);
+ /**
+ * Create a FP NaN literal of given size.
+ * size: The FP size (format).
+ */
+ static FloatingPointLiteral makeNaN(const FloatingPointSize& size);
+ /**
+ * Create a FP infinity literal of given size.
+ * size: The FP size (format).
+ * sign: True for -oo, false otherwise.
+ */
+ static FloatingPointLiteral makeInf(const FloatingPointSize& size, bool sign);
+ /**
+ * Create a FP zero literal of given size.
+ * size: The FP size (format).
+ * sign: True for -zero, false otherwise.
+ */
+ static FloatingPointLiteral makeZero(const FloatingPointSize& size,
+ bool sign);
// clang-format off
-#if @CVC4_USE_SYMFPU@
-// clang-format on
+#if !@CVC4_USE_SYMFPU@
+ // clang-format on
+ /** Catch-all for unimplemented functions. */
+ static void unimplemented(void);
+#endif
- /** Create an FP literal from a symFPU unpacked float. */
- FloatingPointLiteral(SymFPUUnpackedFloatLiteral symuf) : d_symuf(symuf){};
+ /** Constructors. */
+
+ /** Create a FP literal from its IEEE bit-vector representation. */
+ FloatingPointLiteral(uint32_t d_exp_size,
+ uint32_t d_sig_size,
+ const BitVector& bv);
+ FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv);
+
+ /**
+ * Create a FP literal from a signed or unsigned bit-vector value with
+ * respect to given rounding mode.
+ */
+ FloatingPointLiteral(const FloatingPointSize& size,
+ const RoundingMode& rm,
+ const BitVector& bv,
+ bool signedBV);
/**
* Create a FP literal from unpacked representation.
* representation -- for this, the above constructor is to be used while
* creating a SymFPUUnpackedFloatLiteral via symfpu::unpack.
*/
- FloatingPointLiteral(const bool sign,
+ FloatingPointLiteral(const FloatingPointSize& size,
+ const bool sign,
const BitVector& exp,
const BitVector& sig)
- : d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig))
+ : d_fp_size(size)
+// clang-format off
+#if @CVC4_USE_SYMFPU@
+ // clang-format on
+ ,
+ d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig))
+#endif
{
}
-#else
- FloatingPointLiteral(uint32_t, uint32_t, double) { unfinished(); };
+
+// clang-format off
+#if @CVC4_USE_SYMFPU@
+ // clang-format on
+
+ /** Create a FP literal from a symFPU unpacked float. */
+ FloatingPointLiteral(const FloatingPointSize& size,
+ SymFPUUnpackedFloatLiteral symuf)
+ : d_fp_size(size), d_symuf(symuf){};
#endif
+
~FloatingPointLiteral() {}
+ /** Return the size of this FP literal. */
+ const FloatingPointSize& getSize() const { return d_fp_size; };
+
+ /** Return the packed (IEEE-754) representation of this literal. */
+ BitVector pack(void) const;
+
+ /** Floating-point absolute value literal. */
+ FloatingPointLiteral absolute(void) const;
+ /** Floating-point negation literal. */
+ FloatingPointLiteral negate(void) const;
+ /** Floating-point addition literal. */
+ FloatingPointLiteral add(const RoundingMode& rm,
+ const FloatingPointLiteral& arg) const;
+ /** Floating-point subtraction literal. */
+ FloatingPointLiteral sub(const RoundingMode& rm,
+ const FloatingPointLiteral& arg) const;
+ /** Floating-point multiplication literal. */
+ FloatingPointLiteral mult(const RoundingMode& rm,
+ const FloatingPointLiteral& arg) const;
+ /** Floating-point division literal. */
+ FloatingPointLiteral div(const RoundingMode& rm,
+ const FloatingPointLiteral& arg) const;
+ /** Floating-point fused multiplication and addition literal. */
+ FloatingPointLiteral fma(const RoundingMode& rm,
+ const FloatingPointLiteral& arg1,
+ const FloatingPointLiteral& arg2) const;
+ /** Floating-point square root literal. */
+ FloatingPointLiteral sqrt(const RoundingMode& rm) const;
+ /** Floating-point round to integral literal. */
+ FloatingPointLiteral rti(const RoundingMode& rm) const;
+ /** Floating-point remainder literal. */
+ FloatingPointLiteral rem(const FloatingPointLiteral& arg) const;
+
+ /**
+ * Floating-point max literal (total version).
+ * zeroCase: true to return the left (rather than the right operand) in case
+ * of max(-0,+0) or max(+0,-0).
+ */
+ FloatingPointLiteral maxTotal(const FloatingPointLiteral& arg,
+ bool zeroCaseLeft) const;
+ /**
+ * Floating-point min literal (total version).
+ * zeroCase: true to return the left (rather than the right operand) in case
+ * of min(-0,+0) or min(+0,-0).
+ */
+ FloatingPointLiteral minTotal(const FloatingPointLiteral& arg,
+ bool zeroCaseLeft) const;
+
+ /** Equality literal (NOT: fp.eq but =) over floating-point values. */
+ bool operator==(const FloatingPointLiteral& fp) const;
+ /** Floating-point less or equal than literal. */
+ bool operator<=(const FloatingPointLiteral& arg) const;
+ /** Floating-point less than literal. */
+ bool operator<(const FloatingPointLiteral& arg) const;
+
+ /** Get the exponent of this floating-point value. */
+ BitVector getExponent() const;
+ /** Get the significand of this floating-point value. */
+ BitVector getSignificand() const;
+ /** True if this value is a negative value. */
+ bool getSign() const;
+
+ /** Return true if this literal represents a normal value. */
+ bool isNormal(void) const;
+ /** Return true if this literal represents a subnormal value. */
+ bool isSubnormal(void) const;
+ /** Return true if this literal represents a zero value. */
+ bool isZero(void) const;
+ /** Return true if this literal represents an infinite value. */
+ bool isInfinite(void) const;
+ /** Return true if this literal represents a NaN value. */
+ bool isNaN(void) const;
+ /** Return true if this literal represents a negative value. */
+ bool isNegative(void) const;
+ /** Return true if this literal represents a positive value. */
+ bool isPositive(void) const;
+
+ /**
+ * Convert this floating-point literal to a literal of given size, with
+ * respect to given rounding mode.
+ */
+ FloatingPointLiteral convert(const FloatingPointSize& target,
+ const RoundingMode& rm) const;
+
+ /**
+ * Convert this floating-point literal to a signed bit-vector of given size,
+ * with respect to given rounding mode (total version).
+ * Returns given bit-vector 'undefinedCase' in the undefined case.
+ */
+ BitVector convertToSBVTotal(BitVectorSize width,
+ const RoundingMode& rm,
+ BitVector undefinedCase) const;
+ /**
+ * Convert this floating-point literal to an unsigned bit-vector of given
+ * size, with respect to given rounding mode (total version).
+ * Returns given bit-vector 'undefinedCase' in the undefined case.
+ */
+ BitVector convertToUBVTotal(BitVectorSize width,
+ const RoundingMode& rm,
+ BitVector undefinedCase) const;
// clang-format off
#if @CVC4_USE_SYMFPU@
-// clang-format on
+ // clang-format on
/** Return wrapped floating-point literal. */
const SymFPUUnpackedFloatLiteral& getSymUF() const { return d_symuf; }
#else
- /** Catch-all for unimplemented functions. */
- void unfinished(void) const;
/** Dummy hash function. */
size_t hash(void) const;
- /** Dummy comparison operator overload. */
- bool operator==(const FloatingPointLiteral& other) const;
#endif
private:
+ /** The floating-point size of this floating-point literal. */
+ FloatingPointSize d_fp_size;
// clang-format off
#if @CVC4_USE_SYMFPU@
-// clang-format on
+ // clang-format on
/** The actual floating-point value, a SymFPU unpackedFloat. */
SymFPUUnpackedFloatLiteral d_symuf;
#endif
};
-
/* -------------------------------------------------------------------------- */
-}
+} // namespace CVC4
#endif
projects / cvc5.git / commitdiff