summaryrefslogtreecommitdiff
path: root/src/theory/fp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/fp')
-rw-r--r--src/theory/fp/fp_converter.cpp44
-rw-r--r--src/theory/fp/fp_converter.h16
-rw-r--r--src/theory/fp/theory_fp_rewriter.cpp10
-rw-r--r--src/theory/fp/theory_fp_type_rules.cpp6
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback