diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-22 18:01:22 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-22 18:01:22 -0700 |
| commit | 474faec211db41b626ed29d8dde26ff861f40d87 (patch) | |
| tree | 3c5e68fb24113fca9e74c002614a388698d9a5f5 /src/theory/fp/fp_converter.h | |
| parent | 0bb3e14b46a4b2f5cacfadb313c947da73ba7df6 (diff) | |
| parent | 21ee0f18c288d430d08c133f601173be25411187 (diff) | |
Merge branch 'master' into rmTearDownIncrementalrmTearDownIncremental
Diffstat (limited to 'src/theory/fp/fp_converter.h')
| -rw-r--r-- | src/theory/fp/fp_converter.h | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index f1b7c8a83..9900c2987 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -33,9 +33,7 @@ #include "util/floatingpoint_size.h" #include "util/hash.h" -#ifdef CVC5_USE_SYMFPU #include "symfpu/core/unpackedFloat.h" -#endif #ifdef CVC5_SYM_SYMBOLIC_EVAL // This allows debugging of the cvc5 symbolic back-end. @@ -120,9 +118,7 @@ class symbolicProposition : public nodeWrapper protected: bool checkNodeType(const TNode node); -#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicProposition>; // For ITE -#endif public: symbolicProposition(const Node n); @@ -141,9 +137,7 @@ class symbolicRoundingMode : public nodeWrapper protected: bool checkNodeType(const TNode n); -#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>; // For ITE -#endif public: symbolicRoundingMode(const Node n); @@ -183,10 +177,8 @@ class symbolicBitVector : public nodeWrapper bool checkNodeType(const TNode n); friend symbolicBitVector<!isSigned>; // To allow conversion between the types -#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicBitVector<isSigned> >; // For ITE -#endif public: symbolicBitVector(const Node n); @@ -314,7 +306,6 @@ class FpConverter context::CDList<Node> d_additionalAssertions; protected: -#ifdef CVC5_USE_SYMFPU typedef symfpuSymbolic::traits traits; typedef ::symfpu::unpackedFloat<symfpuSymbolic::traits> uf; typedef symfpuSymbolic::traits::rm rm; @@ -348,7 +339,6 @@ class FpConverter /* Creates the relevant components for a variable */ uf buildComponents(TNode current); -#endif }; } // namespace fp |