diff options
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/fp_converter.cpp | 44 | ||||
-rw-r--r-- | src/theory/fp/fp_converter.h | 16 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 10 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_type_rules.cpp | 6 |
4 files changed, 38 insertions, 38 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 1d124045b..5b2f586ba 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -22,7 +22,7 @@ #include "util/floatingpoint.h" #include "util/floatingpoint_literal_symfpu.h" -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU #include "symfpu/core/add.h" #include "symfpu/core/classify.h" #include "symfpu/core/compare.h" @@ -39,11 +39,11 @@ #include "symfpu/utils/properties.h" #endif -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU namespace symfpu { using namespace ::cvc5::theory::fp::symfpuSymbolic; -#define CVC4_SYM_ITE_DFN(T) \ +#define CVC5_SYM_ITE_DFN(T) \ template <> \ struct ite<symbolicProposition, T> \ { \ @@ -114,12 +114,12 @@ using namespace ::cvc5::theory::fp::symfpuSymbolic; } // Can (unsurprisingly) only ITE things which contain Nodes -CVC4_SYM_ITE_DFN(traits::rm); -CVC4_SYM_ITE_DFN(traits::prop); -CVC4_SYM_ITE_DFN(traits::sbv); -CVC4_SYM_ITE_DFN(traits::ubv); +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 CVC4_SYM_ITE_DFN +#undef CVC5_SYM_ITE_DFN template <> traits::ubv orderEncode<traits, traits::ubv>(const traits::ubv &b) @@ -144,7 +144,7 @@ void probabilityAnnotation<traits, traits::prop>(const traits::prop &p, }; #endif -#ifndef CVC4_USE_SYMFPU +#ifndef CVC5_USE_SYMFPU #define SYMFPU_NUMBER_OF_ROUNDING_MODES 5 #endif @@ -241,7 +241,7 @@ symbolicProposition symbolicProposition::operator^( bool symbolicRoundingMode::checkNodeType(const TNode n) { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return n.getType(false).isBitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES); #else return false; @@ -253,7 +253,7 @@ symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n) Assert(checkNodeType(*this)); } -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU symbolicRoundingMode::symbolicRoundingMode(const unsigned v) : nodeWrapper(NodeManager::currentNM()->mkConst( BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v))) @@ -754,7 +754,7 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const FpConverter::FpConverter(context::UserContext* user) : d_additionalAssertions(user) -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU , d_fpMap(user), d_rmMap(user), @@ -767,7 +767,7 @@ FpConverter::FpConverter(context::UserContext* user) FpConverter::~FpConverter() {} -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU Node FpConverter::ufToNode(const fpt &format, const uf &u) const { NodeManager *nm = NodeManager::currentNM(); @@ -844,11 +844,11 @@ FpConverter::uf FpConverter::buildComponents(TNode current) // Non-convertible things should only be added to the stack at the very start, // thus... -#define CVC4_FPCONV_PASSTHROUGH Assert(workStack.empty()) +#define CVC5_FPCONV_PASSTHROUGH Assert(workStack.empty()) Node FpConverter::convert(TNode node) { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU std::vector<TNode> workStack; TNode result = node; @@ -1397,7 +1397,7 @@ Node FpConverter::convert(TNode node) } else { - CVC4_FPCONV_PASSTHROUGH; + CVC5_FPCONV_PASSTHROUGH; return result; } } @@ -1534,7 +1534,7 @@ Node FpConverter::convert(TNode node) /* Fall through... */ default: - CVC4_FPCONV_PASSTHROUGH; + CVC5_FPCONV_PASSTHROUGH; return result; break; } @@ -1652,7 +1652,7 @@ Node FpConverter::convert(TNode node) case kind::ROUNDINGMODE_BITBLAST: /* Fall through ... */ - default: CVC4_FPCONV_PASSTHROUGH; break; + default: CVC5_FPCONV_PASSTHROUGH; break; } } else if (t.isReal()) @@ -1691,12 +1691,12 @@ Node FpConverter::convert(TNode node) "expandDefinition"; break; - default: CVC4_FPCONV_PASSTHROUGH; break; + default: CVC5_FPCONV_PASSTHROUGH; break; } } else { - CVC4_FPCONV_PASSTHROUGH; + CVC5_FPCONV_PASSTHROUGH; } } @@ -1706,13 +1706,13 @@ Node FpConverter::convert(TNode node) #endif } -#undef CVC4_FPCONV_PASSTHROUGH +#undef CVC5_FPCONV_PASSTHROUGH Node FpConverter::getValue(Valuation &val, TNode var) { Assert(Theory::isLeafOf(var, THEORY_FP)); -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU TypeNode t(var.getType()); Assert(t.isRoundingMode() || t.isFloatingPoint()) diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index f3341f442..3a74627d5 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -32,11 +32,11 @@ #include "util/floatingpoint_size.h" #include "util/hash.h" -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU #include "symfpu/core/unpackedFloat.h" #endif -#ifdef CVC4_SYM_SYMBOLIC_EVAL +#ifdef CVC5_SYM_SYMBOLIC_EVAL // This allows debugging of the CVC4 symbolic back-end. // By enabling this and disabling constant folding in the rewriter, // SMT files that have operations on constants will be evaluated @@ -102,12 +102,12 @@ typedef traits::bwt bwt; class nodeWrapper : public Node { protected: -/* CVC4_SYM_SYMBOLIC_EVAL is for debugging CVC4 symbolic back-end issues. +/* CVC5_SYM_SYMBOLIC_EVAL is for debugging CVC4 symbolic back-end issues. * Enable this and disabling constant folding will mean that operations * that are input with constant args are 'folded' using the symbolic encoding * allowing them to be traced via GDB. */ -#ifdef CVC4_SYM_SYMBOLIC_EVAL +#ifdef CVC5_SYM_SYMBOLIC_EVAL nodeWrapper(const Node &n) : Node(theory::Rewriter::rewrite(n)) {} #else nodeWrapper(const Node &n) : Node(n) {} @@ -119,7 +119,7 @@ class symbolicProposition : public nodeWrapper protected: bool checkNodeType(const TNode node); -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicProposition>; // For ITE #endif @@ -140,7 +140,7 @@ class symbolicRoundingMode : public nodeWrapper protected: bool checkNodeType(const TNode n); -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>; // For ITE #endif @@ -182,7 +182,7 @@ class symbolicBitVector : public nodeWrapper bool checkNodeType(const TNode n); friend symbolicBitVector<!isSigned>; // To allow conversion between the types -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicBitVector<isSigned> >; // For ITE #endif @@ -313,7 +313,7 @@ class FpConverter context::CDList<Node> d_additionalAssertions; protected: -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU typedef symfpuSymbolic::traits traits; typedef ::symfpu::unpackedFloat<symfpuSymbolic::traits> uf; typedef symfpuSymbolic::traits::rm rm; diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index ba94dca13..51d2e5bd7 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -194,7 +194,7 @@ namespace rewrite { // Note these cannot be assumed to be symmetric for +0/-0, thus no symmetry reorder RewriteResponse compactMinMax (TNode node, bool isPreRewrite) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS Kind k = node.getKind(); Assert((k == kind::FLOATINGPOINT_MIN) || (k == kind::FLOATINGPOINT_MAX) || (k == kind::FLOATINGPOINT_MIN_TOTAL) @@ -885,7 +885,7 @@ namespace constantFold { bool result; switch (k) { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU case kind::FLOATINGPOINT_COMPONENT_NAN: result = arg0.isNaN(); break; case kind::FLOATINGPOINT_COMPONENT_INF: result = arg0.isInfinite(); break; case kind::FLOATINGPOINT_COMPONENT_ZERO: result = arg0.isZero(); break; @@ -909,7 +909,7 @@ namespace constantFold { // \todo Add a proper interface for this sort of thing to FloatingPoint #1915 return RewriteResponse( REWRITE_DONE, -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU NodeManager::currentNM()->mkConst((BitVector)arg0.getExponent()) #else node @@ -925,7 +925,7 @@ namespace constantFold { return RewriteResponse( REWRITE_DONE, -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU NodeManager::currentNM()->mkConst((BitVector)arg0.getSignificand()) #else node @@ -939,7 +939,7 @@ namespace constantFold { BitVector value; -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU /* \todo fix the numbering of rounding modes so this doesn't need * to call symfpu at all and remove the dependency on fp_converter.h #1915 */ RoundingMode arg0(node[0].getConst<RoundingMode>()); diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp index d7060ad98..44936c440 100644 --- a/src/theory/fp/theory_fp_type_rules.cpp +++ b/src/theory/fp/theory_fp_type_rules.cpp @@ -711,7 +711,7 @@ TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager, } } -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU /* Need to create some symfpu objects as the size of bit-vector * that is needed for this component is dependent on the encoding * used (i.e. whether subnormals are forcibly normalised or not). @@ -751,7 +751,7 @@ TypeNode FloatingPointComponentSignificand::computeType( } } -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU /* As before we need to use some of sympfu. */ FloatingPointSize fps = operandType.getConst<FloatingPointSize>(); uint32_t bw = FloatingPoint::getUnpackedSignificandWidth(fps); @@ -783,7 +783,7 @@ TypeNode RoundingModeBitBlast::computeType(NodeManager* nodeManager, } } - return nodeManager->mkBitVectorType(CVC4_NUM_ROUNDING_MODES); + return nodeManager->mkBitVectorType(CVC5_NUM_ROUNDING_MODES); } Cardinality CardinalityComputer::computeCardinality(TypeNode type) |