diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-09 17:22:07 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-09 17:22:07 -0700 |
| commit | f87f038c5f0821d0fefb01cea00bfdec6004da91 (patch) | |
| tree | d948178e1c0d2dc459a976f0d187d2d41a5437c0 /src/theory/fp/fp_converter.h | |
| parent | 550c49a7dd2b13ea29743458336f0c0a0fb6099a (diff) | |
Rename CVC4_ macros to CVC5_. (#6327)
Diffstat (limited to 'src/theory/fp/fp_converter.h')
| -rw-r--r-- | src/theory/fp/fp_converter.h | 16 |
1 files changed, 8 insertions, 8 deletions
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; |