From 4f5b2c6f5e52ce4bf6e0afd317cd7daaa33c1550 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 13 Sep 2021 09:39:19 -0700 Subject: [PATCH] FP: Rename FpConverter to FpWordBlaster. (#7170) --- src/CMakeLists.txt | 4 +- .../{fp_converter.cpp => fp_word_blaster.cpp} | 196 +++++++++--------- .../fp/{fp_converter.h => fp_word_blaster.h} | 113 +++++----- src/theory/fp/theory_fp.cpp | 64 +++--- src/theory/fp/theory_fp.h | 6 +- src/theory/fp/theory_fp_rewriter.cpp | 2 +- 6 files changed, 190 insertions(+), 195 deletions(-) rename src/theory/fp/{fp_converter.cpp => fp_word_blaster.cpp} (91%) rename src/theory/fp/{fp_converter.h => fp_word_blaster.h} (78%) 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_word_blaster.cpp similarity index 91% rename from src/theory/fp/fp_converter.cpp rename to src/theory/fp/fp_word_blaster.cpp index f6f1f3bb3..70d77abed 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_word_blaster.cpp @@ -13,16 +13,12 @@ * Conversion of floating-point operations to bit-vectors using symfpu. */ -#include "theory/fp/fp_converter.h" +#include "theory/fp/fp_word_blaster.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" @@ -37,6 +33,9 @@ #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; @@ -120,26 +119,26 @@ CVC5_SYM_ITE_DFN(traits::ubv); #undef CVC5_SYM_ITE_DFN template <> -traits::ubv orderEncode(const traits::ubv &b) +traits::ubv orderEncode(const traits::ubv& b) { return orderEncodeBitwise(b); } template <> -stickyRightShiftResult stickyRightShift(const traits::ubv &input, - const traits::ubv &shiftAmount) +stickyRightShiftResult stickyRightShift(const traits::ubv& input, + const traits::ubv& shiftAmount) { return stickyRightShiftBitwise(input, shiftAmount); } template <> -void probabilityAnnotation(const traits::prop &p, - const probability &pr) +void probabilityAnnotation(const traits::prop& p, + const probability& pr) { // For now, do nothing... return; } -}; +}; // namespace symfpu namespace cvc5 { namespace theory { @@ -168,9 +167,9 @@ void traits::invariant(const bool b) return; } -void traits::precondition(const prop &p) { return; } -void traits::postcondition(const prop &p) { return; } -void traits::invariant(const prop &p) { 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; @@ -187,46 +186,46 @@ symbolicProposition::symbolicProposition(const Node n) : nodeWrapper(n) } // Only used within this header so could be friend'd symbolicProposition::symbolicProposition(bool v) : nodeWrapper( - NodeManager::currentNM()->mkConst(BitVector(1U, (v ? 1U : 0U)))) + NodeManager::currentNM()->mkConst(BitVector(1U, (v ? 1U : 0U)))) { Assert(checkNodeType(*this)); } -symbolicProposition::symbolicProposition(const symbolicProposition &old) +symbolicProposition::symbolicProposition(const symbolicProposition& old) : nodeWrapper(old) { Assert(checkNodeType(*this)); } -symbolicProposition symbolicProposition::operator!(void)const +symbolicProposition symbolicProposition::operator!(void) const { return symbolicProposition( NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this)); } symbolicProposition symbolicProposition::operator&&( - const symbolicProposition &op) const + const symbolicProposition& op) const { return symbolicProposition( NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op)); } symbolicProposition symbolicProposition::operator||( - const symbolicProposition &op) const + const symbolicProposition& op) const { return symbolicProposition( NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op)); } symbolicProposition symbolicProposition::operator==( - const symbolicProposition &op) const + const symbolicProposition& op) const { return symbolicProposition( NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op)); } symbolicProposition symbolicProposition::operator^( - const symbolicProposition &op) const + const symbolicProposition& op) const { return symbolicProposition( NodeManager::currentNM()->mkNode(kind::BITVECTOR_XOR, *this, op)); @@ -244,13 +243,13 @@ symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n) symbolicRoundingMode::symbolicRoundingMode(const unsigned v) : nodeWrapper(NodeManager::currentNM()->mkConst( - BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v))) + 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) +symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode& old) : nodeWrapper(old) { Assert(checkNodeType(*this)); @@ -258,7 +257,7 @@ symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old) symbolicProposition symbolicRoundingMode::valid(void) const { - NodeManager *nm = NodeManager::currentNM(); + NodeManager* nm = NodeManager::currentNM(); Node zero(nm->mkConst(BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, 0u))); // Is there a better encoding of this? @@ -278,7 +277,7 @@ symbolicProposition symbolicRoundingMode::valid(void) const } symbolicProposition symbolicRoundingMode::operator==( - const symbolicRoundingMode &op) const + const symbolicRoundingMode& op) const { return symbolicProposition( NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op)); @@ -288,7 +287,7 @@ template Node symbolicBitVector::boolNodeToBV(Node node) const { Assert(node.getType().isBoolean()); - NodeManager *nm = NodeManager::currentNM(); + NodeManager* nm = NodeManager::currentNM(); return nm->mkNode(kind::ITE, node, nm->mkConst(BitVector(1U, 1U)), @@ -300,7 +299,7 @@ Node symbolicBitVector::BVToBoolNode(Node node) const { Assert(node.getType().isBitVector()); Assert(node.getType().getBitVectorSize() == 1); - NodeManager *nm = NodeManager::currentNM(); + NodeManager* nm = NodeManager::currentNM(); return nm->mkNode(kind::EQUAL, node, nm->mkConst(BitVector(1U, 1U))); } @@ -334,19 +333,19 @@ symbolicBitVector::symbolicBitVector(const bwt w, const unsigned v) Assert(checkNodeType(*this)); } template -symbolicBitVector::symbolicBitVector(const symbolicProposition &p) +symbolicBitVector::symbolicBitVector(const symbolicProposition& p) : nodeWrapper(fromProposition(p)) { } template symbolicBitVector::symbolicBitVector( - const symbolicBitVector &old) + const symbolicBitVector& old) : nodeWrapper(old) { Assert(checkNodeType(*this)); } template -symbolicBitVector::symbolicBitVector(const BitVector &old) +symbolicBitVector::symbolicBitVector(const BitVector& old) : nodeWrapper(NodeManager::currentNM()->mkConst(old)) { Assert(checkNodeType(*this)); @@ -360,17 +359,17 @@ bwt symbolicBitVector::getWidth(void) const /*** Constant creation and test ***/ template -symbolicBitVector symbolicBitVector::one(const bwt &w) +symbolicBitVector symbolicBitVector::one(const bwt& w) { return symbolicBitVector(w, 1); } template -symbolicBitVector symbolicBitVector::zero(const bwt &w) +symbolicBitVector symbolicBitVector::zero(const bwt& w) { return symbolicBitVector(w, 0); } template -symbolicBitVector symbolicBitVector::allOnes(const bwt &w) +symbolicBitVector symbolicBitVector::allOnes(const bwt& w) { return symbolicBitVector(~zero(w)); } @@ -387,7 +386,7 @@ symbolicProposition symbolicBitVector::isAllZeros() const } template <> -symbolicBitVector symbolicBitVector::maxValue(const bwt &w) +symbolicBitVector symbolicBitVector::maxValue(const bwt& w) { symbolicBitVector leadingZero(symbolicBitVector::zero(1)); symbolicBitVector base(symbolicBitVector::allOnes(w - 1)); @@ -397,13 +396,13 @@ symbolicBitVector symbolicBitVector::maxValue(const bwt &w) } template <> -symbolicBitVector symbolicBitVector::maxValue(const bwt &w) +symbolicBitVector symbolicBitVector::maxValue(const bwt& w) { return symbolicBitVector::allOnes(w); } template <> -symbolicBitVector symbolicBitVector::minValue(const bwt &w) +symbolicBitVector symbolicBitVector::minValue(const bwt& w) { symbolicBitVector leadingOne(symbolicBitVector::one(1)); symbolicBitVector base(symbolicBitVector::zero(w - 1)); @@ -413,7 +412,7 @@ symbolicBitVector symbolicBitVector::minValue(const bwt &w) } template <> -symbolicBitVector symbolicBitVector::minValue(const bwt &w) +symbolicBitVector symbolicBitVector::minValue(const bwt& w) { return symbolicBitVector::zero(w); } @@ -421,7 +420,7 @@ symbolicBitVector symbolicBitVector::minValue(const bwt &w) /*** Operators ***/ template symbolicBitVector symbolicBitVector::operator<<( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicBitVector( NodeManager::currentNM()->mkNode(kind::BITVECTOR_SHL, *this, op)); @@ -429,7 +428,7 @@ symbolicBitVector symbolicBitVector::operator<<( template symbolicBitVector symbolicBitVector::operator>>( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicBitVector(NodeManager::currentNM()->mkNode( (isSigned) ? kind::BITVECTOR_ASHR : kind::BITVECTOR_LSHR, *this, op)); @@ -437,7 +436,7 @@ symbolicBitVector symbolicBitVector::operator>>( template symbolicBitVector symbolicBitVector::operator|( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicBitVector( NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op)); @@ -445,7 +444,7 @@ symbolicBitVector symbolicBitVector::operator|( template symbolicBitVector symbolicBitVector::operator&( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicBitVector( NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op)); @@ -453,7 +452,7 @@ symbolicBitVector symbolicBitVector::operator&( template symbolicBitVector symbolicBitVector::operator+( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicBitVector( NodeManager::currentNM()->mkNode(kind::BITVECTOR_ADD, *this, op)); @@ -461,7 +460,7 @@ symbolicBitVector symbolicBitVector::operator+( template symbolicBitVector symbolicBitVector::operator-( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicBitVector( NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, *this, op)); @@ -469,7 +468,7 @@ symbolicBitVector symbolicBitVector::operator-( template symbolicBitVector symbolicBitVector::operator*( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicBitVector( NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, *this, op)); @@ -477,7 +476,7 @@ symbolicBitVector symbolicBitVector::operator*( template symbolicBitVector symbolicBitVector::operator/( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicBitVector(NodeManager::currentNM()->mkNode( (isSigned) ? kind::BITVECTOR_SDIV : kind::BITVECTOR_UDIV, *this, op)); @@ -485,7 +484,7 @@ symbolicBitVector symbolicBitVector::operator/( template symbolicBitVector symbolicBitVector::operator%( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicBitVector(NodeManager::currentNM()->mkNode( (isSigned) ? kind::BITVECTOR_SREM : kind::BITVECTOR_UREM, *this, op)); @@ -499,7 +498,7 @@ symbolicBitVector symbolicBitVector::operator-(void) const } template -symbolicBitVector symbolicBitVector::operator~(void)const +symbolicBitVector symbolicBitVector::operator~(void) const { return symbolicBitVector( NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this)); @@ -521,7 +520,7 @@ symbolicBitVector symbolicBitVector::decrement() const template symbolicBitVector symbolicBitVector::signExtendRightShift( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicBitVector( NodeManager::currentNM()->mkNode(kind::BITVECTOR_ASHR, *this, op)); @@ -531,14 +530,14 @@ symbolicBitVector symbolicBitVector::signExtendRightShift( // No overflow checking so these are the same as other operations template symbolicBitVector symbolicBitVector::modularLeftShift( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return *this << op; } template symbolicBitVector symbolicBitVector::modularRightShift( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return *this >> op; } @@ -559,7 +558,7 @@ symbolicBitVector symbolicBitVector::modularDecrement() template symbolicBitVector symbolicBitVector::modularAdd( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return *this + op; } @@ -574,7 +573,7 @@ symbolicBitVector symbolicBitVector::modularNegate() const template symbolicProposition symbolicBitVector::operator==( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicProposition( NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op)); @@ -582,7 +581,7 @@ symbolicProposition symbolicBitVector::operator==( template symbolicProposition symbolicBitVector::operator<=( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { // Consider adding kind::BITVECTOR_SLEBV and BITVECTOR_ULEBV return (*this < op) || (*this == op); @@ -590,14 +589,14 @@ symbolicProposition symbolicBitVector::operator<=( template symbolicProposition symbolicBitVector::operator>=( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return (*this > op) || (*this == op); } template symbolicProposition symbolicBitVector::operator<( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicProposition(NodeManager::currentNM()->mkNode( (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, *this, op)); @@ -605,7 +604,7 @@ symbolicProposition symbolicBitVector::operator<( template symbolicProposition symbolicBitVector::operator>( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicProposition(NodeManager::currentNM()->mkNode( (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, op, *this)); @@ -630,7 +629,7 @@ symbolicBitVector symbolicBitVector::extend(bwt extension) const { NodeBuilder construct(kind::BITVECTOR_SIGN_EXTEND); construct << NodeManager::currentNM()->mkConst( - BitVectorSignExtend(extension)) + BitVectorSignExtend(extension)) << *this; return symbolicBitVector(construct); @@ -641,7 +640,7 @@ symbolicBitVector symbolicBitVector::extend(bwt extension) const { NodeBuilder construct(kind::BITVECTOR_ZERO_EXTEND); construct << NodeManager::currentNM()->mkConst( - BitVectorZeroExtend(extension)) + BitVectorZeroExtend(extension)) << *this; return symbolicBitVector(construct); @@ -655,7 +654,7 @@ symbolicBitVector symbolicBitVector::contract( NodeBuilder construct(kind::BITVECTOR_EXTRACT); construct << NodeManager::currentNM()->mkConst( - BitVectorExtract((this->getWidth() - 1) - reduction, 0)) + BitVectorExtract((this->getWidth() - 1) - reduction, 0)) << *this; return symbolicBitVector(construct); @@ -683,7 +682,7 @@ symbolicBitVector symbolicBitVector::resize( template symbolicBitVector symbolicBitVector::matchWidth( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { Assert(this->getWidth() <= op.getWidth()); return this->extend(op.getWidth() - this->getWidth()); @@ -691,7 +690,7 @@ symbolicBitVector symbolicBitVector::matchWidth( template symbolicBitVector symbolicBitVector::append( - const symbolicBitVector &op) const + const symbolicBitVector& op) const { return symbolicBitVector( NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, *this, op)); @@ -706,7 +705,7 @@ symbolicBitVector symbolicBitVector::extract( NodeBuilder construct(kind::BITVECTOR_EXTRACT); construct << NodeManager::currentNM()->mkConst( - BitVectorExtract(upper, lower)) + BitVectorExtract(upper, lower)) << *this; return symbolicBitVector(construct); @@ -721,7 +720,7 @@ floatingPointTypeInfo::floatingPointTypeInfo(unsigned exp, unsigned sig) : FloatingPointSize(exp, sig) { } -floatingPointTypeInfo::floatingPointTypeInfo(const floatingPointTypeInfo &old) +floatingPointTypeInfo::floatingPointTypeInfo(const floatingPointTypeInfo& old) : FloatingPointSize(old) { } @@ -730,11 +729,10 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const { return NodeManager::currentNM()->mkFloatingPointType(*this); } -} +} // namespace symfpuSymbolic -FpConverter::FpConverter(context::UserContext* user) - : d_additionalAssertions(user) - , +FpWordBlaster::FpWordBlaster(context::UserContext* user) + : d_additionalAssertions(user), d_fpMap(user), d_rmMap(user), d_boolMap(user), @@ -743,11 +741,11 @@ FpConverter::FpConverter(context::UserContext* user) { } -FpConverter::~FpConverter() {} +FpWordBlaster::~FpWordBlaster() {} -Node FpConverter::ufToNode(const fpt &format, const uf &u) const +Node FpWordBlaster::ufToNode(const fpt& format, const uf& u) const { - NodeManager *nm = NodeManager::currentNM(); + NodeManager* nm = NodeManager::currentNM(); FloatingPointSize fps(format.getTypeNode().getConst()); @@ -761,9 +759,9 @@ Node FpConverter::ufToNode(const fpt &format, const uf &u) const return value; } -Node FpConverter::rmToNode(const rm &r) const +Node FpWordBlaster::rmToNode(const rm& r) const { - NodeManager *nm = NodeManager::currentNM(); + NodeManager* nm = NodeManager::currentNM(); Node transVar = r; @@ -792,22 +790,22 @@ Node FpConverter::rmToNode(const rm &r) const return value; } -Node FpConverter::propToNode(const prop &p) const +Node FpWordBlaster::propToNode(const prop& p) const { - NodeManager *nm = NodeManager::currentNM(); + 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; } +Node FpWordBlaster::ubvToNode(const ubv& u) const { return u; } +Node FpWordBlaster::sbvToNode(const sbv& s) const { return s; } // Creates the components constraint -FpConverter::uf FpConverter::buildComponents(TNode current) +FpWordBlaster::uf FpWordBlaster::buildComponents(TNode current) { Assert(Theory::isLeafOf(current, THEORY_FP) || current.getKind() == kind::FLOATINGPOINT_TO_FP_REAL); - NodeManager *nm = NodeManager::currentNM(); + 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), @@ -820,7 +818,7 @@ FpConverter::uf FpConverter::buildComponents(TNode current) return tmp; } -Node FpConverter::convert(TNode node) +Node FpWordBlaster::wordBlast(TNode node) { std::vector visit; std::unordered_map visited; @@ -936,18 +934,16 @@ Node FpConverter::convert(TNode node) /* ---- 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)); + 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)); + d_fpMap.insert(cur, + symfpu::negate( + fpt(t), (*d_fpMap.find(cur[0])).second)); break; case kind::FLOATINGPOINT_SQRT: @@ -1073,33 +1069,29 @@ Node FpConverter::convert(TNode node) Node IEEEBV( nm->mkNode(kind::BITVECTOR_CONCAT, cur[0], cur[1], cur[2])); - d_fpMap.insert( - cur, symfpu::unpack(fpt(t), IEEEBV)); + 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]))); + 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]))); + 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]))); + d_fpMap.insert( + cur, + symfpu::convertUBVToFloat( + fpt(t), (*d_rmMap.find(cur[0])).second, ubv(cur[1]))); break; case kind::FLOATINGPOINT_TO_FP_REAL: @@ -1283,7 +1275,7 @@ Node FpConverter::convert(TNode node) return node; } -Node FpConverter::getValue(Valuation &val, TNode var) +Node FpWordBlaster::getValue(Valuation& val, TNode var) { Assert(Theory::isLeafOf(var, THEORY_FP)); diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_word_blaster.h similarity index 78% rename from src/theory/fp/fp_converter.h rename to src/theory/fp/fp_word_blaster.h index d589eff60..f9ec4fd4e 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_word_blaster.h @@ -21,20 +21,19 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__FP__FP_CONVERTER_H -#define CVC5__THEORY__FP__FP_CONVERTER_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" -#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, @@ -87,9 +86,9 @@ class traits 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); + 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. @@ -107,9 +106,9 @@ class nodeWrapper : public Node * allowing them to be traced via GDB. */ #ifdef CVC5_SYM_SYMBOLIC_EVAL - nodeWrapper(const Node &n) : Node(theory::Rewriter::rewrite(n)) {} + nodeWrapper(const Node& n) : Node(theory::Rewriter::rewrite(n)) {} #else - nodeWrapper(const Node &n) : Node(n) {} + nodeWrapper(const Node& n) : Node(n) {} #endif }; @@ -123,13 +122,13 @@ class symbolicProposition : public nodeWrapper public: symbolicProposition(const Node n); symbolicProposition(bool v); - symbolicProposition(const symbolicProposition &old); + 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; + 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 @@ -142,10 +141,10 @@ class symbolicRoundingMode : public nodeWrapper public: symbolicRoundingMode(const Node n); symbolicRoundingMode(const unsigned v); - symbolicRoundingMode(const symbolicRoundingMode &old); + symbolicRoundingMode(const symbolicRoundingMode& old); symbolicProposition valid(void) const; - symbolicProposition operator==(const symbolicRoundingMode &op) const; + symbolicProposition operator==(const symbolicRoundingMode& op) const; }; // Type function for mapping between types @@ -183,68 +182,68 @@ class symbolicBitVector : public nodeWrapper public: symbolicBitVector(const Node n); symbolicBitVector(const bwt w, const unsigned v); - symbolicBitVector(const symbolicProposition &p); - symbolicBitVector(const symbolicBitVector &old); - symbolicBitVector(const BitVector &old); + 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); + 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); + static symbolicBitVector maxValue(const bwt& w); + static symbolicBitVector minValue(const bwt& w); /*** Operators ***/ symbolicBitVector operator<<( - const symbolicBitVector &op) const; + const symbolicBitVector& op) const; symbolicBitVector operator>>( - const symbolicBitVector &op) const; + const symbolicBitVector& op) const; symbolicBitVector operator|( - const symbolicBitVector &op) const; + const symbolicBitVector& op) const; symbolicBitVector operator&( - const symbolicBitVector &op) const; + const symbolicBitVector& op) const; symbolicBitVector operator+( - const symbolicBitVector &op) const; + const symbolicBitVector& op) const; symbolicBitVector operator-( - const symbolicBitVector &op) const; + const symbolicBitVector& op) const; symbolicBitVector operator*( - const symbolicBitVector &op) const; + const symbolicBitVector& op) const; symbolicBitVector operator/( - const symbolicBitVector &op) const; + const symbolicBitVector& op) const; symbolicBitVector operator%( - const symbolicBitVector &op) const; + const symbolicBitVector& op) const; symbolicBitVector operator-(void) const; - symbolicBitVector operator~(void)const; + symbolicBitVector operator~(void) const; symbolicBitVector increment() const; symbolicBitVector decrement() const; symbolicBitVector signExtendRightShift( - const symbolicBitVector &op) const; + 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; + const symbolicBitVector& op) const; symbolicBitVector modularRightShift( - const symbolicBitVector &op) const; + const symbolicBitVector& op) const; symbolicBitVector modularIncrement() const; symbolicBitVector modularDecrement() const; symbolicBitVector modularAdd( - const symbolicBitVector &op) const; + 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; + 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 @@ -257,9 +256,9 @@ class symbolicBitVector : public nodeWrapper symbolicBitVector contract(bwt reduction) const; symbolicBitVector resize(bwt newSize) const; symbolicBitVector matchWidth( - const symbolicBitVector &op) const; + const symbolicBitVector& op) const; symbolicBitVector append( - const symbolicBitVector &op) const; + const symbolicBitVector& op) const; // Inclusive of end points, thus if the same, extracts just one bit symbolicBitVector extract(bwt upper, bwt lower) const; @@ -272,11 +271,11 @@ class floatingPointTypeInfo : public FloatingPointSize public: floatingPointTypeInfo(const TypeNode t); floatingPointTypeInfo(unsigned exp, unsigned sig); - floatingPointTypeInfo(const floatingPointTypeInfo &old); + floatingPointTypeInfo(const floatingPointTypeInfo& old); TypeNode getTypeNode(void) const; }; -} +} // namespace symfpuSymbolic /** * This class uses SymFPU to convert an expression containing floating-point @@ -289,16 +288,16 @@ class floatingPointTypeInfo : public FloatingPointSize * and unpacking operations are avoided and to make best use of structural * sharing. */ -class FpConverter +class FpWordBlaster { public: /** Constructor. */ - FpConverter(context::UserContext*); + FpWordBlaster(context::UserContext*); /** Destructor. */ - ~FpConverter(); + ~FpWordBlaster(); /** Adds a node to the conversion, returns the converted node */ - Node convert(TNode); + Node wordBlast(TNode); /** * Gives the node representing the value of a word-blasted variable. @@ -334,11 +333,11 @@ class FpConverter * 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; + 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); 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 { -- 2.30.2