theory/evaluator.h
theory/ext_theory.cpp
theory/ext_theory.h
- theory/fp/fp_converter.cpp
- theory/fp/fp_converter.h
+ theory/fp/fp_word_blaster.cpp
+ theory/fp/fp_word_blaster.h
theory/fp/fp_expand_defs.cpp
theory/fp/fp_expand_defs.h
theory/fp/theory_fp.cpp
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Martin Brain, Mathias Preiner, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Conversion of floating-point operations to bit-vectors using symfpu.
- */
-
-#include "theory/fp/fp_converter.h"
-
-#include <vector>
-
-#include "base/check.h"
-#include "expr/node_builder.h"
-#include "theory/theory.h" // theory.h Only needed for the leaf test
-#include "util/floatingpoint.h"
-#include "util/floatingpoint_literal_symfpu.h"
-
-#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"
-
-namespace symfpu {
-using namespace ::cvc5::theory::fp::symfpuSymbolic;
-
-#define CVC5_SYM_ITE_DFN(T) \
- template <> \
- struct ite<symbolicProposition, T> \
- { \
- static const T iteOp(const symbolicProposition& _cond, \
- const T& _l, \
- const T& _r) \
- { \
- ::cvc5::NodeManager* nm = ::cvc5::NodeManager::currentNM(); \
- \
- ::cvc5::Node cond = _cond; \
- ::cvc5::Node l = _l; \
- ::cvc5::Node r = _r; \
- \
- /* Handle some common symfpu idioms */ \
- if (cond.isConst()) \
- { \
- return (cond == nm->mkConst(::cvc5::BitVector(1U, 1U))) ? l : r; \
- } \
- else \
- { \
- if (l.getKind() == ::cvc5::kind::BITVECTOR_ITE) \
- { \
- if (l[1] == r) \
- { \
- return nm->mkNode( \
- ::cvc5::kind::BITVECTOR_ITE, \
- nm->mkNode(::cvc5::kind::BITVECTOR_AND, \
- cond, \
- nm->mkNode(::cvc5::kind::BITVECTOR_NOT, l[0])), \
- l[2], \
- r); \
- } \
- else if (l[2] == r) \
- { \
- return nm->mkNode( \
- ::cvc5::kind::BITVECTOR_ITE, \
- nm->mkNode(::cvc5::kind::BITVECTOR_AND, cond, l[0]), \
- l[1], \
- r); \
- } \
- } \
- else if (r.getKind() == ::cvc5::kind::BITVECTOR_ITE) \
- { \
- if (r[1] == l) \
- { \
- return nm->mkNode( \
- ::cvc5::kind::BITVECTOR_ITE, \
- nm->mkNode(::cvc5::kind::BITVECTOR_AND, \
- nm->mkNode(::cvc5::kind::BITVECTOR_NOT, cond), \
- nm->mkNode(::cvc5::kind::BITVECTOR_NOT, r[0])), \
- r[2], \
- l); \
- } \
- else if (r[2] == l) \
- { \
- return nm->mkNode( \
- ::cvc5::kind::BITVECTOR_ITE, \
- nm->mkNode(::cvc5::kind::BITVECTOR_AND, \
- nm->mkNode(::cvc5::kind::BITVECTOR_NOT, cond), \
- r[0]), \
- r[1], \
- l); \
- } \
- } \
- } \
- return T(nm->mkNode(::cvc5::kind::BITVECTOR_ITE, cond, l, r)); \
- } \
- }
-
-// Can (unsurprisingly) only ITE things which contain Nodes
-CVC5_SYM_ITE_DFN(traits::rm);
-CVC5_SYM_ITE_DFN(traits::prop);
-CVC5_SYM_ITE_DFN(traits::sbv);
-CVC5_SYM_ITE_DFN(traits::ubv);
-
-#undef CVC5_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;
-}
-};
-
-namespace cvc5 {
-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)
-{
- Assert(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))))
-{
- Assert(checkNodeType(*this));
-}
-
-symbolicProposition::symbolicProposition(const symbolicProposition &old)
- : nodeWrapper(old)
-{
- Assert(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)
-{
- return n.getType(false).isBitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES);
-}
-
-symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n)
-{
- Assert(checkNodeType(*this));
-}
-
-symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
- : nodeWrapper(NodeManager::currentNM()->mkConst(
- BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
-{
- Assert((v & (v - 1)) == 0 && v != 0); // Exactly one bit set
- Assert(checkNodeType(*this));
-}
-
-symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old)
- : nodeWrapper(old)
-{
- Assert(checkNodeType(*this));
-}
-
-symbolicProposition symbolicRoundingMode::valid(void) const
-{
- NodeManager *nm = NodeManager::currentNM();
- Node zero(nm->mkConst(BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, 0u)));
-
- // 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, 1u)))),
- 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)
-{
- Assert(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)))
-{
- Assert(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)
-{
- Assert(checkNodeType(*this));
-}
-template <bool isSigned>
-symbolicBitVector<isSigned>::symbolicBitVector(const BitVector &old)
- : nodeWrapper(NodeManager::currentNM()->mkConst(old))
-{
- Assert(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>(::cvc5::NodeManager::currentNM()->mkNode(
- ::cvc5::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>(::cvc5::NodeManager::currentNM()->mkNode(
- ::cvc5::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_ADD, *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, *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, *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_ADD, *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 ***/
-// cvc5 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
-{
- Assert(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
-{
- Assert(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
-{
- Assert(upper >= lower);
-
- NodeBuilder construct(kind::BITVECTOR_EXTRACT);
- construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
- BitVectorExtract(upper, lower))
- << *this;
-
- return symbolicBitVector<isSigned>(construct);
-}
-
-floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode type)
- : FloatingPointSize(type.getConst<FloatingPointSize>())
-{
- Assert(type.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)
- ,
- d_fpMap(user),
- d_rmMap(user),
- d_boolMap(user),
- d_ubvMap(user),
- d_sbvMap(user)
-{
-}
-
-FpConverter::~FpConverter() {}
-
-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(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN),
- nm->mkNode(
- kind::ITE,
- nm->mkNode(kind::EQUAL, transVar, RNA),
- nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY),
- nm->mkNode(
- kind::ITE,
- nm->mkNode(kind::EQUAL, transVar, RTP),
- nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE),
- nm->mkNode(kind::ITE,
- nm->mkNode(kind::EQUAL, transVar, RTN),
- nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE),
- nm->mkConst(RoundingMode::ROUND_TOWARD_ZERO)))));
- return value;
-}
-
-Node FpConverter::propToNode(const prop &p) const
-{
- NodeManager *nm = NodeManager::currentNM();
- Node value =
- nm->mkNode(kind::EQUAL, p, nm->mkConst(::cvc5::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())));
-
- return tmp;
-}
-
-Node FpConverter::convert(TNode node)
-{
- std::vector<TNode> visit;
- std::unordered_map<TNode, bool> visited;
- NodeManager* nm = NodeManager::currentNM();
-
- visit.push_back(node);
-
- while (!visit.empty())
- {
- TNode cur = visit.back();
- visit.pop_back();
- TypeNode t(cur.getType());
-
- /* Already word-blasted, skip. */
- if ((t.isBoolean() && d_boolMap.find(cur) != d_boolMap.end())
- || (t.isRoundingMode() && d_rmMap.find(cur) != d_rmMap.end())
- || (t.isBitVector()
- && (d_sbvMap.find(cur) != d_sbvMap.end()
- || d_ubvMap.find(cur) != d_ubvMap.end()))
- || (t.isFloatingPoint() && d_fpMap.find(cur) != d_fpMap.end()))
- {
- continue;
- }
-
- Kind kind = cur.getKind();
-
- if (t.isReal() && kind != kind::FLOATINGPOINT_TO_REAL_TOTAL)
- {
- // The only nodes with Real sort in Theory FP are of kind
- // kind::FLOATINGPOINT_TO_REAL_TOTAL (kind::FLOATINGPOINT_TO_REAL is
- // rewritten to kind::FLOATINGPOINT_TO_REAL_TOTAL).
- // We don't need to do anything explicitly with them since they 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.
- //
- // We still have to word blast it's arguments, though.
- //
- // All other Real expressions can be skipped.
- continue;
- }
-
- auto it = visited.find(cur);
- if (it == visited.end())
- {
- visited.emplace(cur, 0);
- visit.push_back(cur);
- visit.insert(visit.end(), cur.begin(), cur.end());
- }
- else if (it->second == false)
- {
- it->second = true;
-
- if (t.isRoundingMode())
- {
- /* ---- RoundingMode constants and variables -------------- */
- Assert(Theory::isLeafOf(cur, THEORY_FP));
- if (kind == kind::CONST_ROUNDINGMODE)
- {
- switch (cur.getConst<RoundingMode>())
- {
- case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN:
- d_rmMap.insert(cur, traits::RNE());
- break;
- case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY:
- d_rmMap.insert(cur, traits::RNA());
- break;
- case RoundingMode::ROUND_TOWARD_POSITIVE:
- d_rmMap.insert(cur, traits::RTP());
- break;
- case RoundingMode::ROUND_TOWARD_NEGATIVE:
- d_rmMap.insert(cur, traits::RTN());
- break;
- case RoundingMode::ROUND_TOWARD_ZERO:
- d_rmMap.insert(cur, traits::RTZ());
- break;
- default: Unreachable() << "Unknown rounding mode"; break;
- }
- }
- else
- {
- rm tmp(nm->mkNode(kind::ROUNDINGMODE_BITBLAST, cur));
- d_rmMap.insert(cur, tmp);
- d_additionalAssertions.push_back(tmp.valid());
- }
- }
- else if (t.isFloatingPoint())
- {
- /* ---- FloatingPoint constants and variables ------------- */
- if (Theory::isLeafOf(cur, THEORY_FP))
- {
- if (kind == kind::CONST_FLOATINGPOINT)
- {
- d_fpMap.insert(
- cur,
- symfpu::unpackedFloat<traits>(
- cur.getConst<FloatingPoint>().getLiteral()->getSymUF()));
- }
- else
- {
- d_fpMap.insert(cur, buildComponents(cur));
- }
- }
- else
- {
- /* ---- FloatingPoint operators --------------------------- */
- Assert(kind != kind::CONST_FLOATINGPOINT);
- Assert(kind != kind::VARIABLE);
- Assert(kind != kind::BOUND_VARIABLE && kind != kind::SKOLEM);
-
- switch (kind)
- {
- /* ---- Arithmetic operators ---- */
- case kind::FLOATINGPOINT_ABS:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- d_fpMap.insert(
- cur,
- symfpu::absolute<traits>(fpt(t),
- (*d_fpMap.find(cur[0])).second));
- break;
-
- case kind::FLOATINGPOINT_NEG:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- d_fpMap.insert(
- cur,
- symfpu::negate<traits>(fpt(t),
- (*d_fpMap.find(cur[0])).second));
- break;
-
- case kind::FLOATINGPOINT_SQRT:
- Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- d_fpMap.insert(
- cur,
- symfpu::sqrt<traits>(fpt(t),
- (*d_rmMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second));
- break;
-
- case kind::FLOATINGPOINT_RTI:
- Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- d_fpMap.insert(cur,
- symfpu::roundToIntegral<traits>(
- fpt(t),
- (*d_rmMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second));
- break;
-
- case kind::FLOATINGPOINT_REM:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- d_fpMap.insert(
- cur,
- symfpu::remainder<traits>(fpt(t),
- (*d_fpMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second));
- break;
-
- case kind::FLOATINGPOINT_MAX_TOTAL:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- Assert(cur[2].getType().isBitVector());
- d_fpMap.insert(cur,
- symfpu::max<traits>(fpt(t),
- (*d_fpMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second,
- prop(cur[2])));
- break;
-
- case kind::FLOATINGPOINT_MIN_TOTAL:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- Assert(cur[2].getType().isBitVector());
- d_fpMap.insert(cur,
- symfpu::min<traits>(fpt(t),
- (*d_fpMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second,
- prop(cur[2])));
- break;
-
- case kind::FLOATINGPOINT_ADD:
- Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- Assert(d_fpMap.find(cur[2]) != d_fpMap.end());
- d_fpMap.insert(cur,
- symfpu::add<traits>(fpt(t),
- (*d_rmMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second,
- (*d_fpMap.find(cur[2])).second,
- prop(true)));
- break;
-
- case kind::FLOATINGPOINT_MULT:
- Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- Assert(d_fpMap.find(cur[2]) != d_fpMap.end());
- d_fpMap.insert(
- cur,
- symfpu::multiply<traits>(fpt(t),
- (*d_rmMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second,
- (*d_fpMap.find(cur[2])).second));
- break;
-
- case kind::FLOATINGPOINT_DIV:
- Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- Assert(d_fpMap.find(cur[2]) != d_fpMap.end());
- d_fpMap.insert(
- cur,
- symfpu::divide<traits>(fpt(t),
- (*d_rmMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second,
- (*d_fpMap.find(cur[2])).second));
- break;
-
- case kind::FLOATINGPOINT_FMA:
- Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- Assert(d_fpMap.find(cur[2]) != d_fpMap.end());
- Assert(d_fpMap.find(cur[3]) != d_fpMap.end());
-
- d_fpMap.insert(
- cur,
- symfpu::fma<traits>(fpt(t),
- (*d_rmMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second,
- (*d_fpMap.find(cur[2])).second,
- (*d_fpMap.find(cur[3])).second));
- break;
-
- /* ---- Conversions ---- */
- case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
- Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- d_fpMap.insert(cur,
- symfpu::convertFloatToFloat<traits>(
- fpt(cur[1].getType()),
- fpt(t),
- (*d_rmMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second));
- break;
-
- case kind::FLOATINGPOINT_FP:
- {
- Assert(cur[0].getType().isBitVector());
- Assert(cur[1].getType().isBitVector());
- Assert(cur[2].getType().isBitVector());
-
- Node IEEEBV(
- nm->mkNode(kind::BITVECTOR_CONCAT, cur[0], cur[1], cur[2]));
- d_fpMap.insert(
- cur, symfpu::unpack<traits>(fpt(t), IEEEBV));
- }
- break;
-
- case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
- Assert(cur[0].getType().isBitVector());
- d_fpMap.insert(
- cur, symfpu::unpack<traits>(fpt(t), ubv(cur[0])));
- break;
-
- case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
- Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
- d_fpMap.insert(cur,
- symfpu::convertSBVToFloat<traits>(
- fpt(t),
- (*d_rmMap.find(cur[0])).second,
- sbv(cur[1])));
- break;
-
- case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
- Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
- d_fpMap.insert(cur,
- symfpu::convertUBVToFloat<traits>(
- fpt(t),
- (*d_rmMap.find(cur[0])).second,
- ubv(cur[1])));
- break;
-
- case kind::FLOATINGPOINT_TO_FP_REAL:
- d_fpMap.insert(cur, buildComponents(cur));
- // Rely on the real theory and theory combination
- // to handle the value
- break;
-
- default: Unreachable() << "Unhandled kind " << kind; break;
- }
- }
- }
- else if (t.isBoolean())
- {
- switch (kind)
- {
- /* ---- Comparisons --------------------------------------- */
- case kind::EQUAL:
- {
- TypeNode childType(cur[0].getType());
-
- if (childType.isFloatingPoint())
- {
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- d_boolMap.insert(
- cur,
- symfpu::smtlibEqual<traits>(fpt(childType),
- (*d_fpMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second));
- }
- else if (childType.isRoundingMode())
- {
- Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
- Assert(d_rmMap.find(cur[1]) != d_rmMap.end());
- d_boolMap.insert(cur,
- (*d_rmMap.find(cur[0])).second
- == (*d_rmMap.find(cur[1])).second);
- }
- // else do nothing
- }
- break;
-
- case kind::FLOATINGPOINT_LEQ:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- d_boolMap.insert(cur,
- symfpu::lessThanOrEqual<traits>(
- fpt(cur[0].getType()),
- (*d_fpMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second));
- break;
-
- case kind::FLOATINGPOINT_LT:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- d_boolMap.insert(
- cur,
- symfpu::lessThan<traits>(fpt(cur[0].getType()),
- (*d_fpMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second));
- break;
-
- /* ---- Tester -------------------------------------------- */
- case kind::FLOATINGPOINT_ISN:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- d_boolMap.insert(
- cur,
- symfpu::isNormal<traits>(fpt(cur[0].getType()),
- (*d_fpMap.find(cur[0])).second));
- break;
-
- case kind::FLOATINGPOINT_ISSN:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- d_boolMap.insert(
- cur,
- symfpu::isSubnormal<traits>(fpt(cur[0].getType()),
- (*d_fpMap.find(cur[0])).second));
- break;
-
- case kind::FLOATINGPOINT_ISZ:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- d_boolMap.insert(
- cur,
- symfpu::isZero<traits>(fpt(cur[0].getType()),
- (*d_fpMap.find(cur[0])).second));
- break;
-
- case kind::FLOATINGPOINT_ISINF:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- d_boolMap.insert(
- cur,
- symfpu::isInfinite<traits>(fpt(cur[0].getType()),
- (*d_fpMap.find(cur[0])).second));
- break;
-
- case kind::FLOATINGPOINT_ISNAN:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- d_boolMap.insert(
- cur,
- symfpu::isNaN<traits>(fpt(cur[0].getType()),
- (*d_fpMap.find(cur[0])).second));
- break;
-
- case kind::FLOATINGPOINT_ISNEG:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- d_boolMap.insert(
- cur,
- symfpu::isNegative<traits>(fpt(cur[0].getType()),
- (*d_fpMap.find(cur[0])).second));
- break;
-
- case kind::FLOATINGPOINT_ISPOS:
- Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
- d_boolMap.insert(
- cur,
- symfpu::isPositive<traits>(fpt(cur[0].getType()),
- (*d_fpMap.find(cur[0])).second));
- break;
-
- default:; // do nothing
- }
- }
- else if (t.isBitVector())
- {
- /* ---- Conversions --------------------------------------- */
- if (kind == kind::FLOATINGPOINT_TO_UBV_TOTAL)
- {
- Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- FloatingPointToUBVTotal info =
- cur.getOperator().getConst<FloatingPointToUBVTotal>();
- d_ubvMap.insert(
- cur,
- symfpu::convertFloatToUBV<traits>(fpt(cur[1].getType()),
- (*d_rmMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second,
- info.d_bv_size,
- ubv(cur[2])));
- }
- else if (kind == kind::FLOATINGPOINT_TO_SBV_TOTAL)
- {
- Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
- Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
- FloatingPointToSBVTotal info =
- cur.getOperator().getConst<FloatingPointToSBVTotal>();
-
- d_sbvMap.insert(
- cur,
- symfpu::convertFloatToSBV<traits>(fpt(cur[1].getType()),
- (*d_rmMap.find(cur[0])).second,
- (*d_fpMap.find(cur[1])).second,
- info.d_bv_size,
- sbv(cur[2])));
- }
- // else do nothing
- }
- }
- else
- {
- Assert(visited.at(cur) == 1);
- continue;
- }
- }
-
- if (d_boolMap.find(node) != d_boolMap.end())
- {
- Assert(node.getType().isBoolean());
- return (*d_boolMap.find(node)).second;
- }
- if (d_sbvMap.find(node) != d_sbvMap.end())
- {
- Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL);
- return (*d_sbvMap.find(node)).second;
- }
- if (d_ubvMap.find(node) != d_ubvMap.end())
- {
- Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL);
- return (*d_ubvMap.find(node)).second;
- }
- return node;
-}
-
-Node FpConverter::getValue(Valuation &val, TNode var)
-{
- Assert(Theory::isLeafOf(var, THEORY_FP));
-
- TypeNode t(var.getType());
-
- Assert(t.isRoundingMode() || t.isFloatingPoint())
- << "Asking for the value of a type that is not managed by the "
- "floating-point theory";
-
- if (t.isRoundingMode())
- {
- rmMap::const_iterator i(d_rmMap.find(var));
- if (i == d_rmMap.end())
- {
- return Node::null();
- }
- return rmToNode((*i).second);
- }
-
- fpMap::const_iterator i(d_fpMap.find(var));
- if (i == d_fpMap.end())
- {
- return Node::null();
- }
- return ufToNode(fpt(t), (*i).second);
-}
-
-} // namespace fp
-} // namespace theory
-} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Martin Brain, Mathias Preiner, Aina Niemetz
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Converts floating-point nodes to bit-vector expressions.
- *
- * Uses the symfpu library to convert from floating-point operations to
- * bit-vectors and propositions allowing the theory to be solved by
- * 'bit-blasting'.
- *
- * !!! This header is not to be included in any other headers !!!
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__THEORY__FP__FP_CONVERTER_H
-#define CVC5__THEORY__FP__FP_CONVERTER_H
-
-#include "context/cdhashmap.h"
-#include "context/cdlist.h"
-#include "expr/node.h"
-#include "expr/type_node.h"
-#include "theory/valuation.h"
-#include "util/bitvector.h"
-#include "util/floatingpoint_size.h"
-#include "util/hash.h"
-
-#include "symfpu/core/unpackedFloat.h"
-
-#ifdef CVC5_SYM_SYMBOLIC_EVAL
-// This allows debugging of the cvc5 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 cvc5 {
-namespace theory {
-namespace fp {
-
-/**
- * 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 cvc5'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 cvc5::Node types so that we can debug issues with this back-end
- */
-class nodeWrapper : public Node
-{
- protected:
-/* CVC5_SYM_SYMBOLIC_EVAL is for debugging cvc5 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 CVC5_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);
-
- friend ::symfpu::ite<symbolicProposition, symbolicProposition>; // For ITE
-
- 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);
-
- friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>; // For ITE
-
- 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
-
- friend ::symfpu::ite<symbolicProposition,
- symbolicBitVector<isSigned> >; // For ITE
-
- 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 ***/
- // cvc5 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
-{
- public:
- /** Constructor. */
- FpConverter(context::UserContext*);
- /** Destructor. */
- ~FpConverter();
-
- /** Adds a node to the conversion, returns the converted node */
- Node convert(TNode);
-
- /**
- * Gives the node representing the value of a word-blasted variable.
- * Returns a null node if it has not been word-blasted.
- */
- Node getValue(Valuation&, TNode);
-
- context::CDList<Node> d_additionalAssertions;
-
- protected:
- 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> fpMap;
- typedef context::CDHashMap<Node, rm> rmMap;
- typedef context::CDHashMap<Node, prop> boolMap;
- typedef context::CDHashMap<Node, ubv> ubvMap;
- typedef context::CDHashMap<Node, sbv> sbvMap;
-
- fpMap d_fpMap;
- rmMap d_rmMap;
- boolMap d_boolMap;
- ubvMap d_ubvMap;
- sbvMap d_sbvMap;
-
- /* 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);
-};
-
-} // namespace fp
-} // namespace theory
-} // namespace cvc5
-
-#endif /* CVC5__THEORY__FP__THEORY_FP_H */
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Martin Brain, Mathias Preiner, Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Conversion of floating-point operations to bit-vectors using symfpu.
+ */
+
+#include "theory/fp/fp_word_blaster.h"
+
+#include <vector>
+
+#include "base/check.h"
+#include "expr/node_builder.h"
+#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"
+#include "theory/theory.h" // theory.h Only needed for the leaf test
+#include "util/floatingpoint.h"
+#include "util/floatingpoint_literal_symfpu.h"
+
+namespace symfpu {
+using namespace ::cvc5::theory::fp::symfpuSymbolic;
+
+#define CVC5_SYM_ITE_DFN(T) \
+ template <> \
+ struct ite<symbolicProposition, T> \
+ { \
+ static const T iteOp(const symbolicProposition& _cond, \
+ const T& _l, \
+ const T& _r) \
+ { \
+ ::cvc5::NodeManager* nm = ::cvc5::NodeManager::currentNM(); \
+ \
+ ::cvc5::Node cond = _cond; \
+ ::cvc5::Node l = _l; \
+ ::cvc5::Node r = _r; \
+ \
+ /* Handle some common symfpu idioms */ \
+ if (cond.isConst()) \
+ { \
+ return (cond == nm->mkConst(::cvc5::BitVector(1U, 1U))) ? l : r; \
+ } \
+ else \
+ { \
+ if (l.getKind() == ::cvc5::kind::BITVECTOR_ITE) \
+ { \
+ if (l[1] == r) \
+ { \
+ return nm->mkNode( \
+ ::cvc5::kind::BITVECTOR_ITE, \
+ nm->mkNode(::cvc5::kind::BITVECTOR_AND, \
+ cond, \
+ nm->mkNode(::cvc5::kind::BITVECTOR_NOT, l[0])), \
+ l[2], \
+ r); \
+ } \
+ else if (l[2] == r) \
+ { \
+ return nm->mkNode( \
+ ::cvc5::kind::BITVECTOR_ITE, \
+ nm->mkNode(::cvc5::kind::BITVECTOR_AND, cond, l[0]), \
+ l[1], \
+ r); \
+ } \
+ } \
+ else if (r.getKind() == ::cvc5::kind::BITVECTOR_ITE) \
+ { \
+ if (r[1] == l) \
+ { \
+ return nm->mkNode( \
+ ::cvc5::kind::BITVECTOR_ITE, \
+ nm->mkNode(::cvc5::kind::BITVECTOR_AND, \
+ nm->mkNode(::cvc5::kind::BITVECTOR_NOT, cond), \
+ nm->mkNode(::cvc5::kind::BITVECTOR_NOT, r[0])), \
+ r[2], \
+ l); \
+ } \
+ else if (r[2] == l) \
+ { \
+ return nm->mkNode( \
+ ::cvc5::kind::BITVECTOR_ITE, \
+ nm->mkNode(::cvc5::kind::BITVECTOR_AND, \
+ nm->mkNode(::cvc5::kind::BITVECTOR_NOT, cond), \
+ r[0]), \
+ r[1], \
+ l); \
+ } \
+ } \
+ } \
+ return T(nm->mkNode(::cvc5::kind::BITVECTOR_ITE, cond, l, r)); \
+ } \
+ }
+
+// Can (unsurprisingly) only ITE things which contain Nodes
+CVC5_SYM_ITE_DFN(traits::rm);
+CVC5_SYM_ITE_DFN(traits::prop);
+CVC5_SYM_ITE_DFN(traits::sbv);
+CVC5_SYM_ITE_DFN(traits::ubv);
+
+#undef CVC5_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;
+}
+}; // namespace symfpu
+
+namespace cvc5 {
+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)
+{
+ Assert(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))))
+{
+ Assert(checkNodeType(*this));
+}
+
+symbolicProposition::symbolicProposition(const symbolicProposition& old)
+ : nodeWrapper(old)
+{
+ Assert(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)
+{
+ return n.getType(false).isBitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES);
+}
+
+symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n)
+{
+ Assert(checkNodeType(*this));
+}
+
+symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
+ : nodeWrapper(NodeManager::currentNM()->mkConst(
+ BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
+{
+ Assert((v & (v - 1)) == 0 && v != 0); // Exactly one bit set
+ Assert(checkNodeType(*this));
+}
+
+symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode& old)
+ : nodeWrapper(old)
+{
+ Assert(checkNodeType(*this));
+}
+
+symbolicProposition symbolicRoundingMode::valid(void) const
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Node zero(nm->mkConst(BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, 0u)));
+
+ // 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, 1u)))),
+ 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)
+{
+ Assert(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)))
+{
+ Assert(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)
+{
+ Assert(checkNodeType(*this));
+}
+template <bool isSigned>
+symbolicBitVector<isSigned>::symbolicBitVector(const BitVector& old)
+ : nodeWrapper(NodeManager::currentNM()->mkConst(old))
+{
+ Assert(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>(::cvc5::NodeManager::currentNM()->mkNode(
+ ::cvc5::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>(::cvc5::NodeManager::currentNM()->mkNode(
+ ::cvc5::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_ADD, *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, *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, *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_ADD, *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 ***/
+// cvc5 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
+{
+ Assert(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
+{
+ Assert(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
+{
+ Assert(upper >= lower);
+
+ NodeBuilder construct(kind::BITVECTOR_EXTRACT);
+ construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
+ BitVectorExtract(upper, lower))
+ << *this;
+
+ return symbolicBitVector<isSigned>(construct);
+}
+
+floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode type)
+ : FloatingPointSize(type.getConst<FloatingPointSize>())
+{
+ Assert(type.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);
+}
+} // namespace symfpuSymbolic
+
+FpWordBlaster::FpWordBlaster(context::UserContext* user)
+ : d_additionalAssertions(user),
+ d_fpMap(user),
+ d_rmMap(user),
+ d_boolMap(user),
+ d_ubvMap(user),
+ d_sbvMap(user)
+{
+}
+
+FpWordBlaster::~FpWordBlaster() {}
+
+Node FpWordBlaster::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 FpWordBlaster::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(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN),
+ nm->mkNode(
+ kind::ITE,
+ nm->mkNode(kind::EQUAL, transVar, RNA),
+ nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY),
+ nm->mkNode(
+ kind::ITE,
+ nm->mkNode(kind::EQUAL, transVar, RTP),
+ nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE),
+ nm->mkNode(kind::ITE,
+ nm->mkNode(kind::EQUAL, transVar, RTN),
+ nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE),
+ nm->mkConst(RoundingMode::ROUND_TOWARD_ZERO)))));
+ return value;
+}
+
+Node FpWordBlaster::propToNode(const prop& p) const
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Node value =
+ nm->mkNode(kind::EQUAL, p, nm->mkConst(::cvc5::BitVector(1U, 1U)));
+ return value;
+}
+Node FpWordBlaster::ubvToNode(const ubv& u) const { return u; }
+Node FpWordBlaster::sbvToNode(const sbv& s) const { return s; }
+// Creates the components constraint
+FpWordBlaster::uf FpWordBlaster::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())));
+
+ return tmp;
+}
+
+Node FpWordBlaster::wordBlast(TNode node)
+{
+ std::vector<TNode> visit;
+ std::unordered_map<TNode, bool> visited;
+ NodeManager* nm = NodeManager::currentNM();
+
+ visit.push_back(node);
+
+ while (!visit.empty())
+ {
+ TNode cur = visit.back();
+ visit.pop_back();
+ TypeNode t(cur.getType());
+
+ /* Already word-blasted, skip. */
+ if ((t.isBoolean() && d_boolMap.find(cur) != d_boolMap.end())
+ || (t.isRoundingMode() && d_rmMap.find(cur) != d_rmMap.end())
+ || (t.isBitVector()
+ && (d_sbvMap.find(cur) != d_sbvMap.end()
+ || d_ubvMap.find(cur) != d_ubvMap.end()))
+ || (t.isFloatingPoint() && d_fpMap.find(cur) != d_fpMap.end()))
+ {
+ continue;
+ }
+
+ Kind kind = cur.getKind();
+
+ if (t.isReal() && kind != kind::FLOATINGPOINT_TO_REAL_TOTAL)
+ {
+ // The only nodes with Real sort in Theory FP are of kind
+ // kind::FLOATINGPOINT_TO_REAL_TOTAL (kind::FLOATINGPOINT_TO_REAL is
+ // rewritten to kind::FLOATINGPOINT_TO_REAL_TOTAL).
+ // We don't need to do anything explicitly with them since they 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.
+ //
+ // We still have to word blast it's arguments, though.
+ //
+ // All other Real expressions can be skipped.
+ continue;
+ }
+
+ auto it = visited.find(cur);
+ if (it == visited.end())
+ {
+ visited.emplace(cur, 0);
+ visit.push_back(cur);
+ visit.insert(visit.end(), cur.begin(), cur.end());
+ }
+ else if (it->second == false)
+ {
+ it->second = true;
+
+ if (t.isRoundingMode())
+ {
+ /* ---- RoundingMode constants and variables -------------- */
+ Assert(Theory::isLeafOf(cur, THEORY_FP));
+ if (kind == kind::CONST_ROUNDINGMODE)
+ {
+ switch (cur.getConst<RoundingMode>())
+ {
+ case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN:
+ d_rmMap.insert(cur, traits::RNE());
+ break;
+ case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY:
+ d_rmMap.insert(cur, traits::RNA());
+ break;
+ case RoundingMode::ROUND_TOWARD_POSITIVE:
+ d_rmMap.insert(cur, traits::RTP());
+ break;
+ case RoundingMode::ROUND_TOWARD_NEGATIVE:
+ d_rmMap.insert(cur, traits::RTN());
+ break;
+ case RoundingMode::ROUND_TOWARD_ZERO:
+ d_rmMap.insert(cur, traits::RTZ());
+ break;
+ default: Unreachable() << "Unknown rounding mode"; break;
+ }
+ }
+ else
+ {
+ rm tmp(nm->mkNode(kind::ROUNDINGMODE_BITBLAST, cur));
+ d_rmMap.insert(cur, tmp);
+ d_additionalAssertions.push_back(tmp.valid());
+ }
+ }
+ else if (t.isFloatingPoint())
+ {
+ /* ---- FloatingPoint constants and variables ------------- */
+ if (Theory::isLeafOf(cur, THEORY_FP))
+ {
+ if (kind == kind::CONST_FLOATINGPOINT)
+ {
+ d_fpMap.insert(
+ cur,
+ symfpu::unpackedFloat<traits>(
+ cur.getConst<FloatingPoint>().getLiteral()->getSymUF()));
+ }
+ else
+ {
+ d_fpMap.insert(cur, buildComponents(cur));
+ }
+ }
+ else
+ {
+ /* ---- FloatingPoint operators --------------------------- */
+ Assert(kind != kind::CONST_FLOATINGPOINT);
+ Assert(kind != kind::VARIABLE);
+ Assert(kind != kind::BOUND_VARIABLE && kind != kind::SKOLEM);
+
+ switch (kind)
+ {
+ /* ---- Arithmetic operators ---- */
+ case kind::FLOATINGPOINT_ABS:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ d_fpMap.insert(cur,
+ symfpu::absolute<traits>(
+ fpt(t), (*d_fpMap.find(cur[0])).second));
+ break;
+
+ case kind::FLOATINGPOINT_NEG:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ d_fpMap.insert(cur,
+ symfpu::negate<traits>(
+ fpt(t), (*d_fpMap.find(cur[0])).second));
+ break;
+
+ case kind::FLOATINGPOINT_SQRT:
+ Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ d_fpMap.insert(
+ cur,
+ symfpu::sqrt<traits>(fpt(t),
+ (*d_rmMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second));
+ break;
+
+ case kind::FLOATINGPOINT_RTI:
+ Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ d_fpMap.insert(cur,
+ symfpu::roundToIntegral<traits>(
+ fpt(t),
+ (*d_rmMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second));
+ break;
+
+ case kind::FLOATINGPOINT_REM:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ d_fpMap.insert(
+ cur,
+ symfpu::remainder<traits>(fpt(t),
+ (*d_fpMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second));
+ break;
+
+ case kind::FLOATINGPOINT_MAX_TOTAL:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ Assert(cur[2].getType().isBitVector());
+ d_fpMap.insert(cur,
+ symfpu::max<traits>(fpt(t),
+ (*d_fpMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second,
+ prop(cur[2])));
+ break;
+
+ case kind::FLOATINGPOINT_MIN_TOTAL:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ Assert(cur[2].getType().isBitVector());
+ d_fpMap.insert(cur,
+ symfpu::min<traits>(fpt(t),
+ (*d_fpMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second,
+ prop(cur[2])));
+ break;
+
+ case kind::FLOATINGPOINT_ADD:
+ Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ Assert(d_fpMap.find(cur[2]) != d_fpMap.end());
+ d_fpMap.insert(cur,
+ symfpu::add<traits>(fpt(t),
+ (*d_rmMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second,
+ (*d_fpMap.find(cur[2])).second,
+ prop(true)));
+ break;
+
+ case kind::FLOATINGPOINT_MULT:
+ Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ Assert(d_fpMap.find(cur[2]) != d_fpMap.end());
+ d_fpMap.insert(
+ cur,
+ symfpu::multiply<traits>(fpt(t),
+ (*d_rmMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second,
+ (*d_fpMap.find(cur[2])).second));
+ break;
+
+ case kind::FLOATINGPOINT_DIV:
+ Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ Assert(d_fpMap.find(cur[2]) != d_fpMap.end());
+ d_fpMap.insert(
+ cur,
+ symfpu::divide<traits>(fpt(t),
+ (*d_rmMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second,
+ (*d_fpMap.find(cur[2])).second));
+ break;
+
+ case kind::FLOATINGPOINT_FMA:
+ Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ Assert(d_fpMap.find(cur[2]) != d_fpMap.end());
+ Assert(d_fpMap.find(cur[3]) != d_fpMap.end());
+
+ d_fpMap.insert(
+ cur,
+ symfpu::fma<traits>(fpt(t),
+ (*d_rmMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second,
+ (*d_fpMap.find(cur[2])).second,
+ (*d_fpMap.find(cur[3])).second));
+ break;
+
+ /* ---- Conversions ---- */
+ case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+ Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ d_fpMap.insert(cur,
+ symfpu::convertFloatToFloat<traits>(
+ fpt(cur[1].getType()),
+ fpt(t),
+ (*d_rmMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second));
+ break;
+
+ case kind::FLOATINGPOINT_FP:
+ {
+ Assert(cur[0].getType().isBitVector());
+ Assert(cur[1].getType().isBitVector());
+ Assert(cur[2].getType().isBitVector());
+
+ Node IEEEBV(
+ nm->mkNode(kind::BITVECTOR_CONCAT, cur[0], cur[1], cur[2]));
+ d_fpMap.insert(cur, symfpu::unpack<traits>(fpt(t), IEEEBV));
+ }
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+ Assert(cur[0].getType().isBitVector());
+ d_fpMap.insert(cur, symfpu::unpack<traits>(fpt(t), ubv(cur[0])));
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+ Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
+ d_fpMap.insert(
+ cur,
+ symfpu::convertSBVToFloat<traits>(
+ fpt(t), (*d_rmMap.find(cur[0])).second, sbv(cur[1])));
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+ Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
+ d_fpMap.insert(
+ cur,
+ symfpu::convertUBVToFloat<traits>(
+ fpt(t), (*d_rmMap.find(cur[0])).second, ubv(cur[1])));
+ break;
+
+ case kind::FLOATINGPOINT_TO_FP_REAL:
+ d_fpMap.insert(cur, buildComponents(cur));
+ // Rely on the real theory and theory combination
+ // to handle the value
+ break;
+
+ default: Unreachable() << "Unhandled kind " << kind; break;
+ }
+ }
+ }
+ else if (t.isBoolean())
+ {
+ switch (kind)
+ {
+ /* ---- Comparisons --------------------------------------- */
+ case kind::EQUAL:
+ {
+ TypeNode childType(cur[0].getType());
+
+ if (childType.isFloatingPoint())
+ {
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ d_boolMap.insert(
+ cur,
+ symfpu::smtlibEqual<traits>(fpt(childType),
+ (*d_fpMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second));
+ }
+ else if (childType.isRoundingMode())
+ {
+ Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
+ Assert(d_rmMap.find(cur[1]) != d_rmMap.end());
+ d_boolMap.insert(cur,
+ (*d_rmMap.find(cur[0])).second
+ == (*d_rmMap.find(cur[1])).second);
+ }
+ // else do nothing
+ }
+ break;
+
+ case kind::FLOATINGPOINT_LEQ:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ d_boolMap.insert(cur,
+ symfpu::lessThanOrEqual<traits>(
+ fpt(cur[0].getType()),
+ (*d_fpMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second));
+ break;
+
+ case kind::FLOATINGPOINT_LT:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ d_boolMap.insert(
+ cur,
+ symfpu::lessThan<traits>(fpt(cur[0].getType()),
+ (*d_fpMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second));
+ break;
+
+ /* ---- Tester -------------------------------------------- */
+ case kind::FLOATINGPOINT_ISN:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ d_boolMap.insert(
+ cur,
+ symfpu::isNormal<traits>(fpt(cur[0].getType()),
+ (*d_fpMap.find(cur[0])).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISSN:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ d_boolMap.insert(
+ cur,
+ symfpu::isSubnormal<traits>(fpt(cur[0].getType()),
+ (*d_fpMap.find(cur[0])).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISZ:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ d_boolMap.insert(
+ cur,
+ symfpu::isZero<traits>(fpt(cur[0].getType()),
+ (*d_fpMap.find(cur[0])).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISINF:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ d_boolMap.insert(
+ cur,
+ symfpu::isInfinite<traits>(fpt(cur[0].getType()),
+ (*d_fpMap.find(cur[0])).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISNAN:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ d_boolMap.insert(
+ cur,
+ symfpu::isNaN<traits>(fpt(cur[0].getType()),
+ (*d_fpMap.find(cur[0])).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISNEG:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ d_boolMap.insert(
+ cur,
+ symfpu::isNegative<traits>(fpt(cur[0].getType()),
+ (*d_fpMap.find(cur[0])).second));
+ break;
+
+ case kind::FLOATINGPOINT_ISPOS:
+ Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
+ d_boolMap.insert(
+ cur,
+ symfpu::isPositive<traits>(fpt(cur[0].getType()),
+ (*d_fpMap.find(cur[0])).second));
+ break;
+
+ default:; // do nothing
+ }
+ }
+ else if (t.isBitVector())
+ {
+ /* ---- Conversions --------------------------------------- */
+ if (kind == kind::FLOATINGPOINT_TO_UBV_TOTAL)
+ {
+ Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ FloatingPointToUBVTotal info =
+ cur.getOperator().getConst<FloatingPointToUBVTotal>();
+ d_ubvMap.insert(
+ cur,
+ symfpu::convertFloatToUBV<traits>(fpt(cur[1].getType()),
+ (*d_rmMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second,
+ info.d_bv_size,
+ ubv(cur[2])));
+ }
+ else if (kind == kind::FLOATINGPOINT_TO_SBV_TOTAL)
+ {
+ Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
+ Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
+ FloatingPointToSBVTotal info =
+ cur.getOperator().getConst<FloatingPointToSBVTotal>();
+
+ d_sbvMap.insert(
+ cur,
+ symfpu::convertFloatToSBV<traits>(fpt(cur[1].getType()),
+ (*d_rmMap.find(cur[0])).second,
+ (*d_fpMap.find(cur[1])).second,
+ info.d_bv_size,
+ sbv(cur[2])));
+ }
+ // else do nothing
+ }
+ }
+ else
+ {
+ Assert(visited.at(cur) == 1);
+ continue;
+ }
+ }
+
+ if (d_boolMap.find(node) != d_boolMap.end())
+ {
+ Assert(node.getType().isBoolean());
+ return (*d_boolMap.find(node)).second;
+ }
+ if (d_sbvMap.find(node) != d_sbvMap.end())
+ {
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL);
+ return (*d_sbvMap.find(node)).second;
+ }
+ if (d_ubvMap.find(node) != d_ubvMap.end())
+ {
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL);
+ return (*d_ubvMap.find(node)).second;
+ }
+ return node;
+}
+
+Node FpWordBlaster::getValue(Valuation& val, TNode var)
+{
+ Assert(Theory::isLeafOf(var, THEORY_FP));
+
+ TypeNode t(var.getType());
+
+ Assert(t.isRoundingMode() || t.isFloatingPoint())
+ << "Asking for the value of a type that is not managed by the "
+ "floating-point theory";
+
+ if (t.isRoundingMode())
+ {
+ rmMap::const_iterator i(d_rmMap.find(var));
+ if (i == d_rmMap.end())
+ {
+ return Node::null();
+ }
+ return rmToNode((*i).second);
+ }
+
+ fpMap::const_iterator i(d_fpMap.find(var));
+ if (i == d_fpMap.end())
+ {
+ return Node::null();
+ }
+ return ufToNode(fpt(t), (*i).second);
+}
+
+} // namespace fp
+} // namespace theory
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Martin Brain, Mathias Preiner, Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Converts floating-point nodes to bit-vector expressions.
+ *
+ * Uses the symfpu library to convert from floating-point operations to
+ * bit-vectors and propositions allowing the theory to be solved by
+ * 'bit-blasting'.
+ *
+ * !!! This header is not to be included in any other headers !!!
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__FP__FP_WORD_BLASTER_H
+#define CVC5__THEORY__FP__FP_WORD_BLASTER_H
+
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "symfpu/core/unpackedFloat.h"
+#include "theory/valuation.h"
+#include "util/bitvector.h"
+#include "util/floatingpoint_size.h"
+#include "util/hash.h"
+
+#ifdef CVC5_SYM_SYMBOLIC_EVAL
+// This allows debugging of the cvc5 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 cvc5 {
+namespace theory {
+namespace fp {
+
+/**
+ * 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 cvc5'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 cvc5::Node types so that we can debug issues with this back-end
+ */
+class nodeWrapper : public Node
+{
+ protected:
+/* CVC5_SYM_SYMBOLIC_EVAL is for debugging cvc5 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 CVC5_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);
+
+ friend ::symfpu::ite<symbolicProposition, symbolicProposition>; // For ITE
+
+ 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);
+
+ friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>; // For ITE
+
+ 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
+
+ friend ::symfpu::ite<symbolicProposition,
+ symbolicBitVector<isSigned> >; // For ITE
+
+ 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 ***/
+ // cvc5 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;
+};
+} // namespace symfpuSymbolic
+
+/**
+ * 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 FpWordBlaster
+{
+ public:
+ /** Constructor. */
+ FpWordBlaster(context::UserContext*);
+ /** Destructor. */
+ ~FpWordBlaster();
+
+ /** Adds a node to the conversion, returns the converted node */
+ Node wordBlast(TNode);
+
+ /**
+ * Gives the node representing the value of a word-blasted variable.
+ * Returns a null node if it has not been word-blasted.
+ */
+ Node getValue(Valuation&, TNode);
+
+ context::CDList<Node> d_additionalAssertions;
+
+ protected:
+ 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> fpMap;
+ typedef context::CDHashMap<Node, rm> rmMap;
+ typedef context::CDHashMap<Node, prop> boolMap;
+ typedef context::CDHashMap<Node, ubv> ubvMap;
+ typedef context::CDHashMap<Node, sbv> sbvMap;
+
+ fpMap d_fpMap;
+ rmMap d_rmMap;
+ boolMap d_boolMap;
+ ubvMap d_ubvMap;
+ sbvMap d_sbvMap;
+
+ /* 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);
+};
+
+} // namespace fp
+} // namespace theory
+} // namespace cvc5
+
+#endif /* CVC5__THEORY__FP__THEORY_FP_H */
#include "expr/skolem_manager.h"
#include "options/fp_options.h"
#include "smt/logic_exception.h"
-#include "theory/fp/fp_converter.h"
+#include "theory/fp/fp_word_blaster.h"
#include "theory/fp/theory_fp_rewriter.h"
#include "theory/output_channel.h"
#include "theory/theory_model.h"
: Theory(THEORY_FP, env, out, valuation),
d_notification(*this),
d_registeredTerms(userContext()),
- d_conv(new FpConverter(userContext())),
+ d_wordBlaster(new FpWordBlaster(userContext())),
d_expansionRequested(false),
d_realToFloatMap(userContext()),
d_floatToRealMap(userContext()),
return false;
}
-void TheoryFp::convertAndEquateTerm(TNode node)
+void TheoryFp::wordBlastAndEquateTerm(TNode node)
{
- Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl;
+ Trace("fp-wordBlastTerm")
+ << "TheoryFp::wordBlastTerm(): " << node << std::endl;
- size_t oldSize = d_conv->d_additionalAssertions.size();
+ size_t oldSize = d_wordBlaster->d_additionalAssertions.size();
- Node converted(d_conv->convert(node));
+ Node wordBlasted(d_wordBlaster->wordBlast(node));
- size_t newSize = d_conv->d_additionalAssertions.size();
+ size_t newSize = d_wordBlaster->d_additionalAssertions.size();
- if (converted != node) {
- Debug("fp-convertTerm")
- << "TheoryFp::convertTerm(): before " << node << std::endl;
- Debug("fp-convertTerm")
- << "TheoryFp::convertTerm(): after " << converted << std::endl;
+ if (wordBlasted != node)
+ {
+ Debug("fp-wordBlastTerm")
+ << "TheoryFp::wordBlastTerm(): before " << node << std::endl;
+ Debug("fp-wordBlastTerm")
+ << "TheoryFp::wordBlastTerm(): after " << wordBlasted << std::endl;
}
Assert(oldSize <= newSize);
while (oldSize < newSize)
{
- Node addA = d_conv->d_additionalAssertions[oldSize];
+ Node addA = d_wordBlaster->d_additionalAssertions[oldSize];
- Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion "
- << addA << std::endl;
+ Debug("fp-wordBlastTerm")
+ << "TheoryFp::wordBlastTerm(): additional assertion " << addA
+ << std::endl;
NodeManager* nm = NodeManager::currentNM();
++oldSize;
}
- // Equate the floating-point atom and the converted one.
+ // Equate the floating-point atom and the wordBlasted one.
// Also adds the bit-vectors to the bit-vector solver.
if (node.getType().isBoolean())
{
- if (converted != node)
+ if (wordBlasted != node)
{
- Assert(converted.getType().isBitVector());
+ Assert(wordBlasted.getType().isBitVector());
NodeManager* nm = NodeManager::currentNM();
nm->mkNode(kind::EQUAL,
node,
nm->mkNode(kind::EQUAL,
- converted,
+ wordBlasted,
nm->mkConst(::cvc5::BitVector(1U, 1U)))),
InferenceId::FP_EQUATE_TERM);
}
}
else if (node.getType().isBitVector())
{
- if (converted != node) {
- Assert(converted.getType().isBitVector());
+ if (wordBlasted != node)
+ {
+ Assert(wordBlasted.getType().isBitVector());
handleLemma(
- NodeManager::currentNM()->mkNode(kind::EQUAL, node, converted),
+ NodeManager::currentNM()->mkNode(kind::EQUAL, node, wordBlasted),
InferenceId::FP_EQUATE_TERM);
}
}
* registration. */
if (!options().fp.fpLazyWb)
{
- convertAndEquateTerm(node);
+ wordBlastAndEquateTerm(node);
}
}
return;
&& d_wbFactsCache.find(atom) == d_wbFactsCache.end())
{
d_wbFactsCache.insert(atom);
- convertAndEquateTerm(atom);
+ wordBlastAndEquateTerm(atom);
}
if (atom.getKind() == kind::EQUAL)
if (options().fp.fpLazyWb && d_wbFactsCache.find(n) == d_wbFactsCache.end())
{
d_wbFactsCache.insert(n);
- convertAndEquateTerm(n);
+ wordBlastAndEquateTerm(n);
}
}
}
Node TheoryFp::getModelValue(TNode var) {
- return d_conv->getValue(d_valuation, var);
+ return d_wordBlaster->getValue(d_valuation, var);
}
bool TheoryFp::collectModelInfo(TheoryModel* m,
<< "TheoryFp::collectModelInfo(): relevantVariable " << node
<< std::endl;
- Node converted = d_conv->getValue(d_valuation, node);
- // We only assign the value if the FpConverter actually has one, that is,
- // if FpConverter::getValue() does not return a null node.
- if (!converted.isNull() && !m->assertEquality(node, converted, true))
+ Node wordBlasted = d_wordBlaster->getValue(d_valuation, node);
+ // We only assign the value if the FpWordBlaster actually has one, that is,
+ // if FpWordBlaster::getValue() does not return a null node.
+ if (!wordBlasted.isNull() && !m->assertEquality(node, wordBlasted, true))
{
return false;
}
namespace theory {
namespace fp {
-class FpConverter;
+class FpWordBlaster;
class TheoryFp : public Theory
{
context::CDHashSet<Node> d_registeredTerms;
/** The word-blaster. Translates FP -> BV. */
- std::unique_ptr<FpConverter> d_conv;
+ std::unique_ptr<FpWordBlaster> d_wordBlaster;
bool d_expansionRequested;
- void convertAndEquateTerm(TNode node);
+ void wordBlastAndEquateTerm(TNode node);
/** Interaction with the rest of the solver **/
void handleLemma(Node node, InferenceId id);
#include "base/check.h"
#include "theory/bv/theory_bv_utils.h"
-#include "theory/fp/fp_converter.h"
+#include "theory/fp/fp_word_blaster.h"
#include "util/floatingpoint.h"
namespace cvc5 {
projects / cvc5.git / commitdiff