diff options
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 16 | ||||
| -rw-r--r-- | src/theory/fp/fp_converter.cpp | 1712 | ||||
| -rw-r--r-- | src/theory/fp/fp_converter.h | 305 | ||||
| -rw-r--r-- | src/theory/fp/kinds | 24 | ||||
| -rw-r--r-- | src/theory/fp/theory_fp.cpp | 467 | ||||
| -rw-r--r-- | src/theory/fp/theory_fp.h | 20 | ||||
| -rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 156 | ||||
| -rw-r--r-- | src/theory/fp/theory_fp_type_rules.h | 164 | ||||
| -rw-r--r-- | src/theory/logic_info.cpp | 10 | ||||
| -rw-r--r-- | src/util/floatingpoint.cpp | 646 | ||||
| -rw-r--r-- | src/util/floatingpoint.h | 198 |
11 files changed, 3673 insertions, 45 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index af51ccd45..73357bdef 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -636,6 +636,13 @@ void Smt2Printer::toStream(std::ostream& out, case kind::FLOATINGPOINT_ISNEG: case kind::FLOATINGPOINT_ISPOS: case kind::FLOATINGPOINT_TO_REAL: + case kind::FLOATINGPOINT_COMPONENT_NAN: + case kind::FLOATINGPOINT_COMPONENT_INF: + case kind::FLOATINGPOINT_COMPONENT_ZERO: + case kind::FLOATINGPOINT_COMPONENT_SIGN: + case kind::FLOATINGPOINT_COMPONENT_EXPONENT: + case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: + case kind::ROUNDINGMODE_BITBLAST: out << smtKindString(k, d_variant) << ' '; break; @@ -1055,6 +1062,15 @@ static string smtKindString(Kind k, Variant v) case kind::FLOATINGPOINT_TO_REAL: return "fp.to_real"; case kind::FLOATINGPOINT_TO_REAL_TOTAL: return "fp.to_real_total"; + case kind::FLOATINGPOINT_COMPONENT_NAN: return "NAN"; + case kind::FLOATINGPOINT_COMPONENT_INF: return "INF"; + case kind::FLOATINGPOINT_COMPONENT_ZERO: return "ZERO"; + case kind::FLOATINGPOINT_COMPONENT_SIGN: return "SIGN"; + case kind::FLOATINGPOINT_COMPONENT_EXPONENT: return "EXPONENT"; + case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: return "SIGNIFICAND"; + case kind::ROUNDINGMODE_BITBLAST: + return "RMBITBLAST"; + //string theory case kind::STRING_CONCAT: return "str.++"; case kind::STRING_LENGTH: return v == z3str_variant ? "Length" : "str.len"; 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 diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 8a054e03a..5a7b839aa 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -21,12 +21,30 @@ #ifndef __CVC4__THEORY__FP__FP_CONVERTER_H #define __CVC4__THEORY__FP__FP_CONVERTER_H +#include "base/cvc4_assert.h" #include "context/cdhashmap.h" #include "context/cdlist.h" +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/type.h" #include "theory/valuation.h" +#include "util/bitvector.h" #include "util/floatingpoint.h" #include "util/hash.h" +#ifdef CVC4_USE_SYMFPU +#include "symfpu/core/unpackedFloat.h" +#endif + +#ifdef CVC4_SYM_SYMBOLIC_EVAL +// This allows debugging of the CVC4 symbolic back-end. +// By enabling this and disabling constant folding in the rewriter, +// SMT files that have operations on constants will be evaluated +// during the encoding step, which means that the expressions +// generated by the symbolic back-end can be debugged with gdb. +#include "theory/rewriter.h" +#endif + namespace CVC4 { namespace theory { namespace fp { @@ -35,7 +53,292 @@ typedef PairHashFunction<TypeNode, TypeNode, TypeNodeHashFunction, TypeNodeHashFunction> PairTypeNodeHashFunction; -class FpConverter { +/** + * This is a symfpu symbolic "back-end". It allows the library to be used to + * construct bit-vector expressions that compute floating-point operations. + * This is effectively the glue between symfpu's notion of "signed bit-vector" + * and CVC4's node. + */ +namespace symfpuSymbolic { + +// Forward declarations of the wrapped types so that traits can be defined early +// and used in the implementations +class symbolicRoundingMode; +class floatingPointTypeInfo; +class symbolicProposition; +template <bool T> +class symbolicBitVector; + +// This is the template parameter for symfpu's templates. +class traits +{ + public: + // The six key types that symfpu uses. + typedef unsigned bwt; + typedef symbolicRoundingMode rm; + typedef floatingPointTypeInfo fpt; + typedef symbolicProposition prop; + typedef symbolicBitVector<true> sbv; + typedef symbolicBitVector<false> ubv; + + // Give concrete instances (wrapped nodes) for each rounding mode. + static symbolicRoundingMode RNE(void); + static symbolicRoundingMode RNA(void); + static symbolicRoundingMode RTP(void); + static symbolicRoundingMode RTN(void); + static symbolicRoundingMode RTZ(void); + + // Properties used by symfpu + static void precondition(const bool b); + static void postcondition(const bool b); + static void invariant(const bool b); + static void precondition(const prop &p); + static void postcondition(const prop &p); + static void invariant(const prop &p); +}; + +// Use the same type names as symfpu. +typedef traits::bwt bwt; + +/** + * Wrap the CVC4::Node types so that we can debug issues with this back-end + */ +class nodeWrapper : public Node +{ + protected: +/* CVC4_SYM_SYMBOLIC_EVAL is for debugging CVC4 symbolic back-end issues. + * Enable this and disabling constant folding will mean that operations + * that are input with constant args are 'folded' using the symbolic encoding + * allowing them to be traced via GDB. + */ +#ifdef CVC4_SYM_SYMBOLIC_EVAL + nodeWrapper(const Node &n) : Node(theory::Rewriter::rewrite(n)) {} +#else + nodeWrapper(const Node &n) : Node(n) {} +#endif +}; + +class symbolicProposition : public nodeWrapper +{ + protected: + bool checkNodeType(const TNode node); + +#ifdef CVC4_USE_SYMFPU + friend ::symfpu::ite<symbolicProposition, symbolicProposition>; // For ITE +#endif + + public: + symbolicProposition(const Node n); + symbolicProposition(bool v); + symbolicProposition(const symbolicProposition &old); + + symbolicProposition operator!(void)const; + symbolicProposition operator&&(const symbolicProposition &op) const; + symbolicProposition operator||(const symbolicProposition &op) const; + symbolicProposition operator==(const symbolicProposition &op) const; + symbolicProposition operator^(const symbolicProposition &op) const; +}; + +class symbolicRoundingMode : public nodeWrapper +{ + protected: + bool checkNodeType(const TNode n); + +#ifdef CVC4_USE_SYMFPU + friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>; // For ITE +#endif + + public: + symbolicRoundingMode(const Node n); + symbolicRoundingMode(const unsigned v); + symbolicRoundingMode(const symbolicRoundingMode &old); + + symbolicProposition valid(void) const; + symbolicProposition operator==(const symbolicRoundingMode &op) const; +}; + +// Type function for mapping between types +template <bool T> +struct signedToLiteralType; + +template <> +struct signedToLiteralType<true> +{ + typedef int literalType; +}; +template <> +struct signedToLiteralType<false> +{ + typedef unsigned int literalType; +}; + +template <bool isSigned> +class symbolicBitVector : public nodeWrapper +{ + protected: + typedef typename signedToLiteralType<isSigned>::literalType literalType; + + Node boolNodeToBV(Node node) const; + Node BVToBoolNode(Node node) const; + + Node fromProposition(Node node) const; + Node toProposition(Node node) const; + bool checkNodeType(const TNode n); + friend symbolicBitVector<!isSigned>; // To allow conversion between the types + +#ifdef CVC4_USE_SYMFPU + friend ::symfpu::ite<symbolicProposition, + symbolicBitVector<isSigned> >; // For ITE +#endif + + public: + symbolicBitVector(const Node n); + symbolicBitVector(const bwt w, const unsigned v); + symbolicBitVector(const symbolicProposition &p); + symbolicBitVector(const symbolicBitVector<isSigned> &old); + symbolicBitVector(const BitVector &old); + + bwt getWidth(void) const; + + /*** Constant creation and test ***/ + static symbolicBitVector<isSigned> one(const bwt &w); + static symbolicBitVector<isSigned> zero(const bwt &w); + static symbolicBitVector<isSigned> allOnes(const bwt &w); + + symbolicProposition isAllOnes() const; + symbolicProposition isAllZeros() const; + + static symbolicBitVector<isSigned> maxValue(const bwt &w); + static symbolicBitVector<isSigned> minValue(const bwt &w); + + /*** Operators ***/ + symbolicBitVector<isSigned> operator<<( + const symbolicBitVector<isSigned> &op) const; + symbolicBitVector<isSigned> operator>>( + const symbolicBitVector<isSigned> &op) const; + symbolicBitVector<isSigned> operator|( + const symbolicBitVector<isSigned> &op) const; + symbolicBitVector<isSigned> operator&( + const symbolicBitVector<isSigned> &op) const; + symbolicBitVector<isSigned> operator+( + const symbolicBitVector<isSigned> &op) const; + symbolicBitVector<isSigned> operator-( + const symbolicBitVector<isSigned> &op) const; + symbolicBitVector<isSigned> operator*( + const symbolicBitVector<isSigned> &op) const; + symbolicBitVector<isSigned> operator/( + const symbolicBitVector<isSigned> &op) const; + symbolicBitVector<isSigned> operator%( + const symbolicBitVector<isSigned> &op) const; + symbolicBitVector<isSigned> operator-(void) const; + symbolicBitVector<isSigned> operator~(void)const; + symbolicBitVector<isSigned> increment() const; + symbolicBitVector<isSigned> decrement() const; + symbolicBitVector<isSigned> signExtendRightShift( + const symbolicBitVector<isSigned> &op) const; + + /*** Modular operations ***/ + // This back-end doesn't do any overflow checking so these are the same as + // other operations + symbolicBitVector<isSigned> modularLeftShift( + const symbolicBitVector<isSigned> &op) const; + symbolicBitVector<isSigned> modularRightShift( + const symbolicBitVector<isSigned> &op) const; + symbolicBitVector<isSigned> modularIncrement() const; + symbolicBitVector<isSigned> modularDecrement() const; + symbolicBitVector<isSigned> modularAdd( + const symbolicBitVector<isSigned> &op) const; + symbolicBitVector<isSigned> modularNegate() const; + + /*** Comparisons ***/ + symbolicProposition operator==(const symbolicBitVector<isSigned> &op) const; + symbolicProposition operator<=(const symbolicBitVector<isSigned> &op) const; + symbolicProposition operator>=(const symbolicBitVector<isSigned> &op) const; + symbolicProposition operator<(const symbolicBitVector<isSigned> &op) const; + symbolicProposition operator>(const symbolicBitVector<isSigned> &op) const; + + /*** Type conversion ***/ + // CVC4 nodes make no distinction between signed and unsigned, thus these are + // trivial + symbolicBitVector<true> toSigned(void) const; + symbolicBitVector<false> toUnsigned(void) const; + + /*** Bit hacks ***/ + symbolicBitVector<isSigned> extend(bwt extension) const; + symbolicBitVector<isSigned> contract(bwt reduction) const; + symbolicBitVector<isSigned> resize(bwt newSize) const; + symbolicBitVector<isSigned> matchWidth( + const symbolicBitVector<isSigned> &op) const; + symbolicBitVector<isSigned> append( + const symbolicBitVector<isSigned> &op) const; + + // Inclusive of end points, thus if the same, extracts just one bit + symbolicBitVector<isSigned> extract(bwt upper, bwt lower) const; +}; + +// Use the same type information as the literal back-end but add an interface to +// TypeNodes for convenience. +class floatingPointTypeInfo : public FloatingPointSize +{ + public: + floatingPointTypeInfo(const TypeNode t); + floatingPointTypeInfo(unsigned exp, unsigned sig); + floatingPointTypeInfo(const floatingPointTypeInfo &old); + + TypeNode getTypeNode(void) const; +}; +} + +/** + * This class uses SymFPU to convert an expression containing floating-point + * kinds and operations into a logically equivalent form with bit-vector + * operations replacing the floating-point ones. It also has a getValue method + * to produce an expression which will reconstruct the value of the + * floating-point terms from a valuation. + * + * Internally it caches all of the unpacked floats so that unnecessary packing + * and unpacking operations are avoided and to make best use of structural + * sharing. + */ +class FpConverter +{ + protected: +#ifdef CVC4_USE_SYMFPU + typedef symfpuSymbolic::traits traits; + typedef ::symfpu::unpackedFloat<symfpuSymbolic::traits> uf; + typedef symfpuSymbolic::traits::rm rm; + typedef symfpuSymbolic::traits::fpt fpt; + typedef symfpuSymbolic::traits::prop prop; + typedef symfpuSymbolic::traits::ubv ubv; + typedef symfpuSymbolic::traits::sbv sbv; + + typedef context::CDHashMap<Node, uf, NodeHashFunction> fpMap; + typedef context::CDHashMap<Node, rm, NodeHashFunction> rmMap; + typedef context::CDHashMap<Node, prop, NodeHashFunction> boolMap; + typedef context::CDHashMap<Node, ubv, NodeHashFunction> ubvMap; + typedef context::CDHashMap<Node, sbv, NodeHashFunction> sbvMap; + + fpMap f; + rmMap r; + boolMap b; + ubvMap u; + sbvMap s; + + /* These functions take a symfpu object and convert it to a node. + * These should ensure that constant folding it will give a + * constant of the right type. + */ + + Node ufToNode(const fpt &, const uf &) const; + Node rmToNode(const rm &) const; + Node propToNode(const prop &) const; + Node ubvToNode(const ubv &) const; + Node sbvToNode(const sbv &) const; + + /* Creates the relevant components for a variable */ + uf buildComponents(TNode current); +#endif + public: context::CDList<Node> d_additionalAssertions; diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index 966ed4d71..b1170b42c 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -283,4 +283,28 @@ operator FLOATINGPOINT_TO_REAL_TOTAL 2 "floating-point to real (defined for all typerule FLOATINGPOINT_TO_REAL_TOTAL ::CVC4::theory::fp::FloatingPointToRealTotalTypeRule + +operator FLOATINGPOINT_COMPONENT_NAN 1 "NaN component of a word-blasted floating-point number" +typerule FLOATINGPOINT_COMPONENT_NAN ::CVC4::theory::fp::FloatingPointComponentBit + +operator FLOATINGPOINT_COMPONENT_INF 1 "Inf component of a word-blasted floating-point number" +typerule FLOATINGPOINT_COMPONENT_INF ::CVC4::theory::fp::FloatingPointComponentBit + +operator FLOATINGPOINT_COMPONENT_ZERO 1 "Zero component of a word-blasted floating-point number" +typerule FLOATINGPOINT_COMPONENT_ZERO ::CVC4::theory::fp::FloatingPointComponentBit + +operator FLOATINGPOINT_COMPONENT_SIGN 1 "Sign component of a word-blasted floating-point number" +typerule FLOATINGPOINT_COMPONENT_SIGN ::CVC4::theory::fp::FloatingPointComponentBit + +operator FLOATINGPOINT_COMPONENT_EXPONENT 1 "Exponent component of a word-blasted floating-point number" +typerule FLOATINGPOINT_COMPONENT_EXPONENT ::CVC4::theory::fp::FloatingPointComponentExponent + +operator FLOATINGPOINT_COMPONENT_SIGNIFICAND 1 "Significand component of a word-blasted floating-point number" +typerule FLOATINGPOINT_COMPONENT_SIGNIFICAND ::CVC4::theory::fp::FloatingPointComponentSignificand + + +operator ROUNDINGMODE_BITBLAST 1 "The bit-vector for a non-deterministic rounding mode" +typerule ROUNDINGMODE_BITBLAST ::CVC4::theory::fp::RoundingModeBitBlast + + endtheory diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 748c5c1c6..94733b98d 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -16,6 +16,7 @@ **/ #include "theory/fp/theory_fp.h" +#include "theory/rewriter.h" #include "theory/theory_model.h" #include <set> @@ -95,8 +96,10 @@ Node buildConjunct(const std::vector<TNode> &assumptions) { } // namespace helper /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ -TheoryFp::TheoryFp(context::Context *c, context::UserContext *u, - OutputChannel &out, Valuation valuation, +TheoryFp::TheoryFp(context::Context *c, + context::UserContext *u, + OutputChannel &out, + Valuation valuation, const LogicInfo &logicInfo) : Theory(THEORY_FP, c, u, out, valuation, logicInfo), d_notification(*this), @@ -110,7 +113,11 @@ TheoryFp::TheoryFp(context::Context *c, context::UserContext *u, d_maxMap(u), d_toUBVMap(u), d_toSBVMap(u), - d_toRealMap(u) { + d_toRealMap(u), + realToFloatMap(u), + floatToRealMap(u), + abstractionMap(u) +{ // Kinds that are to be handled in the congruence closure d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ABS); @@ -157,6 +164,14 @@ TheoryFp::TheoryFp(context::Context *c, context::UserContext *u, d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_SBV_TOTAL); d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_REAL_TOTAL); + d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_NAN); + d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_INF); + d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_ZERO); + d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_SIGN); + d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_EXPONENT); + d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND); + d_equalityEngine.addFunctionKind(kind::ROUNDINGMODE_BITBLAST); + } /* TheoryFp::TheoryFp() */ Node TheoryFp::minUF(Node node) { @@ -291,7 +306,7 @@ Node TheoryFp::toRealUF(Node node) { std::vector<TypeNode> args(1); args[0] = t; fun = nm->mkSkolem("floatingpoint_to_real_infinity_and_NaN_case", - nm->mkFunctionType(t, nm->realType()), + nm->mkFunctionType(args, nm->realType()), "floatingpoint_to_real_infinity_and_NaN_case", NodeManager::SKOLEM_EXACT_NAME); d_toRealMap.insert(t, fun); @@ -301,16 +316,85 @@ Node TheoryFp::toRealUF(Node node) { return nm->mkNode(kind::APPLY_UF, fun, node[0]); } -Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) { - Trace("fp-expandDefinition") - << "TheoryFp::expandDefinition(): " << node << std::endl; - +void TheoryFp::enableUF(LogicRequest &lr) +{ if (!this->d_expansionRequested) { - lr.widenLogic( - THEORY_UF); // Needed for conversions to/from real and min/max - lr.widenLogic(THEORY_BV); + // Needed for conversions to/from real and min/max + lr.widenLogic(THEORY_UF); + // THEORY_BV has to be enabled when the logic is set this->d_expansionRequested = true; } + return; +} + +Node TheoryFp::abstractRealToFloat(Node node) +{ + Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL); + TypeNode t(node.getType()); + Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); + + NodeManager *nm = NodeManager::currentNM(); + ComparisonUFMap::const_iterator i(realToFloatMap.find(t)); + + Node fun; + if (i == realToFloatMap.end()) + { + std::vector<TypeNode> args(2); + args[0] = node[0].getType(); + args[1] = node[1].getType(); + fun = nm->mkSkolem("floatingpoint_abstract_real_to_float", + nm->mkFunctionType(args, node.getType()), + "floatingpoint_abstract_real_to_float", + NodeManager::SKOLEM_EXACT_NAME); + realToFloatMap.insert(t, fun); + } + else + { + fun = (*i).second; + } + Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]); + + abstractionMap.insert(uf, node); + + return uf; +} + +Node TheoryFp::abstractFloatToReal(Node node) +{ + Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL); + TypeNode t(node[0].getType()); + Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); + + NodeManager *nm = NodeManager::currentNM(); + ComparisonUFMap::const_iterator i(floatToRealMap.find(t)); + + Node fun; + if (i == floatToRealMap.end()) + { + std::vector<TypeNode> args(2); + args[0] = t; + args[1] = nm->realType(); + fun = nm->mkSkolem("floatingpoint_abstract_float_to_real", + nm->mkFunctionType(args, nm->realType()), + "floatingpoint_abstract_float_to_real", + NodeManager::SKOLEM_EXACT_NAME); + floatToRealMap.insert(t, fun); + } + else + { + fun = (*i).second; + } + Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]); + + abstractionMap.insert(uf, node); + + return uf; +} + +Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) +{ + Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node + << std::endl; Node res = node; @@ -318,14 +402,17 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) { res = removeToFPGeneric::removeToFPGeneric(node); } else if (node.getKind() == kind::FLOATINGPOINT_MIN) { + enableUF(lr); res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MIN_TOTAL, node[0], node[1], minUF(node)); } else if (node.getKind() == kind::FLOATINGPOINT_MAX) { + enableUF(lr); res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MAX_TOTAL, node[0], node[1], maxUF(node)); } else if (node.getKind() == kind::FLOATINGPOINT_TO_UBV) { + enableUF(lr); FloatingPointToUBV info = node.getOperator().getConst<FloatingPointToUBV>(); FloatingPointToUBVTotal newInfo(info); @@ -335,6 +422,7 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) { toUBVUF(node)); } else if (node.getKind() == kind::FLOATINGPOINT_TO_SBV) { + enableUF(lr); FloatingPointToSBV info = node.getOperator().getConst<FloatingPointToSBV>(); FloatingPointToSBVTotal newInfo(info); @@ -344,6 +432,7 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) { toSBVUF(node)); } else if (node.getKind() == kind::FLOATINGPOINT_TO_REAL) { + enableUF(lr); res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL, node[0], toRealUF(node)); @@ -351,6 +440,13 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) { // Do nothing } + // We will need to enable UF to abstract these in ppRewrite + if (res.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL + || res.getKind() == kind::FLOATINGPOINT_TO_FP_REAL) + { + enableUF(lr); + } + if (res != node) { Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node << " rewritten to " << res << std::endl; @@ -359,6 +455,290 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) { return res; } +Node TheoryFp::ppRewrite(TNode node) +{ + Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl; + + Node res = node; + + // Abstract conversion functions + if (node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL) + { + res = abstractFloatToReal(node); + + // Generate some lemmas + NodeManager *nm = NodeManager::currentNM(); + + Node pd = + nm->mkNode(kind::IMPLIES, + nm->mkNode(kind::OR, + nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]), + nm->mkNode(kind::FLOATINGPOINT_ISINF, node[0])), + nm->mkNode(kind::EQUAL, res, node[1])); + handleLemma(pd); + + Node z = + nm->mkNode(kind::IMPLIES, + nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]), + nm->mkNode(kind::EQUAL, res, nm->mkConst(Rational(0U)))); + handleLemma(z); + + // TODO : bounds on the output from largest floats, #1914 + } + else if (node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL) + { + res = abstractRealToFloat(node); + + // Generate some lemmas + NodeManager *nm = NodeManager::currentNM(); + + Node nnan = + nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, res)); + handleLemma(nnan); + + Node z = nm->mkNode( + kind::IMPLIES, + nm->mkNode(kind::EQUAL, node[1], nm->mkConst(Rational(0U))), + nm->mkNode(kind::EQUAL, + res, + nm->mkConst(FloatingPoint::makeZero( + res.getType().getConst<FloatingPointSize>(), false)))); + handleLemma(z); + + // TODO : rounding-mode specific bounds on floats that don't give infinity + // BEWARE of directed rounding! #1914 + } + + if (res != node) + { + Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): node " << node + << " rewritten to " << res << std::endl; + } + + return res; +} + +bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) +{ + Trace("fp-refineAbstraction") << "TheoryFp::refineAbstraction(): " << abstract + << " vs. " << concrete << std::endl; + Kind k = concrete.getKind(); + if (k == kind::FLOATINGPOINT_TO_REAL_TOTAL) + { + // Get the values + Assert(m->hasTerm(abstract)); + Assert(m->hasTerm(concrete[0])); + Assert(m->hasTerm(concrete[1])); + + Node abstractValue = m->getValue(abstract); + Node floatValue = m->getValue(concrete[0]); + Node undefValue = m->getValue(concrete[1]); + + Assert(abstractValue.isConst()); + Assert(floatValue.isConst()); + Assert(undefValue.isConst()); + + // Work out the actual value for those args + NodeManager *nm = NodeManager::currentNM(); + + Node evaluate = + nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL, floatValue, undefValue); + Node concreteValue = Rewriter::rewrite(evaluate); + Assert(concreteValue.isConst()); + + Trace("fp-refineAbstraction") + << "TheoryFp::refineAbstraction(): " << concrete[0] << " = " + << floatValue << std::endl + << "TheoryFp::refineAbstraction(): " << concrete[1] << " = " + << undefValue << std::endl + << "TheoryFp::refineAbstraction(): " << abstract << " = " + << abstractValue << std::endl + << "TheoryFp::refineAbstraction(): " << concrete << " = " + << concreteValue << std::endl; + + if (abstractValue != concreteValue) + { + // Need refinement lemmas + // only in the normal and subnormal case + Assert(floatValue.getConst<FloatingPoint>().isNormal() + || floatValue.getConst<FloatingPoint>().isSubnormal()); + + Node defined = nm->mkNode( + kind::AND, + nm->mkNode(kind::NOT, + nm->mkNode(kind::FLOATINGPOINT_ISNAN, concrete[0])), + nm->mkNode(kind::NOT, + nm->mkNode(kind::FLOATINGPOINT_ISINF, concrete[0]))); + // First the "forward" constraints + Node fg = nm->mkNode( + kind::IMPLIES, + defined, + nm->mkNode( + kind::EQUAL, + nm->mkNode(kind::FLOATINGPOINT_GEQ, concrete[0], floatValue), + nm->mkNode(kind::GEQ, abstract, concreteValue))); + handleLemma(fg); + + Node fl = nm->mkNode( + kind::IMPLIES, + defined, + nm->mkNode( + kind::EQUAL, + nm->mkNode(kind::FLOATINGPOINT_LEQ, concrete[0], floatValue), + nm->mkNode(kind::LEQ, abstract, concreteValue))); + handleLemma(fl); + + // Then the backwards constraints + Node floatAboveAbstract = Rewriter::rewrite( + nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, + nm->mkConst(FloatingPointToFPReal( + concrete[0].getType().getConst<FloatingPointSize>())), + nm->mkConst(roundTowardPositive), + abstractValue)); + + Node bg = nm->mkNode( + kind::IMPLIES, + defined, + nm->mkNode( + kind::EQUAL, + nm->mkNode( + kind::FLOATINGPOINT_GEQ, concrete[0], floatAboveAbstract), + nm->mkNode(kind::GEQ, abstract, abstractValue))); + handleLemma(bg); + + Node floatBelowAbstract = Rewriter::rewrite( + nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, + nm->mkConst(FloatingPointToFPReal( + concrete[0].getType().getConst<FloatingPointSize>())), + nm->mkConst(roundTowardNegative), + abstractValue)); + + Node bl = nm->mkNode( + kind::IMPLIES, + defined, + nm->mkNode( + kind::EQUAL, + nm->mkNode( + kind::FLOATINGPOINT_LEQ, concrete[0], floatBelowAbstract), + nm->mkNode(kind::LEQ, abstract, abstractValue))); + handleLemma(bl); + // TODO : see if the overflow conditions could be improved #1914 + + return true; + } + else + { + // No refinement needed + return false; + } + } + else if (k == kind::FLOATINGPOINT_TO_FP_REAL) + { + // Get the values + Assert(m->hasTerm(abstract)); + Assert(m->hasTerm(concrete[0])); + Assert(m->hasTerm(concrete[1])); + + Node abstractValue = m->getValue(abstract); + Node rmValue = m->getValue(concrete[0]); + Node realValue = m->getValue(concrete[1]); + + Assert(abstractValue.isConst()); + Assert(rmValue.isConst()); + Assert(realValue.isConst()); + + // Work out the actual value for those args + NodeManager *nm = NodeManager::currentNM(); + + Node evaluate = + nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, + nm->mkConst(FloatingPointToFPReal( + concrete.getType().getConst<FloatingPointSize>())), + rmValue, + realValue); + Node concreteValue = Rewriter::rewrite(evaluate); + Assert(concreteValue.isConst()); + + Trace("fp-refineAbstraction") + << "TheoryFp::refineAbstraction(): " << concrete[0] << " = " << rmValue + << std::endl + << "TheoryFp::refineAbstraction(): " << concrete[1] << " = " + << realValue << std::endl + << "TheoryFp::refineAbstraction(): " << abstract << " = " + << abstractValue << std::endl + << "TheoryFp::refineAbstraction(): " << concrete << " = " + << concreteValue << std::endl; + + if (abstractValue != concreteValue) + { + Assert(!abstractValue.getConst<FloatingPoint>().isNaN()); + Assert(!concreteValue.getConst<FloatingPoint>().isNaN()); + + Node correctRoundingMode = nm->mkNode(kind::EQUAL, concrete[0], rmValue); + // TODO : Generalise to all rounding modes #1914 + + // First the "forward" constraints + Node fg = nm->mkNode( + kind::IMPLIES, + correctRoundingMode, + nm->mkNode( + kind::EQUAL, + nm->mkNode(kind::GEQ, concrete[1], realValue), + nm->mkNode(kind::FLOATINGPOINT_GEQ, abstract, concreteValue))); + handleLemma(fg); + + Node fl = nm->mkNode( + kind::IMPLIES, + correctRoundingMode, + nm->mkNode( + kind::EQUAL, + nm->mkNode(kind::LEQ, concrete[1], realValue), + nm->mkNode(kind::FLOATINGPOINT_LEQ, abstract, concreteValue))); + handleLemma(fl); + + // Then the backwards constraints + if (!abstractValue.getConst<FloatingPoint>().isInfinite()) + { + Node realValueOfAbstract = + Rewriter::rewrite(nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL, + abstractValue, + nm->mkConst(Rational(0U)))); + + Node bg = nm->mkNode( + kind::IMPLIES, + correctRoundingMode, + nm->mkNode( + kind::EQUAL, + nm->mkNode(kind::GEQ, concrete[1], realValueOfAbstract), + nm->mkNode(kind::FLOATINGPOINT_GEQ, abstract, abstractValue))); + handleLemma(bg); + + Node bl = nm->mkNode( + kind::IMPLIES, + correctRoundingMode, + nm->mkNode( + kind::EQUAL, + nm->mkNode(kind::LEQ, concrete[1], realValueOfAbstract), + nm->mkNode(kind::FLOATINGPOINT_LEQ, abstract, abstractValue))); + handleLemma(bl); + } + + return true; + } + else + { + // No refinement needed + return false; + } + } + else + { + Unreachable("Unknown abstraction"); + } + + return false; +} + void TheoryFp::convertAndEquateTerm(TNode node) { Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl; size_t oldAdditionalAssertions = d_conv.d_additionalAssertions.size(); @@ -441,6 +821,52 @@ void TheoryFp::registerTerm(TNode node) { d_equalityEngine.addTerm(node); } + // Give the expansion of classifications in terms of equalities + // This should make equality reasoning slightly more powerful. + if ((node.getKind() == kind::FLOATINGPOINT_ISNAN) + || (node.getKind() == kind::FLOATINGPOINT_ISZ) + || (node.getKind() == kind::FLOATINGPOINT_ISINF)) + { + NodeManager *nm = NodeManager::currentNM(); + FloatingPointSize s = node[0].getType().getConst<FloatingPointSize>(); + Node equalityAlias = Node::null(); + + if (node.getKind() == kind::FLOATINGPOINT_ISNAN) + { + equalityAlias = nm->mkNode( + kind::EQUAL, node[0], nm->mkConst(FloatingPoint::makeNaN(s))); + } + else if (node.getKind() == kind::FLOATINGPOINT_ISZ) + { + equalityAlias = nm->mkNode( + kind::OR, + nm->mkNode(kind::EQUAL, + node[0], + nm->mkConst(FloatingPoint::makeZero(s, true))), + nm->mkNode(kind::EQUAL, + node[0], + nm->mkConst(FloatingPoint::makeZero(s, false)))); + } + else if (node.getKind() == kind::FLOATINGPOINT_ISINF) + { + equalityAlias = nm->mkNode( + kind::OR, + nm->mkNode(kind::EQUAL, + node[0], + nm->mkConst(FloatingPoint::makeInf(s, true))), + nm->mkNode(kind::EQUAL, + node[0], + nm->mkConst(FloatingPoint::makeInf(s, false)))); + } + else + { + Unreachable("Only isNaN, isInf and isZero have aliases"); + } + + handleLemma(nm->mkNode(kind::EQUAL, node, equalityAlias)); + } + + // Use symfpu to produce an equivalent bit-vector statement convertAndEquateTerm(node); } return; @@ -545,6 +971,25 @@ void TheoryFp::check(Effort level) { } } + // Resolve the abstractions for the conversion lemmas + // if (level == EFFORT_COMBINATION) { + if (level == EFFORT_LAST_CALL) + { + Trace("fp") << "TheoryFp::check(): checking abstractions" << std::endl; + TheoryModel *m = getValuation().getModel(); + bool lemmaAdded = false; + + for (abstractionMapType::const_iterator i = abstractionMap.begin(); + i != abstractionMap.end(); + ++i) + { + if (m->hasTerm((*i).first)) + { // Is actually used in the model + lemmaAdded |= refineAbstraction(m, (*i).first, (*i).second); + } + } + } + Trace("fp") << "TheoryFp::check(): completed" << std::endl; /* Checking should be handled by the bit-vector engine */ diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 688c6e600..6234ab8ad 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -43,8 +43,11 @@ class TheoryFp : public Theory { void preRegisterTerm(TNode node) override; void addSharedTerm(TNode node) override; + Node ppRewrite(TNode node); + void check(Effort) override; + bool needsCheckLastEffort() { return true; } Node getModelValue(TNode var) override; bool collectModelInfo(TheoryModel* m) override; @@ -100,6 +103,8 @@ class TheoryFp : public Theory { context::CDO<Node> d_conflictNode; /** Uninterpretted functions for partially defined functions. **/ + void enableUF(LogicRequest& lr); + typedef context::CDHashMap<TypeNode, Node, TypeNodeHashFunction> ComparisonUFMap; @@ -122,6 +127,21 @@ class TheoryFp : public Theory { ComparisonUFMap d_toRealMap; Node toRealUF(Node); + + /** Uninterpretted functions for lazy handling of conversions */ + typedef ComparisonUFMap conversionAbstractionMap; + + conversionAbstractionMap realToFloatMap; + conversionAbstractionMap floatToRealMap; + + Node abstractRealToFloat(Node); + Node abstractFloatToReal(Node); + + typedef context::CDHashMap<Node, Node, NodeHashFunction> abstractionMapType; + abstractionMapType abstractionMap; // abstract -> original + + bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete); + }; /* class TheoryFp */ } // namespace fp diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 9fda5c2f6..f502ad547 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -34,6 +34,7 @@ #include <algorithm> #include "base/cvc4_assert.h" +#include "theory/fp/fp_converter.h" #include "theory/fp/theory_fp_rewriter.h" namespace CVC4 { @@ -787,6 +788,118 @@ namespace constantFold { } } + RewriteResponse componentFlag(TNode node, bool) + { + Kind k = node.getKind(); + + Assert((k == kind::FLOATINGPOINT_COMPONENT_NAN) + || (k == kind::FLOATINGPOINT_COMPONENT_INF) + || (k == kind::FLOATINGPOINT_COMPONENT_ZERO) + || (k == kind::FLOATINGPOINT_COMPONENT_SIGN)); + + FloatingPoint arg0(node[0].getConst<FloatingPoint>()); + + bool result; + switch (k) + { +#ifdef CVC4_USE_SYMFPU + case kind::FLOATINGPOINT_COMPONENT_NAN: + result = arg0.getLiteral().nan; + break; + case kind::FLOATINGPOINT_COMPONENT_INF: + result = arg0.getLiteral().inf; + break; + case kind::FLOATINGPOINT_COMPONENT_ZERO: + result = arg0.getLiteral().zero; + break; + case kind::FLOATINGPOINT_COMPONENT_SIGN: + result = arg0.getLiteral().sign; + break; +#endif + default: Unreachable("Unknown kind used in componentFlag"); break; + } + + BitVector res(1U, (result) ? 1U : 0U); + + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(res)); + } + + RewriteResponse componentExponent(TNode node, bool) + { + Assert(node.getKind() == kind::FLOATINGPOINT_COMPONENT_EXPONENT); + + FloatingPoint arg0(node[0].getConst<FloatingPoint>()); + + // \todo Add a proper interface for this sort of thing to FloatingPoint #1915 + return RewriteResponse( + REWRITE_DONE, +#ifdef CVC4_USE_SYMFPU + NodeManager::currentNM()->mkConst((BitVector)arg0.getLiteral().exponent) +#else + node +#endif + ); + } + + RewriteResponse componentSignificand(TNode node, bool) + { + Assert(node.getKind() == kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND); + + FloatingPoint arg0(node[0].getConst<FloatingPoint>()); + + return RewriteResponse(REWRITE_DONE, +#ifdef CVC4_USE_SYMFPU + NodeManager::currentNM()->mkConst( + (BitVector)arg0.getLiteral().significand) +#else + node +#endif + ); + } + + RewriteResponse roundingModeBitBlast(TNode node, bool) + { + Assert(node.getKind() == kind::ROUNDINGMODE_BITBLAST); + + RoundingMode arg0(node[0].getConst<RoundingMode>()); + BitVector value; + +#ifdef CVC4_USE_SYMFPU + /* \todo fix the numbering of rounding modes so this doesn't need + * to call symfpu at all and remove the dependency on fp_converter.h #1915 */ + switch (arg0) + { + case roundNearestTiesToEven: + value = symfpuSymbolic::traits::RNE().getConst<BitVector>(); + break; + + case roundNearestTiesToAway: + value = symfpuSymbolic::traits::RNA().getConst<BitVector>(); + break; + + case roundTowardPositive: + value = symfpuSymbolic::traits::RTP().getConst<BitVector>(); + break; + + case roundTowardNegative: + value = symfpuSymbolic::traits::RTN().getConst<BitVector>(); + break; + + case roundTowardZero: + value = symfpuSymbolic::traits::RTZ().getConst<BitVector>(); + break; + + default: + Unreachable("Unknown rounding mode in roundingModeBitBlast"); + break; + } +#else + value = BitVector(5U, 0U); +#endif + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(value)); + } }; /* CVC4::theory::fp::constantFold */ @@ -871,6 +984,16 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND]; preRewriteTable[kind::EQUAL] = rewrite::equal; + /******** Components for bit-blasting ********/ + preRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] = rewrite::identity; + preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] = rewrite::identity; + preRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity; + + /* Set up the post-rewrite dispatch table */ @@ -943,6 +1066,15 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND]; postRewriteTable[kind::EQUAL] = rewrite::equal; + /******** Components for bit-blasting ********/ + postRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] = rewrite::identity; + postRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity; + /* Set up the post-rewrite constant fold table */ @@ -1017,6 +1149,15 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND]; constantFoldTable[kind::EQUAL] = constantFold::equal; + /******** Components for bit-blasting ********/ + constantFoldTable[kind::FLOATINGPOINT_COMPONENT_NAN] = constantFold::componentFlag; + constantFoldTable[kind::FLOATINGPOINT_COMPONENT_INF] = constantFold::componentFlag; + constantFoldTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = constantFold::componentFlag; + constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = constantFold::componentFlag; + constantFoldTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] = constantFold::componentExponent; + constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] = constantFold::componentSignificand; + constantFoldTable[kind::ROUNDINGMODE_BITBLAST] = constantFold::roundingModeBitBlast; + } @@ -1106,12 +1247,15 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND]; Node rn = res.node; // RewriteResponse is too functional.. if (apartFromRoundingMode) { - if (!(res.node.getKind() == kind::EQUAL)) { // Avoid infinite recursion... - // We are close to being able to constant fold this - // and in many cases the rounding mode really doesn't matter. - // So we can try brute forcing our way through them. - - NodeManager *nm = NodeManager::currentNM(); + if (!(res.node.getKind() == kind::EQUAL) + && // Avoid infinite recursion... + !(res.node.getKind() == kind::ROUNDINGMODE_BITBLAST)) + { // Don't eliminate the bit-blast + // We are close to being able to constant fold this + // and in many cases the rounding mode really doesn't matter. + // So we can try brute forcing our way through them. + + NodeManager *nm = NodeManager::currentNM(); Node RNE(nm->mkConst(roundNearestTiesToEven)); Node RNA(nm->mkConst(roundNearestTiesToAway)); diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index 2f7dd2e01..9589715d2 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -17,6 +17,9 @@ #include "cvc4_private.h" +// This is only needed for checking that components are only applied to leaves. +#include "theory/theory.h" + #ifndef __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H #define __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H @@ -612,6 +615,167 @@ class FloatingPointToRealTotalTypeRule { } }; +class FloatingPointComponentBit +{ + public: + inline static TypeNode computeType( + NodeManager* nodeManager, + TNode n, + bool check) throw(TypeCheckingExceptionPrivate, AssertionException) + { + TRACE("FloatingPointComponentBit"); + + if (check) + { + TypeNode operandType = n[0].getType(check); + + if (!operandType.isFloatingPoint()) + { + throw TypeCheckingExceptionPrivate(n, + "floating-point bit component " + "applied to a non floating-point " + "sort"); + } + if (!(Theory::isLeafOf(n[0], THEORY_FP) + || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) + { + throw TypeCheckingExceptionPrivate(n, + "floating-point bit component " + "applied to a non leaf / to_fp leaf " + "node"); + } + } + + return nodeManager->mkBitVectorType(1); + } +}; + +class FloatingPointComponentExponent +{ + public: + inline static TypeNode computeType( + NodeManager* nodeManager, + TNode n, + bool check) throw(TypeCheckingExceptionPrivate, AssertionException) + { + TRACE("FloatingPointComponentExponent"); + + TypeNode operandType = n[0].getType(check); + + if (check) + { + if (!operandType.isFloatingPoint()) + { + throw TypeCheckingExceptionPrivate(n, + "floating-point exponent component " + "applied to a non floating-point " + "sort"); + } + if (!(Theory::isLeafOf(n[0], THEORY_FP) + || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) + { + throw TypeCheckingExceptionPrivate(n, + "floating-point exponent component " + "applied to a non leaf / to_fp " + "node"); + } + } + +#ifdef CVC4_USE_SYMFPU + /* Need to create some symfpu objects as the size of bit-vector + * that is needed for this component is dependent on the encoding + * used (i.e. whether subnormals are forcibly normalised or not). + * Here we use types from floatingpoint.h which are the literal + * back-end but it should't make a difference. */ + FloatingPointSize fps = operandType.getConst<FloatingPointSize>(); + symfpuLiteral::fpt format(fps); // The symfpu interface to type info + unsigned bw = FloatingPointLiteral::exponentWidth(format); +#else + unsigned bw = 2; +#endif + + return nodeManager->mkBitVectorType(bw); + } +}; + +class FloatingPointComponentSignificand +{ + public: + inline static TypeNode computeType( + NodeManager* nodeManager, + TNode n, + bool check) throw(TypeCheckingExceptionPrivate, AssertionException) + { + TRACE("FloatingPointComponentSignificand"); + + TypeNode operandType = n[0].getType(check); + + if (check) + { + if (!operandType.isFloatingPoint()) + { + throw TypeCheckingExceptionPrivate(n, + "floating-point significand " + "component applied to a non " + "floating-point sort"); + } + if (!(Theory::isLeafOf(n[0], THEORY_FP) + || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) + { + throw TypeCheckingExceptionPrivate(n, + "floating-point significand " + "component applied to a non leaf / " + "to_fp node"); + } + } + +#ifdef CVC4_USE_SYMFPU + /* As before we need to use some of sympfu. */ + FloatingPointSize fps = operandType.getConst<FloatingPointSize>(); + symfpuLiteral::fpt format(fps); + unsigned bw = FloatingPointLiteral::significandWidth(format); +#else + unsigned bw = 1; +#endif + + return nodeManager->mkBitVectorType(bw); + } +}; + +class RoundingModeBitBlast +{ + public: + inline static TypeNode computeType( + NodeManager* nodeManager, + TNode n, + bool check) throw(TypeCheckingExceptionPrivate, AssertionException) + { + TRACE("RoundingModeBitBlast"); + + if (check) + { + TypeNode operandType = n[0].getType(check); + + if (!operandType.isRoundingMode()) + { + throw TypeCheckingExceptionPrivate( + n, "rounding mode bit-blast applied to a non rounding-mode sort"); + } + if (!Theory::isLeafOf(n[0], THEORY_FP)) + { + throw TypeCheckingExceptionPrivate( + n, "rounding mode bit-blast applied to a non leaf node"); + } + } + +#ifdef CVC4_USE_SYMFPU + /* Uses sympfu for the macro. */ + return nodeManager->mkBitVectorType(SYMFPU_NUMBER_OF_ROUNDING_MODES); +#else + return nodeManager->mkBitVectorType(5); +#endif + } +}; class CardinalityComputer { public: diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 41d74b4a0..1c9e3d0ef 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -487,6 +487,16 @@ void LogicInfo::setLogicString(std::string logicString) } } } + + if (d_theories[THEORY_FP]) + { + // THEORY_BV is needed for bit-blasting. + // We have to set this here rather than in expandDefinition as it + // is possible to create variables without any theory specific + // operations, so expandDefinition won't be called. + enableTheory(THEORY_BV); + } + if(*p != '\0') { stringstream err; err << "LogicInfo::setLogicString(): "; diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index fe90279ec..74e6189ed 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -15,8 +15,55 @@ **/ #include "util/floatingpoint.h" - #include "base/cvc4_assert.h" +#include "util/integer.h" + +#include <math.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::prop, T> \ + { \ + static const T &iteOp(const ::CVC4::symfpuLiteral::prop &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 + +#ifndef CVC4_USE_SYMFPU +#define PRECONDITION(X) Assert((X)) +#endif namespace CVC4 { @@ -32,22 +79,428 @@ FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), PrettyCheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s); } -void FloatingPointLiteral::unfinished (void) const { - Unimplemented("Floating-point literals not yet implemented."); +namespace symfpuLiteral { + +// To simplify the property macros +typedef traits t; + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one(const bwt &w) +{ + return wrappedBitVector<isSigned>(w, 1); } - FloatingPoint::FloatingPoint (unsigned e, unsigned s, const BitVector &bv) : - fpl(e,s,0.0), - t(e,s) {} +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero(const bwt &w) +{ + return wrappedBitVector<isSigned>(w, 0); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes(const bwt &w) +{ + return ~wrappedBitVector<isSigned>::zero(w); +} +template <bool isSigned> +prop wrappedBitVector<isSigned>::isAllOnes() const +{ + return (*this == wrappedBitVector<isSigned>::allOnes(this->getWidth())); +} +template <bool isSigned> +prop wrappedBitVector<isSigned>::isAllZeros() const +{ + return (*this == wrappedBitVector<isSigned>::zero(this->getWidth())); +} - static FloatingPointLiteral constructorHelperBitVector (const FloatingPointSize &ct, const RoundingMode &rm, const BitVector &bv, bool signedBV) { - if (signedBV) { - return FloatingPointLiteral(2,2,0.0); - } else { - return FloatingPointLiteral(2,2,0.0); - } - Unreachable("Constructor helper broken"); +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue(const bwt &w) +{ + if (isSigned) + { + BitVector base(w - 1, 0U); + return wrappedBitVector<true>((~base).zeroExtend(1)); + } + else + { + return wrappedBitVector<false>::allOnes(w); + } +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::minValue(const bwt &w) +{ + if (isSigned) + { + BitVector base(w, 1U); + BitVector shiftAmount(w, w - 1); + BitVector result(base.leftShift(shiftAmount)); + return wrappedBitVector<true>(result); + } + else + { + return wrappedBitVector<false>::zero(w); + } +} + +/*** Operators ***/ +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator<<( + const wrappedBitVector<isSigned> &op) const +{ + return this->BitVector::leftShift(op); +} + +template <> +wrappedBitVector<true> wrappedBitVector<true>::operator>>( + const wrappedBitVector<true> &op) const +{ + return this->BitVector::arithRightShift(op); +} + +template <> +wrappedBitVector<false> wrappedBitVector<false>::operator>>( + const wrappedBitVector<false> &op) const +{ + return this->BitVector::logicalRightShift(op); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|( + const wrappedBitVector<isSigned> &op) const +{ + return this->BitVector::operator|(op); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&( + const wrappedBitVector<isSigned> &op) const +{ + return this->BitVector::operator&(op); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+( + const wrappedBitVector<isSigned> &op) const +{ + return this->BitVector::operator+(op); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-( + const wrappedBitVector<isSigned> &op) const +{ + return this->BitVector::operator-(op); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*( + const wrappedBitVector<isSigned> &op) const +{ + return this->BitVector::operator*(op); +} + +template <> +wrappedBitVector<false> wrappedBitVector<false>::operator/( + const wrappedBitVector<false> &op) const +{ + return this->BitVector::unsignedDivTotal(op); +} + +template <> +wrappedBitVector<false> wrappedBitVector<false>::operator%( + const wrappedBitVector<false> &op) const +{ + return this->BitVector::unsignedRemTotal(op); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const +{ + return this->BitVector::operator-(); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void)const +{ + return this->BitVector::operator~(); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::increment() const +{ + return *this + wrappedBitVector<isSigned>::one(this->getWidth()); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const +{ + return *this - wrappedBitVector<isSigned>::one(this->getWidth()); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift( + const wrappedBitVector<isSigned> &op) const +{ + return this->BitVector::arithRightShift(BitVector(this->getWidth(), op)); +} + +/*** Modular opertaions ***/ +// No overflow checking so these are the same as other operations +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularLeftShift( + const wrappedBitVector<isSigned> &op) const +{ + return *this << op; +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularRightShift( + const wrappedBitVector<isSigned> &op) const +{ + return *this >> op; +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularIncrement() const +{ + return this->increment(); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const +{ + return this->decrement(); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularAdd( + const wrappedBitVector<isSigned> &op) const +{ + return *this + op; +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularNegate() const +{ + return -(*this); +} + +/*** Comparisons ***/ + +template <bool isSigned> +prop wrappedBitVector<isSigned>::operator==( + const wrappedBitVector<isSigned> &op) const +{ + return this->BitVector::operator==(op); +} + +template <> +prop wrappedBitVector<true>::operator<=(const wrappedBitVector<true> &op) const +{ + return this->signedLessThanEq(op); +} + +template <> +prop wrappedBitVector<true>::operator>=(const wrappedBitVector<true> &op) const +{ + return !(this->signedLessThan(op)); +} + +template <> +prop wrappedBitVector<true>::operator<(const wrappedBitVector<true> &op) const +{ + return this->signedLessThan(op); +} + +template <> +prop wrappedBitVector<true>::operator>(const wrappedBitVector<true> &op) const +{ + return !(this->signedLessThanEq(op)); +} + +template <> +prop wrappedBitVector<false>::operator<=( + const wrappedBitVector<false> &op) const +{ + return this->unsignedLessThanEq(op); +} + +template <> +prop wrappedBitVector<false>::operator>=( + const wrappedBitVector<false> &op) const +{ + return !(this->unsignedLessThan(op)); +} + +template <> +prop wrappedBitVector<false>::operator<(const wrappedBitVector<false> &op) const +{ + return this->unsignedLessThan(op); +} + +template <> +prop wrappedBitVector<false>::operator>(const wrappedBitVector<false> &op) const +{ + return !(this->unsignedLessThanEq(op)); +} + +/*** Type conversion ***/ +// CVC4 nodes make no distinction between signed and unsigned, thus ... +template <bool isSigned> +wrappedBitVector<true> wrappedBitVector<isSigned>::toSigned(void) const +{ + return wrappedBitVector<true>(*this); +} + +template <bool isSigned> +wrappedBitVector<false> wrappedBitVector<isSigned>::toUnsigned(void) const +{ + return wrappedBitVector<false>(*this); +} + +/*** Bit hacks ***/ + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend( + bwt extension) const +{ + if (isSigned) + { + return this->BitVector::signExtend(extension); + } + else + { + return this->BitVector::zeroExtend(extension); + } +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract( + bwt reduction) const +{ + PRECONDITION(this->getWidth() > reduction); + + return this->extract((this->getWidth() - 1) - reduction, 0); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<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> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth( + const wrappedBitVector<isSigned> &op) const +{ + PRECONDITION(this->getWidth() <= op.getWidth()); + return this->extend(op.getWidth() - this->getWidth()); +} + +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append( + const wrappedBitVector<isSigned> &op) const +{ + return this->BitVector::concat(op); +} + +// Inclusive of end points, thus if the same, extracts just one bit +template <bool isSigned> +wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(bwt upper, + bwt lower) const +{ + PRECONDITION(upper >= lower); + return this->BitVector::extract(upper, lower); +} + +// Explicit instantiation +template class wrappedBitVector<true>; +template class wrappedBitVector<false>; + +rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; }; +rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; }; +rm traits::RTP(void) { return ::CVC4::roundTowardPositive; }; +rm traits::RTN(void) { return ::CVC4::roundTowardNegative; }; +rm traits::RTZ(void) { return ::CVC4::roundTowardZero; }; +// This is a literal back-end so props are actually bools +// so these can be handled in the same way as the internal assertions above + +void traits::precondition(const prop &p) +{ + Assert(p); + return; +} +void traits::postcondition(const prop &p) +{ + Assert(p); + return; +} +void traits::invariant(const prop &p) +{ + Assert(p); + return; +} +} + +#ifndef CVC4_USE_SYMFPU +void FloatingPointLiteral::unfinished(void) const +{ + Unimplemented("Floating-point literals not yet implemented."); +} +#endif + +FloatingPoint::FloatingPoint(unsigned e, unsigned s, const BitVector &bv) + : +#ifdef CVC4_USE_SYMFPU + fpl(symfpu::unpack<symfpuLiteral::traits>(symfpuLiteral::fpt(e, s), bv)), +#else + fpl(e, s, 0.0), +#endif + t(e, s) +{ +} + +static FloatingPointLiteral constructorHelperBitVector( + const FloatingPointSize &ct, + const RoundingMode &rm, + const BitVector &bv, + bool signedBV) +{ +#ifdef CVC4_USE_SYMFPU + if (signedBV) + { + return FloatingPointLiteral( + symfpu::convertSBVToFloat<symfpuLiteral::traits>( + symfpuLiteral::fpt(ct), + symfpuLiteral::rm(rm), + symfpuLiteral::sbv(bv))); + } + else + { + return FloatingPointLiteral( + symfpu::convertUBVToFloat<symfpuLiteral::traits>( + symfpuLiteral::fpt(ct), + symfpuLiteral::rm(rm), + symfpuLiteral::ubv(bv))); + } +#else + return FloatingPointLiteral(2, 2, 0.0); +#endif + Unreachable("Constructor helper broken"); } FloatingPoint::FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const BitVector &bv, bool signedBV) : @@ -60,9 +513,16 @@ void FloatingPointLiteral::unfinished (void) const { Rational two(2,1); if (r.isZero()) { +#ifdef CVC4_USE_SYMFPU + return FloatingPointLiteral::makeZero( + ct, false); // In keeping with the SMT-LIB standard +#else return FloatingPointLiteral(2,2,0.0); +#endif } else { - //int negative = (r.sgn() < 0) ? 1 : 0; +#ifdef CVC4_USE_SYMFPU + int negative = (r.sgn() < 0) ? 1 : 0; +#endif r = r.abs(); // Compute the exponent @@ -114,7 +574,7 @@ void FloatingPointLiteral::unfinished (void) const { // Compute the significand. - unsigned sigBits = ct.significand() + 2; // guard and sticky bits + unsigned sigBits = ct.significandWidth() + 2; // guard and sticky bits BitVector sig(sigBits, 0U); BitVector one(sigBits, 1U); Rational workingSig(0,1); @@ -144,7 +604,20 @@ void FloatingPointLiteral::unfinished (void) const { // 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 + unsigned extension = + FloatingPointLiteral::exponentWidth(exactFormat) - expBits; + + FloatingPointLiteral exactFloat( + negative, exactExp.signExtend(extension), sig); + + // Then cast... + FloatingPointLiteral rounded( + symfpu::convertFloatToFloat(exactFormat, ct, rm, exactFloat)); + return rounded; +#else Unreachable("no concrete implementation of FloatingPointLiteral"); +#endif } Unreachable("Constructor helper broken"); } @@ -155,74 +628,146 @@ void FloatingPointLiteral::unfinished (void) const { FloatingPoint FloatingPoint::makeNaN (const FloatingPointSize &t) { +#ifdef CVC4_USE_SYMFPU + return FloatingPoint( + t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeNaN(t)); +#else return FloatingPoint(2, 2, BitVector(4U,0U)); +#endif } FloatingPoint FloatingPoint::makeInf (const FloatingPointSize &t, bool sign) { +#ifdef CVC4_USE_SYMFPU + return FloatingPoint( + t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeInf(t, sign)); +#else return FloatingPoint(2, 2, BitVector(4U,0U)); +#endif } FloatingPoint FloatingPoint::makeZero (const FloatingPointSize &t, bool sign) { +#ifdef CVC4_USE_SYMFPU + return FloatingPoint( + t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeZero(t, sign)); +#else return FloatingPoint(2, 2, BitVector(4U,0U)); +#endif } /* Operations implemented using symfpu */ FloatingPoint FloatingPoint::absolute (void) const { +#ifdef CVC4_USE_SYMFPU + return FloatingPoint(t, symfpu::absolute<symfpuLiteral::traits>(t, fpl)); +#else return *this; +#endif } FloatingPoint FloatingPoint::negate (void) const { +#ifdef CVC4_USE_SYMFPU + return FloatingPoint(t, symfpu::negate<symfpuLiteral::traits>(t, fpl)); +#else return *this; +#endif } FloatingPoint FloatingPoint::plus (const RoundingMode &rm, const FloatingPoint &arg) const { +#ifdef CVC4_USE_SYMFPU Assert(this->t == arg.t); + return FloatingPoint( + t, symfpu::add<symfpuLiteral::traits>(t, rm, fpl, arg.fpl, true)); +#else return *this; +#endif } FloatingPoint FloatingPoint::sub (const RoundingMode &rm, const FloatingPoint &arg) const { +#ifdef CVC4_USE_SYMFPU Assert(this->t == arg.t); + return FloatingPoint( + t, symfpu::add<symfpuLiteral::traits>(t, rm, fpl, arg.fpl, false)); +#else return *this; +#endif } FloatingPoint FloatingPoint::mult (const RoundingMode &rm, const FloatingPoint &arg) const { +#ifdef CVC4_USE_SYMFPU Assert(this->t == arg.t); + return FloatingPoint( + t, symfpu::multiply<symfpuLiteral::traits>(t, rm, fpl, arg.fpl)); +#else return *this; +#endif } FloatingPoint FloatingPoint::fma (const RoundingMode &rm, const FloatingPoint &arg1, const FloatingPoint &arg2) const { +#ifdef CVC4_USE_SYMFPU Assert(this->t == arg1.t); Assert(this->t == arg2.t); + return FloatingPoint( + t, symfpu::fma<symfpuLiteral::traits>(t, rm, fpl, arg1.fpl, arg2.fpl)); +#else return *this; +#endif } FloatingPoint FloatingPoint::div (const RoundingMode &rm, const FloatingPoint &arg) const { +#ifdef CVC4_USE_SYMFPU Assert(this->t == arg.t); + return FloatingPoint( + t, symfpu::divide<symfpuLiteral::traits>(t, rm, fpl, arg.fpl)); +#else return *this; +#endif } FloatingPoint FloatingPoint::sqrt (const RoundingMode &rm) const { +#ifdef CVC4_USE_SYMFPU + return FloatingPoint(t, symfpu::sqrt<symfpuLiteral::traits>(t, rm, fpl)); +#else return *this; +#endif } FloatingPoint FloatingPoint::rti (const RoundingMode &rm) const { +#ifdef CVC4_USE_SYMFPU + return FloatingPoint( + t, symfpu::roundToIntegral<symfpuLiteral::traits>(t, rm, fpl)); +#else return *this; +#endif } FloatingPoint FloatingPoint::rem (const FloatingPoint &arg) const { +#ifdef CVC4_USE_SYMFPU Assert(this->t == arg.t); + return FloatingPoint( + t, symfpu::remainder<symfpuLiteral::traits>(t, fpl, arg.fpl)); +#else return *this; +#endif } FloatingPoint FloatingPoint::maxTotal (const FloatingPoint &arg, bool zeroCaseLeft) const { +#ifdef CVC4_USE_SYMFPU Assert(this->t == arg.t); + return FloatingPoint( + t, symfpu::max<symfpuLiteral::traits>(t, fpl, arg.fpl, zeroCaseLeft)); +#else return *this; +#endif } FloatingPoint FloatingPoint::minTotal (const FloatingPoint &arg, bool zeroCaseLeft) const { +#ifdef CVC4_USE_SYMFPU Assert(this->t == arg.t); + return FloatingPoint( + t, symfpu::min<symfpuLiteral::traits>(t, fpl, arg.fpl, zeroCaseLeft)); +#else return *this; +#endif } FloatingPoint::PartialFloatingPoint FloatingPoint::max (const FloatingPoint &arg) const { @@ -236,56 +781,109 @@ void FloatingPointLiteral::unfinished (void) const { } bool FloatingPoint::operator ==(const FloatingPoint& fp) const { +#ifdef CVC4_USE_SYMFPU + return ((t == fp.t) + && symfpu::smtlibEqual<symfpuLiteral::traits>(t, fpl, fp.fpl)); +#else return ( (t == fp.t) ); +#endif } bool FloatingPoint::operator <= (const FloatingPoint &arg) const { +#ifdef CVC4_USE_SYMFPU Assert(this->t == arg.t); + return symfpu::lessThanOrEqual<symfpuLiteral::traits>(t, fpl, arg.fpl); +#else return false; +#endif } bool FloatingPoint::operator < (const FloatingPoint &arg) const { +#ifdef CVC4_USE_SYMFPU Assert(this->t == arg.t); + return symfpu::lessThan<symfpuLiteral::traits>(t, fpl, arg.fpl); +#else return false; +#endif } bool FloatingPoint::isNormal (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isNormal<symfpuLiteral::traits>(t, fpl); +#else return false; +#endif } bool FloatingPoint::isSubnormal (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isSubnormal<symfpuLiteral::traits>(t, fpl); +#else return false; +#endif } bool FloatingPoint::isZero (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isZero<symfpuLiteral::traits>(t, fpl); +#else return false; +#endif } bool FloatingPoint::isInfinite (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isInfinite<symfpuLiteral::traits>(t, fpl); +#else return false; +#endif } bool FloatingPoint::isNaN (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isNaN<symfpuLiteral::traits>(t, fpl); +#else return false; +#endif } bool FloatingPoint::isNegative (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isNegative<symfpuLiteral::traits>(t, fpl); +#else return false; +#endif } bool FloatingPoint::isPositive (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isPositive<symfpuLiteral::traits>(t, fpl); +#else return false; +#endif } FloatingPoint FloatingPoint::convert (const FloatingPointSize &target, const RoundingMode &rm) const { +#ifdef CVC4_USE_SYMFPU + return FloatingPoint( + target, + symfpu::convertFloatToFloat<symfpuLiteral::traits>(t, target, rm, fpl)); +#else return *this; +#endif } BitVector FloatingPoint::convertToBVTotal (BitVectorSize width, const RoundingMode &rm, bool signedBV, BitVector undefinedCase) const { +#ifdef CVC4_USE_SYMFPU if (signedBV) - return undefinedCase; + return symfpu::convertFloatToSBV<symfpuLiteral::traits>( + t, rm, fpl, width, undefinedCase); else - return undefinedCase; + return symfpu::convertFloatToUBV<symfpuLiteral::traits>( + t, rm, fpl, width, undefinedCase); +#else + return undefinedCase; +#endif } Rational FloatingPoint::convertToRationalTotal (Rational undefinedCase) const { @@ -309,10 +907,18 @@ void FloatingPointLiteral::unfinished (void) const { return PartialRational(Rational(0U, 1U), true); } else { - +#ifdef CVC4_USE_SYMFPU + Integer sign((this->fpl.getSign()) ? -1 : 1); + Integer exp( + this->fpl.getExponent().toSignedInteger() + - (Integer(t.significand() + - 1))); // -1 as forcibly normalised into the [1,2) range + Integer significand(this->fpl.getSignificand().toInteger()); +#else Integer sign(0); Integer exp(0); Integer significand(0); +#endif Integer signedSignificand(sign * significand); // Only have pow(uint32_t) so we should check this. @@ -333,7 +939,11 @@ void FloatingPointLiteral::unfinished (void) const { } BitVector FloatingPoint::pack (void) const { +#ifdef CVC4_USE_SYMFPU + BitVector bv(symfpu::pack<symfpuLiteral::traits>(this->t, this->fpl)); +#else BitVector bv(4u,0u); +#endif return bv; } diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index fa4573123..95bec903e 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -20,11 +20,15 @@ #ifndef __CVC4__FLOATINGPOINT_H #define __CVC4__FLOATINGPOINT_H -#include <fenv.h> - #include "util/bitvector.h" #include "util/rational.h" +#include <fenv.h> + +#ifdef CVC4_USE_SYMFPU +#include "symfpu/core/unpackedFloat.h" +#endif + namespace CVC4 { // Inline these! inline bool CVC4_PUBLIC validExponentSize (unsigned e) { return e >= 2; } @@ -62,6 +66,22 @@ namespace CVC4 { return (e == fps.e) && (s == fps.s); } + // Implement the interface that symfpu uses for floating-point formats. + inline unsigned exponentWidth(void) const { return this->exponent(); } + inline unsigned significandWidth(void) const { return this->significand(); } + inline unsigned packedWidth(void) const + { + return this->exponentWidth() + this->significandWidth(); + } + inline unsigned packedExponentWidth(void) const + { + return this->exponentWidth(); + } + inline unsigned packedSignificandWidth(void) const + { + return this->significandWidth() - 1; + } + }; /* class FloatingPointSize */ struct CVC4_PUBLIC FloatingPointSizeHashFunction { @@ -95,11 +115,181 @@ namespace CVC4 { } }; /* struct RoundingModeHashFunction */ + /** + * This is a symfpu literal "back-end". It allows the library to be used as + * an arbitrary precision floating-point implementation. This is effectively + * the glue between symfpu's notion of "signed bit-vector" and CVC4's + * BitVector. + */ + namespace symfpuLiteral { + // Forward declaration of wrapper so that traits can be defined early and so + // used in the implementation of wrappedBitVector. + template <bool T> + class wrappedBitVector; + + // This is the template parameter for symfpu's templates. + class traits + { + public: + // The six key types that symfpu uses. + typedef unsigned bwt; + typedef bool prop; + typedef ::CVC4::RoundingMode rm; + typedef ::CVC4::FloatingPointSize fpt; + typedef wrappedBitVector<true> sbv; + typedef wrappedBitVector<false> ubv; + + // Give concrete instances of each rounding mode, mainly for comparisons. + static rm RNE(void); + static rm RNA(void); + static rm RTP(void); + static rm RTN(void); + static rm RTZ(void); + + // The sympfu properties. + static void precondition(const prop &p); + static void postcondition(const prop &p); + static void invariant(const prop &p); + }; + + // Use the same type names as symfpu. + typedef traits::bwt bwt; + typedef traits::prop prop; + typedef traits::rm rm; + typedef traits::fpt fpt; + typedef traits::ubv ubv; + typedef traits::sbv sbv; + + // Type function for mapping between types + template <bool T> + struct signedToLiteralType; + + template <> + struct signedToLiteralType<true> + { + typedef int literalType; + }; + template <> + struct signedToLiteralType<false> + { + typedef unsigned int literalType; + }; + + // This is an additional interface for CVC4::BitVector. + // The template parameter distinguishes signed and unsigned bit-vectors, a + // distinction symfpu uses. + template <bool isSigned> + class wrappedBitVector : public BitVector + { + protected: + typedef typename signedToLiteralType<isSigned>::literalType literalType; + + friend wrappedBitVector<!isSigned>; // To allow conversion between the + // types +#ifdef CVC4_USE_SYMFPU + friend ::symfpu::ite<prop, wrappedBitVector<isSigned> >; // For ITE +#endif + + public: + wrappedBitVector(const bwt w, const unsigned v) : BitVector(w, v) {} + wrappedBitVector(const prop &p) : BitVector(1, p ? 1U : 0U) {} + wrappedBitVector(const wrappedBitVector<isSigned> &old) : BitVector(old) {} + wrappedBitVector(const BitVector &old) : BitVector(old) {} + bwt getWidth(void) const { return getSize(); } + /*** Constant creation and test ***/ + + static wrappedBitVector<isSigned> one(const bwt &w); + static wrappedBitVector<isSigned> zero(const bwt &w); + static wrappedBitVector<isSigned> allOnes(const bwt &w); + + prop isAllOnes() const; + prop isAllZeros() const; + + static wrappedBitVector<isSigned> maxValue(const bwt &w); + static wrappedBitVector<isSigned> minValue(const bwt &w); + + /*** Operators ***/ + wrappedBitVector<isSigned> operator<<( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator>>( + const wrappedBitVector<isSigned> &op) const; + + /* Inherited but ... + * *sigh* if we use the inherited version then it will return a + * CVC4::BitVector which can be converted back to a + * wrappedBitVector<isSigned> but isn't done automatically when working + * out types for templates instantiation. ITE is a particular + * problem as expressions and constants no longer derive the + * same type. There aren't any good solutions in C++, we could + * use CRTP but Liana wouldn't appreciate that, so the following + * pointless wrapping functions are needed. + */ + wrappedBitVector<isSigned> operator|( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator&( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator+( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator-( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator*( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator/( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator%( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator-(void) const; + wrappedBitVector<isSigned> operator~(void)const; + + wrappedBitVector<isSigned> increment() const; + wrappedBitVector<isSigned> decrement() const; + wrappedBitVector<isSigned> signExtendRightShift( + const wrappedBitVector<isSigned> &op) const; + + /*** Modular opertaions ***/ + // No overflow checking so these are the same as other operations + wrappedBitVector<isSigned> modularLeftShift( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> modularRightShift( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> modularIncrement() const; + wrappedBitVector<isSigned> modularDecrement() const; + wrappedBitVector<isSigned> modularAdd( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> modularNegate() const; + + /*** Comparisons ***/ + // Inherited ... ish ... + prop operator==(const wrappedBitVector<isSigned> &op) const; + prop operator<=(const wrappedBitVector<isSigned> &op) const; + prop operator>=(const wrappedBitVector<isSigned> &op) const; + prop operator<(const wrappedBitVector<isSigned> &op) const; + prop operator>(const wrappedBitVector<isSigned> &op) const; + + /*** Type conversion ***/ + wrappedBitVector<true> toSigned(void) const; + wrappedBitVector<false> toUnsigned(void) const; + + /*** Bit hacks ***/ + wrappedBitVector<isSigned> extend(bwt extension) const; + wrappedBitVector<isSigned> contract(bwt reduction) const; + wrappedBitVector<isSigned> resize(bwt newSize) const; + wrappedBitVector<isSigned> matchWidth( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> append( + const wrappedBitVector<isSigned> &op) const; + + // Inclusive of end points, thus if the same, extracts just one bit + wrappedBitVector<isSigned> extract(bwt upper, bwt lower) const; + }; + } /** * A concrete floating point number */ - +#ifdef CVC4_USE_SYMFPU + typedef ::symfpu::unpackedFloat<symfpuLiteral::traits> FloatingPointLiteral; +#else class CVC4_PUBLIC FloatingPointLiteral { public : // This intentional left unfinished as the choice of literal @@ -109,7 +299,6 @@ namespace CVC4 { FloatingPointLiteral(unsigned, unsigned, double) { unfinished(); } FloatingPointLiteral(unsigned, unsigned, const std::string &) { unfinished(); } FloatingPointLiteral(const FloatingPointLiteral &) { unfinished(); } - bool operator == (const FloatingPointLiteral &op) const { unfinished(); return false; @@ -120,6 +309,7 @@ namespace CVC4 { return 23; } }; +#endif class CVC4_PUBLIC FloatingPoint { protected : |