* 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.
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;
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";
**/
#include "theory/fp/fp_converter.h"
+#include "theory/theory.h"
+// theory.h Only needed for the leaf test
#include <stack>
+#ifdef CVC4_USE_SYMFPU
+#include "symfpu/core/add.h"
+#include "symfpu/core/classify.h"
+#include "symfpu/core/compare.h"
+#include "symfpu/core/convert.h"
+#include "symfpu/core/divide.h"
+#include "symfpu/core/fma.h"
+#include "symfpu/core/ite.h"
+#include "symfpu/core/multiply.h"
+#include "symfpu/core/packing.h"
+#include "symfpu/core/remainder.h"
+#include "symfpu/core/sign.h"
+#include "symfpu/core/sqrt.h"
+#include "symfpu/utils/numberOfRoundingModes.h"
+#include "symfpu/utils/properties.h"
+#endif
+
+#ifdef CVC4_USE_SYMFPU
+namespace symfpu {
+using namespace ::CVC4::theory::fp::symfpuSymbolic;
+
+#define CVC4_SYM_ITE_DFN(T) \
+ template <> \
+ struct ite<symbolicProposition, T> \
+ { \
+ static const T iteOp(const symbolicProposition &_cond, \
+ const T &_l, \
+ const T &_r) \
+ { \
+ ::CVC4::NodeManager *nm = ::CVC4::NodeManager::currentNM(); \
+ \
+ ::CVC4::Node cond = _cond; \
+ ::CVC4::Node l = _l; \
+ ::CVC4::Node r = _r; \
+ \
+ /* Handle some common symfpu idioms */ \
+ if (cond.isConst()) \
+ { \
+ return (cond == nm->mkConst(::CVC4::BitVector(1U, 1U))) ? l : r; \
+ } \
+ else \
+ { \
+ if (l.getKind() == ::CVC4::kind::BITVECTOR_ITE) \
+ { \
+ if (l[1] == r) \
+ { \
+ return nm->mkNode( \
+ ::CVC4::kind::BITVECTOR_ITE, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_AND, \
+ cond, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_NOT, l[0])), \
+ l[2], \
+ r); \
+ } \
+ else if (l[2] == r) \
+ { \
+ return nm->mkNode( \
+ ::CVC4::kind::BITVECTOR_ITE, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_AND, cond, l[0]), \
+ l[1], \
+ r); \
+ } \
+ } \
+ else if (r.getKind() == ::CVC4::kind::BITVECTOR_ITE) \
+ { \
+ if (r[1] == l) \
+ { \
+ return nm->mkNode( \
+ ::CVC4::kind::BITVECTOR_ITE, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_AND, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_NOT, cond), \
+ nm->mkNode(::CVC4::kind::BITVECTOR_NOT, r[0])), \
+ r[2], \
+ l); \
+ } \
+ else if (r[2] == l) \
+ { \
+ return nm->mkNode( \
+ ::CVC4::kind::BITVECTOR_ITE, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_AND, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_NOT, cond), \
+ r[0]), \
+ r[1], \
+ l); \
+ } \
+ } \
+ } \
+ return T(nm->mkNode(::CVC4::kind::BITVECTOR_ITE, cond, l, r)); \
+ } \
+ }
+
+// Can (unsurprisingly) only ITE things which contain Nodes
+CVC4_SYM_ITE_DFN(traits::rm);
+CVC4_SYM_ITE_DFN(traits::prop);
+CVC4_SYM_ITE_DFN(traits::sbv);
+CVC4_SYM_ITE_DFN(traits::ubv);
+
+#undef CVC4_SYM_ITE_DFN
+
+template <>
+traits::ubv orderEncode<traits, traits::ubv>(const traits::ubv &b)
+{
+ return orderEncodeBitwise<traits, traits::ubv>(b);
+}
+
+template <>
+stickyRightShiftResult<traits> stickyRightShift(const traits::ubv &input,
+ const traits::ubv &shiftAmount)
+{
+ return stickyRightShiftBitwise<traits>(input, shiftAmount);
+}
+
+template <>
+void probabilityAnnotation<traits, traits::prop>(const traits::prop &p,
+ const probability &pr)
+{
+ // For now, do nothing...
+ return;
+}
+};
+#endif
+
+#ifndef CVC4_USE_SYMFPU
+#define PRECONDITION(X) Assert((X))
+#define SYMFPU_NUMBER_OF_ROUNDING_MODES 5
+#endif
+
namespace CVC4 {
namespace theory {
namespace fp {
+namespace symfpuSymbolic {
+
+symbolicRoundingMode traits::RNE(void) { return symbolicRoundingMode(0x01); };
+symbolicRoundingMode traits::RNA(void) { return symbolicRoundingMode(0x02); };
+symbolicRoundingMode traits::RTP(void) { return symbolicRoundingMode(0x04); };
+symbolicRoundingMode traits::RTN(void) { return symbolicRoundingMode(0x08); };
+symbolicRoundingMode traits::RTZ(void) { return symbolicRoundingMode(0x10); };
+void traits::precondition(const bool b)
+{
+ Assert(b);
+ return;
+}
+void traits::postcondition(const bool b)
+{
+ Assert(b);
+ return;
+}
+void traits::invariant(const bool b)
+{
+ Assert(b);
+ return;
+}
+
+void traits::precondition(const prop &p) { return; }
+void traits::postcondition(const prop &p) { return; }
+void traits::invariant(const prop &p) { return; }
+// This allows us to use the symfpu literal / symbolic assertions in the
+// symbolic back-end
+typedef traits t;
+
+bool symbolicProposition::checkNodeType(const TNode node)
+{
+ TypeNode tn = node.getType(false);
+ return tn.isBitVector() && tn.getBitVectorSize() == 1;
+}
+
+symbolicProposition::symbolicProposition(const Node n) : nodeWrapper(n)
+{
+ PRECONDITION(checkNodeType(*this));
+} // Only used within this header so could be friend'd
+symbolicProposition::symbolicProposition(bool v)
+ : nodeWrapper(
+ NodeManager::currentNM()->mkConst(BitVector(1U, (v ? 1U : 0U))))
+{
+ PRECONDITION(checkNodeType(*this));
+}
+symbolicProposition::symbolicProposition(const symbolicProposition &old)
+ : nodeWrapper(old)
+{
+ PRECONDITION(checkNodeType(*this));
+}
+
+symbolicProposition symbolicProposition::operator!(void)const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this));
+}
+
+symbolicProposition symbolicProposition::operator&&(
+ const symbolicProposition &op) const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op));
+}
+
+symbolicProposition symbolicProposition::operator||(
+ const symbolicProposition &op) const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op));
+}
+
+symbolicProposition symbolicProposition::operator==(
+ const symbolicProposition &op) const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op));
+}
+
+symbolicProposition symbolicProposition::operator^(
+ const symbolicProposition &op) const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_XOR, *this, op));
+}
+
+bool symbolicRoundingMode::checkNodeType(const TNode n)
+{
+#ifdef CVC4_USE_SYMFPU
+ return n.getType(false).isBitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES);
+#else
+ return false;
+#endif
+}
+
+symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n)
+{
+ PRECONDITION(checkNodeType(*this));
+}
+
+#ifdef CVC4_USE_SYMFPU
+symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
+ : nodeWrapper(NodeManager::currentNM()->mkConst(
+ BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
+{
+ PRECONDITION((v & v - 1) == 0 && v != 0); // Exactly one bit set
+ PRECONDITION(checkNodeType(*this));
+}
+#else
+symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
+ : nodeWrapper(NodeManager::currentNM()->mkConst(
+ BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
+{
+ Unreachable();
+}
+#endif
+
+symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old)
+ : nodeWrapper(old)
+{
+ PRECONDITION(checkNodeType(*this));
+}
+
+symbolicProposition symbolicRoundingMode::valid(void) const
+{
+ NodeManager *nm = NodeManager::currentNM();
+ Node zero(nm->mkConst(
+ BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, (long unsigned int)0)));
+
+ // Is there a better encoding of this?
+ return symbolicProposition(nm->mkNode(
+ kind::BITVECTOR_AND,
+ nm->mkNode(kind::BITVECTOR_COMP,
+ nm->mkNode(kind::BITVECTOR_AND,
+ *this,
+ nm->mkNode(kind::BITVECTOR_SUB,
+ *this,
+ nm->mkConst(BitVector(
+ SYMFPU_NUMBER_OF_ROUNDING_MODES,
+ (long unsigned int)1)))),
+ zero),
+ nm->mkNode(kind::BITVECTOR_NOT,
+ nm->mkNode(kind::BITVECTOR_COMP, *this, zero))));
+}
+
+symbolicProposition symbolicRoundingMode::operator==(
+ const symbolicRoundingMode &op) const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op));
+}
+
+template <bool isSigned>
+Node symbolicBitVector<isSigned>::boolNodeToBV(Node node) const
+{
+ Assert(node.getType().isBoolean());
+ NodeManager *nm = NodeManager::currentNM();
+ return nm->mkNode(kind::ITE,
+ node,
+ nm->mkConst(BitVector(1U, 1U)),
+ nm->mkConst(BitVector(1U, 0U)));
+}
+
+template <bool isSigned>
+Node symbolicBitVector<isSigned>::BVToBoolNode(Node node) const
+{
+ Assert(node.getType().isBitVector());
+ Assert(node.getType().getBitVectorSize() == 1);
+ NodeManager *nm = NodeManager::currentNM();
+ return nm->mkNode(kind::EQUAL, node, nm->mkConst(BitVector(1U, 1U)));
+}
+
+template <bool isSigned>
+Node symbolicBitVector<isSigned>::fromProposition(Node node) const
+{
+ return node;
+}
+template <bool isSigned>
+Node symbolicBitVector<isSigned>::toProposition(Node node) const
+{
+ return boolNodeToBV(node);
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned>::symbolicBitVector(const Node n) : nodeWrapper(n)
+{
+ PRECONDITION(checkNodeType(*this));
+}
+
+template <bool isSigned>
+bool symbolicBitVector<isSigned>::checkNodeType(const TNode n)
+{
+ return n.getType(false).isBitVector();
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned>::symbolicBitVector(const bwt w, const unsigned v)
+ : nodeWrapper(NodeManager::currentNM()->mkConst(BitVector(w, v)))
+{
+ PRECONDITION(checkNodeType(*this));
+}
+template <bool isSigned>
+symbolicBitVector<isSigned>::symbolicBitVector(const symbolicProposition &p)
+ : nodeWrapper(fromProposition(p))
+{
+}
+template <bool isSigned>
+symbolicBitVector<isSigned>::symbolicBitVector(
+ const symbolicBitVector<isSigned> &old)
+ : nodeWrapper(old)
+{
+ PRECONDITION(checkNodeType(*this));
+}
+template <bool isSigned>
+symbolicBitVector<isSigned>::symbolicBitVector(const BitVector &old)
+ : nodeWrapper(NodeManager::currentNM()->mkConst(old))
+{
+ PRECONDITION(checkNodeType(*this));
+}
+
+template <bool isSigned>
+bwt symbolicBitVector<isSigned>::getWidth(void) const
+{
+ return this->getType(false).getBitVectorSize();
+}
+
+/*** Constant creation and test ***/
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::one(const bwt &w)
+{
+ return symbolicBitVector<isSigned>(w, 1);
+}
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::zero(const bwt &w)
+{
+ return symbolicBitVector<isSigned>(w, 0);
+}
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::allOnes(const bwt &w)
+{
+ return symbolicBitVector<isSigned>(~zero(w));
+}
+
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::isAllOnes() const
+{
+ return (*this == symbolicBitVector<isSigned>::allOnes(this->getWidth()));
+}
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::isAllZeros() const
+{
+ return (*this == symbolicBitVector<isSigned>::zero(this->getWidth()));
+}
+
+template <>
+symbolicBitVector<true> symbolicBitVector<true>::maxValue(const bwt &w)
+{
+ symbolicBitVector<true> leadingZero(symbolicBitVector<true>::zero(1));
+ symbolicBitVector<true> base(symbolicBitVector<true>::allOnes(w - 1));
+
+ return symbolicBitVector<true>(::CVC4::NodeManager::currentNM()->mkNode(
+ ::CVC4::kind::BITVECTOR_CONCAT, leadingZero, base));
+}
+
+template <>
+symbolicBitVector<false> symbolicBitVector<false>::maxValue(const bwt &w)
+{
+ return symbolicBitVector<false>::allOnes(w);
+}
+
+template <>
+symbolicBitVector<true> symbolicBitVector<true>::minValue(const bwt &w)
+{
+ symbolicBitVector<true> leadingOne(symbolicBitVector<true>::one(1));
+ symbolicBitVector<true> base(symbolicBitVector<true>::zero(w - 1));
+
+ return symbolicBitVector<true>(::CVC4::NodeManager::currentNM()->mkNode(
+ ::CVC4::kind::BITVECTOR_CONCAT, leadingOne, base));
+}
+
+template <>
+symbolicBitVector<false> symbolicBitVector<false>::minValue(const bwt &w)
+{
+ return symbolicBitVector<false>::zero(w);
+}
+
+/*** Operators ***/
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator<<(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_SHL, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator>>(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
+ (isSigned) ? kind::BITVECTOR_ASHR : kind::BITVECTOR_LSHR, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator|(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator&(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator+(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator-(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator*(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator/(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
+ (isSigned) ? kind::BITVECTOR_SDIV : kind::BITVECTOR_UDIV_TOTAL,
+ *this,
+ op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator%(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
+ (isSigned) ? kind::BITVECTOR_SREM : kind::BITVECTOR_UREM_TOTAL,
+ *this,
+ op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator-(void) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_NEG, *this));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator~(void)const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::increment() const
+{
+ return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
+ kind::BITVECTOR_PLUS, *this, one(this->getWidth())));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::decrement() const
+{
+ return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
+ kind::BITVECTOR_SUB, *this, one(this->getWidth())));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::signExtendRightShift(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_ASHR, *this, op));
+}
+
+/*** Modular operations ***/
+// No overflow checking so these are the same as other operations
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularLeftShift(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return *this << op;
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularRightShift(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return *this >> op;
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularIncrement()
+ const
+{
+ return this->increment();
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularDecrement()
+ const
+{
+ return this->decrement();
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularAdd(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return *this + op;
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularNegate() const
+{
+ return -(*this);
+}
+
+/*** Comparisons ***/
+
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::operator==(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op));
+}
+
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::operator<=(
+ const symbolicBitVector<isSigned> &op) const
+{
+ // Consider adding kind::BITVECTOR_SLEBV and BITVECTOR_ULEBV
+ return (*this < op) || (*this == op);
+}
+
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::operator>=(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return (*this > op) || (*this == op);
+}
+
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::operator<(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicProposition(NodeManager::currentNM()->mkNode(
+ (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, *this, op));
+}
+
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::operator>(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicProposition(NodeManager::currentNM()->mkNode(
+ (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, op, *this));
+}
+
+/*** Type conversion ***/
+// CVC4 nodes make no distinction between signed and unsigned, thus ...
+template <bool isSigned>
+symbolicBitVector<true> symbolicBitVector<isSigned>::toSigned(void) const
+{
+ return symbolicBitVector<true>(*this);
+}
+template <bool isSigned>
+symbolicBitVector<false> symbolicBitVector<isSigned>::toUnsigned(void) const
+{
+ return symbolicBitVector<false>(*this);
+}
+
+/*** Bit hacks ***/
+template <>
+symbolicBitVector<true> symbolicBitVector<true>::extend(bwt extension) const
+{
+ NodeBuilder<> construct(kind::BITVECTOR_SIGN_EXTEND);
+ construct << NodeManager::currentNM()->mkConst<BitVectorSignExtend>(
+ BitVectorSignExtend(extension))
+ << *this;
+
+ return symbolicBitVector<true>(construct);
+}
+
+template <>
+symbolicBitVector<false> symbolicBitVector<false>::extend(bwt extension) const
+{
+ NodeBuilder<> construct(kind::BITVECTOR_ZERO_EXTEND);
+ construct << NodeManager::currentNM()->mkConst<BitVectorZeroExtend>(
+ BitVectorZeroExtend(extension))
+ << *this;
+
+ return symbolicBitVector<false>(construct);
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::contract(
+ bwt reduction) const
+{
+ PRECONDITION(this->getWidth() > reduction);
+
+ NodeBuilder<> construct(kind::BITVECTOR_EXTRACT);
+ construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
+ BitVectorExtract((this->getWidth() - 1) - reduction, 0))
+ << *this;
+
+ return symbolicBitVector<isSigned>(construct);
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::resize(
+ bwt newSize) const
+{
+ bwt width = this->getWidth();
+
+ if (newSize > width)
+ {
+ return this->extend(newSize - width);
+ }
+ else if (newSize < width)
+ {
+ return this->contract(width - newSize);
+ }
+ else
+ {
+ return *this;
+ }
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::matchWidth(
+ const symbolicBitVector<isSigned> &op) const
+{
+ PRECONDITION(this->getWidth() <= op.getWidth());
+ return this->extend(op.getWidth() - this->getWidth());
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::append(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, *this, op));
+}
+
+// Inclusive of end points, thus if the same, extracts just one bit
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::extract(
+ bwt upper, bwt lower) const
+{
+ PRECONDITION(upper >= lower);
+
+ NodeBuilder<> construct(kind::BITVECTOR_EXTRACT);
+ construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
+ BitVectorExtract(upper, lower))
+ << *this;
+
+ return symbolicBitVector<isSigned>(construct);
+}
+
+floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode t)
+ : FloatingPointSize(t.getConst<FloatingPointSize>())
+{
+ PRECONDITION(t.isFloatingPoint());
+}
+floatingPointTypeInfo::floatingPointTypeInfo(unsigned exp, unsigned sig)
+ : FloatingPointSize(exp, sig)
+{
+}
+floatingPointTypeInfo::floatingPointTypeInfo(const floatingPointTypeInfo &old)
+ : FloatingPointSize(old)
+{
+}
+
+TypeNode floatingPointTypeInfo::getTypeNode(void) const
+{
+ return NodeManager::currentNM()->mkFloatingPointType(*this);
+}
+}
FpConverter::FpConverter(context::UserContext *user)
- : d_additionalAssertions(user) {}
+ :
+#ifdef CVC4_USE_SYMFPU
+ f(user),
+ r(user),
+ b(user),
+ u(user),
+ s(user),
+#endif
+ d_additionalAssertions(user)
+{
+}
+
+#ifdef CVC4_USE_SYMFPU
+Node FpConverter::ufToNode(const fpt &format, const uf &u) const
+{
+ NodeManager *nm = NodeManager::currentNM();
+
+ FloatingPointSize fps(format.getTypeNode().getConst<FloatingPointSize>());
+
+ // This is not entirely obvious but it builds a float from components
+ // Particularly, if the components can be constant folded, it should
+ // build a Node containing a constant FloatingPoint number
+
+ ubv packed(symfpu::pack<traits>(format, u));
+ Node value =
+ nm->mkNode(nm->mkConst(FloatingPointToFPIEEEBitVector(fps)), packed);
+ return value;
+}
+
+Node FpConverter::rmToNode(const rm &r) const
+{
+ NodeManager *nm = NodeManager::currentNM();
+
+ Node transVar = r;
+
+ Node RNE = traits::RNE();
+ Node RNA = traits::RNA();
+ Node RTP = traits::RTP();
+ Node RTN = traits::RTN();
+ Node RTZ = traits::RTZ();
+
+ Node value = nm->mkNode(
+ kind::ITE,
+ nm->mkNode(kind::EQUAL, transVar, RNE),
+ nm->mkConst(roundNearestTiesToEven),
+ nm->mkNode(kind::ITE,
+ nm->mkNode(kind::EQUAL, transVar, RNA),
+ nm->mkConst(roundNearestTiesToAway),
+ nm->mkNode(kind::ITE,
+ nm->mkNode(kind::EQUAL, transVar, RTP),
+ nm->mkConst(roundTowardPositive),
+ nm->mkNode(kind::ITE,
+ nm->mkNode(kind::EQUAL, transVar, RTN),
+ nm->mkConst(roundTowardNegative),
+ nm->mkConst(roundTowardZero)))));
+ return value;
+}
+
+Node FpConverter::propToNode(const prop &p) const
+{
+ NodeManager *nm = NodeManager::currentNM();
+ Node value =
+ nm->mkNode(kind::EQUAL, p, nm->mkConst(::CVC4::BitVector(1U, 1U)));
+ return value;
+}
+Node FpConverter::ubvToNode(const ubv &u) const { return u; }
+Node FpConverter::sbvToNode(const sbv &s) const { return s; }
+// Creates the components constraint
+FpConverter::uf FpConverter::buildComponents(TNode current)
+{
+ Assert(Theory::isLeafOf(current, THEORY_FP)
+ || current.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
+
+ NodeManager *nm = NodeManager::currentNM();
+ uf tmp(nm->mkNode(kind::FLOATINGPOINT_COMPONENT_NAN, current),
+ nm->mkNode(kind::FLOATINGPOINT_COMPONENT_INF, current),
+ nm->mkNode(kind::FLOATINGPOINT_COMPONENT_ZERO, current),
+ nm->mkNode(kind::FLOATINGPOINT_COMPONENT_SIGN, current),
+ nm->mkNode(kind::FLOATINGPOINT_COMPONENT_EXPONENT, current),
+ nm->mkNode(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND, current));
+
+ d_additionalAssertions.push_back(tmp.valid(fpt(current.getType())));
-Node FpConverter::convert(TNode node) {
- Unimplemented("Conversion not implemented.");
+ return tmp;
}
+#endif
+
+// Non-convertible things should only be added to the stack at the very start,
+// thus...
+#define CVC4_FPCONV_PASSTHROUGH Assert(workStack.empty())
+
+Node FpConverter::convert(TNode node)
+{
+#ifdef CVC4_USE_SYMFPU
+ std::stack<TNode> workStack;
+ TNode result = node;
+
+ workStack.push(node);
+
+ NodeManager *nm = NodeManager::currentNM();
+
+ while (!workStack.empty())
+ {
+ TNode current = workStack.top();
+ workStack.pop();
+ result = current;
+
+ TypeNode t(current.getType());
+
+ if (t.isRoundingMode())
+ {
+ rmMap::const_iterator i(r.find(current));
+
+ if (i == r.end())
+ {
+ if (Theory::isLeafOf(current, THEORY_FP))
+ {
+ if (current.getKind() == kind::CONST_ROUNDINGMODE)
+ {
+ /******** Constants ********/
+ switch (current.getConst<RoundingMode>())
+ {
+ case roundNearestTiesToEven:
+ r.insert(current, traits::RNE());
+ break;
+ case roundNearestTiesToAway:
+ r.insert(current, traits::RNA());
+ break;
+ case roundTowardPositive: r.insert(current, traits::RTP()); break;
+ case roundTowardNegative: r.insert(current, traits::RTN()); break;
+ case roundTowardZero: r.insert(current, traits::RTZ()); break;
+ default: Unreachable("Unknown rounding mode"); break;
+ }
+ }
+ else
+ {
+ /******** Variables ********/
+ rm tmp(nm->mkNode(kind::ROUNDINGMODE_BITBLAST, current));
+ r.insert(current, tmp);
+ d_additionalAssertions.push_back(tmp.valid());
+ }
+ }
+ else
+ {
+ Unreachable("Unknown kind of type RoundingMode");
+ }
+ }
+ // Returns a rounding-mode type so don't alter the return value
+ }
+ else if (t.isFloatingPoint())
+ {
+ fpMap::const_iterator i(f.find(current));
+
+ if (i == f.end())
+ {
+ if (Theory::isLeafOf(current, THEORY_FP))
+ {
+ if (current.getKind() == kind::CONST_FLOATINGPOINT)
+ {
+ /******** Constants ********/
+ f.insert(current,
+ symfpu::unpackedFloat<traits>(
+ current.getConst<FloatingPoint>().getLiteral()));
+ }
+ else
+ {
+ /******** Variables ********/
+ f.insert(current, buildComponents(current));
+ }
+ }
+ else
+ {
+ switch (current.getKind())
+ {
+ case kind::CONST_FLOATINGPOINT:
+ case kind::VARIABLE:
+ case kind::BOUND_VARIABLE:
+ case kind::SKOLEM:
+ Unreachable("Kind should have been handled as a leaf.");
+ break;
+
+ /******** Operations ********/
+ case kind::FLOATINGPOINT_ABS:
+ case kind::FLOATINGPOINT_NEG:
+ {
+ fpMap::const_iterator arg1(f.find(current[0]));
+
+ if (arg1 == f.end())
+ {
+ workStack.push(current);
+ workStack.push(current[0]);
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_ABS:
+ f.insert(current,
+ symfpu::absolute<traits>(fpt(current.getType()),
+ (*arg1).second));
+ break;
+ case kind::FLOATINGPOINT_NEG:
+ f.insert(current,
+ symfpu::negate<traits>(fpt(current.getType()),
+ (*arg1).second));
+ break;
+ default:
+ Unreachable("Unknown unary floating-point function");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_SQRT:
+ case kind::FLOATINGPOINT_RTI:
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ fpMap::const_iterator arg1(f.find(current[1]));
+ bool recurseNeeded = (mode == r.end()) || (arg1 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg1 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_SQRT:
+ f.insert(current,
+ symfpu::sqrt<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second));
+ break;
+ case kind::FLOATINGPOINT_RTI:
+ f.insert(
+ current,
+ symfpu::roundToIntegral<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second));
+ break;
+ default:
+ Unreachable("Unknown unary rounded floating-point function");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_REM:
+ {
+ fpMap::const_iterator arg1(f.find(current[0]));
+ fpMap::const_iterator arg2(f.find(current[1]));
+ bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (arg1 == f.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg2 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ f.insert(
+ current,
+ symfpu::remainder<traits>(
+ fpt(current.getType()), (*arg1).second, (*arg2).second));
+ }
+ break;
+
+ case kind::FLOATINGPOINT_MIN_TOTAL:
+ case kind::FLOATINGPOINT_MAX_TOTAL:
+ {
+ fpMap::const_iterator arg1(f.find(current[0]));
+ fpMap::const_iterator arg2(f.find(current[1]));
+ // current[2] is a bit-vector so we do not need to recurse down it
+
+ bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (arg1 == f.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg2 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_MAX_TOTAL:
+ f.insert(current,
+ symfpu::max<traits>(fpt(current.getType()),
+ (*arg1).second,
+ (*arg2).second,
+ prop(current[2])));
+ break;
+
+ case kind::FLOATINGPOINT_MIN_TOTAL:
+ f.insert(current,
+ symfpu::min<traits>(fpt(current.getType()),
+ (*arg1).second,
+ (*arg2).second,
+ prop(current[2])));
+ break;
+
+ default:
+ Unreachable("Unknown binary floating-point partial function");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_PLUS:
+ case kind::FLOATINGPOINT_SUB:
+ case kind::FLOATINGPOINT_MULT:
+ case kind::FLOATINGPOINT_DIV:
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ fpMap::const_iterator arg1(f.find(current[1]));
+ fpMap::const_iterator arg2(f.find(current[2]));
+ bool recurseNeeded =
+ (mode == r.end()) || (arg1 == f.end()) || (arg2 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg1 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ if (arg2 == f.end())
+ {
+ workStack.push(current[2]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_PLUS:
+ f.insert(current,
+ symfpu::add<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second,
+ (*arg2).second,
+ prop(true)));
+ break;
+
+ case kind::FLOATINGPOINT_SUB:
+ // Should have been removed by the rewriter
+ Unreachable(
+ "Floating-point subtraction should be removed by the "
+ "rewriter.");
+ f.insert(current,
+ symfpu::add<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second,
+ (*arg2).second,
+ prop(false)));
+ break;
+
+ case kind::FLOATINGPOINT_MULT:
+ f.insert(current,
+ symfpu::multiply<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second,
+ (*arg2).second));
+ break;
+ case kind::FLOATINGPOINT_DIV:
+ f.insert(current,
+ symfpu::divide<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second,
+ (*arg2).second));
+ break;
+ case kind::FLOATINGPOINT_REM:
+ /*
+ f.insert(current,
+ symfpu::remainder<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second,
+ (*arg2).second));
+ */
+ Unimplemented(
+ "Remainder with rounding mode not yet supported by "
+ "SMT-LIB");
+ break;
+
+ default:
+ Unreachable("Unknown binary rounded floating-point function");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_FMA:
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ fpMap::const_iterator arg1(f.find(current[1]));
+ fpMap::const_iterator arg2(f.find(current[2]));
+ fpMap::const_iterator arg3(f.find(current[3]));
+ bool recurseNeeded = (mode == r.end()) || (arg1 == f.end())
+ || (arg2 == f.end() || (arg3 == f.end()));
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg1 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ if (arg2 == f.end())
+ {
+ workStack.push(current[2]);
+ }
+ if (arg3 == f.end())
+ {
+ workStack.push(current[3]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ f.insert(current,
+ symfpu::fma<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second,
+ (*arg2).second,
+ (*arg3).second));
+ }
+ break;
+
+ /******** Conversions ********/
+ case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ fpMap::const_iterator arg1(f.find(current[1]));
+ bool recurseNeeded = (mode == r.end()) || (arg1 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg1 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ f.insert(
+ current,
+ symfpu::convertFloatToFloat<traits>(fpt(current[1].getType()),
+ fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second));
+ }
+ break;
+
+ case kind::FLOATINGPOINT_FP:
+ {
+ Node IEEEBV(nm->mkNode(
+ kind::BITVECTOR_CONCAT, current[0], current[1], current[2]));
+ f.insert(current,
+ symfpu::unpack<traits>(fpt(current.getType()), IEEEBV));
+ }
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+ f.insert(current,
+ symfpu::unpack<traits>(fpt(current.getType()),
+ ubv(current[0])));
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+ case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ bool recurseNeeded = (mode == r.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+ f.insert(
+ current,
+ symfpu::convertSBVToFloat<traits>(fpt(current.getType()),
+ (*mode).second,
+ sbv(current[1])));
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+ f.insert(
+ current,
+ symfpu::convertUBVToFloat<traits>(fpt(current.getType()),
+ (*mode).second,
+ ubv(current[1])));
+ break;
+
+ default:
+ Unreachable(
+ "Unknown converstion from bit-vector to floating-point");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_REAL:
+ {
+ f.insert(current, buildComponents(current));
+ // Rely on the real theory and theory combination
+ // to handle the value
+ }
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_GENERIC:
+ Unreachable("Generic to_fp not removed");
+ break;
+
+ default: Unreachable("Unknown kind of type FloatingPoint"); break;
+ }
+ }
+ }
+ // Returns a floating-point type so don't alter the return value
+ }
+ else if (t.isBoolean())
+ {
+ boolMap::const_iterator i(b.find(current));
+
+ if (i == b.end())
+ {
+ switch (current.getKind())
+ {
+ /******** Comparisons ********/
+ case kind::EQUAL:
+ {
+ TypeNode childType(current[0].getType());
+
+ if (childType.isFloatingPoint())
+ {
+ fpMap::const_iterator arg1(f.find(current[0]));
+ fpMap::const_iterator arg2(f.find(current[1]));
+ bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (arg1 == f.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg2 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ b.insert(current,
+ symfpu::smtlibEqual<traits>(
+ fpt(childType), (*arg1).second, (*arg2).second));
+ }
+ else if (childType.isRoundingMode())
+ {
+ rmMap::const_iterator arg1(r.find(current[0]));
+ rmMap::const_iterator arg2(r.find(current[1]));
+ bool recurseNeeded = (arg1 == r.end()) || (arg2 == r.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (arg1 == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg2 == r.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ b.insert(current, (*arg1).second == (*arg2).second);
+ }
+ else
+ {
+ CVC4_FPCONV_PASSTHROUGH;
+ return result;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_LEQ:
+ case kind::FLOATINGPOINT_LT:
+ {
+ TypeNode childType(current[0].getType());
+
+ fpMap::const_iterator arg1(f.find(current[0]));
+ fpMap::const_iterator arg2(f.find(current[1]));
+ bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (arg1 == f.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg2 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_LEQ:
+ b.insert(current,
+ symfpu::lessThanOrEqual<traits>(
+ fpt(childType), (*arg1).second, (*arg2).second));
+ break;
+
+ case kind::FLOATINGPOINT_LT:
+ b.insert(current,
+ symfpu::lessThan<traits>(
+ fpt(childType), (*arg1).second, (*arg2).second));
+ break;
+
+ default:
+ Unreachable("Unknown binary floating-point relation");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_ISN:
+ case kind::FLOATINGPOINT_ISSN:
+ case kind::FLOATINGPOINT_ISZ:
+ case kind::FLOATINGPOINT_ISINF:
+ case kind::FLOATINGPOINT_ISNAN:
+ case kind::FLOATINGPOINT_ISNEG:
+ case kind::FLOATINGPOINT_ISPOS:
+ {
+ TypeNode childType(current[0].getType());
+ fpMap::const_iterator arg1(f.find(current[0]));
+
+ if (arg1 == f.end())
+ {
+ workStack.push(current);
+ workStack.push(current[0]);
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_ISN:
+ b.insert(
+ current,
+ symfpu::isNormal<traits>(fpt(childType), (*arg1).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISSN:
+ b.insert(current,
+ symfpu::isSubnormal<traits>(fpt(childType),
+ (*arg1).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISZ:
+ b.insert(
+ current,
+ symfpu::isZero<traits>(fpt(childType), (*arg1).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISINF:
+ b.insert(
+ current,
+ symfpu::isInfinite<traits>(fpt(childType), (*arg1).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISNAN:
+ b.insert(current,
+ symfpu::isNaN<traits>(fpt(childType), (*arg1).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISPOS:
+ b.insert(
+ current,
+ symfpu::isPositive<traits>(fpt(childType), (*arg1).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISNEG:
+ b.insert(
+ current,
+ symfpu::isNegative<traits>(fpt(childType), (*arg1).second));
+ break;
+
+ default:
+ Unreachable("Unknown unary floating-point relation");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_EQ:
+ case kind::FLOATINGPOINT_GEQ:
+ case kind::FLOATINGPOINT_GT:
+ Unreachable("Kind should have been removed by rewriter.");
+ break;
+
+ // Components will be registered as they are owned by
+ // the floating-point theory. No action is required.
+ case kind::FLOATINGPOINT_COMPONENT_NAN:
+ case kind::FLOATINGPOINT_COMPONENT_INF:
+ case kind::FLOATINGPOINT_COMPONENT_ZERO:
+ case kind::FLOATINGPOINT_COMPONENT_SIGN:
+ /* Fall through... */
+
+ default:
+ CVC4_FPCONV_PASSTHROUGH;
+ return result;
+ break;
+ }
+
+ i = b.find(current);
+ }
+
+ result = (*i).second;
+ }
+ else if (t.isBitVector())
+ {
+ switch (current.getKind())
+ {
+ /******** Conversions ********/
+ case kind::FLOATINGPOINT_TO_UBV_TOTAL:
+ {
+ TypeNode childType(current[1].getType());
+ ubvMap::const_iterator i(u.find(current));
+
+ if (i == u.end())
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ fpMap::const_iterator arg1(f.find(current[1]));
+ bool recurseNeeded = (mode == r.end()) || (arg1 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg1 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ FloatingPointToUBVTotal info =
+ current.getOperator().getConst<FloatingPointToUBVTotal>();
+
+ u.insert(current,
+ symfpu::convertFloatToUBV<traits>(fpt(childType),
+ (*mode).second,
+ (*arg1).second,
+ info.bvs,
+ ubv(current[2])));
+ i = u.find(current);
+ }
+
+ result = (*i).second;
+ }
+ break;
+
+ case kind::FLOATINGPOINT_TO_SBV_TOTAL:
+ {
+ TypeNode childType(current[1].getType());
+ sbvMap::const_iterator i(s.find(current));
+
+ if (i == s.end())
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ fpMap::const_iterator arg1(f.find(current[1]));
+ bool recurseNeeded = (mode == r.end()) || (arg1 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg1 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ FloatingPointToSBVTotal info =
+ current.getOperator().getConst<FloatingPointToSBVTotal>();
+
+ s.insert(current,
+ symfpu::convertFloatToSBV<traits>(fpt(childType),
+ (*mode).second,
+ (*arg1).second,
+ info.bvs,
+ sbv(current[2])));
+
+ i = s.find(current);
+ }
+
+ result = (*i).second;
+ }
+ break;
+
+ case kind::FLOATINGPOINT_TO_UBV:
+ Unreachable(
+ "Partially defined fp.to_ubv should have been removed by "
+ "expandDefinition");
+ break;
+
+ case kind::FLOATINGPOINT_TO_SBV:
+ Unreachable(
+ "Partially defined fp.to_sbv should have been removed by "
+ "expandDefinition");
+ break;
+
+ // Again, no action is needed
+ case kind::FLOATINGPOINT_COMPONENT_EXPONENT:
+ case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND:
+ case kind::ROUNDINGMODE_BITBLAST:
+ /* Fall through ... */
+
+ default: CVC4_FPCONV_PASSTHROUGH; break;
+ }
+ }
+ else if (t.isReal())
+ {
+ switch (current.getKind())
+ {
+ /******** Conversions ********/
+ case kind::FLOATINGPOINT_TO_REAL_TOTAL:
+ {
+ // We need to recurse so that any variables that are only
+ // used under this will have components created
+ // (via auxiliary constraints)
+
+ TypeNode childType(current[0].getType());
+ fpMap::const_iterator arg1(f.find(current[0]));
+
+ if (arg1 == f.end())
+ {
+ workStack.push(current);
+ workStack.push(current[0]);
+ continue; // i.e. recurse!
+ }
+
+ // However we don't need to do anything explicitly with
+ // this as it will be treated as an uninterpreted function
+ // by the real theory and we don't need to bit-blast the
+ // float expression unless we need to say something about
+ // its value.
+ }
+
+ break;
+
+ case kind::FLOATINGPOINT_TO_REAL:
+ Unreachable(
+ "Partially defined fp.to_real should have been removed by "
+ "expandDefinition");
+ break;
+
+ default: CVC4_FPCONV_PASSTHROUGH; break;
+ }
+ }
+ else
+ {
+ CVC4_FPCONV_PASSTHROUGH;
+ }
+ }
+
+ return result;
+#else
+ Unimplemented("Conversion is dependent on SymFPU");
+#endif
+}
+
+#undef CVC4_FPCONV_PASSTHROUGH
+
+Node FpConverter::getValue(Valuation &val, TNode var)
+{
+ Assert(Theory::isLeafOf(var, THEORY_FP));
+
+#ifdef CVC4_USE_SYMFPU
+ TypeNode t(var.getType());
+
+ if (t.isRoundingMode())
+ {
+ rmMap::const_iterator i(r.find(var));
+
+ if (i == r.end())
+ {
+ Unreachable("Asking for the value of an unregistered expression");
+ }
+ else
+ {
+ Node value = rmToNode((*i).second);
+ return value;
+ }
+ }
+ else if (t.isFloatingPoint())
+ {
+ fpMap::const_iterator i(f.find(var));
+
+ if (i == f.end())
+ {
+ Unreachable("Asking for the value of an unregistered expression");
+ }
+ else
+ {
+ Node value = ufToNode(fpt(t), (*i).second);
+ return value;
+ }
+ }
+ else
+ {
+ Unreachable(
+ "Asking for the value of a type that is not managed by the "
+ "floating-point theory");
+ }
+
+ Unreachable("Unable to find value");
+
+#else
+ Unimplemented("Conversion is dependent on SymFPU");
+#endif
-Node FpConverter::getValue(Valuation &val, TNode var) {
- Unimplemented("Conversion not implemented.");
+ return Node::null();
}
} // namespace fp
#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 {
TypeNodeHashFunction>
PairTypeNodeHashFunction;
-class FpConverter {
+/**
+ * This is a symfpu symbolic "back-end". It allows the library to be used to
+ * construct bit-vector expressions that compute floating-point operations.
+ * This is effectively the glue between symfpu's notion of "signed bit-vector"
+ * and CVC4's node.
+ */
+namespace symfpuSymbolic {
+
+// Forward declarations of the wrapped types so that traits can be defined early
+// and used in the implementations
+class symbolicRoundingMode;
+class floatingPointTypeInfo;
+class symbolicProposition;
+template <bool T>
+class symbolicBitVector;
+
+// This is the template parameter for symfpu's templates.
+class traits
+{
+ public:
+ // The six key types that symfpu uses.
+ typedef unsigned bwt;
+ typedef symbolicRoundingMode rm;
+ typedef floatingPointTypeInfo fpt;
+ typedef symbolicProposition prop;
+ typedef symbolicBitVector<true> sbv;
+ typedef symbolicBitVector<false> ubv;
+
+ // Give concrete instances (wrapped nodes) for each rounding mode.
+ static symbolicRoundingMode RNE(void);
+ static symbolicRoundingMode RNA(void);
+ static symbolicRoundingMode RTP(void);
+ static symbolicRoundingMode RTN(void);
+ static symbolicRoundingMode RTZ(void);
+
+ // Properties used by symfpu
+ static void precondition(const bool b);
+ static void postcondition(const bool b);
+ static void invariant(const bool b);
+ static void precondition(const prop &p);
+ static void postcondition(const prop &p);
+ static void invariant(const prop &p);
+};
+
+// Use the same type names as symfpu.
+typedef traits::bwt bwt;
+
+/**
+ * Wrap the CVC4::Node types so that we can debug issues with this back-end
+ */
+class nodeWrapper : public Node
+{
+ protected:
+/* CVC4_SYM_SYMBOLIC_EVAL is for debugging CVC4 symbolic back-end issues.
+ * Enable this and disabling constant folding will mean that operations
+ * that are input with constant args are 'folded' using the symbolic encoding
+ * allowing them to be traced via GDB.
+ */
+#ifdef CVC4_SYM_SYMBOLIC_EVAL
+ nodeWrapper(const Node &n) : Node(theory::Rewriter::rewrite(n)) {}
+#else
+ nodeWrapper(const Node &n) : Node(n) {}
+#endif
+};
+
+class symbolicProposition : public nodeWrapper
+{
+ protected:
+ bool checkNodeType(const TNode node);
+
+#ifdef CVC4_USE_SYMFPU
+ friend ::symfpu::ite<symbolicProposition, symbolicProposition>; // For ITE
+#endif
+
+ public:
+ symbolicProposition(const Node n);
+ symbolicProposition(bool v);
+ symbolicProposition(const symbolicProposition &old);
+
+ symbolicProposition operator!(void)const;
+ symbolicProposition operator&&(const symbolicProposition &op) const;
+ symbolicProposition operator||(const symbolicProposition &op) const;
+ symbolicProposition operator==(const symbolicProposition &op) const;
+ symbolicProposition operator^(const symbolicProposition &op) const;
+};
+
+class symbolicRoundingMode : public nodeWrapper
+{
+ protected:
+ bool checkNodeType(const TNode n);
+
+#ifdef CVC4_USE_SYMFPU
+ friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>; // For ITE
+#endif
+
+ public:
+ symbolicRoundingMode(const Node n);
+ symbolicRoundingMode(const unsigned v);
+ symbolicRoundingMode(const symbolicRoundingMode &old);
+
+ symbolicProposition valid(void) const;
+ symbolicProposition operator==(const symbolicRoundingMode &op) const;
+};
+
+// Type function for mapping between types
+template <bool T>
+struct signedToLiteralType;
+
+template <>
+struct signedToLiteralType<true>
+{
+ typedef int literalType;
+};
+template <>
+struct signedToLiteralType<false>
+{
+ typedef unsigned int literalType;
+};
+
+template <bool isSigned>
+class symbolicBitVector : public nodeWrapper
+{
+ protected:
+ typedef typename signedToLiteralType<isSigned>::literalType literalType;
+
+ Node boolNodeToBV(Node node) const;
+ Node BVToBoolNode(Node node) const;
+
+ Node fromProposition(Node node) const;
+ Node toProposition(Node node) const;
+ bool checkNodeType(const TNode n);
+ friend symbolicBitVector<!isSigned>; // To allow conversion between the types
+
+#ifdef CVC4_USE_SYMFPU
+ friend ::symfpu::ite<symbolicProposition,
+ symbolicBitVector<isSigned> >; // For ITE
+#endif
+
+ public:
+ symbolicBitVector(const Node n);
+ symbolicBitVector(const bwt w, const unsigned v);
+ symbolicBitVector(const symbolicProposition &p);
+ symbolicBitVector(const symbolicBitVector<isSigned> &old);
+ symbolicBitVector(const BitVector &old);
+
+ bwt getWidth(void) const;
+
+ /*** Constant creation and test ***/
+ static symbolicBitVector<isSigned> one(const bwt &w);
+ static symbolicBitVector<isSigned> zero(const bwt &w);
+ static symbolicBitVector<isSigned> allOnes(const bwt &w);
+
+ symbolicProposition isAllOnes() const;
+ symbolicProposition isAllZeros() const;
+
+ static symbolicBitVector<isSigned> maxValue(const bwt &w);
+ static symbolicBitVector<isSigned> minValue(const bwt &w);
+
+ /*** Operators ***/
+ symbolicBitVector<isSigned> operator<<(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator>>(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator|(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator&(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator+(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator-(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator*(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator/(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator%(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator-(void) const;
+ symbolicBitVector<isSigned> operator~(void)const;
+ symbolicBitVector<isSigned> increment() const;
+ symbolicBitVector<isSigned> decrement() const;
+ symbolicBitVector<isSigned> signExtendRightShift(
+ const symbolicBitVector<isSigned> &op) const;
+
+ /*** Modular operations ***/
+ // This back-end doesn't do any overflow checking so these are the same as
+ // other operations
+ symbolicBitVector<isSigned> modularLeftShift(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> modularRightShift(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> modularIncrement() const;
+ symbolicBitVector<isSigned> modularDecrement() const;
+ symbolicBitVector<isSigned> modularAdd(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> modularNegate() const;
+
+ /*** Comparisons ***/
+ symbolicProposition operator==(const symbolicBitVector<isSigned> &op) const;
+ symbolicProposition operator<=(const symbolicBitVector<isSigned> &op) const;
+ symbolicProposition operator>=(const symbolicBitVector<isSigned> &op) const;
+ symbolicProposition operator<(const symbolicBitVector<isSigned> &op) const;
+ symbolicProposition operator>(const symbolicBitVector<isSigned> &op) const;
+
+ /*** Type conversion ***/
+ // CVC4 nodes make no distinction between signed and unsigned, thus these are
+ // trivial
+ symbolicBitVector<true> toSigned(void) const;
+ symbolicBitVector<false> toUnsigned(void) const;
+
+ /*** Bit hacks ***/
+ symbolicBitVector<isSigned> extend(bwt extension) const;
+ symbolicBitVector<isSigned> contract(bwt reduction) const;
+ symbolicBitVector<isSigned> resize(bwt newSize) const;
+ symbolicBitVector<isSigned> matchWidth(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> append(
+ const symbolicBitVector<isSigned> &op) const;
+
+ // Inclusive of end points, thus if the same, extracts just one bit
+ symbolicBitVector<isSigned> extract(bwt upper, bwt lower) const;
+};
+
+// Use the same type information as the literal back-end but add an interface to
+// TypeNodes for convenience.
+class floatingPointTypeInfo : public FloatingPointSize
+{
+ public:
+ floatingPointTypeInfo(const TypeNode t);
+ floatingPointTypeInfo(unsigned exp, unsigned sig);
+ floatingPointTypeInfo(const floatingPointTypeInfo &old);
+
+ TypeNode getTypeNode(void) const;
+};
+}
+
+/**
+ * This class uses SymFPU to convert an expression containing floating-point
+ * kinds and operations into a logically equivalent form with bit-vector
+ * operations replacing the floating-point ones. It also has a getValue method
+ * to produce an expression which will reconstruct the value of the
+ * floating-point terms from a valuation.
+ *
+ * Internally it caches all of the unpacked floats so that unnecessary packing
+ * and unpacking operations are avoided and to make best use of structural
+ * sharing.
+ */
+class FpConverter
+{
+ protected:
+#ifdef CVC4_USE_SYMFPU
+ typedef symfpuSymbolic::traits traits;
+ typedef ::symfpu::unpackedFloat<symfpuSymbolic::traits> uf;
+ typedef symfpuSymbolic::traits::rm rm;
+ typedef symfpuSymbolic::traits::fpt fpt;
+ typedef symfpuSymbolic::traits::prop prop;
+ typedef symfpuSymbolic::traits::ubv ubv;
+ typedef symfpuSymbolic::traits::sbv sbv;
+
+ typedef context::CDHashMap<Node, uf, NodeHashFunction> fpMap;
+ typedef context::CDHashMap<Node, rm, NodeHashFunction> rmMap;
+ typedef context::CDHashMap<Node, prop, NodeHashFunction> boolMap;
+ typedef context::CDHashMap<Node, ubv, NodeHashFunction> ubvMap;
+ typedef context::CDHashMap<Node, sbv, NodeHashFunction> sbvMap;
+
+ fpMap f;
+ rmMap r;
+ boolMap b;
+ ubvMap u;
+ sbvMap s;
+
+ /* These functions take a symfpu object and convert it to a node.
+ * These should ensure that constant folding it will give a
+ * constant of the right type.
+ */
+
+ Node ufToNode(const fpt &, const uf &) const;
+ Node rmToNode(const rm &) const;
+ Node propToNode(const prop &) const;
+ Node ubvToNode(const ubv &) const;
+ Node sbvToNode(const sbv &) const;
+
+ /* Creates the relevant components for a variable */
+ uf buildComponents(TNode current);
+#endif
+
public:
context::CDList<Node> d_additionalAssertions;
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
**/
#include "theory/fp/theory_fp.h"
+#include "theory/rewriter.h"
#include "theory/theory_model.h"
#include <set>
} // 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),
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);
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) {
std::vector<TypeNode> args(1);
args[0] = t;
fun = nm->mkSkolem("floatingpoint_to_real_infinity_and_NaN_case",
- nm->mkFunctionType(t, nm->realType()),
+ nm->mkFunctionType(args, nm->realType()),
"floatingpoint_to_real_infinity_and_NaN_case",
NodeManager::SKOLEM_EXACT_NAME);
d_toRealMap.insert(t, fun);
return nm->mkNode(kind::APPLY_UF, fun, node[0]);
}
-Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) {
- Trace("fp-expandDefinition")
- << "TheoryFp::expandDefinition(): " << node << std::endl;
-
+void TheoryFp::enableUF(LogicRequest &lr)
+{
if (!this->d_expansionRequested) {
- lr.widenLogic(
- THEORY_UF); // Needed for conversions to/from real and min/max
- lr.widenLogic(THEORY_BV);
+ // Needed for conversions to/from real and min/max
+ lr.widenLogic(THEORY_UF);
+ // THEORY_BV has to be enabled when the logic is set
this->d_expansionRequested = true;
}
+ return;
+}
+
+Node TheoryFp::abstractRealToFloat(Node node)
+{
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
+ TypeNode t(node.getType());
+ Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ NodeManager *nm = NodeManager::currentNM();
+ ComparisonUFMap::const_iterator i(realToFloatMap.find(t));
+
+ Node fun;
+ if (i == realToFloatMap.end())
+ {
+ std::vector<TypeNode> args(2);
+ args[0] = node[0].getType();
+ args[1] = node[1].getType();
+ fun = nm->mkSkolem("floatingpoint_abstract_real_to_float",
+ nm->mkFunctionType(args, node.getType()),
+ "floatingpoint_abstract_real_to_float",
+ NodeManager::SKOLEM_EXACT_NAME);
+ realToFloatMap.insert(t, fun);
+ }
+ else
+ {
+ fun = (*i).second;
+ }
+ Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
+
+ abstractionMap.insert(uf, node);
+
+ return uf;
+}
+
+Node TheoryFp::abstractFloatToReal(Node node)
+{
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL);
+ TypeNode t(node[0].getType());
+ Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ NodeManager *nm = NodeManager::currentNM();
+ ComparisonUFMap::const_iterator i(floatToRealMap.find(t));
+
+ Node fun;
+ if (i == floatToRealMap.end())
+ {
+ std::vector<TypeNode> args(2);
+ args[0] = t;
+ args[1] = nm->realType();
+ fun = nm->mkSkolem("floatingpoint_abstract_float_to_real",
+ nm->mkFunctionType(args, nm->realType()),
+ "floatingpoint_abstract_float_to_real",
+ NodeManager::SKOLEM_EXACT_NAME);
+ floatToRealMap.insert(t, fun);
+ }
+ else
+ {
+ fun = (*i).second;
+ }
+ Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
+
+ abstractionMap.insert(uf, node);
+
+ return uf;
+}
+
+Node TheoryFp::expandDefinition(LogicRequest &lr, Node node)
+{
+ Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
+ << std::endl;
Node res = node;
res = removeToFPGeneric::removeToFPGeneric(node);
} else if (node.getKind() == kind::FLOATINGPOINT_MIN) {
+ enableUF(lr);
res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MIN_TOTAL,
node[0], node[1], minUF(node));
} else if (node.getKind() == kind::FLOATINGPOINT_MAX) {
+ enableUF(lr);
res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MAX_TOTAL,
node[0], node[1], maxUF(node));
} else if (node.getKind() == kind::FLOATINGPOINT_TO_UBV) {
+ enableUF(lr);
FloatingPointToUBV info = node.getOperator().getConst<FloatingPointToUBV>();
FloatingPointToUBVTotal newInfo(info);
toUBVUF(node));
} else if (node.getKind() == kind::FLOATINGPOINT_TO_SBV) {
+ enableUF(lr);
FloatingPointToSBV info = node.getOperator().getConst<FloatingPointToSBV>();
FloatingPointToSBVTotal newInfo(info);
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));
// 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;
return res;
}
+Node TheoryFp::ppRewrite(TNode node)
+{
+ Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl;
+
+ Node res = node;
+
+ // Abstract conversion functions
+ if (node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL)
+ {
+ res = abstractFloatToReal(node);
+
+ // Generate some lemmas
+ NodeManager *nm = NodeManager::currentNM();
+
+ Node pd =
+ nm->mkNode(kind::IMPLIES,
+ nm->mkNode(kind::OR,
+ nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]),
+ nm->mkNode(kind::FLOATINGPOINT_ISINF, node[0])),
+ nm->mkNode(kind::EQUAL, res, node[1]));
+ handleLemma(pd);
+
+ Node z =
+ nm->mkNode(kind::IMPLIES,
+ nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]),
+ nm->mkNode(kind::EQUAL, res, nm->mkConst(Rational(0U))));
+ handleLemma(z);
+
+ // TODO : bounds on the output from largest floats, #1914
+ }
+ else if (node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL)
+ {
+ res = abstractRealToFloat(node);
+
+ // Generate some lemmas
+ NodeManager *nm = NodeManager::currentNM();
+
+ Node nnan =
+ nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, res));
+ handleLemma(nnan);
+
+ Node z = nm->mkNode(
+ kind::IMPLIES,
+ nm->mkNode(kind::EQUAL, node[1], nm->mkConst(Rational(0U))),
+ nm->mkNode(kind::EQUAL,
+ res,
+ nm->mkConst(FloatingPoint::makeZero(
+ res.getType().getConst<FloatingPointSize>(), false))));
+ handleLemma(z);
+
+ // TODO : rounding-mode specific bounds on floats that don't give infinity
+ // BEWARE of directed rounding! #1914
+ }
+
+ if (res != node)
+ {
+ Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): node " << node
+ << " rewritten to " << res << std::endl;
+ }
+
+ return res;
+}
+
+bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
+{
+ Trace("fp-refineAbstraction") << "TheoryFp::refineAbstraction(): " << abstract
+ << " vs. " << concrete << std::endl;
+ Kind k = concrete.getKind();
+ if (k == kind::FLOATINGPOINT_TO_REAL_TOTAL)
+ {
+ // Get the values
+ Assert(m->hasTerm(abstract));
+ Assert(m->hasTerm(concrete[0]));
+ Assert(m->hasTerm(concrete[1]));
+
+ Node abstractValue = m->getValue(abstract);
+ Node floatValue = m->getValue(concrete[0]);
+ Node undefValue = m->getValue(concrete[1]);
+
+ Assert(abstractValue.isConst());
+ Assert(floatValue.isConst());
+ Assert(undefValue.isConst());
+
+ // Work out the actual value for those args
+ NodeManager *nm = NodeManager::currentNM();
+
+ Node evaluate =
+ nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL, floatValue, undefValue);
+ Node concreteValue = Rewriter::rewrite(evaluate);
+ Assert(concreteValue.isConst());
+
+ Trace("fp-refineAbstraction")
+ << "TheoryFp::refineAbstraction(): " << concrete[0] << " = "
+ << floatValue << std::endl
+ << "TheoryFp::refineAbstraction(): " << concrete[1] << " = "
+ << undefValue << std::endl
+ << "TheoryFp::refineAbstraction(): " << abstract << " = "
+ << abstractValue << std::endl
+ << "TheoryFp::refineAbstraction(): " << concrete << " = "
+ << concreteValue << std::endl;
+
+ if (abstractValue != concreteValue)
+ {
+ // Need refinement lemmas
+ // only in the normal and subnormal case
+ Assert(floatValue.getConst<FloatingPoint>().isNormal()
+ || floatValue.getConst<FloatingPoint>().isSubnormal());
+
+ Node defined = nm->mkNode(
+ kind::AND,
+ nm->mkNode(kind::NOT,
+ nm->mkNode(kind::FLOATINGPOINT_ISNAN, concrete[0])),
+ nm->mkNode(kind::NOT,
+ nm->mkNode(kind::FLOATINGPOINT_ISINF, concrete[0])));
+ // First the "forward" constraints
+ Node fg = nm->mkNode(
+ kind::IMPLIES,
+ defined,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(kind::FLOATINGPOINT_GEQ, concrete[0], floatValue),
+ nm->mkNode(kind::GEQ, abstract, concreteValue)));
+ handleLemma(fg);
+
+ Node fl = nm->mkNode(
+ kind::IMPLIES,
+ defined,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(kind::FLOATINGPOINT_LEQ, concrete[0], floatValue),
+ nm->mkNode(kind::LEQ, abstract, concreteValue)));
+ handleLemma(fl);
+
+ // Then the backwards constraints
+ Node floatAboveAbstract = Rewriter::rewrite(
+ nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
+ nm->mkConst(FloatingPointToFPReal(
+ concrete[0].getType().getConst<FloatingPointSize>())),
+ nm->mkConst(roundTowardPositive),
+ abstractValue));
+
+ Node bg = nm->mkNode(
+ kind::IMPLIES,
+ defined,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(
+ kind::FLOATINGPOINT_GEQ, concrete[0], floatAboveAbstract),
+ nm->mkNode(kind::GEQ, abstract, abstractValue)));
+ handleLemma(bg);
+
+ Node floatBelowAbstract = Rewriter::rewrite(
+ nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
+ nm->mkConst(FloatingPointToFPReal(
+ concrete[0].getType().getConst<FloatingPointSize>())),
+ nm->mkConst(roundTowardNegative),
+ abstractValue));
+
+ Node bl = nm->mkNode(
+ kind::IMPLIES,
+ defined,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(
+ kind::FLOATINGPOINT_LEQ, concrete[0], floatBelowAbstract),
+ nm->mkNode(kind::LEQ, abstract, abstractValue)));
+ handleLemma(bl);
+ // TODO : see if the overflow conditions could be improved #1914
+
+ return true;
+ }
+ else
+ {
+ // No refinement needed
+ return false;
+ }
+ }
+ else if (k == kind::FLOATINGPOINT_TO_FP_REAL)
+ {
+ // Get the values
+ Assert(m->hasTerm(abstract));
+ Assert(m->hasTerm(concrete[0]));
+ Assert(m->hasTerm(concrete[1]));
+
+ Node abstractValue = m->getValue(abstract);
+ Node rmValue = m->getValue(concrete[0]);
+ Node realValue = m->getValue(concrete[1]);
+
+ Assert(abstractValue.isConst());
+ Assert(rmValue.isConst());
+ Assert(realValue.isConst());
+
+ // Work out the actual value for those args
+ NodeManager *nm = NodeManager::currentNM();
+
+ Node evaluate =
+ nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
+ nm->mkConst(FloatingPointToFPReal(
+ concrete.getType().getConst<FloatingPointSize>())),
+ rmValue,
+ realValue);
+ Node concreteValue = Rewriter::rewrite(evaluate);
+ Assert(concreteValue.isConst());
+
+ Trace("fp-refineAbstraction")
+ << "TheoryFp::refineAbstraction(): " << concrete[0] << " = " << rmValue
+ << std::endl
+ << "TheoryFp::refineAbstraction(): " << concrete[1] << " = "
+ << realValue << std::endl
+ << "TheoryFp::refineAbstraction(): " << abstract << " = "
+ << abstractValue << std::endl
+ << "TheoryFp::refineAbstraction(): " << concrete << " = "
+ << concreteValue << std::endl;
+
+ if (abstractValue != concreteValue)
+ {
+ Assert(!abstractValue.getConst<FloatingPoint>().isNaN());
+ Assert(!concreteValue.getConst<FloatingPoint>().isNaN());
+
+ Node correctRoundingMode = nm->mkNode(kind::EQUAL, concrete[0], rmValue);
+ // TODO : Generalise to all rounding modes #1914
+
+ // First the "forward" constraints
+ Node fg = nm->mkNode(
+ kind::IMPLIES,
+ correctRoundingMode,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(kind::GEQ, concrete[1], realValue),
+ nm->mkNode(kind::FLOATINGPOINT_GEQ, abstract, concreteValue)));
+ handleLemma(fg);
+
+ Node fl = nm->mkNode(
+ kind::IMPLIES,
+ correctRoundingMode,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(kind::LEQ, concrete[1], realValue),
+ nm->mkNode(kind::FLOATINGPOINT_LEQ, abstract, concreteValue)));
+ handleLemma(fl);
+
+ // Then the backwards constraints
+ if (!abstractValue.getConst<FloatingPoint>().isInfinite())
+ {
+ Node realValueOfAbstract =
+ Rewriter::rewrite(nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL,
+ abstractValue,
+ nm->mkConst(Rational(0U))));
+
+ Node bg = nm->mkNode(
+ kind::IMPLIES,
+ correctRoundingMode,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(kind::GEQ, concrete[1], realValueOfAbstract),
+ nm->mkNode(kind::FLOATINGPOINT_GEQ, abstract, abstractValue)));
+ handleLemma(bg);
+
+ Node bl = nm->mkNode(
+ kind::IMPLIES,
+ correctRoundingMode,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(kind::LEQ, concrete[1], realValueOfAbstract),
+ nm->mkNode(kind::FLOATINGPOINT_LEQ, abstract, abstractValue)));
+ handleLemma(bl);
+ }
+
+ return true;
+ }
+ else
+ {
+ // No refinement needed
+ return false;
+ }
+ }
+ else
+ {
+ Unreachable("Unknown abstraction");
+ }
+
+ return false;
+}
+
void TheoryFp::convertAndEquateTerm(TNode node) {
Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl;
size_t oldAdditionalAssertions = d_conv.d_additionalAssertions.size();
d_equalityEngine.addTerm(node);
}
+ // Give the expansion of classifications in terms of equalities
+ // This should make equality reasoning slightly more powerful.
+ if ((node.getKind() == kind::FLOATINGPOINT_ISNAN)
+ || (node.getKind() == kind::FLOATINGPOINT_ISZ)
+ || (node.getKind() == kind::FLOATINGPOINT_ISINF))
+ {
+ NodeManager *nm = NodeManager::currentNM();
+ FloatingPointSize s = node[0].getType().getConst<FloatingPointSize>();
+ Node equalityAlias = Node::null();
+
+ if (node.getKind() == kind::FLOATINGPOINT_ISNAN)
+ {
+ equalityAlias = nm->mkNode(
+ kind::EQUAL, node[0], nm->mkConst(FloatingPoint::makeNaN(s)));
+ }
+ else if (node.getKind() == kind::FLOATINGPOINT_ISZ)
+ {
+ equalityAlias = nm->mkNode(
+ kind::OR,
+ nm->mkNode(kind::EQUAL,
+ node[0],
+ nm->mkConst(FloatingPoint::makeZero(s, true))),
+ nm->mkNode(kind::EQUAL,
+ node[0],
+ nm->mkConst(FloatingPoint::makeZero(s, false))));
+ }
+ else if (node.getKind() == kind::FLOATINGPOINT_ISINF)
+ {
+ equalityAlias = nm->mkNode(
+ kind::OR,
+ nm->mkNode(kind::EQUAL,
+ node[0],
+ nm->mkConst(FloatingPoint::makeInf(s, true))),
+ nm->mkNode(kind::EQUAL,
+ node[0],
+ nm->mkConst(FloatingPoint::makeInf(s, false))));
+ }
+ else
+ {
+ Unreachable("Only isNaN, isInf and isZero have aliases");
+ }
+
+ handleLemma(nm->mkNode(kind::EQUAL, node, equalityAlias));
+ }
+
+ // Use symfpu to produce an equivalent bit-vector statement
convertAndEquateTerm(node);
}
return;
}
}
+ // 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 */
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;
context::CDO<Node> d_conflictNode;
/** Uninterpretted functions for partially defined functions. **/
+ void enableUF(LogicRequest& lr);
+
typedef context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>
ComparisonUFMap;
ComparisonUFMap d_toRealMap;
Node toRealUF(Node);
+
+ /** Uninterpretted functions for lazy handling of conversions */
+ typedef ComparisonUFMap conversionAbstractionMap;
+
+ conversionAbstractionMap realToFloatMap;
+ conversionAbstractionMap floatToRealMap;
+
+ Node abstractRealToFloat(Node);
+ Node abstractFloatToReal(Node);
+
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> abstractionMapType;
+ abstractionMapType abstractionMap; // abstract -> original
+
+ bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
+
}; /* class TheoryFp */
} // namespace fp
#include <algorithm>
#include "base/cvc4_assert.h"
+#include "theory/fp/fp_converter.h"
#include "theory/fp/theory_fp_rewriter.h"
namespace CVC4 {
}
}
+ RewriteResponse componentFlag(TNode node, bool)
+ {
+ Kind k = node.getKind();
+
+ Assert((k == kind::FLOATINGPOINT_COMPONENT_NAN)
+ || (k == kind::FLOATINGPOINT_COMPONENT_INF)
+ || (k == kind::FLOATINGPOINT_COMPONENT_ZERO)
+ || (k == kind::FLOATINGPOINT_COMPONENT_SIGN));
+
+ FloatingPoint arg0(node[0].getConst<FloatingPoint>());
+
+ bool result;
+ switch (k)
+ {
+#ifdef CVC4_USE_SYMFPU
+ case kind::FLOATINGPOINT_COMPONENT_NAN:
+ result = arg0.getLiteral().nan;
+ break;
+ case kind::FLOATINGPOINT_COMPONENT_INF:
+ result = arg0.getLiteral().inf;
+ break;
+ case kind::FLOATINGPOINT_COMPONENT_ZERO:
+ result = arg0.getLiteral().zero;
+ break;
+ case kind::FLOATINGPOINT_COMPONENT_SIGN:
+ result = arg0.getLiteral().sign;
+ break;
+#endif
+ default: Unreachable("Unknown kind used in componentFlag"); break;
+ }
+
+ BitVector res(1U, (result) ? 1U : 0U);
+
+ return RewriteResponse(REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(res));
+ }
+
+ RewriteResponse componentExponent(TNode node, bool)
+ {
+ Assert(node.getKind() == kind::FLOATINGPOINT_COMPONENT_EXPONENT);
+
+ FloatingPoint arg0(node[0].getConst<FloatingPoint>());
+
+ // \todo Add a proper interface for this sort of thing to FloatingPoint #1915
+ return RewriteResponse(
+ REWRITE_DONE,
+#ifdef CVC4_USE_SYMFPU
+ NodeManager::currentNM()->mkConst((BitVector)arg0.getLiteral().exponent)
+#else
+ node
+#endif
+ );
+ }
+
+ RewriteResponse componentSignificand(TNode node, bool)
+ {
+ Assert(node.getKind() == kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND);
+
+ FloatingPoint arg0(node[0].getConst<FloatingPoint>());
+
+ return RewriteResponse(REWRITE_DONE,
+#ifdef CVC4_USE_SYMFPU
+ NodeManager::currentNM()->mkConst(
+ (BitVector)arg0.getLiteral().significand)
+#else
+ node
+#endif
+ );
+ }
+
+ RewriteResponse roundingModeBitBlast(TNode node, bool)
+ {
+ Assert(node.getKind() == kind::ROUNDINGMODE_BITBLAST);
+
+ RoundingMode arg0(node[0].getConst<RoundingMode>());
+ BitVector value;
+
+#ifdef CVC4_USE_SYMFPU
+ /* \todo fix the numbering of rounding modes so this doesn't need
+ * to call symfpu at all and remove the dependency on fp_converter.h #1915 */
+ switch (arg0)
+ {
+ case roundNearestTiesToEven:
+ value = symfpuSymbolic::traits::RNE().getConst<BitVector>();
+ break;
+
+ case roundNearestTiesToAway:
+ value = symfpuSymbolic::traits::RNA().getConst<BitVector>();
+ break;
+
+ case roundTowardPositive:
+ value = symfpuSymbolic::traits::RTP().getConst<BitVector>();
+ break;
+
+ case roundTowardNegative:
+ value = symfpuSymbolic::traits::RTN().getConst<BitVector>();
+ break;
+
+ case roundTowardZero:
+ value = symfpuSymbolic::traits::RTZ().getConst<BitVector>();
+ break;
+
+ default:
+ Unreachable("Unknown rounding mode in roundingModeBitBlast");
+ break;
+ }
+#else
+ value = BitVector(5U, 0U);
+#endif
+ return RewriteResponse(REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(value));
+ }
}; /* CVC4::theory::fp::constantFold */
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 */
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 */
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;
+
}
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));
#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
}
};
+class FloatingPointComponentBit
+{
+ public:
+ inline static TypeNode computeType(
+ NodeManager* nodeManager,
+ TNode n,
+ bool check) throw(TypeCheckingExceptionPrivate, AssertionException)
+ {
+ TRACE("FloatingPointComponentBit");
+
+ if (check)
+ {
+ TypeNode operandType = n[0].getType(check);
+
+ if (!operandType.isFloatingPoint())
+ {
+ throw TypeCheckingExceptionPrivate(n,
+ "floating-point bit component "
+ "applied to a non floating-point "
+ "sort");
+ }
+ if (!(Theory::isLeafOf(n[0], THEORY_FP)
+ || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
+ {
+ throw TypeCheckingExceptionPrivate(n,
+ "floating-point bit component "
+ "applied to a non leaf / to_fp leaf "
+ "node");
+ }
+ }
+
+ return nodeManager->mkBitVectorType(1);
+ }
+};
+
+class FloatingPointComponentExponent
+{
+ public:
+ inline static TypeNode computeType(
+ NodeManager* nodeManager,
+ TNode n,
+ bool check) throw(TypeCheckingExceptionPrivate, AssertionException)
+ {
+ TRACE("FloatingPointComponentExponent");
+
+ TypeNode operandType = n[0].getType(check);
+
+ if (check)
+ {
+ if (!operandType.isFloatingPoint())
+ {
+ throw TypeCheckingExceptionPrivate(n,
+ "floating-point exponent component "
+ "applied to a non floating-point "
+ "sort");
+ }
+ if (!(Theory::isLeafOf(n[0], THEORY_FP)
+ || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
+ {
+ throw TypeCheckingExceptionPrivate(n,
+ "floating-point exponent component "
+ "applied to a non leaf / to_fp "
+ "node");
+ }
+ }
+
+#ifdef CVC4_USE_SYMFPU
+ /* Need to create some symfpu objects as the size of bit-vector
+ * that is needed for this component is dependent on the encoding
+ * used (i.e. whether subnormals are forcibly normalised or not).
+ * Here we use types from floatingpoint.h which are the literal
+ * back-end but it should't make a difference. */
+ FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
+ symfpuLiteral::fpt format(fps); // The symfpu interface to type info
+ unsigned bw = FloatingPointLiteral::exponentWidth(format);
+#else
+ unsigned bw = 2;
+#endif
+
+ return nodeManager->mkBitVectorType(bw);
+ }
+};
+
+class FloatingPointComponentSignificand
+{
+ public:
+ inline static TypeNode computeType(
+ NodeManager* nodeManager,
+ TNode n,
+ bool check) throw(TypeCheckingExceptionPrivate, AssertionException)
+ {
+ TRACE("FloatingPointComponentSignificand");
+
+ TypeNode operandType = n[0].getType(check);
+
+ if (check)
+ {
+ if (!operandType.isFloatingPoint())
+ {
+ throw TypeCheckingExceptionPrivate(n,
+ "floating-point significand "
+ "component applied to a non "
+ "floating-point sort");
+ }
+ if (!(Theory::isLeafOf(n[0], THEORY_FP)
+ || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
+ {
+ throw TypeCheckingExceptionPrivate(n,
+ "floating-point significand "
+ "component applied to a non leaf / "
+ "to_fp node");
+ }
+ }
+
+#ifdef CVC4_USE_SYMFPU
+ /* As before we need to use some of sympfu. */
+ FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
+ symfpuLiteral::fpt format(fps);
+ unsigned bw = FloatingPointLiteral::significandWidth(format);
+#else
+ unsigned bw = 1;
+#endif
+
+ return nodeManager->mkBitVectorType(bw);
+ }
+};
+
+class RoundingModeBitBlast
+{
+ public:
+ inline static TypeNode computeType(
+ NodeManager* nodeManager,
+ TNode n,
+ bool check) throw(TypeCheckingExceptionPrivate, AssertionException)
+ {
+ TRACE("RoundingModeBitBlast");
+
+ if (check)
+ {
+ TypeNode operandType = n[0].getType(check);
+
+ if (!operandType.isRoundingMode())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "rounding mode bit-blast applied to a non rounding-mode sort");
+ }
+ if (!Theory::isLeafOf(n[0], THEORY_FP))
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "rounding mode bit-blast applied to a non leaf node");
+ }
+ }
+
+#ifdef CVC4_USE_SYMFPU
+ /* Uses sympfu for the macro. */
+ return nodeManager->mkBitVectorType(SYMFPU_NUMBER_OF_ROUNDING_MODES);
+#else
+ return nodeManager->mkBitVectorType(5);
+#endif
+ }
+};
class CardinalityComputer {
public:
}
}
}
+
+ 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(): ";
**/
#include "util/floatingpoint.h"
-
#include "base/cvc4_assert.h"
+#include "util/integer.h"
+
+#include <math.h>
+
+#ifdef CVC4_USE_SYMFPU
+#include "symfpu/core/add.h"
+#include "symfpu/core/classify.h"
+#include "symfpu/core/compare.h"
+#include "symfpu/core/convert.h"
+#include "symfpu/core/divide.h"
+#include "symfpu/core/fma.h"
+#include "symfpu/core/ite.h"
+#include "symfpu/core/multiply.h"
+#include "symfpu/core/packing.h"
+#include "symfpu/core/remainder.h"
+#include "symfpu/core/sign.h"
+#include "symfpu/core/sqrt.h"
+#include "symfpu/utils/numberOfRoundingModes.h"
+#include "symfpu/utils/properties.h"
+#endif
+
+#ifdef CVC4_USE_SYMFPU
+namespace symfpu {
+
+#define CVC4_LIT_ITE_DFN(T) \
+ template <> \
+ struct ite<::CVC4::symfpuLiteral::prop, T> \
+ { \
+ static const T &iteOp(const ::CVC4::symfpuLiteral::prop &cond, \
+ const T &l, \
+ const T &r) \
+ { \
+ return cond ? l : r; \
+ } \
+ }
+
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::rm);
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::prop);
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::sbv);
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv);
+
+#undef CVC4_LIT_ITE_DFN
+}
+#endif
+
+#ifndef CVC4_USE_SYMFPU
+#define PRECONDITION(X) Assert((X))
+#endif
namespace CVC4 {
PrettyCheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s);
}
-void FloatingPointLiteral::unfinished (void) const {
- Unimplemented("Floating-point literals not yet implemented.");
+namespace symfpuLiteral {
+
+// To simplify the property macros
+typedef traits t;
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one(const bwt &w)
+{
+ return wrappedBitVector<isSigned>(w, 1);
}
- FloatingPoint::FloatingPoint (unsigned e, unsigned s, const BitVector &bv) :
- fpl(e,s,0.0),
- t(e,s) {}
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero(const bwt &w)
+{
+ return wrappedBitVector<isSigned>(w, 0);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes(const bwt &w)
+{
+ return ~wrappedBitVector<isSigned>::zero(w);
+}
+template <bool isSigned>
+prop wrappedBitVector<isSigned>::isAllOnes() const
+{
+ return (*this == wrappedBitVector<isSigned>::allOnes(this->getWidth()));
+}
+template <bool isSigned>
+prop wrappedBitVector<isSigned>::isAllZeros() const
+{
+ return (*this == wrappedBitVector<isSigned>::zero(this->getWidth()));
+}
- static FloatingPointLiteral constructorHelperBitVector (const FloatingPointSize &ct, const RoundingMode &rm, const BitVector &bv, bool signedBV) {
- if (signedBV) {
- return FloatingPointLiteral(2,2,0.0);
- } else {
- return FloatingPointLiteral(2,2,0.0);
- }
- Unreachable("Constructor helper broken");
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue(const bwt &w)
+{
+ if (isSigned)
+ {
+ BitVector base(w - 1, 0U);
+ return wrappedBitVector<true>((~base).zeroExtend(1));
+ }
+ else
+ {
+ return wrappedBitVector<false>::allOnes(w);
+ }
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::minValue(const bwt &w)
+{
+ if (isSigned)
+ {
+ BitVector base(w, 1U);
+ BitVector shiftAmount(w, w - 1);
+ BitVector result(base.leftShift(shiftAmount));
+ return wrappedBitVector<true>(result);
+ }
+ else
+ {
+ return wrappedBitVector<false>::zero(w);
+ }
+}
+
+/*** Operators ***/
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator<<(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::leftShift(op);
+}
+
+template <>
+wrappedBitVector<true> wrappedBitVector<true>::operator>>(
+ const wrappedBitVector<true> &op) const
+{
+ return this->BitVector::arithRightShift(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator>>(
+ const wrappedBitVector<false> &op) const
+{
+ return this->BitVector::logicalRightShift(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::operator|(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::operator&(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::operator+(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::operator-(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::operator*(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator/(
+ const wrappedBitVector<false> &op) const
+{
+ return this->BitVector::unsignedDivTotal(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator%(
+ const wrappedBitVector<false> &op) const
+{
+ return this->BitVector::unsignedRemTotal(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const
+{
+ return this->BitVector::operator-();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void)const
+{
+ return this->BitVector::operator~();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::increment() const
+{
+ return *this + wrappedBitVector<isSigned>::one(this->getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const
+{
+ return *this - wrappedBitVector<isSigned>::one(this->getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::arithRightShift(BitVector(this->getWidth(), op));
+}
+
+/*** Modular opertaions ***/
+// No overflow checking so these are the same as other operations
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularLeftShift(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return *this << op;
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularRightShift(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return *this >> op;
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularIncrement() const
+{
+ return this->increment();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const
+{
+ return this->decrement();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularAdd(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return *this + op;
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularNegate() const
+{
+ return -(*this);
+}
+
+/*** Comparisons ***/
+
+template <bool isSigned>
+prop wrappedBitVector<isSigned>::operator==(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::operator==(op);
+}
+
+template <>
+prop wrappedBitVector<true>::operator<=(const wrappedBitVector<true> &op) const
+{
+ return this->signedLessThanEq(op);
+}
+
+template <>
+prop wrappedBitVector<true>::operator>=(const wrappedBitVector<true> &op) const
+{
+ return !(this->signedLessThan(op));
+}
+
+template <>
+prop wrappedBitVector<true>::operator<(const wrappedBitVector<true> &op) const
+{
+ return this->signedLessThan(op);
+}
+
+template <>
+prop wrappedBitVector<true>::operator>(const wrappedBitVector<true> &op) const
+{
+ return !(this->signedLessThanEq(op));
+}
+
+template <>
+prop wrappedBitVector<false>::operator<=(
+ const wrappedBitVector<false> &op) const
+{
+ return this->unsignedLessThanEq(op);
+}
+
+template <>
+prop wrappedBitVector<false>::operator>=(
+ const wrappedBitVector<false> &op) const
+{
+ return !(this->unsignedLessThan(op));
+}
+
+template <>
+prop wrappedBitVector<false>::operator<(const wrappedBitVector<false> &op) const
+{
+ return this->unsignedLessThan(op);
+}
+
+template <>
+prop wrappedBitVector<false>::operator>(const wrappedBitVector<false> &op) const
+{
+ return !(this->unsignedLessThanEq(op));
+}
+
+/*** Type conversion ***/
+// CVC4 nodes make no distinction between signed and unsigned, thus ...
+template <bool isSigned>
+wrappedBitVector<true> wrappedBitVector<isSigned>::toSigned(void) const
+{
+ return wrappedBitVector<true>(*this);
+}
+
+template <bool isSigned>
+wrappedBitVector<false> wrappedBitVector<isSigned>::toUnsigned(void) const
+{
+ return wrappedBitVector<false>(*this);
+}
+
+/*** Bit hacks ***/
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend(
+ bwt extension) const
+{
+ if (isSigned)
+ {
+ return this->BitVector::signExtend(extension);
+ }
+ else
+ {
+ return this->BitVector::zeroExtend(extension);
+ }
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
+ bwt reduction) const
+{
+ PRECONDITION(this->getWidth() > reduction);
+
+ return this->extract((this->getWidth() - 1) - reduction, 0);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::resize(bwt newSize) const
+{
+ bwt width = this->getWidth();
+
+ if (newSize > width)
+ {
+ return this->extend(newSize - width);
+ }
+ else if (newSize < width)
+ {
+ return this->contract(width - newSize);
+ }
+ else
+ {
+ return *this;
+ }
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth(
+ const wrappedBitVector<isSigned> &op) const
+{
+ PRECONDITION(this->getWidth() <= op.getWidth());
+ return this->extend(op.getWidth() - this->getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::concat(op);
+}
+
+// Inclusive of end points, thus if the same, extracts just one bit
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(bwt upper,
+ bwt lower) const
+{
+ PRECONDITION(upper >= lower);
+ return this->BitVector::extract(upper, lower);
+}
+
+// Explicit instantiation
+template class wrappedBitVector<true>;
+template class wrappedBitVector<false>;
+
+rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; };
+rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; };
+rm traits::RTP(void) { return ::CVC4::roundTowardPositive; };
+rm traits::RTN(void) { return ::CVC4::roundTowardNegative; };
+rm traits::RTZ(void) { return ::CVC4::roundTowardZero; };
+// This is a literal back-end so props are actually bools
+// so these can be handled in the same way as the internal assertions above
+
+void traits::precondition(const prop &p)
+{
+ Assert(p);
+ return;
+}
+void traits::postcondition(const prop &p)
+{
+ Assert(p);
+ return;
+}
+void traits::invariant(const prop &p)
+{
+ Assert(p);
+ return;
+}
+}
+
+#ifndef CVC4_USE_SYMFPU
+void FloatingPointLiteral::unfinished(void) const
+{
+ Unimplemented("Floating-point literals not yet implemented.");
+}
+#endif
+
+FloatingPoint::FloatingPoint(unsigned e, unsigned s, const BitVector &bv)
+ :
+#ifdef CVC4_USE_SYMFPU
+ fpl(symfpu::unpack<symfpuLiteral::traits>(symfpuLiteral::fpt(e, s), bv)),
+#else
+ fpl(e, s, 0.0),
+#endif
+ t(e, s)
+{
+}
+
+static FloatingPointLiteral constructorHelperBitVector(
+ const FloatingPointSize &ct,
+ const RoundingMode &rm,
+ const BitVector &bv,
+ bool signedBV)
+{
+#ifdef CVC4_USE_SYMFPU
+ if (signedBV)
+ {
+ return FloatingPointLiteral(
+ symfpu::convertSBVToFloat<symfpuLiteral::traits>(
+ symfpuLiteral::fpt(ct),
+ symfpuLiteral::rm(rm),
+ symfpuLiteral::sbv(bv)));
+ }
+ else
+ {
+ return FloatingPointLiteral(
+ symfpu::convertUBVToFloat<symfpuLiteral::traits>(
+ symfpuLiteral::fpt(ct),
+ symfpuLiteral::rm(rm),
+ symfpuLiteral::ubv(bv)));
+ }
+#else
+ return FloatingPointLiteral(2, 2, 0.0);
+#endif
+ Unreachable("Constructor helper broken");
}
FloatingPoint::FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const BitVector &bv, bool signedBV) :
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
// 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);
// 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");
}
FloatingPoint FloatingPoint::makeNaN (const FloatingPointSize &t) {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(
+ t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeNaN(t));
+#else
return FloatingPoint(2, 2, BitVector(4U,0U));
+#endif
}
FloatingPoint FloatingPoint::makeInf (const FloatingPointSize &t, bool sign) {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(
+ t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeInf(t, sign));
+#else
return FloatingPoint(2, 2, BitVector(4U,0U));
+#endif
}
FloatingPoint FloatingPoint::makeZero (const FloatingPointSize &t, bool sign) {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(
+ t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeZero(t, sign));
+#else
return FloatingPoint(2, 2, BitVector(4U,0U));
+#endif
}
/* Operations implemented using symfpu */
FloatingPoint FloatingPoint::absolute (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(t, symfpu::absolute<symfpuLiteral::traits>(t, fpl));
+#else
return *this;
+#endif
}
FloatingPoint FloatingPoint::negate (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(t, symfpu::negate<symfpuLiteral::traits>(t, fpl));
+#else
return *this;
+#endif
}
FloatingPoint FloatingPoint::plus (const RoundingMode &rm, const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::add<symfpuLiteral::traits>(t, rm, fpl, arg.fpl, true));
+#else
return *this;
+#endif
}
FloatingPoint FloatingPoint::sub (const RoundingMode &rm, const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::add<symfpuLiteral::traits>(t, rm, fpl, arg.fpl, false));
+#else
return *this;
+#endif
}
FloatingPoint FloatingPoint::mult (const RoundingMode &rm, const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::multiply<symfpuLiteral::traits>(t, rm, fpl, arg.fpl));
+#else
return *this;
+#endif
}
FloatingPoint FloatingPoint::fma (const RoundingMode &rm, const FloatingPoint &arg1, const FloatingPoint &arg2) const {
+#ifdef CVC4_USE_SYMFPU
Assert(this->t == arg1.t);
Assert(this->t == arg2.t);
+ return FloatingPoint(
+ t, symfpu::fma<symfpuLiteral::traits>(t, rm, fpl, arg1.fpl, arg2.fpl));
+#else
return *this;
+#endif
}
FloatingPoint FloatingPoint::div (const RoundingMode &rm, const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::divide<symfpuLiteral::traits>(t, rm, fpl, arg.fpl));
+#else
return *this;
+#endif
}
FloatingPoint FloatingPoint::sqrt (const RoundingMode &rm) const {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(t, symfpu::sqrt<symfpuLiteral::traits>(t, rm, fpl));
+#else
return *this;
+#endif
}
FloatingPoint FloatingPoint::rti (const RoundingMode &rm) const {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(
+ t, symfpu::roundToIntegral<symfpuLiteral::traits>(t, rm, fpl));
+#else
return *this;
+#endif
}
FloatingPoint FloatingPoint::rem (const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::remainder<symfpuLiteral::traits>(t, fpl, arg.fpl));
+#else
return *this;
+#endif
}
FloatingPoint FloatingPoint::maxTotal (const FloatingPoint &arg, bool zeroCaseLeft) const {
+#ifdef CVC4_USE_SYMFPU
Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::max<symfpuLiteral::traits>(t, fpl, arg.fpl, zeroCaseLeft));
+#else
return *this;
+#endif
}
FloatingPoint FloatingPoint::minTotal (const FloatingPoint &arg, bool zeroCaseLeft) const {
+#ifdef CVC4_USE_SYMFPU
Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::min<symfpuLiteral::traits>(t, fpl, arg.fpl, zeroCaseLeft));
+#else
return *this;
+#endif
}
FloatingPoint::PartialFloatingPoint FloatingPoint::max (const FloatingPoint &arg) const {
}
bool FloatingPoint::operator ==(const FloatingPoint& fp) const {
+#ifdef CVC4_USE_SYMFPU
+ return ((t == fp.t)
+ && symfpu::smtlibEqual<symfpuLiteral::traits>(t, fpl, fp.fpl));
+#else
return ( (t == fp.t) );
+#endif
}
bool FloatingPoint::operator <= (const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
Assert(this->t == arg.t);
+ return symfpu::lessThanOrEqual<symfpuLiteral::traits>(t, fpl, arg.fpl);
+#else
return false;
+#endif
}
bool FloatingPoint::operator < (const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
Assert(this->t == arg.t);
+ return symfpu::lessThan<symfpuLiteral::traits>(t, fpl, arg.fpl);
+#else
return false;
+#endif
}
bool FloatingPoint::isNormal (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isNormal<symfpuLiteral::traits>(t, fpl);
+#else
return false;
+#endif
}
bool FloatingPoint::isSubnormal (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isSubnormal<symfpuLiteral::traits>(t, fpl);
+#else
return false;
+#endif
}
bool FloatingPoint::isZero (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isZero<symfpuLiteral::traits>(t, fpl);
+#else
return false;
+#endif
}
bool FloatingPoint::isInfinite (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isInfinite<symfpuLiteral::traits>(t, fpl);
+#else
return false;
+#endif
}
bool FloatingPoint::isNaN (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isNaN<symfpuLiteral::traits>(t, fpl);
+#else
return false;
+#endif
}
bool FloatingPoint::isNegative (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isNegative<symfpuLiteral::traits>(t, fpl);
+#else
return false;
+#endif
}
bool FloatingPoint::isPositive (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isPositive<symfpuLiteral::traits>(t, fpl);
+#else
return false;
+#endif
}
FloatingPoint FloatingPoint::convert (const FloatingPointSize &target, const RoundingMode &rm) const {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(
+ target,
+ symfpu::convertFloatToFloat<symfpuLiteral::traits>(t, target, rm, fpl));
+#else
return *this;
+#endif
}
BitVector FloatingPoint::convertToBVTotal (BitVectorSize width, const RoundingMode &rm, bool signedBV, BitVector undefinedCase) const {
+#ifdef CVC4_USE_SYMFPU
if (signedBV)
- return undefinedCase;
+ return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
+ t, rm, fpl, width, undefinedCase);
else
- return undefinedCase;
+ return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
+ t, rm, fpl, width, undefinedCase);
+#else
+ return undefinedCase;
+#endif
}
Rational FloatingPoint::convertToRationalTotal (Rational undefinedCase) const {
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.
}
BitVector FloatingPoint::pack (void) const {
+#ifdef CVC4_USE_SYMFPU
+ BitVector bv(symfpu::pack<symfpuLiteral::traits>(this->t, this->fpl));
+#else
BitVector bv(4u,0u);
+#endif
return bv;
}
#ifndef __CVC4__FLOATINGPOINT_H
#define __CVC4__FLOATINGPOINT_H
-#include <fenv.h>
-
#include "util/bitvector.h"
#include "util/rational.h"
+#include <fenv.h>
+
+#ifdef CVC4_USE_SYMFPU
+#include "symfpu/core/unpackedFloat.h"
+#endif
+
namespace CVC4 {
// Inline these!
inline bool CVC4_PUBLIC validExponentSize (unsigned e) { return e >= 2; }
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 {
}
}; /* struct RoundingModeHashFunction */
+ /**
+ * This is a symfpu literal "back-end". It allows the library to be used as
+ * an arbitrary precision floating-point implementation. This is effectively
+ * the glue between symfpu's notion of "signed bit-vector" and CVC4's
+ * BitVector.
+ */
+ namespace symfpuLiteral {
+ // Forward declaration of wrapper so that traits can be defined early and so
+ // used in the implementation of wrappedBitVector.
+ template <bool T>
+ class wrappedBitVector;
+
+ // This is the template parameter for symfpu's templates.
+ class traits
+ {
+ public:
+ // The six key types that symfpu uses.
+ typedef unsigned bwt;
+ typedef bool prop;
+ typedef ::CVC4::RoundingMode rm;
+ typedef ::CVC4::FloatingPointSize fpt;
+ typedef wrappedBitVector<true> sbv;
+ typedef wrappedBitVector<false> ubv;
+
+ // Give concrete instances of each rounding mode, mainly for comparisons.
+ static rm RNE(void);
+ static rm RNA(void);
+ static rm RTP(void);
+ static rm RTN(void);
+ static rm RTZ(void);
+
+ // The sympfu properties.
+ static void precondition(const prop &p);
+ static void postcondition(const prop &p);
+ static void invariant(const prop &p);
+ };
+
+ // Use the same type names as symfpu.
+ typedef traits::bwt bwt;
+ typedef traits::prop prop;
+ typedef traits::rm rm;
+ typedef traits::fpt fpt;
+ typedef traits::ubv ubv;
+ typedef traits::sbv sbv;
+
+ // Type function for mapping between types
+ template <bool T>
+ struct signedToLiteralType;
+
+ template <>
+ struct signedToLiteralType<true>
+ {
+ typedef int literalType;
+ };
+ template <>
+ struct signedToLiteralType<false>
+ {
+ typedef unsigned int literalType;
+ };
+
+ // This is an additional interface for CVC4::BitVector.
+ // The template parameter distinguishes signed and unsigned bit-vectors, a
+ // distinction symfpu uses.
+ template <bool isSigned>
+ class wrappedBitVector : public BitVector
+ {
+ protected:
+ typedef typename signedToLiteralType<isSigned>::literalType literalType;
+
+ friend wrappedBitVector<!isSigned>; // To allow conversion between the
+ // types
+#ifdef CVC4_USE_SYMFPU
+ friend ::symfpu::ite<prop, wrappedBitVector<isSigned> >; // For ITE
+#endif
+
+ public:
+ wrappedBitVector(const bwt w, const unsigned v) : BitVector(w, v) {}
+ wrappedBitVector(const prop &p) : BitVector(1, p ? 1U : 0U) {}
+ wrappedBitVector(const wrappedBitVector<isSigned> &old) : BitVector(old) {}
+ wrappedBitVector(const BitVector &old) : BitVector(old) {}
+ bwt getWidth(void) const { return getSize(); }
+ /*** Constant creation and test ***/
+
+ static wrappedBitVector<isSigned> one(const bwt &w);
+ static wrappedBitVector<isSigned> zero(const bwt &w);
+ static wrappedBitVector<isSigned> allOnes(const bwt &w);
+
+ prop isAllOnes() const;
+ prop isAllZeros() const;
+
+ static wrappedBitVector<isSigned> maxValue(const bwt &w);
+ static wrappedBitVector<isSigned> minValue(const bwt &w);
+
+ /*** Operators ***/
+ wrappedBitVector<isSigned> operator<<(
+ const wrappedBitVector<isSigned> &op) const;
+ wrappedBitVector<isSigned> operator>>(
+ const wrappedBitVector<isSigned> &op) const;
+
+ /* Inherited but ...
+ * *sigh* if we use the inherited version then it will return a
+ * CVC4::BitVector which can be converted back to a
+ * wrappedBitVector<isSigned> but isn't done automatically when working
+ * out types for templates instantiation. ITE is a particular
+ * problem as expressions and constants no longer derive the
+ * same type. There aren't any good solutions in C++, we could
+ * use CRTP but Liana wouldn't appreciate that, so the following
+ * pointless wrapping functions are needed.
+ */
+ wrappedBitVector<isSigned> operator|(
+ const wrappedBitVector<isSigned> &op) const;
+ wrappedBitVector<isSigned> operator&(
+ const wrappedBitVector<isSigned> &op) const;
+ wrappedBitVector<isSigned> operator+(
+ const wrappedBitVector<isSigned> &op) const;
+ wrappedBitVector<isSigned> operator-(
+ const wrappedBitVector<isSigned> &op) const;
+ wrappedBitVector<isSigned> operator*(
+ const wrappedBitVector<isSigned> &op) const;
+ wrappedBitVector<isSigned> operator/(
+ const wrappedBitVector<isSigned> &op) const;
+ wrappedBitVector<isSigned> operator%(
+ const wrappedBitVector<isSigned> &op) const;
+ wrappedBitVector<isSigned> operator-(void) const;
+ wrappedBitVector<isSigned> operator~(void)const;
+
+ wrappedBitVector<isSigned> increment() const;
+ wrappedBitVector<isSigned> decrement() const;
+ wrappedBitVector<isSigned> signExtendRightShift(
+ const wrappedBitVector<isSigned> &op) const;
+
+ /*** Modular opertaions ***/
+ // No overflow checking so these are the same as other operations
+ wrappedBitVector<isSigned> modularLeftShift(
+ const wrappedBitVector<isSigned> &op) const;
+ wrappedBitVector<isSigned> modularRightShift(
+ const wrappedBitVector<isSigned> &op) const;
+ wrappedBitVector<isSigned> modularIncrement() const;
+ wrappedBitVector<isSigned> modularDecrement() const;
+ wrappedBitVector<isSigned> modularAdd(
+ const wrappedBitVector<isSigned> &op) const;
+ wrappedBitVector<isSigned> modularNegate() const;
+
+ /*** Comparisons ***/
+ // Inherited ... ish ...
+ prop operator==(const wrappedBitVector<isSigned> &op) const;
+ prop operator<=(const wrappedBitVector<isSigned> &op) const;
+ prop operator>=(const wrappedBitVector<isSigned> &op) const;
+ prop operator<(const wrappedBitVector<isSigned> &op) const;
+ prop operator>(const wrappedBitVector<isSigned> &op) const;
+
+ /*** Type conversion ***/
+ wrappedBitVector<true> toSigned(void) const;
+ wrappedBitVector<false> toUnsigned(void) const;
+
+ /*** Bit hacks ***/
+ wrappedBitVector<isSigned> extend(bwt extension) const;
+ wrappedBitVector<isSigned> contract(bwt reduction) const;
+ wrappedBitVector<isSigned> resize(bwt newSize) const;
+ wrappedBitVector<isSigned> matchWidth(
+ const wrappedBitVector<isSigned> &op) const;
+ wrappedBitVector<isSigned> append(
+ const wrappedBitVector<isSigned> &op) const;
+
+ // Inclusive of end points, thus if the same, extracts just one bit
+ wrappedBitVector<isSigned> extract(bwt upper, bwt lower) const;
+ };
+ }
/**
* A concrete floating point number
*/
-
+#ifdef CVC4_USE_SYMFPU
+ typedef ::symfpu::unpackedFloat<symfpuLiteral::traits> FloatingPointLiteral;
+#else
class CVC4_PUBLIC FloatingPointLiteral {
public :
// This intentional left unfinished as the choice of literal
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;
return 23;
}
};
+#endif
class CVC4_PUBLIC FloatingPoint {
protected :
projects / cvc5.git / commitdiff