From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 23 Jun 2021 18:19:13 +0000 (-0700)
Subject: FP: Remove sections guarded with undefined macro SYMFPUPROPISBOOL. (#6786)
X-Git-Tag: cvc5-1.0.0~1566
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a5fd20bfe05e6d1a0a9dfc99bc8a668b613d9a19;p=cvc5.git

FP: Remove sections guarded with undefined macro SYMFPUPROPISBOOL. (#6786)
---

diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp
index 11bb05c70..a499b9666 100644
--- a/src/theory/fp/fp_expand_defs.cpp
+++ b/src/theory/fp/fp_expand_defs.cpp
@@ -51,11 +51,7 @@ Node FpExpandDefs::minUF(Node node)
     args[1] = t;
     fun = sm->mkDummySkolem("floatingpoint_min_zero_case",
                             nm->mkFunctionType(args,
-#ifdef SYMFPUPROPISBOOL
-                                               nm->booleanType()
-#else
                                                nm->mkBitVectorType(1U)
-#endif
                                                    ),
                             "floatingpoint_min_zero_case",
                             NodeManager::SKOLEM_EXACT_NAME);
@@ -89,11 +85,7 @@ Node FpExpandDefs::maxUF(Node node)
     args[1] = t;
     fun = sm->mkDummySkolem("floatingpoint_max_zero_case",
                             nm->mkFunctionType(args,
-#ifdef SYMFPUPROPISBOOL
-                                               nm->booleanType()
-#else
                                                nm->mkBitVectorType(1U)
-#endif
                                                    ),
                             "floatingpoint_max_zero_case",
                             NodeManager::SKOLEM_EXACT_NAME);
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 77dba0724..1c8f10f77 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -525,36 +525,32 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
   size_t newAdditionalAssertions = d_conv->d_additionalAssertions.size();
   Assert(oldAdditionalAssertions <= newAdditionalAssertions);
 
-  while (oldAdditionalAssertions < newAdditionalAssertions) {
+  while (oldAdditionalAssertions < newAdditionalAssertions)
+  {
     Node addA = d_conv->d_additionalAssertions[oldAdditionalAssertions];
 
     Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion  "
                             << addA << std::endl;
 
-#ifdef SYMFPUPROPISBOOL
-    handleLemma(addA, false, true);
-#else
-    NodeManager *nm = NodeManager::currentNM();
+    NodeManager* nm = NodeManager::currentNM();
 
     handleLemma(
         nm->mkNode(kind::EQUAL, addA, nm->mkConst(::cvc5::BitVector(1U, 1U))),
         InferenceId::FP_EQUATE_TERM);
-#endif
 
     ++oldAdditionalAssertions;
   }
 
   // Equate the floating-point atom and the converted one.
   // Also adds the bit-vectors to the bit-vector solver.
-  if (node.getType().isBoolean()) {
-    if (converted != node) {
+  if (node.getType().isBoolean())
+  {
+    if (converted != node)
+    {
       Assert(converted.getType().isBitVector());
 
-      NodeManager *nm = NodeManager::currentNM();
+      NodeManager* nm = NodeManager::currentNM();
 
-#ifdef SYMFPUPROPISBOOL
-      handleLemma(nm->mkNode(kind::EQUAL, node, converted));
-#else
       handleLemma(
           nm->mkNode(kind::EQUAL,
                      node,
@@ -562,13 +558,14 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
                                 converted,
                                 nm->mkConst(::cvc5::BitVector(1U, 1U)))),
           InferenceId::FP_EQUATE_TERM);
-#endif
-
-    } else {
+    }
+    else
+    {
       Assert((node.getKind() == kind::EQUAL));
     }
-
-  } else if (node.getType().isBitVector()) {
+  }
+  else if (node.getType().isBitVector())
+  {
     if (converted != node) {
       Assert(converted.getType().isBitVector());