From 4e96b1d5e01260acc79bdbb86322e23c7cf9567f Mon Sep 17 00:00:00 2001 From: Martin Date: Tue, 15 May 2018 00:18:31 +0100 Subject: [PATCH] Floating point theory solver based on SymFPU (#1895) * Add some symfpu accessor functions to reduce the size of the literal 'back-end'. * Enable the bit-vector theory when setting the logic, not in expandDefinition. This is needed because it is possible to add variables of float or rounding mode sort but not use any theory specific functions or predicates and thus not enable the bit-vector theory. * Use symfpu to implement the literal floating-point objects. * Add kinds for bit-blasted components. * Print the new kinds. * Typing rules for the new kinds. * Constant folding for the component kinds. * Add support for components to the theory solver. * Add explicit equivalences between classification functions and equalities. * Use symfpu to do symbolic conversions of floating-point operations. * Implement conversions via (over-)approximation and refinement. * Correct a copy and paste error in the generation of uninterpretted functions for conversions. --- src/printer/smt2/smt2_printer.cpp | 16 + src/theory/fp/fp_converter.cpp | 1712 +++++++++++++++++++++++++- src/theory/fp/fp_converter.h | 305 ++++- src/theory/fp/kinds | 24 + src/theory/fp/theory_fp.cpp | 467 ++++++- src/theory/fp/theory_fp.h | 20 + src/theory/fp/theory_fp_rewriter.cpp | 156 ++- src/theory/fp/theory_fp_type_rules.h | 164 +++ src/theory/logic_info.cpp | 10 + src/util/floatingpoint.cpp | 646 +++++++++- 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 +#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 \ + { \ + 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(const traits::ubv &b) +{ + return orderEncodeBitwise(b); +} + +template <> +stickyRightShiftResult stickyRightShift(const traits::ubv &input, + const traits::ubv &shiftAmount) +{ + return stickyRightShiftBitwise(input, shiftAmount); +} + +template <> +void probabilityAnnotation(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 +Node symbolicBitVector::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 +Node symbolicBitVector::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 +Node symbolicBitVector::fromProposition(Node node) const +{ + return node; +} +template +Node symbolicBitVector::toProposition(Node node) const +{ + return boolNodeToBV(node); +} + +template +symbolicBitVector::symbolicBitVector(const Node n) : nodeWrapper(n) +{ + PRECONDITION(checkNodeType(*this)); +} + +template +bool symbolicBitVector::checkNodeType(const TNode n) +{ + return n.getType(false).isBitVector(); +} + +template +symbolicBitVector::symbolicBitVector(const bwt w, const unsigned v) + : nodeWrapper(NodeManager::currentNM()->mkConst(BitVector(w, v))) +{ + PRECONDITION(checkNodeType(*this)); +} +template +symbolicBitVector::symbolicBitVector(const symbolicProposition &p) + : nodeWrapper(fromProposition(p)) +{ +} +template +symbolicBitVector::symbolicBitVector( + const symbolicBitVector &old) + : nodeWrapper(old) +{ + PRECONDITION(checkNodeType(*this)); +} +template +symbolicBitVector::symbolicBitVector(const BitVector &old) + : nodeWrapper(NodeManager::currentNM()->mkConst(old)) +{ + PRECONDITION(checkNodeType(*this)); +} + +template +bwt symbolicBitVector::getWidth(void) const +{ + return this->getType(false).getBitVectorSize(); +} + +/*** Constant creation and test ***/ +template +symbolicBitVector symbolicBitVector::one(const bwt &w) +{ + return symbolicBitVector(w, 1); +} +template +symbolicBitVector symbolicBitVector::zero(const bwt &w) +{ + return symbolicBitVector(w, 0); +} +template +symbolicBitVector symbolicBitVector::allOnes(const bwt &w) +{ + return symbolicBitVector(~zero(w)); +} + +template +symbolicProposition symbolicBitVector::isAllOnes() const +{ + return (*this == symbolicBitVector::allOnes(this->getWidth())); +} +template +symbolicProposition symbolicBitVector::isAllZeros() const +{ + return (*this == symbolicBitVector::zero(this->getWidth())); +} + +template <> +symbolicBitVector symbolicBitVector::maxValue(const bwt &w) +{ + symbolicBitVector leadingZero(symbolicBitVector::zero(1)); + symbolicBitVector base(symbolicBitVector::allOnes(w - 1)); + + return symbolicBitVector(::CVC4::NodeManager::currentNM()->mkNode( + ::CVC4::kind::BITVECTOR_CONCAT, leadingZero, base)); +} + +template <> +symbolicBitVector symbolicBitVector::maxValue(const bwt &w) +{ + return symbolicBitVector::allOnes(w); +} + +template <> +symbolicBitVector symbolicBitVector::minValue(const bwt &w) +{ + symbolicBitVector leadingOne(symbolicBitVector::one(1)); + symbolicBitVector base(symbolicBitVector::zero(w - 1)); + + return symbolicBitVector(::CVC4::NodeManager::currentNM()->mkNode( + ::CVC4::kind::BITVECTOR_CONCAT, leadingOne, base)); +} + +template <> +symbolicBitVector symbolicBitVector::minValue(const bwt &w) +{ + return symbolicBitVector::zero(w); +} + +/*** Operators ***/ +template +symbolicBitVector symbolicBitVector::operator<<( + const symbolicBitVector &op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_SHL, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator>>( + const symbolicBitVector &op) const +{ + return symbolicBitVector(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_ASHR : kind::BITVECTOR_LSHR, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator|( + const symbolicBitVector &op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator&( + const symbolicBitVector &op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator+( + const symbolicBitVector &op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator-( + const symbolicBitVector &op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator*( + const symbolicBitVector &op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator/( + const symbolicBitVector &op) const +{ + return symbolicBitVector(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_SDIV : kind::BITVECTOR_UDIV_TOTAL, + *this, + op)); +} + +template +symbolicBitVector symbolicBitVector::operator%( + const symbolicBitVector &op) const +{ + return symbolicBitVector(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_SREM : kind::BITVECTOR_UREM_TOTAL, + *this, + op)); +} + +template +symbolicBitVector symbolicBitVector::operator-(void) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_NEG, *this)); +} + +template +symbolicBitVector symbolicBitVector::operator~(void)const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this)); +} + +template +symbolicBitVector symbolicBitVector::increment() const +{ + return symbolicBitVector(NodeManager::currentNM()->mkNode( + kind::BITVECTOR_PLUS, *this, one(this->getWidth()))); +} + +template +symbolicBitVector symbolicBitVector::decrement() const +{ + return symbolicBitVector(NodeManager::currentNM()->mkNode( + kind::BITVECTOR_SUB, *this, one(this->getWidth()))); +} + +template +symbolicBitVector symbolicBitVector::signExtendRightShift( + const symbolicBitVector &op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_ASHR, *this, op)); +} + +/*** Modular operations ***/ +// No overflow checking so these are the same as other operations +template +symbolicBitVector symbolicBitVector::modularLeftShift( + const symbolicBitVector &op) const +{ + return *this << op; +} + +template +symbolicBitVector symbolicBitVector::modularRightShift( + const symbolicBitVector &op) const +{ + return *this >> op; +} + +template +symbolicBitVector symbolicBitVector::modularIncrement() + const +{ + return this->increment(); +} + +template +symbolicBitVector symbolicBitVector::modularDecrement() + const +{ + return this->decrement(); +} + +template +symbolicBitVector symbolicBitVector::modularAdd( + const symbolicBitVector &op) const +{ + return *this + op; +} + +template +symbolicBitVector symbolicBitVector::modularNegate() const +{ + return -(*this); +} + +/*** Comparisons ***/ + +template +symbolicProposition symbolicBitVector::operator==( + const symbolicBitVector &op) const +{ + return symbolicProposition( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op)); +} + +template +symbolicProposition symbolicBitVector::operator<=( + const symbolicBitVector &op) const +{ + // Consider adding kind::BITVECTOR_SLEBV and BITVECTOR_ULEBV + return (*this < op) || (*this == op); +} + +template +symbolicProposition symbolicBitVector::operator>=( + const symbolicBitVector &op) const +{ + return (*this > op) || (*this == op); +} + +template +symbolicProposition symbolicBitVector::operator<( + const symbolicBitVector &op) const +{ + return symbolicProposition(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, *this, op)); +} + +template +symbolicProposition symbolicBitVector::operator>( + const symbolicBitVector &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 +symbolicBitVector symbolicBitVector::toSigned(void) const +{ + return symbolicBitVector(*this); +} +template +symbolicBitVector symbolicBitVector::toUnsigned(void) const +{ + return symbolicBitVector(*this); +} + +/*** Bit hacks ***/ +template <> +symbolicBitVector symbolicBitVector::extend(bwt extension) const +{ + NodeBuilder<> construct(kind::BITVECTOR_SIGN_EXTEND); + construct << NodeManager::currentNM()->mkConst( + BitVectorSignExtend(extension)) + << *this; + + return symbolicBitVector(construct); +} + +template <> +symbolicBitVector symbolicBitVector::extend(bwt extension) const +{ + NodeBuilder<> construct(kind::BITVECTOR_ZERO_EXTEND); + construct << NodeManager::currentNM()->mkConst( + BitVectorZeroExtend(extension)) + << *this; + + return symbolicBitVector(construct); +} + +template +symbolicBitVector symbolicBitVector::contract( + bwt reduction) const +{ + PRECONDITION(this->getWidth() > reduction); + + NodeBuilder<> construct(kind::BITVECTOR_EXTRACT); + construct << NodeManager::currentNM()->mkConst( + BitVectorExtract((this->getWidth() - 1) - reduction, 0)) + << *this; + + return symbolicBitVector(construct); +} + +template +symbolicBitVector symbolicBitVector::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 +symbolicBitVector symbolicBitVector::matchWidth( + const symbolicBitVector &op) const +{ + PRECONDITION(this->getWidth() <= op.getWidth()); + return this->extend(op.getWidth() - this->getWidth()); +} + +template +symbolicBitVector symbolicBitVector::append( + const symbolicBitVector &op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, *this, op)); +} + +// Inclusive of end points, thus if the same, extracts just one bit +template +symbolicBitVector symbolicBitVector::extract( + bwt upper, bwt lower) const +{ + PRECONDITION(upper >= lower); + + NodeBuilder<> construct(kind::BITVECTOR_EXTRACT); + construct << NodeManager::currentNM()->mkConst( + BitVectorExtract(upper, lower)) + << *this; + + return symbolicBitVector(construct); +} + +floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode t) + : FloatingPointSize(t.getConst()) +{ + 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()); + + // 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(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 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()) + { + 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( + current.getConst().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(fpt(current.getType()), + (*arg1).second)); + break; + case kind::FLOATINGPOINT_NEG: + f.insert(current, + symfpu::negate(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(fpt(current.getType()), + (*mode).second, + (*arg1).second)); + break; + case kind::FLOATINGPOINT_RTI: + f.insert( + current, + symfpu::roundToIntegral(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( + 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(fpt(current.getType()), + (*arg1).second, + (*arg2).second, + prop(current[2]))); + break; + + case kind::FLOATINGPOINT_MIN_TOTAL: + f.insert(current, + symfpu::min(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(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(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second, + prop(false))); + break; + + case kind::FLOATINGPOINT_MULT: + f.insert(current, + symfpu::multiply(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second)); + break; + case kind::FLOATINGPOINT_DIV: + f.insert(current, + symfpu::divide(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second)); + break; + case kind::FLOATINGPOINT_REM: + /* + f.insert(current, + symfpu::remainder(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(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(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(fpt(current.getType()), IEEEBV)); + } + break; + + case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + f.insert(current, + symfpu::unpack(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(fpt(current.getType()), + (*mode).second, + sbv(current[1]))); + break; + + case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + f.insert( + current, + symfpu::convertUBVToFloat(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( + 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( + fpt(childType), (*arg1).second, (*arg2).second)); + break; + + case kind::FLOATINGPOINT_LT: + b.insert(current, + symfpu::lessThan( + 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(fpt(childType), (*arg1).second)); + break; + + case kind::FLOATINGPOINT_ISSN: + b.insert(current, + symfpu::isSubnormal(fpt(childType), + (*arg1).second)); + break; + + case kind::FLOATINGPOINT_ISZ: + b.insert( + current, + symfpu::isZero(fpt(childType), (*arg1).second)); + break; + + case kind::FLOATINGPOINT_ISINF: + b.insert( + current, + symfpu::isInfinite(fpt(childType), (*arg1).second)); + break; + + case kind::FLOATINGPOINT_ISNAN: + b.insert(current, + symfpu::isNaN(fpt(childType), (*arg1).second)); + break; + + case kind::FLOATINGPOINT_ISPOS: + b.insert( + current, + symfpu::isPositive(fpt(childType), (*arg1).second)); + break; + + case kind::FLOATINGPOINT_ISNEG: + b.insert( + current, + symfpu::isNegative(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(); + + u.insert(current, + symfpu::convertFloatToUBV(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(); + + s.insert(current, + symfpu::convertFloatToSBV(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 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 +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 sbv; + typedef symbolicBitVector 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; // 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; // 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 +struct signedToLiteralType; + +template <> +struct signedToLiteralType +{ + typedef int literalType; +}; +template <> +struct signedToLiteralType +{ + typedef unsigned int literalType; +}; + +template +class symbolicBitVector : public nodeWrapper +{ + protected: + typedef typename signedToLiteralType::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; // To allow conversion between the types + +#ifdef CVC4_USE_SYMFPU + friend ::symfpu::ite >; // For ITE +#endif + + public: + symbolicBitVector(const Node n); + symbolicBitVector(const bwt w, const unsigned v); + symbolicBitVector(const symbolicProposition &p); + symbolicBitVector(const symbolicBitVector &old); + symbolicBitVector(const BitVector &old); + + bwt getWidth(void) const; + + /*** Constant creation and test ***/ + static symbolicBitVector one(const bwt &w); + static symbolicBitVector zero(const bwt &w); + static symbolicBitVector allOnes(const bwt &w); + + symbolicProposition isAllOnes() const; + symbolicProposition isAllZeros() const; + + static symbolicBitVector maxValue(const bwt &w); + static symbolicBitVector minValue(const bwt &w); + + /*** Operators ***/ + symbolicBitVector operator<<( + const symbolicBitVector &op) const; + symbolicBitVector operator>>( + const symbolicBitVector &op) const; + symbolicBitVector operator|( + const symbolicBitVector &op) const; + symbolicBitVector operator&( + const symbolicBitVector &op) const; + symbolicBitVector operator+( + const symbolicBitVector &op) const; + symbolicBitVector operator-( + const symbolicBitVector &op) const; + symbolicBitVector operator*( + const symbolicBitVector &op) const; + symbolicBitVector operator/( + const symbolicBitVector &op) const; + symbolicBitVector operator%( + const symbolicBitVector &op) const; + symbolicBitVector operator-(void) const; + symbolicBitVector operator~(void)const; + symbolicBitVector increment() const; + symbolicBitVector decrement() const; + symbolicBitVector signExtendRightShift( + const symbolicBitVector &op) const; + + /*** Modular operations ***/ + // This back-end doesn't do any overflow checking so these are the same as + // other operations + symbolicBitVector modularLeftShift( + const symbolicBitVector &op) const; + symbolicBitVector modularRightShift( + const symbolicBitVector &op) const; + symbolicBitVector modularIncrement() const; + symbolicBitVector modularDecrement() const; + symbolicBitVector modularAdd( + const symbolicBitVector &op) const; + symbolicBitVector modularNegate() const; + + /*** Comparisons ***/ + symbolicProposition operator==(const symbolicBitVector &op) const; + symbolicProposition operator<=(const symbolicBitVector &op) const; + symbolicProposition operator>=(const symbolicBitVector &op) const; + symbolicProposition operator<(const symbolicBitVector &op) const; + symbolicProposition operator>(const symbolicBitVector &op) const; + + /*** Type conversion ***/ + // CVC4 nodes make no distinction between signed and unsigned, thus these are + // trivial + symbolicBitVector toSigned(void) const; + symbolicBitVector toUnsigned(void) const; + + /*** Bit hacks ***/ + symbolicBitVector extend(bwt extension) const; + symbolicBitVector contract(bwt reduction) const; + symbolicBitVector resize(bwt newSize) const; + symbolicBitVector matchWidth( + const symbolicBitVector &op) const; + symbolicBitVector append( + const symbolicBitVector &op) const; + + // Inclusive of end points, thus if the same, extracts just one bit + symbolicBitVector 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 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 fpMap; + typedef context::CDHashMap rmMap; + typedef context::CDHashMap boolMap; + typedef context::CDHashMap ubvMap; + typedef context::CDHashMap 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 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 @@ -95,8 +96,10 @@ Node buildConjunct(const std::vector &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 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 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 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(); 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(); 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(), 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().isNormal() + || floatValue.getConst().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())), + 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())), + 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())), + 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().isNaN()); + Assert(!concreteValue.getConst().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().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(); + 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 d_conflictNode; /** Uninterpretted functions for partially defined functions. **/ + void enableUF(LogicRequest& lr); + typedef context::CDHashMap 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 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 #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()); + + 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()); + + // \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()); + + 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()); + 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(); + break; + + case roundNearestTiesToAway: + value = symfpuSymbolic::traits::RNA().getConst(); + break; + + case roundTowardPositive: + value = symfpuSymbolic::traits::RTP().getConst(); + break; + + case roundTowardNegative: + value = symfpuSymbolic::traits::RTN().getConst(); + break; + + case roundTowardZero: + value = symfpuSymbolic::traits::RTZ().getConst(); + 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(); + 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(); + 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 + +#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 +wrappedBitVector wrappedBitVector::one(const bwt &w) +{ + return wrappedBitVector(w, 1); } - FloatingPoint::FloatingPoint (unsigned e, unsigned s, const BitVector &bv) : - fpl(e,s,0.0), - t(e,s) {} +template +wrappedBitVector wrappedBitVector::zero(const bwt &w) +{ + return wrappedBitVector(w, 0); +} + +template +wrappedBitVector wrappedBitVector::allOnes(const bwt &w) +{ + return ~wrappedBitVector::zero(w); +} +template +prop wrappedBitVector::isAllOnes() const +{ + return (*this == wrappedBitVector::allOnes(this->getWidth())); +} +template +prop wrappedBitVector::isAllZeros() const +{ + return (*this == wrappedBitVector::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 +wrappedBitVector wrappedBitVector::maxValue(const bwt &w) +{ + if (isSigned) + { + BitVector base(w - 1, 0U); + return wrappedBitVector((~base).zeroExtend(1)); + } + else + { + return wrappedBitVector::allOnes(w); + } +} + +template +wrappedBitVector wrappedBitVector::minValue(const bwt &w) +{ + if (isSigned) + { + BitVector base(w, 1U); + BitVector shiftAmount(w, w - 1); + BitVector result(base.leftShift(shiftAmount)); + return wrappedBitVector(result); + } + else + { + return wrappedBitVector::zero(w); + } +} + +/*** Operators ***/ +template +wrappedBitVector wrappedBitVector::operator<<( + const wrappedBitVector &op) const +{ + return this->BitVector::leftShift(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator>>( + const wrappedBitVector &op) const +{ + return this->BitVector::arithRightShift(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator>>( + const wrappedBitVector &op) const +{ + return this->BitVector::logicalRightShift(op); +} + +template +wrappedBitVector wrappedBitVector::operator|( + const wrappedBitVector &op) const +{ + return this->BitVector::operator|(op); +} + +template +wrappedBitVector wrappedBitVector::operator&( + const wrappedBitVector &op) const +{ + return this->BitVector::operator&(op); +} + +template +wrappedBitVector wrappedBitVector::operator+( + const wrappedBitVector &op) const +{ + return this->BitVector::operator+(op); +} + +template +wrappedBitVector wrappedBitVector::operator-( + const wrappedBitVector &op) const +{ + return this->BitVector::operator-(op); +} + +template +wrappedBitVector wrappedBitVector::operator*( + const wrappedBitVector &op) const +{ + return this->BitVector::operator*(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator/( + const wrappedBitVector &op) const +{ + return this->BitVector::unsignedDivTotal(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator%( + const wrappedBitVector &op) const +{ + return this->BitVector::unsignedRemTotal(op); +} + +template +wrappedBitVector wrappedBitVector::operator-(void) const +{ + return this->BitVector::operator-(); +} + +template +wrappedBitVector wrappedBitVector::operator~(void)const +{ + return this->BitVector::operator~(); +} + +template +wrappedBitVector wrappedBitVector::increment() const +{ + return *this + wrappedBitVector::one(this->getWidth()); +} + +template +wrappedBitVector wrappedBitVector::decrement() const +{ + return *this - wrappedBitVector::one(this->getWidth()); +} + +template +wrappedBitVector wrappedBitVector::signExtendRightShift( + const wrappedBitVector &op) const +{ + return this->BitVector::arithRightShift(BitVector(this->getWidth(), op)); +} + +/*** Modular opertaions ***/ +// No overflow checking so these are the same as other operations +template +wrappedBitVector wrappedBitVector::modularLeftShift( + const wrappedBitVector &op) const +{ + return *this << op; +} + +template +wrappedBitVector wrappedBitVector::modularRightShift( + const wrappedBitVector &op) const +{ + return *this >> op; +} + +template +wrappedBitVector wrappedBitVector::modularIncrement() const +{ + return this->increment(); +} + +template +wrappedBitVector wrappedBitVector::modularDecrement() const +{ + return this->decrement(); +} + +template +wrappedBitVector wrappedBitVector::modularAdd( + const wrappedBitVector &op) const +{ + return *this + op; +} + +template +wrappedBitVector wrappedBitVector::modularNegate() const +{ + return -(*this); +} + +/*** Comparisons ***/ + +template +prop wrappedBitVector::operator==( + const wrappedBitVector &op) const +{ + return this->BitVector::operator==(op); +} + +template <> +prop wrappedBitVector::operator<=(const wrappedBitVector &op) const +{ + return this->signedLessThanEq(op); +} + +template <> +prop wrappedBitVector::operator>=(const wrappedBitVector &op) const +{ + return !(this->signedLessThan(op)); +} + +template <> +prop wrappedBitVector::operator<(const wrappedBitVector &op) const +{ + return this->signedLessThan(op); +} + +template <> +prop wrappedBitVector::operator>(const wrappedBitVector &op) const +{ + return !(this->signedLessThanEq(op)); +} + +template <> +prop wrappedBitVector::operator<=( + const wrappedBitVector &op) const +{ + return this->unsignedLessThanEq(op); +} + +template <> +prop wrappedBitVector::operator>=( + const wrappedBitVector &op) const +{ + return !(this->unsignedLessThan(op)); +} + +template <> +prop wrappedBitVector::operator<(const wrappedBitVector &op) const +{ + return this->unsignedLessThan(op); +} + +template <> +prop wrappedBitVector::operator>(const wrappedBitVector &op) const +{ + return !(this->unsignedLessThanEq(op)); +} + +/*** Type conversion ***/ +// CVC4 nodes make no distinction between signed and unsigned, thus ... +template +wrappedBitVector wrappedBitVector::toSigned(void) const +{ + return wrappedBitVector(*this); +} + +template +wrappedBitVector wrappedBitVector::toUnsigned(void) const +{ + return wrappedBitVector(*this); +} + +/*** Bit hacks ***/ + +template +wrappedBitVector wrappedBitVector::extend( + bwt extension) const +{ + if (isSigned) + { + return this->BitVector::signExtend(extension); + } + else + { + return this->BitVector::zeroExtend(extension); + } +} + +template +wrappedBitVector wrappedBitVector::contract( + bwt reduction) const +{ + PRECONDITION(this->getWidth() > reduction); + + return this->extract((this->getWidth() - 1) - reduction, 0); +} + +template +wrappedBitVector wrappedBitVector::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 +wrappedBitVector wrappedBitVector::matchWidth( + const wrappedBitVector &op) const +{ + PRECONDITION(this->getWidth() <= op.getWidth()); + return this->extend(op.getWidth() - this->getWidth()); +} + +template +wrappedBitVector wrappedBitVector::append( + const wrappedBitVector &op) const +{ + return this->BitVector::concat(op); +} + +// Inclusive of end points, thus if the same, extracts just one bit +template +wrappedBitVector wrappedBitVector::extract(bwt upper, + bwt lower) const +{ + PRECONDITION(upper >= lower); + return this->BitVector::extract(upper, lower); +} + +// Explicit instantiation +template class wrappedBitVector; +template class wrappedBitVector; + +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::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::fpt(ct), + symfpuLiteral::rm(rm), + symfpuLiteral::sbv(bv))); + } + else + { + return FloatingPointLiteral( + symfpu::convertUBVToFloat( + 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::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::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::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(t, fpl)); +#else return *this; +#endif } FloatingPoint FloatingPoint::negate (void) const { +#ifdef CVC4_USE_SYMFPU + return FloatingPoint(t, symfpu::negate(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(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(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(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(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(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(t, rm, fpl)); +#else return *this; +#endif } FloatingPoint FloatingPoint::rti (const RoundingMode &rm) const { +#ifdef CVC4_USE_SYMFPU + return FloatingPoint( + t, symfpu::roundToIntegral(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(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(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(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(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(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(t, fpl, arg.fpl); +#else return false; +#endif } bool FloatingPoint::isNormal (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isNormal(t, fpl); +#else return false; +#endif } bool FloatingPoint::isSubnormal (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isSubnormal(t, fpl); +#else return false; +#endif } bool FloatingPoint::isZero (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isZero(t, fpl); +#else return false; +#endif } bool FloatingPoint::isInfinite (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isInfinite(t, fpl); +#else return false; +#endif } bool FloatingPoint::isNaN (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isNaN(t, fpl); +#else return false; +#endif } bool FloatingPoint::isNegative (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isNegative(t, fpl); +#else return false; +#endif } bool FloatingPoint::isPositive (void) const { +#ifdef CVC4_USE_SYMFPU + return symfpu::isPositive(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(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( + t, rm, fpl, width, undefinedCase); else - return undefinedCase; + return symfpu::convertFloatToUBV( + 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(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 - #include "util/bitvector.h" #include "util/rational.h" +#include + +#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 + 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 sbv; + typedef wrappedBitVector 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 + struct signedToLiteralType; + + template <> + struct signedToLiteralType + { + typedef int literalType; + }; + template <> + struct signedToLiteralType + { + 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 + class wrappedBitVector : public BitVector + { + protected: + typedef typename signedToLiteralType::literalType literalType; + + friend wrappedBitVector; // To allow conversion between the + // types +#ifdef CVC4_USE_SYMFPU + friend ::symfpu::ite >; // 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 &old) : BitVector(old) {} + wrappedBitVector(const BitVector &old) : BitVector(old) {} + bwt getWidth(void) const { return getSize(); } + /*** Constant creation and test ***/ + + static wrappedBitVector one(const bwt &w); + static wrappedBitVector zero(const bwt &w); + static wrappedBitVector allOnes(const bwt &w); + + prop isAllOnes() const; + prop isAllZeros() const; + + static wrappedBitVector maxValue(const bwt &w); + static wrappedBitVector minValue(const bwt &w); + + /*** Operators ***/ + wrappedBitVector operator<<( + const wrappedBitVector &op) const; + wrappedBitVector operator>>( + const wrappedBitVector &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 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 operator|( + const wrappedBitVector &op) const; + wrappedBitVector operator&( + const wrappedBitVector &op) const; + wrappedBitVector operator+( + const wrappedBitVector &op) const; + wrappedBitVector operator-( + const wrappedBitVector &op) const; + wrappedBitVector operator*( + const wrappedBitVector &op) const; + wrappedBitVector operator/( + const wrappedBitVector &op) const; + wrappedBitVector operator%( + const wrappedBitVector &op) const; + wrappedBitVector operator-(void) const; + wrappedBitVector operator~(void)const; + + wrappedBitVector increment() const; + wrappedBitVector decrement() const; + wrappedBitVector signExtendRightShift( + const wrappedBitVector &op) const; + + /*** Modular opertaions ***/ + // No overflow checking so these are the same as other operations + wrappedBitVector modularLeftShift( + const wrappedBitVector &op) const; + wrappedBitVector modularRightShift( + const wrappedBitVector &op) const; + wrappedBitVector modularIncrement() const; + wrappedBitVector modularDecrement() const; + wrappedBitVector modularAdd( + const wrappedBitVector &op) const; + wrappedBitVector modularNegate() const; + + /*** Comparisons ***/ + // Inherited ... ish ... + prop operator==(const wrappedBitVector &op) const; + prop operator<=(const wrappedBitVector &op) const; + prop operator>=(const wrappedBitVector &op) const; + prop operator<(const wrappedBitVector &op) const; + prop operator>(const wrappedBitVector &op) const; + + /*** Type conversion ***/ + wrappedBitVector toSigned(void) const; + wrappedBitVector toUnsigned(void) const; + + /*** Bit hacks ***/ + wrappedBitVector extend(bwt extension) const; + wrappedBitVector contract(bwt reduction) const; + wrappedBitVector resize(bwt newSize) const; + wrappedBitVector matchWidth( + const wrappedBitVector &op) const; + wrappedBitVector append( + const wrappedBitVector &op) const; + + // Inclusive of end points, thus if the same, extracts just one bit + wrappedBitVector extract(bwt upper, bwt lower) const; + }; + } /** * A concrete floating point number */ - +#ifdef CVC4_USE_SYMFPU + typedef ::symfpu::unpackedFloat 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 : -- 2.30.2