From: Aina Niemetz Date: Mon, 13 Sep 2021 16:39:19 +0000 (-0700) Subject: FP: Rename FpConverter to FpWordBlaster. (#7170) X-Git-Tag: cvc5-1.0.0~1225 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f5b2c6f5e52ce4bf6e0afd317cd7daaa33c1550;p=cvc5.git FP: Rename FpConverter to FpWordBlaster. (#7170) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 42434adab..223d3ff1f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -705,8 +705,8 @@ libcvc5_add_sources( 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 diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp deleted file mode 100644 index f6f1f3bb3..000000000 --- a/src/theory/fp/fp_converter.cpp +++ /dev/null @@ -1,1316 +0,0 @@ -/****************************************************************************** - * 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 - -#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 \ - { \ - 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(const traits::ubv &b) -{ - return orderEncodeBitwise(b); -} - -template <> -stickyRightShiftResult stickyRightShift(const traits::ubv &input, - const traits::ubv &shiftAmount) -{ - return stickyRightShiftBitwise(input, shiftAmount); -} - -template <> -void probabilityAnnotation(const traits::prop &p, - const probability &pr) -{ - // For now, do nothing... - return; -} -}; - -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 -Node symbolicBitVector::boolNodeToBV(Node node) const -{ - Assert(node.getType().isBoolean()); - NodeManager *nm = NodeManager::currentNM(); - return nm->mkNode(kind::ITE, - node, - nm->mkConst(BitVector(1U, 1U)), - nm->mkConst(BitVector(1U, 0U))); -} - -template -Node symbolicBitVector::BVToBoolNode(Node node) const -{ - Assert(node.getType().isBitVector()); - Assert(node.getType().getBitVectorSize() == 1); - NodeManager *nm = NodeManager::currentNM(); - return nm->mkNode(kind::EQUAL, node, nm->mkConst(BitVector(1U, 1U))); -} - -template -Node symbolicBitVector::fromProposition(Node node) const -{ - return node; -} -template -Node symbolicBitVector::toProposition(Node node) const -{ - return boolNodeToBV(node); -} - -template -symbolicBitVector::symbolicBitVector(const Node n) : nodeWrapper(n) -{ - Assert(checkNodeType(*this)); -} - -template -bool symbolicBitVector::checkNodeType(const TNode n) -{ - return n.getType(false).isBitVector(); -} - -template -symbolicBitVector::symbolicBitVector(const bwt w, const unsigned v) - : nodeWrapper(NodeManager::currentNM()->mkConst(BitVector(w, v))) -{ - Assert(checkNodeType(*this)); -} -template -symbolicBitVector::symbolicBitVector(const symbolicProposition &p) - : nodeWrapper(fromProposition(p)) -{ -} -template -symbolicBitVector::symbolicBitVector( - const symbolicBitVector &old) - : nodeWrapper(old) -{ - Assert(checkNodeType(*this)); -} -template -symbolicBitVector::symbolicBitVector(const BitVector &old) - : nodeWrapper(NodeManager::currentNM()->mkConst(old)) -{ - Assert(checkNodeType(*this)); -} - -template -bwt symbolicBitVector::getWidth(void) const -{ - return this->getType(false).getBitVectorSize(); -} - -/*** Constant creation and test ***/ -template -symbolicBitVector symbolicBitVector::one(const bwt &w) -{ - return symbolicBitVector(w, 1); -} -template -symbolicBitVector symbolicBitVector::zero(const bwt &w) -{ - return symbolicBitVector(w, 0); -} -template -symbolicBitVector symbolicBitVector::allOnes(const bwt &w) -{ - return symbolicBitVector(~zero(w)); -} - -template -symbolicProposition symbolicBitVector::isAllOnes() const -{ - return (*this == symbolicBitVector::allOnes(this->getWidth())); -} -template -symbolicProposition symbolicBitVector::isAllZeros() const -{ - return (*this == symbolicBitVector::zero(this->getWidth())); -} - -template <> -symbolicBitVector symbolicBitVector::maxValue(const bwt &w) -{ - symbolicBitVector leadingZero(symbolicBitVector::zero(1)); - symbolicBitVector base(symbolicBitVector::allOnes(w - 1)); - - return symbolicBitVector(::cvc5::NodeManager::currentNM()->mkNode( - ::cvc5::kind::BITVECTOR_CONCAT, leadingZero, base)); -} - -template <> -symbolicBitVector symbolicBitVector::maxValue(const bwt &w) -{ - return symbolicBitVector::allOnes(w); -} - -template <> -symbolicBitVector symbolicBitVector::minValue(const bwt &w) -{ - symbolicBitVector leadingOne(symbolicBitVector::one(1)); - symbolicBitVector base(symbolicBitVector::zero(w - 1)); - - return symbolicBitVector(::cvc5::NodeManager::currentNM()->mkNode( - ::cvc5::kind::BITVECTOR_CONCAT, leadingOne, base)); -} - -template <> -symbolicBitVector symbolicBitVector::minValue(const bwt &w) -{ - return symbolicBitVector::zero(w); -} - -/*** Operators ***/ -template -symbolicBitVector symbolicBitVector::operator<<( - const symbolicBitVector &op) const -{ - return symbolicBitVector( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_SHL, *this, op)); -} - -template -symbolicBitVector symbolicBitVector::operator>>( - const symbolicBitVector &op) const -{ - return symbolicBitVector(NodeManager::currentNM()->mkNode( - (isSigned) ? kind::BITVECTOR_ASHR : kind::BITVECTOR_LSHR, *this, op)); -} - -template -symbolicBitVector symbolicBitVector::operator|( - const symbolicBitVector &op) const -{ - return symbolicBitVector( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op)); -} - -template -symbolicBitVector symbolicBitVector::operator&( - const symbolicBitVector &op) const -{ - return symbolicBitVector( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op)); -} - -template -symbolicBitVector symbolicBitVector::operator+( - const symbolicBitVector &op) const -{ - return symbolicBitVector( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_ADD, *this, op)); -} - -template -symbolicBitVector symbolicBitVector::operator-( - const symbolicBitVector &op) const -{ - return symbolicBitVector( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, *this, op)); -} - -template -symbolicBitVector symbolicBitVector::operator*( - const symbolicBitVector &op) const -{ - return symbolicBitVector( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, *this, op)); -} - -template -symbolicBitVector symbolicBitVector::operator/( - const symbolicBitVector &op) const -{ - return symbolicBitVector(NodeManager::currentNM()->mkNode( - (isSigned) ? kind::BITVECTOR_SDIV : kind::BITVECTOR_UDIV, *this, op)); -} - -template -symbolicBitVector symbolicBitVector::operator%( - const symbolicBitVector &op) const -{ - return symbolicBitVector(NodeManager::currentNM()->mkNode( - (isSigned) ? kind::BITVECTOR_SREM : kind::BITVECTOR_UREM, *this, op)); -} - -template -symbolicBitVector symbolicBitVector::operator-(void) const -{ - return symbolicBitVector( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_NEG, *this)); -} - -template -symbolicBitVector symbolicBitVector::operator~(void)const -{ - return symbolicBitVector( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this)); -} - -template -symbolicBitVector symbolicBitVector::increment() const -{ - return symbolicBitVector(NodeManager::currentNM()->mkNode( - kind::BITVECTOR_ADD, *this, one(this->getWidth()))); -} - -template -symbolicBitVector symbolicBitVector::decrement() const -{ - return symbolicBitVector(NodeManager::currentNM()->mkNode( - kind::BITVECTOR_SUB, *this, one(this->getWidth()))); -} - -template -symbolicBitVector symbolicBitVector::signExtendRightShift( - const symbolicBitVector &op) const -{ - return symbolicBitVector( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_ASHR, *this, op)); -} - -/*** Modular operations ***/ -// No overflow checking so these are the same as other operations -template -symbolicBitVector symbolicBitVector::modularLeftShift( - const symbolicBitVector &op) const -{ - return *this << op; -} - -template -symbolicBitVector symbolicBitVector::modularRightShift( - const symbolicBitVector &op) const -{ - return *this >> op; -} - -template -symbolicBitVector symbolicBitVector::modularIncrement() - const -{ - return this->increment(); -} - -template -symbolicBitVector symbolicBitVector::modularDecrement() - const -{ - return this->decrement(); -} - -template -symbolicBitVector symbolicBitVector::modularAdd( - const symbolicBitVector &op) const -{ - return *this + op; -} - -template -symbolicBitVector symbolicBitVector::modularNegate() const -{ - return -(*this); -} - -/*** Comparisons ***/ - -template -symbolicProposition symbolicBitVector::operator==( - const symbolicBitVector &op) const -{ - return symbolicProposition( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op)); -} - -template -symbolicProposition symbolicBitVector::operator<=( - const symbolicBitVector &op) const -{ - // Consider adding kind::BITVECTOR_SLEBV and BITVECTOR_ULEBV - return (*this < op) || (*this == op); -} - -template -symbolicProposition symbolicBitVector::operator>=( - const symbolicBitVector &op) const -{ - return (*this > op) || (*this == op); -} - -template -symbolicProposition symbolicBitVector::operator<( - const symbolicBitVector &op) const -{ - return symbolicProposition(NodeManager::currentNM()->mkNode( - (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, *this, op)); -} - -template -symbolicProposition symbolicBitVector::operator>( - const symbolicBitVector &op) const -{ - return symbolicProposition(NodeManager::currentNM()->mkNode( - (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, op, *this)); -} - -/*** Type conversion ***/ -// cvc5 nodes make no distinction between signed and unsigned, thus ... -template -symbolicBitVector symbolicBitVector::toSigned(void) const -{ - return symbolicBitVector(*this); -} -template -symbolicBitVector symbolicBitVector::toUnsigned(void) const -{ - return symbolicBitVector(*this); -} - -/*** Bit hacks ***/ -template <> -symbolicBitVector symbolicBitVector::extend(bwt extension) const -{ - NodeBuilder construct(kind::BITVECTOR_SIGN_EXTEND); - construct << NodeManager::currentNM()->mkConst( - BitVectorSignExtend(extension)) - << *this; - - return symbolicBitVector(construct); -} - -template <> -symbolicBitVector symbolicBitVector::extend(bwt extension) const -{ - NodeBuilder construct(kind::BITVECTOR_ZERO_EXTEND); - construct << NodeManager::currentNM()->mkConst( - BitVectorZeroExtend(extension)) - << *this; - - return symbolicBitVector(construct); -} - -template -symbolicBitVector symbolicBitVector::contract( - bwt reduction) const -{ - Assert(this->getWidth() > reduction); - - NodeBuilder construct(kind::BITVECTOR_EXTRACT); - construct << NodeManager::currentNM()->mkConst( - BitVectorExtract((this->getWidth() - 1) - reduction, 0)) - << *this; - - return symbolicBitVector(construct); -} - -template -symbolicBitVector symbolicBitVector::resize( - bwt newSize) const -{ - bwt width = this->getWidth(); - - if (newSize > width) - { - return this->extend(newSize - width); - } - else if (newSize < width) - { - return this->contract(width - newSize); - } - else - { - return *this; - } -} - -template -symbolicBitVector symbolicBitVector::matchWidth( - const symbolicBitVector &op) const -{ - Assert(this->getWidth() <= op.getWidth()); - return this->extend(op.getWidth() - this->getWidth()); -} - -template -symbolicBitVector symbolicBitVector::append( - const symbolicBitVector &op) const -{ - return symbolicBitVector( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, *this, op)); -} - -// Inclusive of end points, thus if the same, extracts just one bit -template -symbolicBitVector symbolicBitVector::extract( - bwt upper, bwt lower) const -{ - Assert(upper >= lower); - - NodeBuilder construct(kind::BITVECTOR_EXTRACT); - construct << NodeManager::currentNM()->mkConst( - BitVectorExtract(upper, lower)) - << *this; - - return symbolicBitVector(construct); -} - -floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode type) - : FloatingPointSize(type.getConst()) -{ - 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()); - - // This is not entirely obvious but it builds a float from components - // Particularly, if the components can be constant folded, it should - // build a Node containing a constant FloatingPoint number - - ubv packed(symfpu::pack(format, u)); - Node value = - nm->mkNode(nm->mkConst(FloatingPointToFPIEEEBitVector(fps)), packed); - return value; -} - -Node FpConverter::rmToNode(const rm &r) const -{ - NodeManager *nm = NodeManager::currentNM(); - - Node transVar = r; - - Node RNE = traits::RNE(); - Node RNA = traits::RNA(); - Node RTP = traits::RTP(); - Node RTN = traits::RTN(); - Node RTZ = traits::RTZ(); - - Node value = nm->mkNode( - kind::ITE, - nm->mkNode(kind::EQUAL, transVar, RNE), - nm->mkConst(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 visit; - std::unordered_map 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()) - { - 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( - cur.getConst().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(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(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(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( - 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(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(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(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(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(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(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(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( - 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(fpt(t), IEEEBV)); - } - break; - - case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: - Assert(cur[0].getType().isBitVector()); - d_fpMap.insert( - cur, symfpu::unpack(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( - 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( - 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(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( - 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(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(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(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(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(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(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(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(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(); - d_ubvMap.insert( - cur, - symfpu::convertFloatToUBV(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(); - - d_sbvMap.insert( - cur, - symfpu::convertFloatToSBV(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 diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h deleted file mode 100644 index d589eff60..000000000 --- a/src/theory/fp/fp_converter.h +++ /dev/null @@ -1,351 +0,0 @@ -/****************************************************************************** - * 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 -class symbolicBitVector; - -// This is the template parameter for symfpu's templates. -class traits -{ - public: - // The six key types that symfpu uses. - typedef unsigned bwt; - typedef symbolicRoundingMode rm; - typedef floatingPointTypeInfo fpt; - typedef symbolicProposition prop; - typedef symbolicBitVector sbv; - typedef symbolicBitVector ubv; - - // Give concrete instances (wrapped nodes) for each rounding mode. - static symbolicRoundingMode RNE(void); - static symbolicRoundingMode RNA(void); - static symbolicRoundingMode RTP(void); - static symbolicRoundingMode RTN(void); - static symbolicRoundingMode RTZ(void); - - // Properties used by symfpu - static void precondition(const bool b); - static void postcondition(const bool b); - static void invariant(const bool b); - static void precondition(const prop &p); - static void postcondition(const prop &p); - static void invariant(const prop &p); -}; - -// Use the same type names as symfpu. -typedef traits::bwt bwt; - -/** - * Wrap the 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; // 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; // 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 -struct signedToLiteralType; - -template <> -struct signedToLiteralType -{ - typedef int literalType; -}; -template <> -struct signedToLiteralType -{ - typedef unsigned int literalType; -}; - -template -class symbolicBitVector : public nodeWrapper -{ - protected: - typedef typename signedToLiteralType::literalType literalType; - - Node boolNodeToBV(Node node) const; - Node BVToBoolNode(Node node) const; - - Node fromProposition(Node node) const; - Node toProposition(Node node) const; - bool checkNodeType(const TNode n); - friend symbolicBitVector; // To allow conversion between the types - - friend ::symfpu::ite >; // For ITE - - public: - symbolicBitVector(const Node n); - symbolicBitVector(const bwt w, const unsigned v); - symbolicBitVector(const symbolicProposition &p); - symbolicBitVector(const symbolicBitVector &old); - symbolicBitVector(const BitVector &old); - - bwt getWidth(void) const; - - /*** Constant creation and test ***/ - static symbolicBitVector one(const bwt &w); - static symbolicBitVector zero(const bwt &w); - static symbolicBitVector allOnes(const bwt &w); - - symbolicProposition isAllOnes() const; - symbolicProposition isAllZeros() const; - - static symbolicBitVector maxValue(const bwt &w); - static symbolicBitVector minValue(const bwt &w); - - /*** Operators ***/ - symbolicBitVector operator<<( - const symbolicBitVector &op) const; - symbolicBitVector operator>>( - const symbolicBitVector &op) const; - symbolicBitVector operator|( - const symbolicBitVector &op) const; - symbolicBitVector operator&( - const symbolicBitVector &op) const; - symbolicBitVector operator+( - const symbolicBitVector &op) const; - symbolicBitVector operator-( - const symbolicBitVector &op) const; - symbolicBitVector operator*( - const symbolicBitVector &op) const; - symbolicBitVector operator/( - const symbolicBitVector &op) const; - symbolicBitVector operator%( - const symbolicBitVector &op) const; - symbolicBitVector operator-(void) const; - symbolicBitVector operator~(void)const; - symbolicBitVector increment() const; - symbolicBitVector decrement() const; - symbolicBitVector signExtendRightShift( - const symbolicBitVector &op) const; - - /*** Modular operations ***/ - // This back-end doesn't do any overflow checking so these are the same as - // other operations - symbolicBitVector modularLeftShift( - const symbolicBitVector &op) const; - symbolicBitVector modularRightShift( - const symbolicBitVector &op) const; - symbolicBitVector modularIncrement() const; - symbolicBitVector modularDecrement() const; - symbolicBitVector modularAdd( - const symbolicBitVector &op) const; - symbolicBitVector modularNegate() const; - - /*** Comparisons ***/ - symbolicProposition operator==(const symbolicBitVector &op) const; - symbolicProposition operator<=(const symbolicBitVector &op) const; - symbolicProposition operator>=(const symbolicBitVector &op) const; - symbolicProposition operator<(const symbolicBitVector &op) const; - symbolicProposition operator>(const symbolicBitVector &op) const; - - /*** Type conversion ***/ - // cvc5 nodes make no distinction between signed and unsigned, thus these are - // trivial - symbolicBitVector toSigned(void) const; - symbolicBitVector toUnsigned(void) const; - - /*** Bit hacks ***/ - symbolicBitVector extend(bwt extension) const; - symbolicBitVector contract(bwt reduction) const; - symbolicBitVector resize(bwt newSize) const; - symbolicBitVector matchWidth( - const symbolicBitVector &op) const; - symbolicBitVector append( - const symbolicBitVector &op) const; - - // Inclusive of end points, thus if the same, extracts just one bit - symbolicBitVector extract(bwt upper, bwt lower) const; -}; - -// Use the same type information as the literal back-end but add an interface to -// TypeNodes for convenience. -class floatingPointTypeInfo : public FloatingPointSize -{ - public: - floatingPointTypeInfo(const TypeNode t); - floatingPointTypeInfo(unsigned exp, unsigned sig); - floatingPointTypeInfo(const floatingPointTypeInfo &old); - - TypeNode getTypeNode(void) const; -}; -} - -/** - * This class uses SymFPU to convert an expression containing floating-point - * kinds and operations into a logically equivalent form with bit-vector - * operations replacing the floating-point ones. It also has a getValue method - * to produce an expression which will reconstruct the value of the - * floating-point terms from a valuation. - * - * Internally it caches all of the unpacked floats so that unnecessary packing - * and unpacking operations are avoided and to make best use of structural - * sharing. - */ -class FpConverter -{ - 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 d_additionalAssertions; - - protected: - typedef symfpuSymbolic::traits traits; - typedef ::symfpu::unpackedFloat uf; - typedef symfpuSymbolic::traits::rm rm; - typedef symfpuSymbolic::traits::fpt fpt; - typedef symfpuSymbolic::traits::prop prop; - typedef symfpuSymbolic::traits::ubv ubv; - typedef symfpuSymbolic::traits::sbv sbv; - - typedef context::CDHashMap fpMap; - typedef context::CDHashMap rmMap; - typedef context::CDHashMap boolMap; - typedef context::CDHashMap ubvMap; - typedef context::CDHashMap sbvMap; - - fpMap 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 */ diff --git a/src/theory/fp/fp_word_blaster.cpp b/src/theory/fp/fp_word_blaster.cpp new file mode 100644 index 000000000..70d77abed --- /dev/null +++ b/src/theory/fp/fp_word_blaster.cpp @@ -0,0 +1,1308 @@ +/****************************************************************************** + * 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 + +#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 \ + { \ + 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(const traits::ubv& b) +{ + return orderEncodeBitwise(b); +} + +template <> +stickyRightShiftResult stickyRightShift(const traits::ubv& input, + const traits::ubv& shiftAmount) +{ + return stickyRightShiftBitwise(input, shiftAmount); +} + +template <> +void probabilityAnnotation(const traits::prop& p, + const probability& pr) +{ + // For now, do nothing... + return; +} +}; // 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 +Node symbolicBitVector::boolNodeToBV(Node node) const +{ + Assert(node.getType().isBoolean()); + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::ITE, + node, + nm->mkConst(BitVector(1U, 1U)), + nm->mkConst(BitVector(1U, 0U))); +} + +template +Node symbolicBitVector::BVToBoolNode(Node node) const +{ + Assert(node.getType().isBitVector()); + Assert(node.getType().getBitVectorSize() == 1); + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::EQUAL, node, nm->mkConst(BitVector(1U, 1U))); +} + +template +Node symbolicBitVector::fromProposition(Node node) const +{ + return node; +} +template +Node symbolicBitVector::toProposition(Node node) const +{ + return boolNodeToBV(node); +} + +template +symbolicBitVector::symbolicBitVector(const Node n) : nodeWrapper(n) +{ + Assert(checkNodeType(*this)); +} + +template +bool symbolicBitVector::checkNodeType(const TNode n) +{ + return n.getType(false).isBitVector(); +} + +template +symbolicBitVector::symbolicBitVector(const bwt w, const unsigned v) + : nodeWrapper(NodeManager::currentNM()->mkConst(BitVector(w, v))) +{ + Assert(checkNodeType(*this)); +} +template +symbolicBitVector::symbolicBitVector(const symbolicProposition& p) + : nodeWrapper(fromProposition(p)) +{ +} +template +symbolicBitVector::symbolicBitVector( + const symbolicBitVector& old) + : nodeWrapper(old) +{ + Assert(checkNodeType(*this)); +} +template +symbolicBitVector::symbolicBitVector(const BitVector& old) + : nodeWrapper(NodeManager::currentNM()->mkConst(old)) +{ + Assert(checkNodeType(*this)); +} + +template +bwt symbolicBitVector::getWidth(void) const +{ + return this->getType(false).getBitVectorSize(); +} + +/*** Constant creation and test ***/ +template +symbolicBitVector symbolicBitVector::one(const bwt& w) +{ + return symbolicBitVector(w, 1); +} +template +symbolicBitVector symbolicBitVector::zero(const bwt& w) +{ + return symbolicBitVector(w, 0); +} +template +symbolicBitVector symbolicBitVector::allOnes(const bwt& w) +{ + return symbolicBitVector(~zero(w)); +} + +template +symbolicProposition symbolicBitVector::isAllOnes() const +{ + return (*this == symbolicBitVector::allOnes(this->getWidth())); +} +template +symbolicProposition symbolicBitVector::isAllZeros() const +{ + return (*this == symbolicBitVector::zero(this->getWidth())); +} + +template <> +symbolicBitVector symbolicBitVector::maxValue(const bwt& w) +{ + symbolicBitVector leadingZero(symbolicBitVector::zero(1)); + symbolicBitVector base(symbolicBitVector::allOnes(w - 1)); + + return symbolicBitVector(::cvc5::NodeManager::currentNM()->mkNode( + ::cvc5::kind::BITVECTOR_CONCAT, leadingZero, base)); +} + +template <> +symbolicBitVector symbolicBitVector::maxValue(const bwt& w) +{ + return symbolicBitVector::allOnes(w); +} + +template <> +symbolicBitVector symbolicBitVector::minValue(const bwt& w) +{ + symbolicBitVector leadingOne(symbolicBitVector::one(1)); + symbolicBitVector base(symbolicBitVector::zero(w - 1)); + + return symbolicBitVector(::cvc5::NodeManager::currentNM()->mkNode( + ::cvc5::kind::BITVECTOR_CONCAT, leadingOne, base)); +} + +template <> +symbolicBitVector symbolicBitVector::minValue(const bwt& w) +{ + return symbolicBitVector::zero(w); +} + +/*** Operators ***/ +template +symbolicBitVector symbolicBitVector::operator<<( + const symbolicBitVector& op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_SHL, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator>>( + const symbolicBitVector& op) const +{ + return symbolicBitVector(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_ASHR : kind::BITVECTOR_LSHR, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator|( + const symbolicBitVector& op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator&( + const symbolicBitVector& op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator+( + const symbolicBitVector& op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_ADD, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator-( + const symbolicBitVector& op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator*( + const symbolicBitVector& op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator/( + const symbolicBitVector& op) const +{ + return symbolicBitVector(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_SDIV : kind::BITVECTOR_UDIV, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator%( + const symbolicBitVector& op) const +{ + return symbolicBitVector(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_SREM : kind::BITVECTOR_UREM, *this, op)); +} + +template +symbolicBitVector symbolicBitVector::operator-(void) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_NEG, *this)); +} + +template +symbolicBitVector symbolicBitVector::operator~(void) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this)); +} + +template +symbolicBitVector symbolicBitVector::increment() const +{ + return symbolicBitVector(NodeManager::currentNM()->mkNode( + kind::BITVECTOR_ADD, *this, one(this->getWidth()))); +} + +template +symbolicBitVector symbolicBitVector::decrement() const +{ + return symbolicBitVector(NodeManager::currentNM()->mkNode( + kind::BITVECTOR_SUB, *this, one(this->getWidth()))); +} + +template +symbolicBitVector symbolicBitVector::signExtendRightShift( + const symbolicBitVector& op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_ASHR, *this, op)); +} + +/*** Modular operations ***/ +// No overflow checking so these are the same as other operations +template +symbolicBitVector symbolicBitVector::modularLeftShift( + const symbolicBitVector& op) const +{ + return *this << op; +} + +template +symbolicBitVector symbolicBitVector::modularRightShift( + const symbolicBitVector& op) const +{ + return *this >> op; +} + +template +symbolicBitVector symbolicBitVector::modularIncrement() + const +{ + return this->increment(); +} + +template +symbolicBitVector symbolicBitVector::modularDecrement() + const +{ + return this->decrement(); +} + +template +symbolicBitVector symbolicBitVector::modularAdd( + const symbolicBitVector& op) const +{ + return *this + op; +} + +template +symbolicBitVector symbolicBitVector::modularNegate() const +{ + return -(*this); +} + +/*** Comparisons ***/ + +template +symbolicProposition symbolicBitVector::operator==( + const symbolicBitVector& op) const +{ + return symbolicProposition( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op)); +} + +template +symbolicProposition symbolicBitVector::operator<=( + const symbolicBitVector& op) const +{ + // Consider adding kind::BITVECTOR_SLEBV and BITVECTOR_ULEBV + return (*this < op) || (*this == op); +} + +template +symbolicProposition symbolicBitVector::operator>=( + const symbolicBitVector& op) const +{ + return (*this > op) || (*this == op); +} + +template +symbolicProposition symbolicBitVector::operator<( + const symbolicBitVector& op) const +{ + return symbolicProposition(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, *this, op)); +} + +template +symbolicProposition symbolicBitVector::operator>( + const symbolicBitVector& op) const +{ + return symbolicProposition(NodeManager::currentNM()->mkNode( + (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, op, *this)); +} + +/*** Type conversion ***/ +// cvc5 nodes make no distinction between signed and unsigned, thus ... +template +symbolicBitVector symbolicBitVector::toSigned(void) const +{ + return symbolicBitVector(*this); +} +template +symbolicBitVector symbolicBitVector::toUnsigned(void) const +{ + return symbolicBitVector(*this); +} + +/*** Bit hacks ***/ +template <> +symbolicBitVector symbolicBitVector::extend(bwt extension) const +{ + NodeBuilder construct(kind::BITVECTOR_SIGN_EXTEND); + construct << NodeManager::currentNM()->mkConst( + BitVectorSignExtend(extension)) + << *this; + + return symbolicBitVector(construct); +} + +template <> +symbolicBitVector symbolicBitVector::extend(bwt extension) const +{ + NodeBuilder construct(kind::BITVECTOR_ZERO_EXTEND); + construct << NodeManager::currentNM()->mkConst( + BitVectorZeroExtend(extension)) + << *this; + + return symbolicBitVector(construct); +} + +template +symbolicBitVector symbolicBitVector::contract( + bwt reduction) const +{ + Assert(this->getWidth() > reduction); + + NodeBuilder construct(kind::BITVECTOR_EXTRACT); + construct << NodeManager::currentNM()->mkConst( + BitVectorExtract((this->getWidth() - 1) - reduction, 0)) + << *this; + + return symbolicBitVector(construct); +} + +template +symbolicBitVector symbolicBitVector::resize( + bwt newSize) const +{ + bwt width = this->getWidth(); + + if (newSize > width) + { + return this->extend(newSize - width); + } + else if (newSize < width) + { + return this->contract(width - newSize); + } + else + { + return *this; + } +} + +template +symbolicBitVector symbolicBitVector::matchWidth( + const symbolicBitVector& op) const +{ + Assert(this->getWidth() <= op.getWidth()); + return this->extend(op.getWidth() - this->getWidth()); +} + +template +symbolicBitVector symbolicBitVector::append( + const symbolicBitVector& op) const +{ + return symbolicBitVector( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, *this, op)); +} + +// Inclusive of end points, thus if the same, extracts just one bit +template +symbolicBitVector symbolicBitVector::extract( + bwt upper, bwt lower) const +{ + Assert(upper >= lower); + + NodeBuilder construct(kind::BITVECTOR_EXTRACT); + construct << NodeManager::currentNM()->mkConst( + BitVectorExtract(upper, lower)) + << *this; + + return symbolicBitVector(construct); +} + +floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode type) + : FloatingPointSize(type.getConst()) +{ + 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()); + + // This is not entirely obvious but it builds a float from components + // Particularly, if the components can be constant folded, it should + // build a Node containing a constant FloatingPoint number + + ubv packed(symfpu::pack(format, u)); + Node value = + nm->mkNode(nm->mkConst(FloatingPointToFPIEEEBitVector(fps)), packed); + return value; +} + +Node 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 visit; + std::unordered_map 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()) + { + 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( + cur.getConst().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( + 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( + 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(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( + 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(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(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(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(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(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(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(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( + 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(fpt(t), IEEEBV)); + } + break; + + case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + Assert(cur[0].getType().isBitVector()); + d_fpMap.insert(cur, symfpu::unpack(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( + 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( + 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(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( + 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(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(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(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(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(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(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(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(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(); + d_ubvMap.insert( + cur, + symfpu::convertFloatToUBV(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(); + + d_sbvMap.insert( + cur, + symfpu::convertFloatToSBV(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 diff --git a/src/theory/fp/fp_word_blaster.h b/src/theory/fp/fp_word_blaster.h new file mode 100644 index 000000000..f9ec4fd4e --- /dev/null +++ b/src/theory/fp/fp_word_blaster.h @@ -0,0 +1,350 @@ +/****************************************************************************** + * 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 +class symbolicBitVector; + +// This is the template parameter for symfpu's templates. +class traits +{ + public: + // The six key types that symfpu uses. + typedef unsigned bwt; + typedef symbolicRoundingMode rm; + typedef floatingPointTypeInfo fpt; + typedef symbolicProposition prop; + typedef symbolicBitVector sbv; + typedef symbolicBitVector ubv; + + // Give concrete instances (wrapped nodes) for each rounding mode. + static symbolicRoundingMode RNE(void); + static symbolicRoundingMode RNA(void); + static symbolicRoundingMode RTP(void); + static symbolicRoundingMode RTN(void); + static symbolicRoundingMode RTZ(void); + + // Properties used by symfpu + static void precondition(const bool b); + static void postcondition(const bool b); + static void invariant(const bool b); + static void precondition(const prop& p); + static void postcondition(const prop& p); + static void invariant(const prop& p); +}; + +// Use the same type names as symfpu. +typedef traits::bwt bwt; + +/** + * Wrap the 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; // 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; // 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 +struct signedToLiteralType; + +template <> +struct signedToLiteralType +{ + typedef int literalType; +}; +template <> +struct signedToLiteralType +{ + typedef unsigned int literalType; +}; + +template +class symbolicBitVector : public nodeWrapper +{ + protected: + typedef typename signedToLiteralType::literalType literalType; + + Node boolNodeToBV(Node node) const; + Node BVToBoolNode(Node node) const; + + Node fromProposition(Node node) const; + Node toProposition(Node node) const; + bool checkNodeType(const TNode n); + friend symbolicBitVector; // To allow conversion between the types + + friend ::symfpu::ite >; // For ITE + + public: + symbolicBitVector(const Node n); + symbolicBitVector(const bwt w, const unsigned v); + symbolicBitVector(const symbolicProposition& p); + symbolicBitVector(const symbolicBitVector& old); + symbolicBitVector(const BitVector& old); + + bwt getWidth(void) const; + + /*** Constant creation and test ***/ + static symbolicBitVector one(const bwt& w); + static symbolicBitVector zero(const bwt& w); + static symbolicBitVector allOnes(const bwt& w); + + symbolicProposition isAllOnes() const; + symbolicProposition isAllZeros() const; + + static symbolicBitVector maxValue(const bwt& w); + static symbolicBitVector minValue(const bwt& w); + + /*** Operators ***/ + symbolicBitVector operator<<( + const symbolicBitVector& op) const; + symbolicBitVector operator>>( + const symbolicBitVector& op) const; + symbolicBitVector operator|( + const symbolicBitVector& op) const; + symbolicBitVector operator&( + const symbolicBitVector& op) const; + symbolicBitVector operator+( + const symbolicBitVector& op) const; + symbolicBitVector operator-( + const symbolicBitVector& op) const; + symbolicBitVector operator*( + const symbolicBitVector& op) const; + symbolicBitVector operator/( + const symbolicBitVector& op) const; + symbolicBitVector operator%( + const symbolicBitVector& op) const; + symbolicBitVector operator-(void) const; + symbolicBitVector operator~(void) const; + symbolicBitVector increment() const; + symbolicBitVector decrement() const; + symbolicBitVector signExtendRightShift( + const symbolicBitVector& op) const; + + /*** Modular operations ***/ + // This back-end doesn't do any overflow checking so these are the same as + // other operations + symbolicBitVector modularLeftShift( + const symbolicBitVector& op) const; + symbolicBitVector modularRightShift( + const symbolicBitVector& op) const; + symbolicBitVector modularIncrement() const; + symbolicBitVector modularDecrement() const; + symbolicBitVector modularAdd( + const symbolicBitVector& op) const; + symbolicBitVector modularNegate() const; + + /*** Comparisons ***/ + symbolicProposition operator==(const symbolicBitVector& op) const; + symbolicProposition operator<=(const symbolicBitVector& op) const; + symbolicProposition operator>=(const symbolicBitVector& op) const; + symbolicProposition operator<(const symbolicBitVector& op) const; + symbolicProposition operator>(const symbolicBitVector& op) const; + + /*** Type conversion ***/ + // cvc5 nodes make no distinction between signed and unsigned, thus these are + // trivial + symbolicBitVector toSigned(void) const; + symbolicBitVector toUnsigned(void) const; + + /*** Bit hacks ***/ + symbolicBitVector extend(bwt extension) const; + symbolicBitVector contract(bwt reduction) const; + symbolicBitVector resize(bwt newSize) const; + symbolicBitVector matchWidth( + const symbolicBitVector& op) const; + symbolicBitVector append( + const symbolicBitVector& op) const; + + // Inclusive of end points, thus if the same, extracts just one bit + symbolicBitVector extract(bwt upper, bwt lower) const; +}; + +// Use the same type information as the literal back-end but add an interface to +// TypeNodes for convenience. +class floatingPointTypeInfo : public FloatingPointSize +{ + public: + floatingPointTypeInfo(const TypeNode t); + floatingPointTypeInfo(unsigned exp, unsigned sig); + floatingPointTypeInfo(const floatingPointTypeInfo& old); + + TypeNode getTypeNode(void) const; +}; +} // 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 d_additionalAssertions; + + protected: + typedef symfpuSymbolic::traits traits; + typedef ::symfpu::unpackedFloat uf; + typedef symfpuSymbolic::traits::rm rm; + typedef symfpuSymbolic::traits::fpt fpt; + typedef symfpuSymbolic::traits::prop prop; + typedef symfpuSymbolic::traits::ubv ubv; + typedef symfpuSymbolic::traits::sbv sbv; + + typedef context::CDHashMap fpMap; + typedef context::CDHashMap rmMap; + typedef context::CDHashMap boolMap; + typedef context::CDHashMap ubvMap; + typedef context::CDHashMap sbvMap; + + fpMap 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 */ diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index d4ecbd357..5ee5fd7d8 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -24,7 +24,7 @@ #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" @@ -63,7 +63,7 @@ TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation) : 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()), @@ -511,31 +511,34 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) 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(); @@ -546,13 +549,13 @@ void TheoryFp::convertAndEquateTerm(TNode node) ++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(); @@ -560,7 +563,7 @@ void TheoryFp::convertAndEquateTerm(TNode node) nm->mkNode(kind::EQUAL, node, nm->mkNode(kind::EQUAL, - converted, + wordBlasted, nm->mkConst(::cvc5::BitVector(1U, 1U)))), InferenceId::FP_EQUATE_TERM); } @@ -571,11 +574,12 @@ void TheoryFp::convertAndEquateTerm(TNode node) } 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); } } @@ -657,7 +661,7 @@ void TheoryFp::registerTerm(TNode node) * registration. */ if (!options().fp.fpLazyWb) { - convertAndEquateTerm(node); + wordBlastAndEquateTerm(node); } } return; @@ -760,7 +764,7 @@ bool TheoryFp::preNotifyFact( && d_wbFactsCache.find(atom) == d_wbFactsCache.end()) { d_wbFactsCache.insert(atom); - convertAndEquateTerm(atom); + wordBlastAndEquateTerm(atom); } if (atom.getKind() == kind::EQUAL) @@ -793,7 +797,7 @@ void TheoryFp::notifySharedTerm(TNode n) if (options().fp.fpLazyWb && d_wbFactsCache.find(n) == d_wbFactsCache.end()) { d_wbFactsCache.insert(n); - convertAndEquateTerm(n); + wordBlastAndEquateTerm(n); } } @@ -818,7 +822,7 @@ TrustNode TheoryFp::explain(TNode 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, @@ -880,10 +884,10 @@ bool TheoryFp::collectModelValues(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; } diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 663be2f81..9dd532a5d 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -33,7 +33,7 @@ namespace cvc5 { namespace theory { namespace fp { -class FpConverter; +class FpWordBlaster; class TheoryFp : public Theory { @@ -120,11 +120,11 @@ class TheoryFp : public Theory context::CDHashSet d_registeredTerms; /** The word-blaster. Translates FP -> BV. */ - std::unique_ptr d_conv; + std::unique_ptr 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); diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 8bc7900de..91fe183ec 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -38,7 +38,7 @@ #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 {