summaryrefslogtreecommitdiff
path: root/src/theory/fp
diff options
context:
space:
mode:
authorMartin <martin.brain@cs.ox.ac.uk>2018-05-15 00:18:31 +0100
committerGitHub <noreply@github.com>2018-05-15 00:18:31 +0100
commit4e96b1d5e01260acc79bdbb86322e23c7cf9567f (patch)
tree283fa5091023234bbc601b87d62e4610c05a4981 /src/theory/fp
parent0c6681152ca422f7ace1bd1d3c3dac7823de2c14 (diff)
Floating point theory solver based on SymFPU (#1895)
* Add some symfpu accessor functions to reduce the size of the literal 'back-end'. * Enable the bit-vector theory when setting the logic, not in expandDefinition. This is needed because it is possible to add variables of float or rounding mode sort but not use any theory specific functions or predicates and thus not enable the bit-vector theory. * Use symfpu to implement the literal floating-point objects. * Add kinds for bit-blasted components. * Print the new kinds. * Typing rules for the new kinds. * Constant folding for the component kinds. * Add support for components to the theory solver. * Add explicit equivalences between classification functions and equalities. * Use symfpu to do symbolic conversions of floating-point operations. * Implement conversions via (over-)approximation and refinement. * Correct a copy and paste error in the generation of uninterpretted functions for conversions.
Diffstat (limited to 'src/theory/fp')
-rw-r--r--src/theory/fp/fp_converter.cpp1712
-rw-r--r--src/theory/fp/fp_converter.h305
-rw-r--r--src/theory/fp/kinds24
-rw-r--r--src/theory/fp/theory_fp.cpp467
-rw-r--r--src/theory/fp/theory_fp.h20
-rw-r--r--src/theory/fp/theory_fp_rewriter.cpp156
-rw-r--r--src/theory/fp/theory_fp_type_rules.h164
7 files changed, 2825 insertions, 23 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index aba95d2ec..464aa497e 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -13,22 +13,1724 @@
**/
#include "theory/fp/fp_converter.h"
+#include "theory/theory.h"
+// theory.h Only needed for the leaf test
#include <stack>
+#ifdef CVC4_USE_SYMFPU
+#include "symfpu/core/add.h"
+#include "symfpu/core/classify.h"
+#include "symfpu/core/compare.h"
+#include "symfpu/core/convert.h"
+#include "symfpu/core/divide.h"
+#include "symfpu/core/fma.h"
+#include "symfpu/core/ite.h"
+#include "symfpu/core/multiply.h"
+#include "symfpu/core/packing.h"
+#include "symfpu/core/remainder.h"
+#include "symfpu/core/sign.h"
+#include "symfpu/core/sqrt.h"
+#include "symfpu/utils/numberOfRoundingModes.h"
+#include "symfpu/utils/properties.h"
+#endif
+
+#ifdef CVC4_USE_SYMFPU
+namespace symfpu {
+using namespace ::CVC4::theory::fp::symfpuSymbolic;
+
+#define CVC4_SYM_ITE_DFN(T) \
+ template <> \
+ struct ite<symbolicProposition, T> \
+ { \
+ static const T iteOp(const symbolicProposition &_cond, \
+ const T &_l, \
+ const T &_r) \
+ { \
+ ::CVC4::NodeManager *nm = ::CVC4::NodeManager::currentNM(); \
+ \
+ ::CVC4::Node cond = _cond; \
+ ::CVC4::Node l = _l; \
+ ::CVC4::Node r = _r; \
+ \
+ /* Handle some common symfpu idioms */ \
+ if (cond.isConst()) \
+ { \
+ return (cond == nm->mkConst(::CVC4::BitVector(1U, 1U))) ? l : r; \
+ } \
+ else \
+ { \
+ if (l.getKind() == ::CVC4::kind::BITVECTOR_ITE) \
+ { \
+ if (l[1] == r) \
+ { \
+ return nm->mkNode( \
+ ::CVC4::kind::BITVECTOR_ITE, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_AND, \
+ cond, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_NOT, l[0])), \
+ l[2], \
+ r); \
+ } \
+ else if (l[2] == r) \
+ { \
+ return nm->mkNode( \
+ ::CVC4::kind::BITVECTOR_ITE, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_AND, cond, l[0]), \
+ l[1], \
+ r); \
+ } \
+ } \
+ else if (r.getKind() == ::CVC4::kind::BITVECTOR_ITE) \
+ { \
+ if (r[1] == l) \
+ { \
+ return nm->mkNode( \
+ ::CVC4::kind::BITVECTOR_ITE, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_AND, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_NOT, cond), \
+ nm->mkNode(::CVC4::kind::BITVECTOR_NOT, r[0])), \
+ r[2], \
+ l); \
+ } \
+ else if (r[2] == l) \
+ { \
+ return nm->mkNode( \
+ ::CVC4::kind::BITVECTOR_ITE, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_AND, \
+ nm->mkNode(::CVC4::kind::BITVECTOR_NOT, cond), \
+ r[0]), \
+ r[1], \
+ l); \
+ } \
+ } \
+ } \
+ return T(nm->mkNode(::CVC4::kind::BITVECTOR_ITE, cond, l, r)); \
+ } \
+ }
+
+// Can (unsurprisingly) only ITE things which contain Nodes
+CVC4_SYM_ITE_DFN(traits::rm);
+CVC4_SYM_ITE_DFN(traits::prop);
+CVC4_SYM_ITE_DFN(traits::sbv);
+CVC4_SYM_ITE_DFN(traits::ubv);
+
+#undef CVC4_SYM_ITE_DFN
+
+template <>
+traits::ubv orderEncode<traits, traits::ubv>(const traits::ubv &b)
+{
+ return orderEncodeBitwise<traits, traits::ubv>(b);
+}
+
+template <>
+stickyRightShiftResult<traits> stickyRightShift(const traits::ubv &input,
+ const traits::ubv &shiftAmount)
+{
+ return stickyRightShiftBitwise<traits>(input, shiftAmount);
+}
+
+template <>
+void probabilityAnnotation<traits, traits::prop>(const traits::prop &p,
+ const probability &pr)
+{
+ // For now, do nothing...
+ return;
+}
+};
+#endif
+
+#ifndef CVC4_USE_SYMFPU
+#define PRECONDITION(X) Assert((X))
+#define SYMFPU_NUMBER_OF_ROUNDING_MODES 5
+#endif
+
namespace CVC4 {
namespace theory {
namespace fp {
+namespace symfpuSymbolic {
+
+symbolicRoundingMode traits::RNE(void) { return symbolicRoundingMode(0x01); };
+symbolicRoundingMode traits::RNA(void) { return symbolicRoundingMode(0x02); };
+symbolicRoundingMode traits::RTP(void) { return symbolicRoundingMode(0x04); };
+symbolicRoundingMode traits::RTN(void) { return symbolicRoundingMode(0x08); };
+symbolicRoundingMode traits::RTZ(void) { return symbolicRoundingMode(0x10); };
+void traits::precondition(const bool b)
+{
+ Assert(b);
+ return;
+}
+void traits::postcondition(const bool b)
+{
+ Assert(b);
+ return;
+}
+void traits::invariant(const bool b)
+{
+ Assert(b);
+ return;
+}
+
+void traits::precondition(const prop &p) { return; }
+void traits::postcondition(const prop &p) { return; }
+void traits::invariant(const prop &p) { return; }
+// This allows us to use the symfpu literal / symbolic assertions in the
+// symbolic back-end
+typedef traits t;
+
+bool symbolicProposition::checkNodeType(const TNode node)
+{
+ TypeNode tn = node.getType(false);
+ return tn.isBitVector() && tn.getBitVectorSize() == 1;
+}
+
+symbolicProposition::symbolicProposition(const Node n) : nodeWrapper(n)
+{
+ PRECONDITION(checkNodeType(*this));
+} // Only used within this header so could be friend'd
+symbolicProposition::symbolicProposition(bool v)
+ : nodeWrapper(
+ NodeManager::currentNM()->mkConst(BitVector(1U, (v ? 1U : 0U))))
+{
+ PRECONDITION(checkNodeType(*this));
+}
+symbolicProposition::symbolicProposition(const symbolicProposition &old)
+ : nodeWrapper(old)
+{
+ PRECONDITION(checkNodeType(*this));
+}
+
+symbolicProposition symbolicProposition::operator!(void)const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this));
+}
+
+symbolicProposition symbolicProposition::operator&&(
+ const symbolicProposition &op) const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op));
+}
+
+symbolicProposition symbolicProposition::operator||(
+ const symbolicProposition &op) const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op));
+}
+
+symbolicProposition symbolicProposition::operator==(
+ const symbolicProposition &op) const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op));
+}
+
+symbolicProposition symbolicProposition::operator^(
+ const symbolicProposition &op) const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_XOR, *this, op));
+}
+
+bool symbolicRoundingMode::checkNodeType(const TNode n)
+{
+#ifdef CVC4_USE_SYMFPU
+ return n.getType(false).isBitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES);
+#else
+ return false;
+#endif
+}
+
+symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n)
+{
+ PRECONDITION(checkNodeType(*this));
+}
+
+#ifdef CVC4_USE_SYMFPU
+symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
+ : nodeWrapper(NodeManager::currentNM()->mkConst(
+ BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
+{
+ PRECONDITION((v & v - 1) == 0 && v != 0); // Exactly one bit set
+ PRECONDITION(checkNodeType(*this));
+}
+#else
+symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
+ : nodeWrapper(NodeManager::currentNM()->mkConst(
+ BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
+{
+ Unreachable();
+}
+#endif
+
+symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old)
+ : nodeWrapper(old)
+{
+ PRECONDITION(checkNodeType(*this));
+}
+
+symbolicProposition symbolicRoundingMode::valid(void) const
+{
+ NodeManager *nm = NodeManager::currentNM();
+ Node zero(nm->mkConst(
+ BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, (long unsigned int)0)));
+
+ // Is there a better encoding of this?
+ return symbolicProposition(nm->mkNode(
+ kind::BITVECTOR_AND,
+ nm->mkNode(kind::BITVECTOR_COMP,
+ nm->mkNode(kind::BITVECTOR_AND,
+ *this,
+ nm->mkNode(kind::BITVECTOR_SUB,
+ *this,
+ nm->mkConst(BitVector(
+ SYMFPU_NUMBER_OF_ROUNDING_MODES,
+ (long unsigned int)1)))),
+ zero),
+ nm->mkNode(kind::BITVECTOR_NOT,
+ nm->mkNode(kind::BITVECTOR_COMP, *this, zero))));
+}
+
+symbolicProposition symbolicRoundingMode::operator==(
+ const symbolicRoundingMode &op) const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op));
+}
+
+template <bool isSigned>
+Node symbolicBitVector<isSigned>::boolNodeToBV(Node node) const
+{
+ Assert(node.getType().isBoolean());
+ NodeManager *nm = NodeManager::currentNM();
+ return nm->mkNode(kind::ITE,
+ node,
+ nm->mkConst(BitVector(1U, 1U)),
+ nm->mkConst(BitVector(1U, 0U)));
+}
+
+template <bool isSigned>
+Node symbolicBitVector<isSigned>::BVToBoolNode(Node node) const
+{
+ Assert(node.getType().isBitVector());
+ Assert(node.getType().getBitVectorSize() == 1);
+ NodeManager *nm = NodeManager::currentNM();
+ return nm->mkNode(kind::EQUAL, node, nm->mkConst(BitVector(1U, 1U)));
+}
+
+template <bool isSigned>
+Node symbolicBitVector<isSigned>::fromProposition(Node node) const
+{
+ return node;
+}
+template <bool isSigned>
+Node symbolicBitVector<isSigned>::toProposition(Node node) const
+{
+ return boolNodeToBV(node);
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned>::symbolicBitVector(const Node n) : nodeWrapper(n)
+{
+ PRECONDITION(checkNodeType(*this));
+}
+
+template <bool isSigned>
+bool symbolicBitVector<isSigned>::checkNodeType(const TNode n)
+{
+ return n.getType(false).isBitVector();
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned>::symbolicBitVector(const bwt w, const unsigned v)
+ : nodeWrapper(NodeManager::currentNM()->mkConst(BitVector(w, v)))
+{
+ PRECONDITION(checkNodeType(*this));
+}
+template <bool isSigned>
+symbolicBitVector<isSigned>::symbolicBitVector(const symbolicProposition &p)
+ : nodeWrapper(fromProposition(p))
+{
+}
+template <bool isSigned>
+symbolicBitVector<isSigned>::symbolicBitVector(
+ const symbolicBitVector<isSigned> &old)
+ : nodeWrapper(old)
+{
+ PRECONDITION(checkNodeType(*this));
+}
+template <bool isSigned>
+symbolicBitVector<isSigned>::symbolicBitVector(const BitVector &old)
+ : nodeWrapper(NodeManager::currentNM()->mkConst(old))
+{
+ PRECONDITION(checkNodeType(*this));
+}
+
+template <bool isSigned>
+bwt symbolicBitVector<isSigned>::getWidth(void) const
+{
+ return this->getType(false).getBitVectorSize();
+}
+
+/*** Constant creation and test ***/
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::one(const bwt &w)
+{
+ return symbolicBitVector<isSigned>(w, 1);
+}
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::zero(const bwt &w)
+{
+ return symbolicBitVector<isSigned>(w, 0);
+}
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::allOnes(const bwt &w)
+{
+ return symbolicBitVector<isSigned>(~zero(w));
+}
+
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::isAllOnes() const
+{
+ return (*this == symbolicBitVector<isSigned>::allOnes(this->getWidth()));
+}
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::isAllZeros() const
+{
+ return (*this == symbolicBitVector<isSigned>::zero(this->getWidth()));
+}
+
+template <>
+symbolicBitVector<true> symbolicBitVector<true>::maxValue(const bwt &w)
+{
+ symbolicBitVector<true> leadingZero(symbolicBitVector<true>::zero(1));
+ symbolicBitVector<true> base(symbolicBitVector<true>::allOnes(w - 1));
+
+ return symbolicBitVector<true>(::CVC4::NodeManager::currentNM()->mkNode(
+ ::CVC4::kind::BITVECTOR_CONCAT, leadingZero, base));
+}
+
+template <>
+symbolicBitVector<false> symbolicBitVector<false>::maxValue(const bwt &w)
+{
+ return symbolicBitVector<false>::allOnes(w);
+}
+
+template <>
+symbolicBitVector<true> symbolicBitVector<true>::minValue(const bwt &w)
+{
+ symbolicBitVector<true> leadingOne(symbolicBitVector<true>::one(1));
+ symbolicBitVector<true> base(symbolicBitVector<true>::zero(w - 1));
+
+ return symbolicBitVector<true>(::CVC4::NodeManager::currentNM()->mkNode(
+ ::CVC4::kind::BITVECTOR_CONCAT, leadingOne, base));
+}
+
+template <>
+symbolicBitVector<false> symbolicBitVector<false>::minValue(const bwt &w)
+{
+ return symbolicBitVector<false>::zero(w);
+}
+
+/*** Operators ***/
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator<<(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_SHL, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator>>(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
+ (isSigned) ? kind::BITVECTOR_ASHR : kind::BITVECTOR_LSHR, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator|(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator&(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator+(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator-(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator*(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, *this, op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator/(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
+ (isSigned) ? kind::BITVECTOR_SDIV : kind::BITVECTOR_UDIV_TOTAL,
+ *this,
+ op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator%(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
+ (isSigned) ? kind::BITVECTOR_SREM : kind::BITVECTOR_UREM_TOTAL,
+ *this,
+ op));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator-(void) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_NEG, *this));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator~(void)const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::increment() const
+{
+ return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
+ kind::BITVECTOR_PLUS, *this, one(this->getWidth())));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::decrement() const
+{
+ return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
+ kind::BITVECTOR_SUB, *this, one(this->getWidth())));
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::signExtendRightShift(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_ASHR, *this, op));
+}
+
+/*** Modular operations ***/
+// No overflow checking so these are the same as other operations
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularLeftShift(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return *this << op;
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularRightShift(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return *this >> op;
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularIncrement()
+ const
+{
+ return this->increment();
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularDecrement()
+ const
+{
+ return this->decrement();
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularAdd(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return *this + op;
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularNegate() const
+{
+ return -(*this);
+}
+
+/*** Comparisons ***/
+
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::operator==(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicProposition(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op));
+}
+
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::operator<=(
+ const symbolicBitVector<isSigned> &op) const
+{
+ // Consider adding kind::BITVECTOR_SLEBV and BITVECTOR_ULEBV
+ return (*this < op) || (*this == op);
+}
+
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::operator>=(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return (*this > op) || (*this == op);
+}
+
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::operator<(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicProposition(NodeManager::currentNM()->mkNode(
+ (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, *this, op));
+}
+
+template <bool isSigned>
+symbolicProposition symbolicBitVector<isSigned>::operator>(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicProposition(NodeManager::currentNM()->mkNode(
+ (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, op, *this));
+}
+
+/*** Type conversion ***/
+// CVC4 nodes make no distinction between signed and unsigned, thus ...
+template <bool isSigned>
+symbolicBitVector<true> symbolicBitVector<isSigned>::toSigned(void) const
+{
+ return symbolicBitVector<true>(*this);
+}
+template <bool isSigned>
+symbolicBitVector<false> symbolicBitVector<isSigned>::toUnsigned(void) const
+{
+ return symbolicBitVector<false>(*this);
+}
+
+/*** Bit hacks ***/
+template <>
+symbolicBitVector<true> symbolicBitVector<true>::extend(bwt extension) const
+{
+ NodeBuilder<> construct(kind::BITVECTOR_SIGN_EXTEND);
+ construct << NodeManager::currentNM()->mkConst<BitVectorSignExtend>(
+ BitVectorSignExtend(extension))
+ << *this;
+
+ return symbolicBitVector<true>(construct);
+}
+
+template <>
+symbolicBitVector<false> symbolicBitVector<false>::extend(bwt extension) const
+{
+ NodeBuilder<> construct(kind::BITVECTOR_ZERO_EXTEND);
+ construct << NodeManager::currentNM()->mkConst<BitVectorZeroExtend>(
+ BitVectorZeroExtend(extension))
+ << *this;
+
+ return symbolicBitVector<false>(construct);
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::contract(
+ bwt reduction) const
+{
+ PRECONDITION(this->getWidth() > reduction);
+
+ NodeBuilder<> construct(kind::BITVECTOR_EXTRACT);
+ construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
+ BitVectorExtract((this->getWidth() - 1) - reduction, 0))
+ << *this;
+
+ return symbolicBitVector<isSigned>(construct);
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::resize(
+ bwt newSize) const
+{
+ bwt width = this->getWidth();
+
+ if (newSize > width)
+ {
+ return this->extend(newSize - width);
+ }
+ else if (newSize < width)
+ {
+ return this->contract(width - newSize);
+ }
+ else
+ {
+ return *this;
+ }
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::matchWidth(
+ const symbolicBitVector<isSigned> &op) const
+{
+ PRECONDITION(this->getWidth() <= op.getWidth());
+ return this->extend(op.getWidth() - this->getWidth());
+}
+
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::append(
+ const symbolicBitVector<isSigned> &op) const
+{
+ return symbolicBitVector<isSigned>(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, *this, op));
+}
+
+// Inclusive of end points, thus if the same, extracts just one bit
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::extract(
+ bwt upper, bwt lower) const
+{
+ PRECONDITION(upper >= lower);
+
+ NodeBuilder<> construct(kind::BITVECTOR_EXTRACT);
+ construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
+ BitVectorExtract(upper, lower))
+ << *this;
+
+ return symbolicBitVector<isSigned>(construct);
+}
+
+floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode t)
+ : FloatingPointSize(t.getConst<FloatingPointSize>())
+{
+ PRECONDITION(t.isFloatingPoint());
+}
+floatingPointTypeInfo::floatingPointTypeInfo(unsigned exp, unsigned sig)
+ : FloatingPointSize(exp, sig)
+{
+}
+floatingPointTypeInfo::floatingPointTypeInfo(const floatingPointTypeInfo &old)
+ : FloatingPointSize(old)
+{
+}
+
+TypeNode floatingPointTypeInfo::getTypeNode(void) const
+{
+ return NodeManager::currentNM()->mkFloatingPointType(*this);
+}
+}
FpConverter::FpConverter(context::UserContext *user)
- : d_additionalAssertions(user) {}
+ :
+#ifdef CVC4_USE_SYMFPU
+ f(user),
+ r(user),
+ b(user),
+ u(user),
+ s(user),
+#endif
+ d_additionalAssertions(user)
+{
+}
+
+#ifdef CVC4_USE_SYMFPU
+Node FpConverter::ufToNode(const fpt &format, const uf &u) const
+{
+ NodeManager *nm = NodeManager::currentNM();
+
+ FloatingPointSize fps(format.getTypeNode().getConst<FloatingPointSize>());
+
+ // This is not entirely obvious but it builds a float from components
+ // Particularly, if the components can be constant folded, it should
+ // build a Node containing a constant FloatingPoint number
+
+ ubv packed(symfpu::pack<traits>(format, u));
+ Node value =
+ nm->mkNode(nm->mkConst(FloatingPointToFPIEEEBitVector(fps)), packed);
+ return value;
+}
+
+Node FpConverter::rmToNode(const rm &r) const
+{
+ NodeManager *nm = NodeManager::currentNM();
+
+ Node transVar = r;
+
+ Node RNE = traits::RNE();
+ Node RNA = traits::RNA();
+ Node RTP = traits::RTP();
+ Node RTN = traits::RTN();
+ Node RTZ = traits::RTZ();
+
+ Node value = nm->mkNode(
+ kind::ITE,
+ nm->mkNode(kind::EQUAL, transVar, RNE),
+ nm->mkConst(roundNearestTiesToEven),
+ nm->mkNode(kind::ITE,
+ nm->mkNode(kind::EQUAL, transVar, RNA),
+ nm->mkConst(roundNearestTiesToAway),
+ nm->mkNode(kind::ITE,
+ nm->mkNode(kind::EQUAL, transVar, RTP),
+ nm->mkConst(roundTowardPositive),
+ nm->mkNode(kind::ITE,
+ nm->mkNode(kind::EQUAL, transVar, RTN),
+ nm->mkConst(roundTowardNegative),
+ nm->mkConst(roundTowardZero)))));
+ return value;
+}
+
+Node FpConverter::propToNode(const prop &p) const
+{
+ NodeManager *nm = NodeManager::currentNM();
+ Node value =
+ nm->mkNode(kind::EQUAL, p, nm->mkConst(::CVC4::BitVector(1U, 1U)));
+ return value;
+}
+Node FpConverter::ubvToNode(const ubv &u) const { return u; }
+Node FpConverter::sbvToNode(const sbv &s) const { return s; }
+// Creates the components constraint
+FpConverter::uf FpConverter::buildComponents(TNode current)
+{
+ Assert(Theory::isLeafOf(current, THEORY_FP)
+ || current.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
+
+ NodeManager *nm = NodeManager::currentNM();
+ uf tmp(nm->mkNode(kind::FLOATINGPOINT_COMPONENT_NAN, current),
+ nm->mkNode(kind::FLOATINGPOINT_COMPONENT_INF, current),
+ nm->mkNode(kind::FLOATINGPOINT_COMPONENT_ZERO, current),
+ nm->mkNode(kind::FLOATINGPOINT_COMPONENT_SIGN, current),
+ nm->mkNode(kind::FLOATINGPOINT_COMPONENT_EXPONENT, current),
+ nm->mkNode(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND, current));
+
+ d_additionalAssertions.push_back(tmp.valid(fpt(current.getType())));
-Node FpConverter::convert(TNode node) {
- Unimplemented("Conversion not implemented.");
+ return tmp;
}
+#endif
+
+// Non-convertible things should only be added to the stack at the very start,
+// thus...
+#define CVC4_FPCONV_PASSTHROUGH Assert(workStack.empty())
+
+Node FpConverter::convert(TNode node)
+{
+#ifdef CVC4_USE_SYMFPU
+ std::stack<TNode> workStack;
+ TNode result = node;
+
+ workStack.push(node);
+
+ NodeManager *nm = NodeManager::currentNM();
+
+ while (!workStack.empty())
+ {
+ TNode current = workStack.top();
+ workStack.pop();
+ result = current;
+
+ TypeNode t(current.getType());
+
+ if (t.isRoundingMode())
+ {
+ rmMap::const_iterator i(r.find(current));
+
+ if (i == r.end())
+ {
+ if (Theory::isLeafOf(current, THEORY_FP))
+ {
+ if (current.getKind() == kind::CONST_ROUNDINGMODE)
+ {
+ /******** Constants ********/
+ switch (current.getConst<RoundingMode>())
+ {
+ case roundNearestTiesToEven:
+ r.insert(current, traits::RNE());
+ break;
+ case roundNearestTiesToAway:
+ r.insert(current, traits::RNA());
+ break;
+ case roundTowardPositive: r.insert(current, traits::RTP()); break;
+ case roundTowardNegative: r.insert(current, traits::RTN()); break;
+ case roundTowardZero: r.insert(current, traits::RTZ()); break;
+ default: Unreachable("Unknown rounding mode"); break;
+ }
+ }
+ else
+ {
+ /******** Variables ********/
+ rm tmp(nm->mkNode(kind::ROUNDINGMODE_BITBLAST, current));
+ r.insert(current, tmp);
+ d_additionalAssertions.push_back(tmp.valid());
+ }
+ }
+ else
+ {
+ Unreachable("Unknown kind of type RoundingMode");
+ }
+ }
+ // Returns a rounding-mode type so don't alter the return value
+ }
+ else if (t.isFloatingPoint())
+ {
+ fpMap::const_iterator i(f.find(current));
+
+ if (i == f.end())
+ {
+ if (Theory::isLeafOf(current, THEORY_FP))
+ {
+ if (current.getKind() == kind::CONST_FLOATINGPOINT)
+ {
+ /******** Constants ********/
+ f.insert(current,
+ symfpu::unpackedFloat<traits>(
+ current.getConst<FloatingPoint>().getLiteral()));
+ }
+ else
+ {
+ /******** Variables ********/
+ f.insert(current, buildComponents(current));
+ }
+ }
+ else
+ {
+ switch (current.getKind())
+ {
+ case kind::CONST_FLOATINGPOINT:
+ case kind::VARIABLE:
+ case kind::BOUND_VARIABLE:
+ case kind::SKOLEM:
+ Unreachable("Kind should have been handled as a leaf.");
+ break;
+
+ /******** Operations ********/
+ case kind::FLOATINGPOINT_ABS:
+ case kind::FLOATINGPOINT_NEG:
+ {
+ fpMap::const_iterator arg1(f.find(current[0]));
+
+ if (arg1 == f.end())
+ {
+ workStack.push(current);
+ workStack.push(current[0]);
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_ABS:
+ f.insert(current,
+ symfpu::absolute<traits>(fpt(current.getType()),
+ (*arg1).second));
+ break;
+ case kind::FLOATINGPOINT_NEG:
+ f.insert(current,
+ symfpu::negate<traits>(fpt(current.getType()),
+ (*arg1).second));
+ break;
+ default:
+ Unreachable("Unknown unary floating-point function");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_SQRT:
+ case kind::FLOATINGPOINT_RTI:
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ fpMap::const_iterator arg1(f.find(current[1]));
+ bool recurseNeeded = (mode == r.end()) || (arg1 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg1 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_SQRT:
+ f.insert(current,
+ symfpu::sqrt<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second));
+ break;
+ case kind::FLOATINGPOINT_RTI:
+ f.insert(
+ current,
+ symfpu::roundToIntegral<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second));
+ break;
+ default:
+ Unreachable("Unknown unary rounded floating-point function");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_REM:
+ {
+ fpMap::const_iterator arg1(f.find(current[0]));
+ fpMap::const_iterator arg2(f.find(current[1]));
+ bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (arg1 == f.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg2 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ f.insert(
+ current,
+ symfpu::remainder<traits>(
+ fpt(current.getType()), (*arg1).second, (*arg2).second));
+ }
+ break;
+
+ case kind::FLOATINGPOINT_MIN_TOTAL:
+ case kind::FLOATINGPOINT_MAX_TOTAL:
+ {
+ fpMap::const_iterator arg1(f.find(current[0]));
+ fpMap::const_iterator arg2(f.find(current[1]));
+ // current[2] is a bit-vector so we do not need to recurse down it
+
+ bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (arg1 == f.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg2 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_MAX_TOTAL:
+ f.insert(current,
+ symfpu::max<traits>(fpt(current.getType()),
+ (*arg1).second,
+ (*arg2).second,
+ prop(current[2])));
+ break;
+
+ case kind::FLOATINGPOINT_MIN_TOTAL:
+ f.insert(current,
+ symfpu::min<traits>(fpt(current.getType()),
+ (*arg1).second,
+ (*arg2).second,
+ prop(current[2])));
+ break;
+
+ default:
+ Unreachable("Unknown binary floating-point partial function");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_PLUS:
+ case kind::FLOATINGPOINT_SUB:
+ case kind::FLOATINGPOINT_MULT:
+ case kind::FLOATINGPOINT_DIV:
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ fpMap::const_iterator arg1(f.find(current[1]));
+ fpMap::const_iterator arg2(f.find(current[2]));
+ bool recurseNeeded =
+ (mode == r.end()) || (arg1 == f.end()) || (arg2 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg1 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ if (arg2 == f.end())
+ {
+ workStack.push(current[2]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_PLUS:
+ f.insert(current,
+ symfpu::add<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second,
+ (*arg2).second,
+ prop(true)));
+ break;
+
+ case kind::FLOATINGPOINT_SUB:
+ // Should have been removed by the rewriter
+ Unreachable(
+ "Floating-point subtraction should be removed by the "
+ "rewriter.");
+ f.insert(current,
+ symfpu::add<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second,
+ (*arg2).second,
+ prop(false)));
+ break;
+
+ case kind::FLOATINGPOINT_MULT:
+ f.insert(current,
+ symfpu::multiply<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second,
+ (*arg2).second));
+ break;
+ case kind::FLOATINGPOINT_DIV:
+ f.insert(current,
+ symfpu::divide<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second,
+ (*arg2).second));
+ break;
+ case kind::FLOATINGPOINT_REM:
+ /*
+ f.insert(current,
+ symfpu::remainder<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second,
+ (*arg2).second));
+ */
+ Unimplemented(
+ "Remainder with rounding mode not yet supported by "
+ "SMT-LIB");
+ break;
+
+ default:
+ Unreachable("Unknown binary rounded floating-point function");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_FMA:
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ fpMap::const_iterator arg1(f.find(current[1]));
+ fpMap::const_iterator arg2(f.find(current[2]));
+ fpMap::const_iterator arg3(f.find(current[3]));
+ bool recurseNeeded = (mode == r.end()) || (arg1 == f.end())
+ || (arg2 == f.end() || (arg3 == f.end()));
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg1 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ if (arg2 == f.end())
+ {
+ workStack.push(current[2]);
+ }
+ if (arg3 == f.end())
+ {
+ workStack.push(current[3]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ f.insert(current,
+ symfpu::fma<traits>(fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second,
+ (*arg2).second,
+ (*arg3).second));
+ }
+ break;
+
+ /******** Conversions ********/
+ case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ fpMap::const_iterator arg1(f.find(current[1]));
+ bool recurseNeeded = (mode == r.end()) || (arg1 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg1 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ f.insert(
+ current,
+ symfpu::convertFloatToFloat<traits>(fpt(current[1].getType()),
+ fpt(current.getType()),
+ (*mode).second,
+ (*arg1).second));
+ }
+ break;
+
+ case kind::FLOATINGPOINT_FP:
+ {
+ Node IEEEBV(nm->mkNode(
+ kind::BITVECTOR_CONCAT, current[0], current[1], current[2]));
+ f.insert(current,
+ symfpu::unpack<traits>(fpt(current.getType()), IEEEBV));
+ }
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+ f.insert(current,
+ symfpu::unpack<traits>(fpt(current.getType()),
+ ubv(current[0])));
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+ case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ bool recurseNeeded = (mode == r.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+ f.insert(
+ current,
+ symfpu::convertSBVToFloat<traits>(fpt(current.getType()),
+ (*mode).second,
+ sbv(current[1])));
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+ f.insert(
+ current,
+ symfpu::convertUBVToFloat<traits>(fpt(current.getType()),
+ (*mode).second,
+ ubv(current[1])));
+ break;
+
+ default:
+ Unreachable(
+ "Unknown converstion from bit-vector to floating-point");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_REAL:
+ {
+ f.insert(current, buildComponents(current));
+ // Rely on the real theory and theory combination
+ // to handle the value
+ }
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_GENERIC:
+ Unreachable("Generic to_fp not removed");
+ break;
+
+ default: Unreachable("Unknown kind of type FloatingPoint"); break;
+ }
+ }
+ }
+ // Returns a floating-point type so don't alter the return value
+ }
+ else if (t.isBoolean())
+ {
+ boolMap::const_iterator i(b.find(current));
+
+ if (i == b.end())
+ {
+ switch (current.getKind())
+ {
+ /******** Comparisons ********/
+ case kind::EQUAL:
+ {
+ TypeNode childType(current[0].getType());
+
+ if (childType.isFloatingPoint())
+ {
+ fpMap::const_iterator arg1(f.find(current[0]));
+ fpMap::const_iterator arg2(f.find(current[1]));
+ bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (arg1 == f.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg2 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ b.insert(current,
+ symfpu::smtlibEqual<traits>(
+ fpt(childType), (*arg1).second, (*arg2).second));
+ }
+ else if (childType.isRoundingMode())
+ {
+ rmMap::const_iterator arg1(r.find(current[0]));
+ rmMap::const_iterator arg2(r.find(current[1]));
+ bool recurseNeeded = (arg1 == r.end()) || (arg2 == r.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (arg1 == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg2 == r.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ b.insert(current, (*arg1).second == (*arg2).second);
+ }
+ else
+ {
+ CVC4_FPCONV_PASSTHROUGH;
+ return result;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_LEQ:
+ case kind::FLOATINGPOINT_LT:
+ {
+ TypeNode childType(current[0].getType());
+
+ fpMap::const_iterator arg1(f.find(current[0]));
+ fpMap::const_iterator arg2(f.find(current[1]));
+ bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (arg1 == f.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg2 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_LEQ:
+ b.insert(current,
+ symfpu::lessThanOrEqual<traits>(
+ fpt(childType), (*arg1).second, (*arg2).second));
+ break;
+
+ case kind::FLOATINGPOINT_LT:
+ b.insert(current,
+ symfpu::lessThan<traits>(
+ fpt(childType), (*arg1).second, (*arg2).second));
+ break;
+
+ default:
+ Unreachable("Unknown binary floating-point relation");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_ISN:
+ case kind::FLOATINGPOINT_ISSN:
+ case kind::FLOATINGPOINT_ISZ:
+ case kind::FLOATINGPOINT_ISINF:
+ case kind::FLOATINGPOINT_ISNAN:
+ case kind::FLOATINGPOINT_ISNEG:
+ case kind::FLOATINGPOINT_ISPOS:
+ {
+ TypeNode childType(current[0].getType());
+ fpMap::const_iterator arg1(f.find(current[0]));
+
+ if (arg1 == f.end())
+ {
+ workStack.push(current);
+ workStack.push(current[0]);
+ continue; // i.e. recurse!
+ }
+
+ switch (current.getKind())
+ {
+ case kind::FLOATINGPOINT_ISN:
+ b.insert(
+ current,
+ symfpu::isNormal<traits>(fpt(childType), (*arg1).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISSN:
+ b.insert(current,
+ symfpu::isSubnormal<traits>(fpt(childType),
+ (*arg1).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISZ:
+ b.insert(
+ current,
+ symfpu::isZero<traits>(fpt(childType), (*arg1).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISINF:
+ b.insert(
+ current,
+ symfpu::isInfinite<traits>(fpt(childType), (*arg1).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISNAN:
+ b.insert(current,
+ symfpu::isNaN<traits>(fpt(childType), (*arg1).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISPOS:
+ b.insert(
+ current,
+ symfpu::isPositive<traits>(fpt(childType), (*arg1).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISNEG:
+ b.insert(
+ current,
+ symfpu::isNegative<traits>(fpt(childType), (*arg1).second));
+ break;
+
+ default:
+ Unreachable("Unknown unary floating-point relation");
+ break;
+ }
+ }
+ break;
+
+ case kind::FLOATINGPOINT_EQ:
+ case kind::FLOATINGPOINT_GEQ:
+ case kind::FLOATINGPOINT_GT:
+ Unreachable("Kind should have been removed by rewriter.");
+ break;
+
+ // Components will be registered as they are owned by
+ // the floating-point theory. No action is required.
+ case kind::FLOATINGPOINT_COMPONENT_NAN:
+ case kind::FLOATINGPOINT_COMPONENT_INF:
+ case kind::FLOATINGPOINT_COMPONENT_ZERO:
+ case kind::FLOATINGPOINT_COMPONENT_SIGN:
+ /* Fall through... */
+
+ default:
+ CVC4_FPCONV_PASSTHROUGH;
+ return result;
+ break;
+ }
+
+ i = b.find(current);
+ }
+
+ result = (*i).second;
+ }
+ else if (t.isBitVector())
+ {
+ switch (current.getKind())
+ {
+ /******** Conversions ********/
+ case kind::FLOATINGPOINT_TO_UBV_TOTAL:
+ {
+ TypeNode childType(current[1].getType());
+ ubvMap::const_iterator i(u.find(current));
+
+ if (i == u.end())
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ fpMap::const_iterator arg1(f.find(current[1]));
+ bool recurseNeeded = (mode == r.end()) || (arg1 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg1 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ FloatingPointToUBVTotal info =
+ current.getOperator().getConst<FloatingPointToUBVTotal>();
+
+ u.insert(current,
+ symfpu::convertFloatToUBV<traits>(fpt(childType),
+ (*mode).second,
+ (*arg1).second,
+ info.bvs,
+ ubv(current[2])));
+ i = u.find(current);
+ }
+
+ result = (*i).second;
+ }
+ break;
+
+ case kind::FLOATINGPOINT_TO_SBV_TOTAL:
+ {
+ TypeNode childType(current[1].getType());
+ sbvMap::const_iterator i(s.find(current));
+
+ if (i == s.end())
+ {
+ rmMap::const_iterator mode(r.find(current[0]));
+ fpMap::const_iterator arg1(f.find(current[1]));
+ bool recurseNeeded = (mode == r.end()) || (arg1 == f.end());
+
+ if (recurseNeeded)
+ {
+ workStack.push(current);
+ if (mode == r.end())
+ {
+ workStack.push(current[0]);
+ }
+ if (arg1 == f.end())
+ {
+ workStack.push(current[1]);
+ }
+ continue; // i.e. recurse!
+ }
+
+ FloatingPointToSBVTotal info =
+ current.getOperator().getConst<FloatingPointToSBVTotal>();
+
+ s.insert(current,
+ symfpu::convertFloatToSBV<traits>(fpt(childType),
+ (*mode).second,
+ (*arg1).second,
+ info.bvs,
+ sbv(current[2])));
+
+ i = s.find(current);
+ }
+
+ result = (*i).second;
+ }
+ break;
+
+ case kind::FLOATINGPOINT_TO_UBV:
+ Unreachable(
+ "Partially defined fp.to_ubv should have been removed by "
+ "expandDefinition");
+ break;
+
+ case kind::FLOATINGPOINT_TO_SBV:
+ Unreachable(
+ "Partially defined fp.to_sbv should have been removed by "
+ "expandDefinition");
+ break;
+
+ // Again, no action is needed
+ case kind::FLOATINGPOINT_COMPONENT_EXPONENT:
+ case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND:
+ case kind::ROUNDINGMODE_BITBLAST:
+ /* Fall through ... */
+
+ default: CVC4_FPCONV_PASSTHROUGH; break;
+ }
+ }
+ else if (t.isReal())
+ {
+ switch (current.getKind())
+ {
+ /******** Conversions ********/
+ case kind::FLOATINGPOINT_TO_REAL_TOTAL:
+ {
+ // We need to recurse so that any variables that are only
+ // used under this will have components created
+ // (via auxiliary constraints)
+
+ TypeNode childType(current[0].getType());
+ fpMap::const_iterator arg1(f.find(current[0]));
+
+ if (arg1 == f.end())
+ {
+ workStack.push(current);
+ workStack.push(current[0]);
+ continue; // i.e. recurse!
+ }
+
+ // However we don't need to do anything explicitly with
+ // this as it will be treated as an uninterpreted function
+ // by the real theory and we don't need to bit-blast the
+ // float expression unless we need to say something about
+ // its value.
+ }
+
+ break;
+
+ case kind::FLOATINGPOINT_TO_REAL:
+ Unreachable(
+ "Partially defined fp.to_real should have been removed by "
+ "expandDefinition");
+ break;
+
+ default: CVC4_FPCONV_PASSTHROUGH; break;
+ }
+ }
+ else
+ {
+ CVC4_FPCONV_PASSTHROUGH;
+ }
+ }
+
+ return result;
+#else
+ Unimplemented("Conversion is dependent on SymFPU");
+#endif
+}
+
+#undef CVC4_FPCONV_PASSTHROUGH
+
+Node FpConverter::getValue(Valuation &val, TNode var)
+{
+ Assert(Theory::isLeafOf(var, THEORY_FP));
+
+#ifdef CVC4_USE_SYMFPU
+ TypeNode t(var.getType());
+
+ if (t.isRoundingMode())
+ {
+ rmMap::const_iterator i(r.find(var));
+
+ if (i == r.end())
+ {
+ Unreachable("Asking for the value of an unregistered expression");
+ }
+ else
+ {
+ Node value = rmToNode((*i).second);
+ return value;
+ }
+ }
+ else if (t.isFloatingPoint())
+ {
+ fpMap::const_iterator i(f.find(var));
+
+ if (i == f.end())
+ {
+ Unreachable("Asking for the value of an unregistered expression");
+ }
+ else
+ {
+ Node value = ufToNode(fpt(t), (*i).second);
+ return value;
+ }
+ }
+ else
+ {
+ Unreachable(
+ "Asking for the value of a type that is not managed by the "
+ "floating-point theory");
+ }
+
+ Unreachable("Unable to find value");
+
+#else
+ Unimplemented("Conversion is dependent on SymFPU");
+#endif
-Node FpConverter::getValue(Valuation &val, TNode var) {
- Unimplemented("Conversion not implemented.");
+ return Node::null();
}
} // namespace fp
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index 8a054e03a..5a7b839aa 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -21,12 +21,30 @@
#ifndef __CVC4__THEORY__FP__FP_CONVERTER_H
#define __CVC4__THEORY__FP__FP_CONVERTER_H
+#include "base/cvc4_assert.h"
#include "context/cdhashmap.h"
#include "context/cdlist.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/type.h"
#include "theory/valuation.h"
+#include "util/bitvector.h"
#include "util/floatingpoint.h"
#include "util/hash.h"
+#ifdef CVC4_USE_SYMFPU
+#include "symfpu/core/unpackedFloat.h"
+#endif
+
+#ifdef CVC4_SYM_SYMBOLIC_EVAL
+// This allows debugging of the CVC4 symbolic back-end.
+// By enabling this and disabling constant folding in the rewriter,
+// SMT files that have operations on constants will be evaluated
+// during the encoding step, which means that the expressions
+// generated by the symbolic back-end can be debugged with gdb.
+#include "theory/rewriter.h"
+#endif
+
namespace CVC4 {
namespace theory {
namespace fp {
@@ -35,7 +53,292 @@ typedef PairHashFunction<TypeNode, TypeNode, TypeNodeHashFunction,
TypeNodeHashFunction>
PairTypeNodeHashFunction;
-class FpConverter {
+/**
+ * This is a symfpu symbolic "back-end". It allows the library to be used to
+ * construct bit-vector expressions that compute floating-point operations.
+ * This is effectively the glue between symfpu's notion of "signed bit-vector"
+ * and CVC4's node.
+ */
+namespace symfpuSymbolic {
+
+// Forward declarations of the wrapped types so that traits can be defined early
+// and used in the implementations
+class symbolicRoundingMode;
+class floatingPointTypeInfo;
+class symbolicProposition;
+template <bool T>
+class symbolicBitVector;
+
+// This is the template parameter for symfpu's templates.
+class traits
+{
+ public:
+ // The six key types that symfpu uses.
+ typedef unsigned bwt;
+ typedef symbolicRoundingMode rm;
+ typedef floatingPointTypeInfo fpt;
+ typedef symbolicProposition prop;
+ typedef symbolicBitVector<true> sbv;
+ typedef symbolicBitVector<false> ubv;
+
+ // Give concrete instances (wrapped nodes) for each rounding mode.
+ static symbolicRoundingMode RNE(void);
+ static symbolicRoundingMode RNA(void);
+ static symbolicRoundingMode RTP(void);
+ static symbolicRoundingMode RTN(void);
+ static symbolicRoundingMode RTZ(void);
+
+ // Properties used by symfpu
+ static void precondition(const bool b);
+ static void postcondition(const bool b);
+ static void invariant(const bool b);
+ static void precondition(const prop &p);
+ static void postcondition(const prop &p);
+ static void invariant(const prop &p);
+};
+
+// Use the same type names as symfpu.
+typedef traits::bwt bwt;
+
+/**
+ * Wrap the CVC4::Node types so that we can debug issues with this back-end
+ */
+class nodeWrapper : public Node
+{
+ protected:
+/* CVC4_SYM_SYMBOLIC_EVAL is for debugging CVC4 symbolic back-end issues.
+ * Enable this and disabling constant folding will mean that operations
+ * that are input with constant args are 'folded' using the symbolic encoding
+ * allowing them to be traced via GDB.
+ */
+#ifdef CVC4_SYM_SYMBOLIC_EVAL
+ nodeWrapper(const Node &n) : Node(theory::Rewriter::rewrite(n)) {}
+#else
+ nodeWrapper(const Node &n) : Node(n) {}
+#endif
+};
+
+class symbolicProposition : public nodeWrapper
+{
+ protected:
+ bool checkNodeType(const TNode node);
+
+#ifdef CVC4_USE_SYMFPU
+ friend ::symfpu::ite<symbolicProposition, symbolicProposition>; // For ITE
+#endif
+
+ public:
+ symbolicProposition(const Node n);
+ symbolicProposition(bool v);
+ symbolicProposition(const symbolicProposition &old);
+
+ symbolicProposition operator!(void)const;
+ symbolicProposition operator&&(const symbolicProposition &op) const;
+ symbolicProposition operator||(const symbolicProposition &op) const;
+ symbolicProposition operator==(const symbolicProposition &op) const;
+ symbolicProposition operator^(const symbolicProposition &op) const;
+};
+
+class symbolicRoundingMode : public nodeWrapper
+{
+ protected:
+ bool checkNodeType(const TNode n);
+
+#ifdef CVC4_USE_SYMFPU
+ friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>; // For ITE
+#endif
+
+ public:
+ symbolicRoundingMode(const Node n);
+ symbolicRoundingMode(const unsigned v);
+ symbolicRoundingMode(const symbolicRoundingMode &old);
+
+ symbolicProposition valid(void) const;
+ symbolicProposition operator==(const symbolicRoundingMode &op) const;
+};
+
+// Type function for mapping between types
+template <bool T>
+struct signedToLiteralType;
+
+template <>
+struct signedToLiteralType<true>
+{
+ typedef int literalType;
+};
+template <>
+struct signedToLiteralType<false>
+{
+ typedef unsigned int literalType;
+};
+
+template <bool isSigned>
+class symbolicBitVector : public nodeWrapper
+{
+ protected:
+ typedef typename signedToLiteralType<isSigned>::literalType literalType;
+
+ Node boolNodeToBV(Node node) const;
+ Node BVToBoolNode(Node node) const;
+
+ Node fromProposition(Node node) const;
+ Node toProposition(Node node) const;
+ bool checkNodeType(const TNode n);
+ friend symbolicBitVector<!isSigned>; // To allow conversion between the types
+
+#ifdef CVC4_USE_SYMFPU
+ friend ::symfpu::ite<symbolicProposition,
+ symbolicBitVector<isSigned> >; // For ITE
+#endif
+
+ public:
+ symbolicBitVector(const Node n);
+ symbolicBitVector(const bwt w, const unsigned v);
+ symbolicBitVector(const symbolicProposition &p);
+ symbolicBitVector(const symbolicBitVector<isSigned> &old);
+ symbolicBitVector(const BitVector &old);
+
+ bwt getWidth(void) const;
+
+ /*** Constant creation and test ***/
+ static symbolicBitVector<isSigned> one(const bwt &w);
+ static symbolicBitVector<isSigned> zero(const bwt &w);
+ static symbolicBitVector<isSigned> allOnes(const bwt &w);
+
+ symbolicProposition isAllOnes() const;
+ symbolicProposition isAllZeros() const;
+
+ static symbolicBitVector<isSigned> maxValue(const bwt &w);
+ static symbolicBitVector<isSigned> minValue(const bwt &w);
+
+ /*** Operators ***/
+ symbolicBitVector<isSigned> operator<<(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator>>(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator|(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator&(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator+(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator-(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator*(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator/(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator%(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> operator-(void) const;
+ symbolicBitVector<isSigned> operator~(void)const;
+ symbolicBitVector<isSigned> increment() const;
+ symbolicBitVector<isSigned> decrement() const;
+ symbolicBitVector<isSigned> signExtendRightShift(
+ const symbolicBitVector<isSigned> &op) const;
+
+ /*** Modular operations ***/
+ // This back-end doesn't do any overflow checking so these are the same as
+ // other operations
+ symbolicBitVector<isSigned> modularLeftShift(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> modularRightShift(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> modularIncrement() const;
+ symbolicBitVector<isSigned> modularDecrement() const;
+ symbolicBitVector<isSigned> modularAdd(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> modularNegate() const;
+
+ /*** Comparisons ***/
+ symbolicProposition operator==(const symbolicBitVector<isSigned> &op) const;
+ symbolicProposition operator<=(const symbolicBitVector<isSigned> &op) const;
+ symbolicProposition operator>=(const symbolicBitVector<isSigned> &op) const;
+ symbolicProposition operator<(const symbolicBitVector<isSigned> &op) const;
+ symbolicProposition operator>(const symbolicBitVector<isSigned> &op) const;
+
+ /*** Type conversion ***/
+ // CVC4 nodes make no distinction between signed and unsigned, thus these are
+ // trivial
+ symbolicBitVector<true> toSigned(void) const;
+ symbolicBitVector<false> toUnsigned(void) const;
+
+ /*** Bit hacks ***/
+ symbolicBitVector<isSigned> extend(bwt extension) const;
+ symbolicBitVector<isSigned> contract(bwt reduction) const;
+ symbolicBitVector<isSigned> resize(bwt newSize) const;
+ symbolicBitVector<isSigned> matchWidth(
+ const symbolicBitVector<isSigned> &op) const;
+ symbolicBitVector<isSigned> append(
+ const symbolicBitVector<isSigned> &op) const;
+
+ // Inclusive of end points, thus if the same, extracts just one bit
+ symbolicBitVector<isSigned> extract(bwt upper, bwt lower) const;
+};
+
+// Use the same type information as the literal back-end but add an interface to
+// TypeNodes for convenience.
+class floatingPointTypeInfo : public FloatingPointSize
+{
+ public:
+ floatingPointTypeInfo(const TypeNode t);
+ floatingPointTypeInfo(unsigned exp, unsigned sig);
+ floatingPointTypeInfo(const floatingPointTypeInfo &old);
+
+ TypeNode getTypeNode(void) const;
+};
+}
+
+/**
+ * This class uses SymFPU to convert an expression containing floating-point
+ * kinds and operations into a logically equivalent form with bit-vector
+ * operations replacing the floating-point ones. It also has a getValue method
+ * to produce an expression which will reconstruct the value of the
+ * floating-point terms from a valuation.
+ *
+ * Internally it caches all of the unpacked floats so that unnecessary packing
+ * and unpacking operations are avoided and to make best use of structural
+ * sharing.
+ */
+class FpConverter
+{
+ protected:
+#ifdef CVC4_USE_SYMFPU
+ typedef symfpuSymbolic::traits traits;
+ typedef ::symfpu::unpackedFloat<symfpuSymbolic::traits> uf;
+ typedef symfpuSymbolic::traits::rm rm;
+ typedef symfpuSymbolic::traits::fpt fpt;
+ typedef symfpuSymbolic::traits::prop prop;
+ typedef symfpuSymbolic::traits::ubv ubv;
+ typedef symfpuSymbolic::traits::sbv sbv;
+
+ typedef context::CDHashMap<Node, uf, NodeHashFunction> fpMap;
+ typedef context::CDHashMap<Node, rm, NodeHashFunction> rmMap;
+ typedef context::CDHashMap<Node, prop, NodeHashFunction> boolMap;
+ typedef context::CDHashMap<Node, ubv, NodeHashFunction> ubvMap;
+ typedef context::CDHashMap<Node, sbv, NodeHashFunction> sbvMap;
+
+ fpMap f;
+ rmMap r;
+ boolMap b;
+ ubvMap u;
+ sbvMap s;
+
+ /* These functions take a symfpu object and convert it to a node.
+ * These should ensure that constant folding it will give a
+ * constant of the right type.
+ */
+
+ Node ufToNode(const fpt &, const uf &) const;
+ Node rmToNode(const rm &) const;
+ Node propToNode(const prop &) const;
+ Node ubvToNode(const ubv &) const;
+ Node sbvToNode(const sbv &) const;
+
+ /* Creates the relevant components for a variable */
+ uf buildComponents(TNode current);
+#endif
+
public:
context::CDList<Node> d_additionalAssertions;
diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds
index 966ed4d71..b1170b42c 100644
--- a/src/theory/fp/kinds
+++ b/src/theory/fp/kinds
@@ -283,4 +283,28 @@ operator FLOATINGPOINT_TO_REAL_TOTAL 2 "floating-point to real (defined for all
typerule FLOATINGPOINT_TO_REAL_TOTAL ::CVC4::theory::fp::FloatingPointToRealTotalTypeRule
+
+operator FLOATINGPOINT_COMPONENT_NAN 1 "NaN component of a word-blasted floating-point number"
+typerule FLOATINGPOINT_COMPONENT_NAN ::CVC4::theory::fp::FloatingPointComponentBit
+
+operator FLOATINGPOINT_COMPONENT_INF 1 "Inf component of a word-blasted floating-point number"
+typerule FLOATINGPOINT_COMPONENT_INF ::CVC4::theory::fp::FloatingPointComponentBit
+
+operator FLOATINGPOINT_COMPONENT_ZERO 1 "Zero component of a word-blasted floating-point number"
+typerule FLOATINGPOINT_COMPONENT_ZERO ::CVC4::theory::fp::FloatingPointComponentBit
+
+operator FLOATINGPOINT_COMPONENT_SIGN 1 "Sign component of a word-blasted floating-point number"
+typerule FLOATINGPOINT_COMPONENT_SIGN ::CVC4::theory::fp::FloatingPointComponentBit
+
+operator FLOATINGPOINT_COMPONENT_EXPONENT 1 "Exponent component of a word-blasted floating-point number"
+typerule FLOATINGPOINT_COMPONENT_EXPONENT ::CVC4::theory::fp::FloatingPointComponentExponent
+
+operator FLOATINGPOINT_COMPONENT_SIGNIFICAND 1 "Significand component of a word-blasted floating-point number"
+typerule FLOATINGPOINT_COMPONENT_SIGNIFICAND ::CVC4::theory::fp::FloatingPointComponentSignificand
+
+
+operator ROUNDINGMODE_BITBLAST 1 "The bit-vector for a non-deterministic rounding mode"
+typerule ROUNDINGMODE_BITBLAST ::CVC4::theory::fp::RoundingModeBitBlast
+
+
endtheory
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 748c5c1c6..94733b98d 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -16,6 +16,7 @@
**/
#include "theory/fp/theory_fp.h"
+#include "theory/rewriter.h"
#include "theory/theory_model.h"
#include <set>
@@ -95,8 +96,10 @@ Node buildConjunct(const std::vector<TNode> &assumptions) {
} // namespace helper
/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-TheoryFp::TheoryFp(context::Context *c, context::UserContext *u,
- OutputChannel &out, Valuation valuation,
+TheoryFp::TheoryFp(context::Context *c,
+ context::UserContext *u,
+ OutputChannel &out,
+ Valuation valuation,
const LogicInfo &logicInfo)
: Theory(THEORY_FP, c, u, out, valuation, logicInfo),
d_notification(*this),
@@ -110,7 +113,11 @@ TheoryFp::TheoryFp(context::Context *c, context::UserContext *u,
d_maxMap(u),
d_toUBVMap(u),
d_toSBVMap(u),
- d_toRealMap(u) {
+ d_toRealMap(u),
+ realToFloatMap(u),
+ floatToRealMap(u),
+ abstractionMap(u)
+{
// Kinds that are to be handled in the congruence closure
d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_ABS);
@@ -157,6 +164,14 @@ TheoryFp::TheoryFp(context::Context *c, context::UserContext *u,
d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_SBV_TOTAL);
d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_TO_REAL_TOTAL);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_NAN);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_INF);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_ZERO);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_SIGN);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_EXPONENT);
+ d_equalityEngine.addFunctionKind(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND);
+ d_equalityEngine.addFunctionKind(kind::ROUNDINGMODE_BITBLAST);
+
} /* TheoryFp::TheoryFp() */
Node TheoryFp::minUF(Node node) {
@@ -291,7 +306,7 @@ Node TheoryFp::toRealUF(Node node) {
std::vector<TypeNode> args(1);
args[0] = t;
fun = nm->mkSkolem("floatingpoint_to_real_infinity_and_NaN_case",
- nm->mkFunctionType(t, nm->realType()),
+ nm->mkFunctionType(args, nm->realType()),
"floatingpoint_to_real_infinity_and_NaN_case",
NodeManager::SKOLEM_EXACT_NAME);
d_toRealMap.insert(t, fun);
@@ -301,16 +316,85 @@ Node TheoryFp::toRealUF(Node node) {
return nm->mkNode(kind::APPLY_UF, fun, node[0]);
}
-Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) {
- Trace("fp-expandDefinition")
- << "TheoryFp::expandDefinition(): " << node << std::endl;
-
+void TheoryFp::enableUF(LogicRequest &lr)
+{
if (!this->d_expansionRequested) {
- lr.widenLogic(
- THEORY_UF); // Needed for conversions to/from real and min/max
- lr.widenLogic(THEORY_BV);
+ // Needed for conversions to/from real and min/max
+ lr.widenLogic(THEORY_UF);
+ // THEORY_BV has to be enabled when the logic is set
this->d_expansionRequested = true;
}
+ return;
+}
+
+Node TheoryFp::abstractRealToFloat(Node node)
+{
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
+ TypeNode t(node.getType());
+ Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ NodeManager *nm = NodeManager::currentNM();
+ ComparisonUFMap::const_iterator i(realToFloatMap.find(t));
+
+ Node fun;
+ if (i == realToFloatMap.end())
+ {
+ std::vector<TypeNode> args(2);
+ args[0] = node[0].getType();
+ args[1] = node[1].getType();
+ fun = nm->mkSkolem("floatingpoint_abstract_real_to_float",
+ nm->mkFunctionType(args, node.getType()),
+ "floatingpoint_abstract_real_to_float",
+ NodeManager::SKOLEM_EXACT_NAME);
+ realToFloatMap.insert(t, fun);
+ }
+ else
+ {
+ fun = (*i).second;
+ }
+ Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
+
+ abstractionMap.insert(uf, node);
+
+ return uf;
+}
+
+Node TheoryFp::abstractFloatToReal(Node node)
+{
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL);
+ TypeNode t(node[0].getType());
+ Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ NodeManager *nm = NodeManager::currentNM();
+ ComparisonUFMap::const_iterator i(floatToRealMap.find(t));
+
+ Node fun;
+ if (i == floatToRealMap.end())
+ {
+ std::vector<TypeNode> args(2);
+ args[0] = t;
+ args[1] = nm->realType();
+ fun = nm->mkSkolem("floatingpoint_abstract_float_to_real",
+ nm->mkFunctionType(args, nm->realType()),
+ "floatingpoint_abstract_float_to_real",
+ NodeManager::SKOLEM_EXACT_NAME);
+ floatToRealMap.insert(t, fun);
+ }
+ else
+ {
+ fun = (*i).second;
+ }
+ Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
+
+ abstractionMap.insert(uf, node);
+
+ return uf;
+}
+
+Node TheoryFp::expandDefinition(LogicRequest &lr, Node node)
+{
+ Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
+ << std::endl;
Node res = node;
@@ -318,14 +402,17 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) {
res = removeToFPGeneric::removeToFPGeneric(node);
} else if (node.getKind() == kind::FLOATINGPOINT_MIN) {
+ enableUF(lr);
res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MIN_TOTAL,
node[0], node[1], minUF(node));
} else if (node.getKind() == kind::FLOATINGPOINT_MAX) {
+ enableUF(lr);
res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MAX_TOTAL,
node[0], node[1], maxUF(node));
} else if (node.getKind() == kind::FLOATINGPOINT_TO_UBV) {
+ enableUF(lr);
FloatingPointToUBV info = node.getOperator().getConst<FloatingPointToUBV>();
FloatingPointToUBVTotal newInfo(info);
@@ -335,6 +422,7 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) {
toUBVUF(node));
} else if (node.getKind() == kind::FLOATINGPOINT_TO_SBV) {
+ enableUF(lr);
FloatingPointToSBV info = node.getOperator().getConst<FloatingPointToSBV>();
FloatingPointToSBVTotal newInfo(info);
@@ -344,6 +432,7 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) {
toSBVUF(node));
} else if (node.getKind() == kind::FLOATINGPOINT_TO_REAL) {
+ enableUF(lr);
res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL,
node[0], toRealUF(node));
@@ -351,6 +440,13 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) {
// Do nothing
}
+ // We will need to enable UF to abstract these in ppRewrite
+ if (res.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL
+ || res.getKind() == kind::FLOATINGPOINT_TO_FP_REAL)
+ {
+ enableUF(lr);
+ }
+
if (res != node) {
Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
<< " rewritten to " << res << std::endl;
@@ -359,6 +455,290 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node) {
return res;
}
+Node TheoryFp::ppRewrite(TNode node)
+{
+ Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl;
+
+ Node res = node;
+
+ // Abstract conversion functions
+ if (node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL)
+ {
+ res = abstractFloatToReal(node);
+
+ // Generate some lemmas
+ NodeManager *nm = NodeManager::currentNM();
+
+ Node pd =
+ nm->mkNode(kind::IMPLIES,
+ nm->mkNode(kind::OR,
+ nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]),
+ nm->mkNode(kind::FLOATINGPOINT_ISINF, node[0])),
+ nm->mkNode(kind::EQUAL, res, node[1]));
+ handleLemma(pd);
+
+ Node z =
+ nm->mkNode(kind::IMPLIES,
+ nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]),
+ nm->mkNode(kind::EQUAL, res, nm->mkConst(Rational(0U))));
+ handleLemma(z);
+
+ // TODO : bounds on the output from largest floats, #1914
+ }
+ else if (node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL)
+ {
+ res = abstractRealToFloat(node);
+
+ // Generate some lemmas
+ NodeManager *nm = NodeManager::currentNM();
+
+ Node nnan =
+ nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, res));
+ handleLemma(nnan);
+
+ Node z = nm->mkNode(
+ kind::IMPLIES,
+ nm->mkNode(kind::EQUAL, node[1], nm->mkConst(Rational(0U))),
+ nm->mkNode(kind::EQUAL,
+ res,
+ nm->mkConst(FloatingPoint::makeZero(
+ res.getType().getConst<FloatingPointSize>(), false))));
+ handleLemma(z);
+
+ // TODO : rounding-mode specific bounds on floats that don't give infinity
+ // BEWARE of directed rounding! #1914
+ }
+
+ if (res != node)
+ {
+ Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): node " << node
+ << " rewritten to " << res << std::endl;
+ }
+
+ return res;
+}
+
+bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
+{
+ Trace("fp-refineAbstraction") << "TheoryFp::refineAbstraction(): " << abstract
+ << " vs. " << concrete << std::endl;
+ Kind k = concrete.getKind();
+ if (k == kind::FLOATINGPOINT_TO_REAL_TOTAL)
+ {
+ // Get the values
+ Assert(m->hasTerm(abstract));
+ Assert(m->hasTerm(concrete[0]));
+ Assert(m->hasTerm(concrete[1]));
+
+ Node abstractValue = m->getValue(abstract);
+ Node floatValue = m->getValue(concrete[0]);
+ Node undefValue = m->getValue(concrete[1]);
+
+ Assert(abstractValue.isConst());
+ Assert(floatValue.isConst());
+ Assert(undefValue.isConst());
+
+ // Work out the actual value for those args
+ NodeManager *nm = NodeManager::currentNM();
+
+ Node evaluate =
+ nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL, floatValue, undefValue);
+ Node concreteValue = Rewriter::rewrite(evaluate);
+ Assert(concreteValue.isConst());
+
+ Trace("fp-refineAbstraction")
+ << "TheoryFp::refineAbstraction(): " << concrete[0] << " = "
+ << floatValue << std::endl
+ << "TheoryFp::refineAbstraction(): " << concrete[1] << " = "
+ << undefValue << std::endl
+ << "TheoryFp::refineAbstraction(): " << abstract << " = "
+ << abstractValue << std::endl
+ << "TheoryFp::refineAbstraction(): " << concrete << " = "
+ << concreteValue << std::endl;
+
+ if (abstractValue != concreteValue)
+ {
+ // Need refinement lemmas
+ // only in the normal and subnormal case
+ Assert(floatValue.getConst<FloatingPoint>().isNormal()
+ || floatValue.getConst<FloatingPoint>().isSubnormal());
+
+ Node defined = nm->mkNode(
+ kind::AND,
+ nm->mkNode(kind::NOT,
+ nm->mkNode(kind::FLOATINGPOINT_ISNAN, concrete[0])),
+ nm->mkNode(kind::NOT,
+ nm->mkNode(kind::FLOATINGPOINT_ISINF, concrete[0])));
+ // First the "forward" constraints
+ Node fg = nm->mkNode(
+ kind::IMPLIES,
+ defined,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(kind::FLOATINGPOINT_GEQ, concrete[0], floatValue),
+ nm->mkNode(kind::GEQ, abstract, concreteValue)));
+ handleLemma(fg);
+
+ Node fl = nm->mkNode(
+ kind::IMPLIES,
+ defined,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(kind::FLOATINGPOINT_LEQ, concrete[0], floatValue),
+ nm->mkNode(kind::LEQ, abstract, concreteValue)));
+ handleLemma(fl);
+
+ // Then the backwards constraints
+ Node floatAboveAbstract = Rewriter::rewrite(
+ nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
+ nm->mkConst(FloatingPointToFPReal(
+ concrete[0].getType().getConst<FloatingPointSize>())),
+ nm->mkConst(roundTowardPositive),
+ abstractValue));
+
+ Node bg = nm->mkNode(
+ kind::IMPLIES,
+ defined,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(
+ kind::FLOATINGPOINT_GEQ, concrete[0], floatAboveAbstract),
+ nm->mkNode(kind::GEQ, abstract, abstractValue)));
+ handleLemma(bg);
+
+ Node floatBelowAbstract = Rewriter::rewrite(
+ nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
+ nm->mkConst(FloatingPointToFPReal(
+ concrete[0].getType().getConst<FloatingPointSize>())),
+ nm->mkConst(roundTowardNegative),
+ abstractValue));
+
+ Node bl = nm->mkNode(
+ kind::IMPLIES,
+ defined,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(
+ kind::FLOATINGPOINT_LEQ, concrete[0], floatBelowAbstract),
+ nm->mkNode(kind::LEQ, abstract, abstractValue)));
+ handleLemma(bl);
+ // TODO : see if the overflow conditions could be improved #1914
+
+ return true;
+ }
+ else
+ {
+ // No refinement needed
+ return false;
+ }
+ }
+ else if (k == kind::FLOATINGPOINT_TO_FP_REAL)
+ {
+ // Get the values
+ Assert(m->hasTerm(abstract));
+ Assert(m->hasTerm(concrete[0]));
+ Assert(m->hasTerm(concrete[1]));
+
+ Node abstractValue = m->getValue(abstract);
+ Node rmValue = m->getValue(concrete[0]);
+ Node realValue = m->getValue(concrete[1]);
+
+ Assert(abstractValue.isConst());
+ Assert(rmValue.isConst());
+ Assert(realValue.isConst());
+
+ // Work out the actual value for those args
+ NodeManager *nm = NodeManager::currentNM();
+
+ Node evaluate =
+ nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
+ nm->mkConst(FloatingPointToFPReal(
+ concrete.getType().getConst<FloatingPointSize>())),
+ rmValue,
+ realValue);
+ Node concreteValue = Rewriter::rewrite(evaluate);
+ Assert(concreteValue.isConst());
+
+ Trace("fp-refineAbstraction")
+ << "TheoryFp::refineAbstraction(): " << concrete[0] << " = " << rmValue
+ << std::endl
+ << "TheoryFp::refineAbstraction(): " << concrete[1] << " = "
+ << realValue << std::endl
+ << "TheoryFp::refineAbstraction(): " << abstract << " = "
+ << abstractValue << std::endl
+ << "TheoryFp::refineAbstraction(): " << concrete << " = "
+ << concreteValue << std::endl;
+
+ if (abstractValue != concreteValue)
+ {
+ Assert(!abstractValue.getConst<FloatingPoint>().isNaN());
+ Assert(!concreteValue.getConst<FloatingPoint>().isNaN());
+
+ Node correctRoundingMode = nm->mkNode(kind::EQUAL, concrete[0], rmValue);
+ // TODO : Generalise to all rounding modes #1914
+
+ // First the "forward" constraints
+ Node fg = nm->mkNode(
+ kind::IMPLIES,
+ correctRoundingMode,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(kind::GEQ, concrete[1], realValue),
+ nm->mkNode(kind::FLOATINGPOINT_GEQ, abstract, concreteValue)));
+ handleLemma(fg);
+
+ Node fl = nm->mkNode(
+ kind::IMPLIES,
+ correctRoundingMode,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(kind::LEQ, concrete[1], realValue),
+ nm->mkNode(kind::FLOATINGPOINT_LEQ, abstract, concreteValue)));
+ handleLemma(fl);
+
+ // Then the backwards constraints
+ if (!abstractValue.getConst<FloatingPoint>().isInfinite())
+ {
+ Node realValueOfAbstract =
+ Rewriter::rewrite(nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL,
+ abstractValue,
+ nm->mkConst(Rational(0U))));
+
+ Node bg = nm->mkNode(
+ kind::IMPLIES,
+ correctRoundingMode,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(kind::GEQ, concrete[1], realValueOfAbstract),
+ nm->mkNode(kind::FLOATINGPOINT_GEQ, abstract, abstractValue)));
+ handleLemma(bg);
+
+ Node bl = nm->mkNode(
+ kind::IMPLIES,
+ correctRoundingMode,
+ nm->mkNode(
+ kind::EQUAL,
+ nm->mkNode(kind::LEQ, concrete[1], realValueOfAbstract),
+ nm->mkNode(kind::FLOATINGPOINT_LEQ, abstract, abstractValue)));
+ handleLemma(bl);
+ }
+
+ return true;
+ }
+ else
+ {
+ // No refinement needed
+ return false;
+ }
+ }
+ else
+ {
+ Unreachable("Unknown abstraction");
+ }
+
+ return false;
+}
+
void TheoryFp::convertAndEquateTerm(TNode node) {
Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl;
size_t oldAdditionalAssertions = d_conv.d_additionalAssertions.size();
@@ -441,6 +821,52 @@ void TheoryFp::registerTerm(TNode node) {
d_equalityEngine.addTerm(node);
}
+ // Give the expansion of classifications in terms of equalities
+ // This should make equality reasoning slightly more powerful.
+ if ((node.getKind() == kind::FLOATINGPOINT_ISNAN)
+ || (node.getKind() == kind::FLOATINGPOINT_ISZ)
+ || (node.getKind() == kind::FLOATINGPOINT_ISINF))
+ {
+ NodeManager *nm = NodeManager::currentNM();
+ FloatingPointSize s = node[0].getType().getConst<FloatingPointSize>();
+ Node equalityAlias = Node::null();
+
+ if (node.getKind() == kind::FLOATINGPOINT_ISNAN)
+ {
+ equalityAlias = nm->mkNode(
+ kind::EQUAL, node[0], nm->mkConst(FloatingPoint::makeNaN(s)));
+ }
+ else if (node.getKind() == kind::FLOATINGPOINT_ISZ)
+ {
+ equalityAlias = nm->mkNode(
+ kind::OR,
+ nm->mkNode(kind::EQUAL,
+ node[0],
+ nm->mkConst(FloatingPoint::makeZero(s, true))),
+ nm->mkNode(kind::EQUAL,
+ node[0],
+ nm->mkConst(FloatingPoint::makeZero(s, false))));
+ }
+ else if (node.getKind() == kind::FLOATINGPOINT_ISINF)
+ {
+ equalityAlias = nm->mkNode(
+ kind::OR,
+ nm->mkNode(kind::EQUAL,
+ node[0],
+ nm->mkConst(FloatingPoint::makeInf(s, true))),
+ nm->mkNode(kind::EQUAL,
+ node[0],
+ nm->mkConst(FloatingPoint::makeInf(s, false))));
+ }
+ else
+ {
+ Unreachable("Only isNaN, isInf and isZero have aliases");
+ }
+
+ handleLemma(nm->mkNode(kind::EQUAL, node, equalityAlias));
+ }
+
+ // Use symfpu to produce an equivalent bit-vector statement
convertAndEquateTerm(node);
}
return;
@@ -545,6 +971,25 @@ void TheoryFp::check(Effort level) {
}
}
+ // Resolve the abstractions for the conversion lemmas
+ // if (level == EFFORT_COMBINATION) {
+ if (level == EFFORT_LAST_CALL)
+ {
+ Trace("fp") << "TheoryFp::check(): checking abstractions" << std::endl;
+ TheoryModel *m = getValuation().getModel();
+ bool lemmaAdded = false;
+
+ for (abstractionMapType::const_iterator i = abstractionMap.begin();
+ i != abstractionMap.end();
+ ++i)
+ {
+ if (m->hasTerm((*i).first))
+ { // Is actually used in the model
+ lemmaAdded |= refineAbstraction(m, (*i).first, (*i).second);
+ }
+ }
+ }
+
Trace("fp") << "TheoryFp::check(): completed" << std::endl;
/* Checking should be handled by the bit-vector engine */
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 688c6e600..6234ab8ad 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -43,8 +43,11 @@ class TheoryFp : public Theory {
void preRegisterTerm(TNode node) override;
void addSharedTerm(TNode node) override;
+ Node ppRewrite(TNode node);
+
void check(Effort) override;
+ bool needsCheckLastEffort() { return true; }
Node getModelValue(TNode var) override;
bool collectModelInfo(TheoryModel* m) override;
@@ -100,6 +103,8 @@ class TheoryFp : public Theory {
context::CDO<Node> d_conflictNode;
/** Uninterpretted functions for partially defined functions. **/
+ void enableUF(LogicRequest& lr);
+
typedef context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>
ComparisonUFMap;
@@ -122,6 +127,21 @@ class TheoryFp : public Theory {
ComparisonUFMap d_toRealMap;
Node toRealUF(Node);
+
+ /** Uninterpretted functions for lazy handling of conversions */
+ typedef ComparisonUFMap conversionAbstractionMap;
+
+ conversionAbstractionMap realToFloatMap;
+ conversionAbstractionMap floatToRealMap;
+
+ Node abstractRealToFloat(Node);
+ Node abstractFloatToReal(Node);
+
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> abstractionMapType;
+ abstractionMapType abstractionMap; // abstract -> original
+
+ bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
+
}; /* class TheoryFp */
} // namespace fp
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 9fda5c2f6..f502ad547 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -34,6 +34,7 @@
#include <algorithm>
#include "base/cvc4_assert.h"
+#include "theory/fp/fp_converter.h"
#include "theory/fp/theory_fp_rewriter.h"
namespace CVC4 {
@@ -787,6 +788,118 @@ namespace constantFold {
}
}
+ RewriteResponse componentFlag(TNode node, bool)
+ {
+ Kind k = node.getKind();
+
+ Assert((k == kind::FLOATINGPOINT_COMPONENT_NAN)
+ || (k == kind::FLOATINGPOINT_COMPONENT_INF)
+ || (k == kind::FLOATINGPOINT_COMPONENT_ZERO)
+ || (k == kind::FLOATINGPOINT_COMPONENT_SIGN));
+
+ FloatingPoint arg0(node[0].getConst<FloatingPoint>());
+
+ bool result;
+ switch (k)
+ {
+#ifdef CVC4_USE_SYMFPU
+ case kind::FLOATINGPOINT_COMPONENT_NAN:
+ result = arg0.getLiteral().nan;
+ break;
+ case kind::FLOATINGPOINT_COMPONENT_INF:
+ result = arg0.getLiteral().inf;
+ break;
+ case kind::FLOATINGPOINT_COMPONENT_ZERO:
+ result = arg0.getLiteral().zero;
+ break;
+ case kind::FLOATINGPOINT_COMPONENT_SIGN:
+ result = arg0.getLiteral().sign;
+ break;
+#endif
+ default: Unreachable("Unknown kind used in componentFlag"); break;
+ }
+
+ BitVector res(1U, (result) ? 1U : 0U);
+
+ return RewriteResponse(REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(res));
+ }
+
+ RewriteResponse componentExponent(TNode node, bool)
+ {
+ Assert(node.getKind() == kind::FLOATINGPOINT_COMPONENT_EXPONENT);
+
+ FloatingPoint arg0(node[0].getConst<FloatingPoint>());
+
+ // \todo Add a proper interface for this sort of thing to FloatingPoint #1915
+ return RewriteResponse(
+ REWRITE_DONE,
+#ifdef CVC4_USE_SYMFPU
+ NodeManager::currentNM()->mkConst((BitVector)arg0.getLiteral().exponent)
+#else
+ node
+#endif
+ );
+ }
+
+ RewriteResponse componentSignificand(TNode node, bool)
+ {
+ Assert(node.getKind() == kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND);
+
+ FloatingPoint arg0(node[0].getConst<FloatingPoint>());
+
+ return RewriteResponse(REWRITE_DONE,
+#ifdef CVC4_USE_SYMFPU
+ NodeManager::currentNM()->mkConst(
+ (BitVector)arg0.getLiteral().significand)
+#else
+ node
+#endif
+ );
+ }
+
+ RewriteResponse roundingModeBitBlast(TNode node, bool)
+ {
+ Assert(node.getKind() == kind::ROUNDINGMODE_BITBLAST);
+
+ RoundingMode arg0(node[0].getConst<RoundingMode>());
+ BitVector value;
+
+#ifdef CVC4_USE_SYMFPU
+ /* \todo fix the numbering of rounding modes so this doesn't need
+ * to call symfpu at all and remove the dependency on fp_converter.h #1915 */
+ switch (arg0)
+ {
+ case roundNearestTiesToEven:
+ value = symfpuSymbolic::traits::RNE().getConst<BitVector>();
+ break;
+
+ case roundNearestTiesToAway:
+ value = symfpuSymbolic::traits::RNA().getConst<BitVector>();
+ break;
+
+ case roundTowardPositive:
+ value = symfpuSymbolic::traits::RTP().getConst<BitVector>();
+ break;
+
+ case roundTowardNegative:
+ value = symfpuSymbolic::traits::RTN().getConst<BitVector>();
+ break;
+
+ case roundTowardZero:
+ value = symfpuSymbolic::traits::RTZ().getConst<BitVector>();
+ break;
+
+ default:
+ Unreachable("Unknown rounding mode in roundingModeBitBlast");
+ break;
+ }
+#else
+ value = BitVector(5U, 0U);
+#endif
+ return RewriteResponse(REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(value));
+ }
}; /* CVC4::theory::fp::constantFold */
@@ -871,6 +984,16 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND];
preRewriteTable[kind::EQUAL] = rewrite::equal;
+ /******** Components for bit-blasting ********/
+ preRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] = rewrite::identity;
+ preRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity;
+
+
/* Set up the post-rewrite dispatch table */
@@ -943,6 +1066,15 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND];
postRewriteTable[kind::EQUAL] = rewrite::equal;
+ /******** Components for bit-blasting ********/
+ postRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] = rewrite::identity;
+ postRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity;
+
/* Set up the post-rewrite constant fold table */
@@ -1017,6 +1149,15 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND];
constantFoldTable[kind::EQUAL] = constantFold::equal;
+ /******** Components for bit-blasting ********/
+ constantFoldTable[kind::FLOATINGPOINT_COMPONENT_NAN] = constantFold::componentFlag;
+ constantFoldTable[kind::FLOATINGPOINT_COMPONENT_INF] = constantFold::componentFlag;
+ constantFoldTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = constantFold::componentFlag;
+ constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = constantFold::componentFlag;
+ constantFoldTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] = constantFold::componentExponent;
+ constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] = constantFold::componentSignificand;
+ constantFoldTable[kind::ROUNDINGMODE_BITBLAST] = constantFold::roundingModeBitBlast;
+
}
@@ -1106,12 +1247,15 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND];
Node rn = res.node; // RewriteResponse is too functional..
if (apartFromRoundingMode) {
- if (!(res.node.getKind() == kind::EQUAL)) { // Avoid infinite recursion...
- // We are close to being able to constant fold this
- // and in many cases the rounding mode really doesn't matter.
- // So we can try brute forcing our way through them.
-
- NodeManager *nm = NodeManager::currentNM();
+ if (!(res.node.getKind() == kind::EQUAL)
+ && // Avoid infinite recursion...
+ !(res.node.getKind() == kind::ROUNDINGMODE_BITBLAST))
+ { // Don't eliminate the bit-blast
+ // We are close to being able to constant fold this
+ // and in many cases the rounding mode really doesn't matter.
+ // So we can try brute forcing our way through them.
+
+ NodeManager *nm = NodeManager::currentNM();
Node RNE(nm->mkConst(roundNearestTiesToEven));
Node RNA(nm->mkConst(roundNearestTiesToAway));
diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index 2f7dd2e01..9589715d2 100644
--- a/src/theory/fp/theory_fp_type_rules.h
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -17,6 +17,9 @@
#include "cvc4_private.h"
+// This is only needed for checking that components are only applied to leaves.
+#include "theory/theory.h"
+
#ifndef __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
#define __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
@@ -612,6 +615,167 @@ class FloatingPointToRealTotalTypeRule {
}
};
+class FloatingPointComponentBit
+{
+ public:
+ inline static TypeNode computeType(
+ NodeManager* nodeManager,
+ TNode n,
+ bool check) throw(TypeCheckingExceptionPrivate, AssertionException)
+ {
+ TRACE("FloatingPointComponentBit");
+
+ if (check)
+ {
+ TypeNode operandType = n[0].getType(check);
+
+ if (!operandType.isFloatingPoint())
+ {
+ throw TypeCheckingExceptionPrivate(n,
+ "floating-point bit component "
+ "applied to a non floating-point "
+ "sort");
+ }
+ if (!(Theory::isLeafOf(n[0], THEORY_FP)
+ || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
+ {
+ throw TypeCheckingExceptionPrivate(n,
+ "floating-point bit component "
+ "applied to a non leaf / to_fp leaf "
+ "node");
+ }
+ }
+
+ return nodeManager->mkBitVectorType(1);
+ }
+};
+
+class FloatingPointComponentExponent
+{
+ public:
+ inline static TypeNode computeType(
+ NodeManager* nodeManager,
+ TNode n,
+ bool check) throw(TypeCheckingExceptionPrivate, AssertionException)
+ {
+ TRACE("FloatingPointComponentExponent");
+
+ TypeNode operandType = n[0].getType(check);
+
+ if (check)
+ {
+ if (!operandType.isFloatingPoint())
+ {
+ throw TypeCheckingExceptionPrivate(n,
+ "floating-point exponent component "
+ "applied to a non floating-point "
+ "sort");
+ }
+ if (!(Theory::isLeafOf(n[0], THEORY_FP)
+ || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
+ {
+ throw TypeCheckingExceptionPrivate(n,
+ "floating-point exponent component "
+ "applied to a non leaf / to_fp "
+ "node");
+ }
+ }
+
+#ifdef CVC4_USE_SYMFPU
+ /* Need to create some symfpu objects as the size of bit-vector
+ * that is needed for this component is dependent on the encoding
+ * used (i.e. whether subnormals are forcibly normalised or not).
+ * Here we use types from floatingpoint.h which are the literal
+ * back-end but it should't make a difference. */
+ FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
+ symfpuLiteral::fpt format(fps); // The symfpu interface to type info
+ unsigned bw = FloatingPointLiteral::exponentWidth(format);
+#else
+ unsigned bw = 2;
+#endif
+
+ return nodeManager->mkBitVectorType(bw);
+ }
+};
+
+class FloatingPointComponentSignificand
+{
+ public:
+ inline static TypeNode computeType(
+ NodeManager* nodeManager,
+ TNode n,
+ bool check) throw(TypeCheckingExceptionPrivate, AssertionException)
+ {
+ TRACE("FloatingPointComponentSignificand");
+
+ TypeNode operandType = n[0].getType(check);
+
+ if (check)
+ {
+ if (!operandType.isFloatingPoint())
+ {
+ throw TypeCheckingExceptionPrivate(n,
+ "floating-point significand "
+ "component applied to a non "
+ "floating-point sort");
+ }
+ if (!(Theory::isLeafOf(n[0], THEORY_FP)
+ || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
+ {
+ throw TypeCheckingExceptionPrivate(n,
+ "floating-point significand "
+ "component applied to a non leaf / "
+ "to_fp node");
+ }
+ }
+
+#ifdef CVC4_USE_SYMFPU
+ /* As before we need to use some of sympfu. */
+ FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
+ symfpuLiteral::fpt format(fps);
+ unsigned bw = FloatingPointLiteral::significandWidth(format);
+#else
+ unsigned bw = 1;
+#endif
+
+ return nodeManager->mkBitVectorType(bw);
+ }
+};
+
+class RoundingModeBitBlast
+{
+ public:
+ inline static TypeNode computeType(
+ NodeManager* nodeManager,
+ TNode n,
+ bool check) throw(TypeCheckingExceptionPrivate, AssertionException)
+ {
+ TRACE("RoundingModeBitBlast");
+
+ if (check)
+ {
+ TypeNode operandType = n[0].getType(check);
+
+ if (!operandType.isRoundingMode())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "rounding mode bit-blast applied to a non rounding-mode sort");
+ }
+ if (!Theory::isLeafOf(n[0], THEORY_FP))
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "rounding mode bit-blast applied to a non leaf node");
+ }
+ }
+
+#ifdef CVC4_USE_SYMFPU
+ /* Uses sympfu for the macro. */
+ return nodeManager->mkBitVectorType(SYMFPU_NUMBER_OF_ROUNDING_MODES);
+#else
+ return nodeManager->mkBitVectorType(5);
+#endif
+ }
+};
class CardinalityComputer {
public:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback