diff options
Diffstat (limited to 'src/theory/fp/fp_converter.cpp')
-rw-r--r-- | src/theory/fp/fp_converter.cpp | 1712 |
1 files changed, 1707 insertions, 5 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index aba95d2ec..464aa497e 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -13,22 +13,1724 @@ **/ #include "theory/fp/fp_converter.h" +#include "theory/theory.h" +// theory.h Only needed for the leaf test #include <stack> +#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 { +using namespace ::CVC4::theory::fp::symfpuSymbolic; + +#define CVC4_SYM_ITE_DFN(T) \ + template <> \ + struct ite<symbolicProposition, T> \ + { \ + static const T iteOp(const symbolicProposition &_cond, \ + const T &_l, \ + const T &_r) \ + { \ + ::CVC4::NodeManager *nm = ::CVC4::NodeManager::currentNM(); \ + \ + ::CVC4::Node cond = _cond; \ + ::CVC4::Node l = _l; \ + ::CVC4::Node r = _r; \ + \ + /* Handle some common symfpu idioms */ \ + if (cond.isConst()) \ + { \ + return (cond == nm->mkConst(::CVC4::BitVector(1U, 1U))) ? l : r; \ + } \ + else \ + { \ + if (l.getKind() == ::CVC4::kind::BITVECTOR_ITE) \ + { \ + if (l[1] == r) \ + { \ + return nm->mkNode( \ + ::CVC4::kind::BITVECTOR_ITE, \ + nm->mkNode(::CVC4::kind::BITVECTOR_AND, \ + cond, \ + nm->mkNode(::CVC4::kind::BITVECTOR_NOT, l[0])), \ + l[2], \ + r); \ + } \ + else if (l[2] == r) \ + { \ + return nm->mkNode( \ + ::CVC4::kind::BITVECTOR_ITE, \ + nm->mkNode(::CVC4::kind::BITVECTOR_AND, cond, l[0]), \ + l[1], \ + r); \ + } \ + } \ + else if (r.getKind() == ::CVC4::kind::BITVECTOR_ITE) \ + { \ + if (r[1] == l) \ + { \ + return nm->mkNode( \ + ::CVC4::kind::BITVECTOR_ITE, \ + nm->mkNode(::CVC4::kind::BITVECTOR_AND, \ + nm->mkNode(::CVC4::kind::BITVECTOR_NOT, cond), \ + nm->mkNode(::CVC4::kind::BITVECTOR_NOT, r[0])), \ + r[2], \ + l); \ + } \ + else if (r[2] == l) \ + { \ + return nm->mkNode( \ + ::CVC4::kind::BITVECTOR_ITE, \ + nm->mkNode(::CVC4::kind::BITVECTOR_AND, \ + nm->mkNode(::CVC4::kind::BITVECTOR_NOT, cond), \ + r[0]), \ + r[1], \ + l); \ + } \ + } \ + } \ + return T(nm->mkNode(::CVC4::kind::BITVECTOR_ITE, cond, l, r)); \ + } \ + } + +// Can (unsurprisingly) only ITE things which contain Nodes +CVC4_SYM_ITE_DFN(traits::rm); +CVC4_SYM_ITE_DFN(traits::prop); +CVC4_SYM_ITE_DFN(traits::sbv); +CVC4_SYM_ITE_DFN(traits::ubv); + +#undef CVC4_SYM_ITE_DFN + +template <> +traits::ubv orderEncode<traits, traits::ubv>(const traits::ubv &b) +{ + return orderEncodeBitwise<traits, traits::ubv>(b); +} + +template <> +stickyRightShiftResult<traits> stickyRightShift(const traits::ubv &input, + const traits::ubv &shiftAmount) +{ + return stickyRightShiftBitwise<traits>(input, shiftAmount); +} + +template <> +void probabilityAnnotation<traits, traits::prop>(const traits::prop &p, + const probability &pr) +{ + // For now, do nothing... + return; +} +}; +#endif + +#ifndef CVC4_USE_SYMFPU +#define PRECONDITION(X) Assert((X)) +#define SYMFPU_NUMBER_OF_ROUNDING_MODES 5 +#endif + namespace CVC4 { namespace theory { namespace fp { +namespace symfpuSymbolic { + +symbolicRoundingMode traits::RNE(void) { return symbolicRoundingMode(0x01); }; +symbolicRoundingMode traits::RNA(void) { return symbolicRoundingMode(0x02); }; +symbolicRoundingMode traits::RTP(void) { return symbolicRoundingMode(0x04); }; +symbolicRoundingMode traits::RTN(void) { return symbolicRoundingMode(0x08); }; +symbolicRoundingMode traits::RTZ(void) { return symbolicRoundingMode(0x10); }; +void traits::precondition(const bool b) +{ + Assert(b); + return; +} +void traits::postcondition(const bool b) +{ + Assert(b); + return; +} +void traits::invariant(const bool b) +{ + Assert(b); + return; +} + +void traits::precondition(const prop &p) { return; } +void traits::postcondition(const prop &p) { return; } +void traits::invariant(const prop &p) { return; } +// This allows us to use the symfpu literal / symbolic assertions in the +// symbolic back-end +typedef traits t; + +bool symbolicProposition::checkNodeType(const TNode node) +{ + TypeNode tn = node.getType(false); + return tn.isBitVector() && tn.getBitVectorSize() == 1; +} + +symbolicProposition::symbolicProposition(const Node n) : nodeWrapper(n) +{ + PRECONDITION(checkNodeType(*this)); +} // Only used within this header so could be friend'd +symbolicProposition::symbolicProposition(bool v) + : nodeWrapper( + NodeManager::currentNM()->mkConst(BitVector(1U, (v ? 1U : 0U)))) +{ + PRECONDITION(checkNodeType(*this)); +} +symbolicProposition::symbolicProposition(const symbolicProposition &old) + : nodeWrapper(old) +{ + PRECONDITION(checkNodeType(*this)); +} + +symbolicProposition symbolicProposition::operator!(void)const +{ + return symbolicProposition( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this)); +} + +symbolicProposition symbolicProposition::operator&&( + const symbolicProposition &op) const +{ + return symbolicProposition( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op)); +} + +symbolicProposition symbolicProposition::operator||( + const symbolicProposition &op) const +{ + return symbolicProposition( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op)); +} + +symbolicProposition symbolicProposition::operator==( + const symbolicProposition &op) const +{ + return symbolicProposition( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op)); +} + +symbolicProposition symbolicProposition::operator^( + const symbolicProposition &op) const +{ + return symbolicProposition( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_XOR, *this, op)); +} + +bool symbolicRoundingMode::checkNodeType(const TNode n) +{ +#ifdef CVC4_USE_SYMFPU + return n.getType(false).isBitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES); +#else + return false; +#endif +} + +symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n) +{ + PRECONDITION(checkNodeType(*this)); +} + +#ifdef CVC4_USE_SYMFPU +symbolicRoundingMode::symbolicRoundingMode(const unsigned v) + : nodeWrapper(NodeManager::currentNM()->mkConst( + BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v))) +{ + PRECONDITION((v & v - 1) == 0 && v != 0); // Exactly one bit set + PRECONDITION(checkNodeType(*this)); +} +#else +symbolicRoundingMode::symbolicRoundingMode(const unsigned v) + : nodeWrapper(NodeManager::currentNM()->mkConst( + BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v))) +{ + Unreachable(); +} +#endif + +symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old) + : nodeWrapper(old) +{ + PRECONDITION(checkNodeType(*this)); +} + +symbolicProposition symbolicRoundingMode::valid(void) const +{ + NodeManager *nm = NodeManager::currentNM(); + Node zero(nm->mkConst( + BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, (long unsigned int)0))); + + // Is there a better encoding of this? + return symbolicProposition(nm->mkNode( + kind::BITVECTOR_AND, + nm->mkNode(kind::BITVECTOR_COMP, + nm->mkNode(kind::BITVECTOR_AND, + *this, + nm->mkNode(kind::BITVECTOR_SUB, + *this, + nm->mkConst(BitVector( + SYMFPU_NUMBER_OF_ROUNDING_MODES, + (long unsigned int)1)))), + zero), + nm->mkNode(kind::BITVECTOR_NOT, + nm->mkNode(kind::BITVECTOR_COMP, *this, zero)))); +} + +symbolicProposition symbolicRoundingMode::operator==( + const symbolicRoundingMode &op) const +{ + return symbolicProposition( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op)); +} + +template <bool isSigned> +Node symbolicBitVector<isSigned>::boolNodeToBV(Node node) const +{ + Assert(node.getType().isBoolean()); + NodeManager *nm = NodeManager::currentNM(); + return nm->mkNode(kind::ITE, + node, + nm->mkConst(BitVector(1U, 1U)), + nm->mkConst(BitVector(1U, 0U))); +} + +template <bool isSigned> +Node symbolicBitVector<isSigned>::BVToBoolNode(Node node) const +{ + Assert(node.getType().isBitVector()); + Assert(node.getType().getBitVectorSize() == 1); + NodeManager *nm = NodeManager::currentNM(); + return nm->mkNode(kind::EQUAL, node, nm->mkConst(BitVector(1U, 1U))); +} + +template <bool isSigned> +Node symbolicBitVector<isSigned>::fromProposition(Node node) const +{ + return node; +} +template <bool isSigned> +Node symbolicBitVector<isSigned>::toProposition(Node node) const +{ + return boolNodeToBV(node); +} + +template <bool isSigned> +symbolicBitVector<isSigned>::symbolicBitVector(const Node n) : nodeWrapper(n) +{ + PRECONDITION(checkNodeType(*this)); +} + +template <bool isSigned> +bool symbolicBitVector<isSigned>::checkNodeType(const TNode n) +{ + return n.getType(false).isBitVector(); +} + +template <bool isSigned> +symbolicBitVector<isSigned>::symbolicBitVector(const bwt w, const unsigned v) + : nodeWrapper(NodeManager::currentNM()->mkConst(BitVector(w, v))) +{ + PRECONDITION(checkNodeType(*this)); +} +template <bool isSigned> +symbolicBitVector<isSigned>::symbolicBitVector(const symbolicProposition &p) + : nodeWrapper(fromProposition(p)) +{ +} +template <bool isSigned> +symbolicBitVector<isSigned>::symbolicBitVector( + const symbolicBitVector<isSigned> &old) + : nodeWrapper(old) +{ + PRECONDITION(checkNodeType(*this)); +} +template <bool isSigned> +symbolicBitVector<isSigned>::symbolicBitVector(const BitVector &old) + : nodeWrapper(NodeManager::currentNM()->mkConst(old)) +{ + PRECONDITION(checkNodeType(*this)); +} + +template <bool isSigned> +bwt symbolicBitVector<isSigned>::getWidth(void) const +{ + return this->getType(false).getBitVectorSize(); +} + +/*** Constant creation and test ***/ +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::one(const bwt &w) +{ + return symbolicBitVector<isSigned>(w, 1); +} +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::zero(const bwt &w) +{ + return symbolicBitVector<isSigned>(w, 0); +} +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::allOnes(const bwt &w) +{ + return symbolicBitVector<isSigned>(~zero(w)); +} + +template <bool isSigned> +symbolicProposition symbolicBitVector<isSigned>::isAllOnes() const +{ + return (*this == symbolicBitVector<isSigned>::allOnes(this->getWidth())); +} +template <bool isSigned> +symbolicProposition symbolicBitVector<isSigned>::isAllZeros() const +{ + return (*this == symbolicBitVector<isSigned>::zero(this->getWidth())); +} + +template <> +symbolicBitVector<true> symbolicBitVector<true>::maxValue(const bwt &w) +{ + symbolicBitVector<true> leadingZero(symbolicBitVector<true>::zero(1)); + symbolicBitVector<true> base(symbolicBitVector<true>::allOnes(w - 1)); + + return symbolicBitVector<true>(::CVC4::NodeManager::currentNM()->mkNode( + ::CVC4::kind::BITVECTOR_CONCAT, leadingZero, base)); +} + +template <> +symbolicBitVector<false> symbolicBitVector<false>::maxValue(const bwt &w) +{ + return symbolicBitVector<false>::allOnes(w); +} + +template <> +symbolicBitVector<true> symbolicBitVector<true>::minValue(const bwt &w) +{ + symbolicBitVector<true> leadingOne(symbolicBitVector<true>::one(1)); + symbolicBitVector<true> base(symbolicBitVector<true>::zero(w - 1)); + + return symbolicBitVector<true>(::CVC4::NodeManager::currentNM()->mkNode( + ::CVC4::kind::BITVECTOR_CONCAT, leadingOne, base)); +} + +template <> +symbolicBitVector<false> symbolicBitVector<false>::minValue(const bwt &w) +{ + return symbolicBitVector<false>::zero(w); +} + +/*** Operators ***/ +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator<<( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicBitVector<isSigned>( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_SHL, *this, op)); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator>>( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_ASHR : kind::BITVECTOR_LSHR, *this, op)); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator|( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicBitVector<isSigned>( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op)); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator&( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicBitVector<isSigned>( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op)); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator+( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicBitVector<isSigned>( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, *this, op)); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator-( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicBitVector<isSigned>( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, *this, op)); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator*( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicBitVector<isSigned>( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, *this, op)); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator/( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_SDIV : kind::BITVECTOR_UDIV_TOTAL, + *this, + op)); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator%( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_SREM : kind::BITVECTOR_UREM_TOTAL, + *this, + op)); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator-(void) const +{ + return symbolicBitVector<isSigned>( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_NEG, *this)); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator~(void)const +{ + return symbolicBitVector<isSigned>( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this)); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::increment() const +{ + return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode( + kind::BITVECTOR_PLUS, *this, one(this->getWidth()))); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::decrement() const +{ + return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode( + kind::BITVECTOR_SUB, *this, one(this->getWidth()))); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::signExtendRightShift( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicBitVector<isSigned>( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_ASHR, *this, op)); +} + +/*** Modular operations ***/ +// No overflow checking so these are the same as other operations +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularLeftShift( + const symbolicBitVector<isSigned> &op) const +{ + return *this << op; +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularRightShift( + const symbolicBitVector<isSigned> &op) const +{ + return *this >> op; +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularIncrement() + const +{ + return this->increment(); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularDecrement() + const +{ + return this->decrement(); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularAdd( + const symbolicBitVector<isSigned> &op) const +{ + return *this + op; +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularNegate() const +{ + return -(*this); +} + +/*** Comparisons ***/ + +template <bool isSigned> +symbolicProposition symbolicBitVector<isSigned>::operator==( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicProposition( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op)); +} + +template <bool isSigned> +symbolicProposition symbolicBitVector<isSigned>::operator<=( + const symbolicBitVector<isSigned> &op) const +{ + // Consider adding kind::BITVECTOR_SLEBV and BITVECTOR_ULEBV + return (*this < op) || (*this == op); +} + +template <bool isSigned> +symbolicProposition symbolicBitVector<isSigned>::operator>=( + const symbolicBitVector<isSigned> &op) const +{ + return (*this > op) || (*this == op); +} + +template <bool isSigned> +symbolicProposition symbolicBitVector<isSigned>::operator<( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicProposition(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, *this, op)); +} + +template <bool isSigned> +symbolicProposition symbolicBitVector<isSigned>::operator>( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicProposition(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, op, *this)); +} + +/*** Type conversion ***/ +// CVC4 nodes make no distinction between signed and unsigned, thus ... +template <bool isSigned> +symbolicBitVector<true> symbolicBitVector<isSigned>::toSigned(void) const +{ + return symbolicBitVector<true>(*this); +} +template <bool isSigned> +symbolicBitVector<false> symbolicBitVector<isSigned>::toUnsigned(void) const +{ + return symbolicBitVector<false>(*this); +} + +/*** Bit hacks ***/ +template <> +symbolicBitVector<true> symbolicBitVector<true>::extend(bwt extension) const +{ + NodeBuilder<> construct(kind::BITVECTOR_SIGN_EXTEND); + construct << NodeManager::currentNM()->mkConst<BitVectorSignExtend>( + BitVectorSignExtend(extension)) + << *this; + + return symbolicBitVector<true>(construct); +} + +template <> +symbolicBitVector<false> symbolicBitVector<false>::extend(bwt extension) const +{ + NodeBuilder<> construct(kind::BITVECTOR_ZERO_EXTEND); + construct << NodeManager::currentNM()->mkConst<BitVectorZeroExtend>( + BitVectorZeroExtend(extension)) + << *this; + + return symbolicBitVector<false>(construct); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::contract( + bwt reduction) const +{ + PRECONDITION(this->getWidth() > reduction); + + NodeBuilder<> construct(kind::BITVECTOR_EXTRACT); + construct << NodeManager::currentNM()->mkConst<BitVectorExtract>( + BitVectorExtract((this->getWidth() - 1) - reduction, 0)) + << *this; + + return symbolicBitVector<isSigned>(construct); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::resize( + bwt newSize) const +{ + bwt width = this->getWidth(); + + if (newSize > width) + { + return this->extend(newSize - width); + } + else if (newSize < width) + { + return this->contract(width - newSize); + } + else + { + return *this; + } +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::matchWidth( + const symbolicBitVector<isSigned> &op) const +{ + PRECONDITION(this->getWidth() <= op.getWidth()); + return this->extend(op.getWidth() - this->getWidth()); +} + +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::append( + const symbolicBitVector<isSigned> &op) const +{ + return symbolicBitVector<isSigned>( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, *this, op)); +} + +// Inclusive of end points, thus if the same, extracts just one bit +template <bool isSigned> +symbolicBitVector<isSigned> symbolicBitVector<isSigned>::extract( + bwt upper, bwt lower) const +{ + PRECONDITION(upper >= lower); + + NodeBuilder<> construct(kind::BITVECTOR_EXTRACT); + construct << NodeManager::currentNM()->mkConst<BitVectorExtract>( + BitVectorExtract(upper, lower)) + << *this; + + return symbolicBitVector<isSigned>(construct); +} + +floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode t) + : FloatingPointSize(t.getConst<FloatingPointSize>()) +{ + PRECONDITION(t.isFloatingPoint()); +} +floatingPointTypeInfo::floatingPointTypeInfo(unsigned exp, unsigned sig) + : FloatingPointSize(exp, sig) +{ +} +floatingPointTypeInfo::floatingPointTypeInfo(const floatingPointTypeInfo &old) + : FloatingPointSize(old) +{ +} + +TypeNode floatingPointTypeInfo::getTypeNode(void) const +{ + return NodeManager::currentNM()->mkFloatingPointType(*this); +} +} FpConverter::FpConverter(context::UserContext *user) - : d_additionalAssertions(user) {} + : +#ifdef CVC4_USE_SYMFPU + f(user), + r(user), + b(user), + u(user), + s(user), +#endif + d_additionalAssertions(user) +{ +} + +#ifdef CVC4_USE_SYMFPU +Node FpConverter::ufToNode(const fpt &format, const uf &u) const +{ + NodeManager *nm = NodeManager::currentNM(); + + FloatingPointSize fps(format.getTypeNode().getConst<FloatingPointSize>()); + + // This is not entirely obvious but it builds a float from components + // Particularly, if the components can be constant folded, it should + // build a Node containing a constant FloatingPoint number + + ubv packed(symfpu::pack<traits>(format, u)); + Node value = + nm->mkNode(nm->mkConst(FloatingPointToFPIEEEBitVector(fps)), packed); + return value; +} + +Node FpConverter::rmToNode(const rm &r) const +{ + NodeManager *nm = NodeManager::currentNM(); + + Node transVar = r; + + Node RNE = traits::RNE(); + Node RNA = traits::RNA(); + Node RTP = traits::RTP(); + Node RTN = traits::RTN(); + Node RTZ = traits::RTZ(); + + Node value = nm->mkNode( + kind::ITE, + nm->mkNode(kind::EQUAL, transVar, RNE), + nm->mkConst(roundNearestTiesToEven), + nm->mkNode(kind::ITE, + nm->mkNode(kind::EQUAL, transVar, RNA), + nm->mkConst(roundNearestTiesToAway), + nm->mkNode(kind::ITE, + nm->mkNode(kind::EQUAL, transVar, RTP), + nm->mkConst(roundTowardPositive), + nm->mkNode(kind::ITE, + nm->mkNode(kind::EQUAL, transVar, RTN), + nm->mkConst(roundTowardNegative), + nm->mkConst(roundTowardZero))))); + return value; +} + +Node FpConverter::propToNode(const prop &p) const +{ + NodeManager *nm = NodeManager::currentNM(); + Node value = + nm->mkNode(kind::EQUAL, p, nm->mkConst(::CVC4::BitVector(1U, 1U))); + return value; +} +Node FpConverter::ubvToNode(const ubv &u) const { return u; } +Node FpConverter::sbvToNode(const sbv &s) const { return s; } +// Creates the components constraint +FpConverter::uf FpConverter::buildComponents(TNode current) +{ + Assert(Theory::isLeafOf(current, THEORY_FP) + || current.getKind() == kind::FLOATINGPOINT_TO_FP_REAL); + + NodeManager *nm = NodeManager::currentNM(); + uf tmp(nm->mkNode(kind::FLOATINGPOINT_COMPONENT_NAN, current), + nm->mkNode(kind::FLOATINGPOINT_COMPONENT_INF, current), + nm->mkNode(kind::FLOATINGPOINT_COMPONENT_ZERO, current), + nm->mkNode(kind::FLOATINGPOINT_COMPONENT_SIGN, current), + nm->mkNode(kind::FLOATINGPOINT_COMPONENT_EXPONENT, current), + nm->mkNode(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND, current)); + + d_additionalAssertions.push_back(tmp.valid(fpt(current.getType()))); -Node FpConverter::convert(TNode node) { - Unimplemented("Conversion not implemented."); + return tmp; } +#endif + +// Non-convertible things should only be added to the stack at the very start, +// thus... +#define CVC4_FPCONV_PASSTHROUGH Assert(workStack.empty()) + +Node FpConverter::convert(TNode node) +{ +#ifdef CVC4_USE_SYMFPU + std::stack<TNode> workStack; + TNode result = node; + + workStack.push(node); + + NodeManager *nm = NodeManager::currentNM(); + + while (!workStack.empty()) + { + TNode current = workStack.top(); + workStack.pop(); + result = current; + + TypeNode t(current.getType()); + + if (t.isRoundingMode()) + { + rmMap::const_iterator i(r.find(current)); + + if (i == r.end()) + { + if (Theory::isLeafOf(current, THEORY_FP)) + { + if (current.getKind() == kind::CONST_ROUNDINGMODE) + { + /******** Constants ********/ + switch (current.getConst<RoundingMode>()) + { + case roundNearestTiesToEven: + r.insert(current, traits::RNE()); + break; + case roundNearestTiesToAway: + r.insert(current, traits::RNA()); + break; + case roundTowardPositive: r.insert(current, traits::RTP()); break; + case roundTowardNegative: r.insert(current, traits::RTN()); break; + case roundTowardZero: r.insert(current, traits::RTZ()); break; + default: Unreachable("Unknown rounding mode"); break; + } + } + else + { + /******** Variables ********/ + rm tmp(nm->mkNode(kind::ROUNDINGMODE_BITBLAST, current)); + r.insert(current, tmp); + d_additionalAssertions.push_back(tmp.valid()); + } + } + else + { + Unreachable("Unknown kind of type RoundingMode"); + } + } + // Returns a rounding-mode type so don't alter the return value + } + else if (t.isFloatingPoint()) + { + fpMap::const_iterator i(f.find(current)); + + if (i == f.end()) + { + if (Theory::isLeafOf(current, THEORY_FP)) + { + if (current.getKind() == kind::CONST_FLOATINGPOINT) + { + /******** Constants ********/ + f.insert(current, + symfpu::unpackedFloat<traits>( + current.getConst<FloatingPoint>().getLiteral())); + } + else + { + /******** Variables ********/ + f.insert(current, buildComponents(current)); + } + } + else + { + switch (current.getKind()) + { + case kind::CONST_FLOATINGPOINT: + case kind::VARIABLE: + case kind::BOUND_VARIABLE: + case kind::SKOLEM: + Unreachable("Kind should have been handled as a leaf."); + break; + + /******** Operations ********/ + case kind::FLOATINGPOINT_ABS: + case kind::FLOATINGPOINT_NEG: + { + fpMap::const_iterator arg1(f.find(current[0])); + + if (arg1 == f.end()) + { + workStack.push(current); + workStack.push(current[0]); + continue; // i.e. recurse! + } + + switch (current.getKind()) + { + case kind::FLOATINGPOINT_ABS: + f.insert(current, + symfpu::absolute<traits>(fpt(current.getType()), + (*arg1).second)); + break; + case kind::FLOATINGPOINT_NEG: + f.insert(current, + symfpu::negate<traits>(fpt(current.getType()), + (*arg1).second)); + break; + default: + Unreachable("Unknown unary floating-point function"); + break; + } + } + break; + + case kind::FLOATINGPOINT_SQRT: + case kind::FLOATINGPOINT_RTI: + { + rmMap::const_iterator mode(r.find(current[0])); + fpMap::const_iterator arg1(f.find(current[1])); + bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + + if (recurseNeeded) + { + workStack.push(current); + if (mode == r.end()) + { + workStack.push(current[0]); + } + if (arg1 == f.end()) + { + workStack.push(current[1]); + } + continue; // i.e. recurse! + } + + switch (current.getKind()) + { + case kind::FLOATINGPOINT_SQRT: + f.insert(current, + symfpu::sqrt<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second)); + break; + case kind::FLOATINGPOINT_RTI: + f.insert( + current, + symfpu::roundToIntegral<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second)); + break; + default: + Unreachable("Unknown unary rounded floating-point function"); + break; + } + } + break; + + case kind::FLOATINGPOINT_REM: + { + fpMap::const_iterator arg1(f.find(current[0])); + fpMap::const_iterator arg2(f.find(current[1])); + bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + + if (recurseNeeded) + { + workStack.push(current); + if (arg1 == f.end()) + { + workStack.push(current[0]); + } + if (arg2 == f.end()) + { + workStack.push(current[1]); + } + continue; // i.e. recurse! + } + + f.insert( + current, + symfpu::remainder<traits>( + fpt(current.getType()), (*arg1).second, (*arg2).second)); + } + break; + + case kind::FLOATINGPOINT_MIN_TOTAL: + case kind::FLOATINGPOINT_MAX_TOTAL: + { + fpMap::const_iterator arg1(f.find(current[0])); + fpMap::const_iterator arg2(f.find(current[1])); + // current[2] is a bit-vector so we do not need to recurse down it + + bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + + if (recurseNeeded) + { + workStack.push(current); + if (arg1 == f.end()) + { + workStack.push(current[0]); + } + if (arg2 == f.end()) + { + workStack.push(current[1]); + } + continue; // i.e. recurse! + } + + switch (current.getKind()) + { + case kind::FLOATINGPOINT_MAX_TOTAL: + f.insert(current, + symfpu::max<traits>(fpt(current.getType()), + (*arg1).second, + (*arg2).second, + prop(current[2]))); + break; + + case kind::FLOATINGPOINT_MIN_TOTAL: + f.insert(current, + symfpu::min<traits>(fpt(current.getType()), + (*arg1).second, + (*arg2).second, + prop(current[2]))); + break; + + default: + Unreachable("Unknown binary floating-point partial function"); + break; + } + } + break; + + case kind::FLOATINGPOINT_PLUS: + case kind::FLOATINGPOINT_SUB: + case kind::FLOATINGPOINT_MULT: + case kind::FLOATINGPOINT_DIV: + { + rmMap::const_iterator mode(r.find(current[0])); + fpMap::const_iterator arg1(f.find(current[1])); + fpMap::const_iterator arg2(f.find(current[2])); + bool recurseNeeded = + (mode == r.end()) || (arg1 == f.end()) || (arg2 == f.end()); + + if (recurseNeeded) + { + workStack.push(current); + if (mode == r.end()) + { + workStack.push(current[0]); + } + if (arg1 == f.end()) + { + workStack.push(current[1]); + } + if (arg2 == f.end()) + { + workStack.push(current[2]); + } + continue; // i.e. recurse! + } + + switch (current.getKind()) + { + case kind::FLOATINGPOINT_PLUS: + f.insert(current, + symfpu::add<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second, + prop(true))); + break; + + case kind::FLOATINGPOINT_SUB: + // Should have been removed by the rewriter + Unreachable( + "Floating-point subtraction should be removed by the " + "rewriter."); + f.insert(current, + symfpu::add<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second, + prop(false))); + break; + + case kind::FLOATINGPOINT_MULT: + f.insert(current, + symfpu::multiply<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second)); + break; + case kind::FLOATINGPOINT_DIV: + f.insert(current, + symfpu::divide<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second)); + break; + case kind::FLOATINGPOINT_REM: + /* + f.insert(current, + symfpu::remainder<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second)); + */ + Unimplemented( + "Remainder with rounding mode not yet supported by " + "SMT-LIB"); + break; + + default: + Unreachable("Unknown binary rounded floating-point function"); + break; + } + } + break; + + case kind::FLOATINGPOINT_FMA: + { + rmMap::const_iterator mode(r.find(current[0])); + fpMap::const_iterator arg1(f.find(current[1])); + fpMap::const_iterator arg2(f.find(current[2])); + fpMap::const_iterator arg3(f.find(current[3])); + bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()) + || (arg2 == f.end() || (arg3 == f.end())); + + if (recurseNeeded) + { + workStack.push(current); + if (mode == r.end()) + { + workStack.push(current[0]); + } + if (arg1 == f.end()) + { + workStack.push(current[1]); + } + if (arg2 == f.end()) + { + workStack.push(current[2]); + } + if (arg3 == f.end()) + { + workStack.push(current[3]); + } + continue; // i.e. recurse! + } + + f.insert(current, + symfpu::fma<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second, + (*arg3).second)); + } + break; + + /******** Conversions ********/ + case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: + { + rmMap::const_iterator mode(r.find(current[0])); + fpMap::const_iterator arg1(f.find(current[1])); + bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + + if (recurseNeeded) + { + workStack.push(current); + if (mode == r.end()) + { + workStack.push(current[0]); + } + if (arg1 == f.end()) + { + workStack.push(current[1]); + } + continue; // i.e. recurse! + } + + f.insert( + current, + symfpu::convertFloatToFloat<traits>(fpt(current[1].getType()), + fpt(current.getType()), + (*mode).second, + (*arg1).second)); + } + break; + + case kind::FLOATINGPOINT_FP: + { + Node IEEEBV(nm->mkNode( + kind::BITVECTOR_CONCAT, current[0], current[1], current[2])); + f.insert(current, + symfpu::unpack<traits>(fpt(current.getType()), IEEEBV)); + } + break; + + case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + f.insert(current, + symfpu::unpack<traits>(fpt(current.getType()), + ubv(current[0]))); + break; + + case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + { + rmMap::const_iterator mode(r.find(current[0])); + bool recurseNeeded = (mode == r.end()); + + if (recurseNeeded) + { + workStack.push(current); + if (mode == r.end()) + { + workStack.push(current[0]); + } + continue; // i.e. recurse! + } + + switch (current.getKind()) + { + case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + f.insert( + current, + symfpu::convertSBVToFloat<traits>(fpt(current.getType()), + (*mode).second, + sbv(current[1]))); + break; + + case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + f.insert( + current, + symfpu::convertUBVToFloat<traits>(fpt(current.getType()), + (*mode).second, + ubv(current[1]))); + break; + + default: + Unreachable( + "Unknown converstion from bit-vector to floating-point"); + break; + } + } + break; + + case kind::FLOATINGPOINT_TO_FP_REAL: + { + f.insert(current, buildComponents(current)); + // Rely on the real theory and theory combination + // to handle the value + } + break; + + case kind::FLOATINGPOINT_TO_FP_GENERIC: + Unreachable("Generic to_fp not removed"); + break; + + default: Unreachable("Unknown kind of type FloatingPoint"); break; + } + } + } + // Returns a floating-point type so don't alter the return value + } + else if (t.isBoolean()) + { + boolMap::const_iterator i(b.find(current)); + + if (i == b.end()) + { + switch (current.getKind()) + { + /******** Comparisons ********/ + case kind::EQUAL: + { + TypeNode childType(current[0].getType()); + + if (childType.isFloatingPoint()) + { + fpMap::const_iterator arg1(f.find(current[0])); + fpMap::const_iterator arg2(f.find(current[1])); + bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + + if (recurseNeeded) + { + workStack.push(current); + if (arg1 == f.end()) + { + workStack.push(current[0]); + } + if (arg2 == f.end()) + { + workStack.push(current[1]); + } + continue; // i.e. recurse! + } + + b.insert(current, + symfpu::smtlibEqual<traits>( + fpt(childType), (*arg1).second, (*arg2).second)); + } + else if (childType.isRoundingMode()) + { + rmMap::const_iterator arg1(r.find(current[0])); + rmMap::const_iterator arg2(r.find(current[1])); + bool recurseNeeded = (arg1 == r.end()) || (arg2 == r.end()); + + if (recurseNeeded) + { + workStack.push(current); + if (arg1 == r.end()) + { + workStack.push(current[0]); + } + if (arg2 == r.end()) + { + workStack.push(current[1]); + } + continue; // i.e. recurse! + } + + b.insert(current, (*arg1).second == (*arg2).second); + } + else + { + CVC4_FPCONV_PASSTHROUGH; + return result; + } + } + break; + + case kind::FLOATINGPOINT_LEQ: + case kind::FLOATINGPOINT_LT: + { + TypeNode childType(current[0].getType()); + + fpMap::const_iterator arg1(f.find(current[0])); + fpMap::const_iterator arg2(f.find(current[1])); + bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + + if (recurseNeeded) + { + workStack.push(current); + if (arg1 == f.end()) + { + workStack.push(current[0]); + } + if (arg2 == f.end()) + { + workStack.push(current[1]); + } + continue; // i.e. recurse! + } + + switch (current.getKind()) + { + case kind::FLOATINGPOINT_LEQ: + b.insert(current, + symfpu::lessThanOrEqual<traits>( + fpt(childType), (*arg1).second, (*arg2).second)); + break; + + case kind::FLOATINGPOINT_LT: + b.insert(current, + symfpu::lessThan<traits>( + fpt(childType), (*arg1).second, (*arg2).second)); + break; + + default: + Unreachable("Unknown binary floating-point relation"); + break; + } + } + break; + + case kind::FLOATINGPOINT_ISN: + case kind::FLOATINGPOINT_ISSN: + case kind::FLOATINGPOINT_ISZ: + case kind::FLOATINGPOINT_ISINF: + case kind::FLOATINGPOINT_ISNAN: + case kind::FLOATINGPOINT_ISNEG: + case kind::FLOATINGPOINT_ISPOS: + { + TypeNode childType(current[0].getType()); + fpMap::const_iterator arg1(f.find(current[0])); + + if (arg1 == f.end()) + { + workStack.push(current); + workStack.push(current[0]); + continue; // i.e. recurse! + } + + switch (current.getKind()) + { + case kind::FLOATINGPOINT_ISN: + b.insert( + current, + symfpu::isNormal<traits>(fpt(childType), (*arg1).second)); + break; + + case kind::FLOATINGPOINT_ISSN: + b.insert(current, + symfpu::isSubnormal<traits>(fpt(childType), + (*arg1).second)); + break; + + case kind::FLOATINGPOINT_ISZ: + b.insert( + current, + symfpu::isZero<traits>(fpt(childType), (*arg1).second)); + break; + + case kind::FLOATINGPOINT_ISINF: + b.insert( + current, + symfpu::isInfinite<traits>(fpt(childType), (*arg1).second)); + break; + + case kind::FLOATINGPOINT_ISNAN: + b.insert(current, + symfpu::isNaN<traits>(fpt(childType), (*arg1).second)); + break; + + case kind::FLOATINGPOINT_ISPOS: + b.insert( + current, + symfpu::isPositive<traits>(fpt(childType), (*arg1).second)); + break; + + case kind::FLOATINGPOINT_ISNEG: + b.insert( + current, + symfpu::isNegative<traits>(fpt(childType), (*arg1).second)); + break; + + default: + Unreachable("Unknown unary floating-point relation"); + break; + } + } + break; + + case kind::FLOATINGPOINT_EQ: + case kind::FLOATINGPOINT_GEQ: + case kind::FLOATINGPOINT_GT: + Unreachable("Kind should have been removed by rewriter."); + break; + + // Components will be registered as they are owned by + // the floating-point theory. No action is required. + case kind::FLOATINGPOINT_COMPONENT_NAN: + case kind::FLOATINGPOINT_COMPONENT_INF: + case kind::FLOATINGPOINT_COMPONENT_ZERO: + case kind::FLOATINGPOINT_COMPONENT_SIGN: + /* Fall through... */ + + default: + CVC4_FPCONV_PASSTHROUGH; + return result; + break; + } + + i = b.find(current); + } + + result = (*i).second; + } + else if (t.isBitVector()) + { + switch (current.getKind()) + { + /******** Conversions ********/ + case kind::FLOATINGPOINT_TO_UBV_TOTAL: + { + TypeNode childType(current[1].getType()); + ubvMap::const_iterator i(u.find(current)); + + if (i == u.end()) + { + rmMap::const_iterator mode(r.find(current[0])); + fpMap::const_iterator arg1(f.find(current[1])); + bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + + if (recurseNeeded) + { + workStack.push(current); + if (mode == r.end()) + { + workStack.push(current[0]); + } + if (arg1 == f.end()) + { + workStack.push(current[1]); + } + continue; // i.e. recurse! + } + + FloatingPointToUBVTotal info = + current.getOperator().getConst<FloatingPointToUBVTotal>(); + + u.insert(current, + symfpu::convertFloatToUBV<traits>(fpt(childType), + (*mode).second, + (*arg1).second, + info.bvs, + ubv(current[2]))); + i = u.find(current); + } + + result = (*i).second; + } + break; + + case kind::FLOATINGPOINT_TO_SBV_TOTAL: + { + TypeNode childType(current[1].getType()); + sbvMap::const_iterator i(s.find(current)); + + if (i == s.end()) + { + rmMap::const_iterator mode(r.find(current[0])); + fpMap::const_iterator arg1(f.find(current[1])); + bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + + if (recurseNeeded) + { + workStack.push(current); + if (mode == r.end()) + { + workStack.push(current[0]); + } + if (arg1 == f.end()) + { + workStack.push(current[1]); + } + continue; // i.e. recurse! + } + + FloatingPointToSBVTotal info = + current.getOperator().getConst<FloatingPointToSBVTotal>(); + + s.insert(current, + symfpu::convertFloatToSBV<traits>(fpt(childType), + (*mode).second, + (*arg1).second, + info.bvs, + sbv(current[2]))); + + i = s.find(current); + } + + result = (*i).second; + } + break; + + case kind::FLOATINGPOINT_TO_UBV: + Unreachable( + "Partially defined fp.to_ubv should have been removed by " + "expandDefinition"); + break; + + case kind::FLOATINGPOINT_TO_SBV: + Unreachable( + "Partially defined fp.to_sbv should have been removed by " + "expandDefinition"); + break; + + // Again, no action is needed + case kind::FLOATINGPOINT_COMPONENT_EXPONENT: + case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: + case kind::ROUNDINGMODE_BITBLAST: + /* Fall through ... */ + + default: CVC4_FPCONV_PASSTHROUGH; break; + } + } + else if (t.isReal()) + { + switch (current.getKind()) + { + /******** Conversions ********/ + case kind::FLOATINGPOINT_TO_REAL_TOTAL: + { + // We need to recurse so that any variables that are only + // used under this will have components created + // (via auxiliary constraints) + + TypeNode childType(current[0].getType()); + fpMap::const_iterator arg1(f.find(current[0])); + + if (arg1 == f.end()) + { + workStack.push(current); + workStack.push(current[0]); + continue; // i.e. recurse! + } + + // However we don't need to do anything explicitly with + // this as it will be treated as an uninterpreted function + // by the real theory and we don't need to bit-blast the + // float expression unless we need to say something about + // its value. + } + + break; + + case kind::FLOATINGPOINT_TO_REAL: + Unreachable( + "Partially defined fp.to_real should have been removed by " + "expandDefinition"); + break; + + default: CVC4_FPCONV_PASSTHROUGH; break; + } + } + else + { + CVC4_FPCONV_PASSTHROUGH; + } + } + + return result; +#else + Unimplemented("Conversion is dependent on SymFPU"); +#endif +} + +#undef CVC4_FPCONV_PASSTHROUGH + +Node FpConverter::getValue(Valuation &val, TNode var) +{ + Assert(Theory::isLeafOf(var, THEORY_FP)); + +#ifdef CVC4_USE_SYMFPU + TypeNode t(var.getType()); + + if (t.isRoundingMode()) + { + rmMap::const_iterator i(r.find(var)); + + if (i == r.end()) + { + Unreachable("Asking for the value of an unregistered expression"); + } + else + { + Node value = rmToNode((*i).second); + return value; + } + } + else if (t.isFloatingPoint()) + { + fpMap::const_iterator i(f.find(var)); + + if (i == f.end()) + { + Unreachable("Asking for the value of an unregistered expression"); + } + else + { + Node value = ufToNode(fpt(t), (*i).second); + return value; + } + } + else + { + Unreachable( + "Asking for the value of a type that is not managed by the " + "floating-point theory"); + } + + Unreachable("Unable to find value"); + +#else + Unimplemented("Conversion is dependent on SymFPU"); +#endif -Node FpConverter::getValue(Valuation &val, TNode var) { - Unimplemented("Conversion not implemented."); + return Node::null(); } } // namespace fp |