From: yoni206 <yoni206@users.noreply.github.com>
Date: Thu, 8 Oct 2020 00:20:52 +0000 (-0700)
Subject: fix unit failures on debug without symfpu (#5212)
X-Git-Tag: cvc5-1.0.0~2738
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=900a7217f8843a17f5ea6bb744b6013f2f394ed7;p=cvc5.git

fix unit failures on debug without symfpu (#5212)

The following tests fail (locally) when compiling with debug and without symfpu:

unit/api/sort_black (Failed)
unit/theory/logic_info_white (Failed)
unit/util/floatingpoint_black (Child aborted)

This PR conditions the relevant parts of these tests to the availability of symfpu.

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
---

diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index 53563f833..e9f0e04ea 100644
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -17,6 +17,7 @@
 #include <cxxtest/TestSuite.h>
 
 #include "api/cvc4cpp.h"
+#include "base/configuration.h"
 
 using namespace CVC4::api;
 
@@ -271,18 +272,24 @@ void SortBlack::testGetBVSize()
 
 void SortBlack::testGetFPExponentSize()
 {
-  Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-  TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize());
-  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&);
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+    TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize());
+    Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+    TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&);
+  }
 }
 
 void SortBlack::testGetFPSignificandSize()
 {
-  Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-  TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize());
-  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&);
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+    TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize());
+    Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+    TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&);
+  }
 }
 
 void SortBlack::testGetDatatypeParamSorts()
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 7990d9e54..055ff41cc 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -16,9 +16,9 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include "base/configuration.h"
 #include "expr/kind.h"
 #include "theory/logic_info.h"
-
 using namespace CVC4;
 using namespace CVC4::theory;
 
@@ -533,46 +533,65 @@ public:
                      CVC4::IllegalArgumentException&);
     TS_ASSERT_THROWS(info.disableTheory(THEORY_UF),
                      CVC4::IllegalArgumentException&);
-
     info = info.getUnlockedCopy();
-    TS_ASSERT( !info.isLocked() );
+    TS_ASSERT(!info.isLocked());
     info.disableTheory(THEORY_STRINGS);
     info.disableTheory(THEORY_SETS);
     info.disableTheory(THEORY_BAGS);
     info.arithOnlyLinear();
     info.disableIntegers();
     info.lock();
-    TS_ASSERT_EQUALS(info.getLogicString(), "SEP_AUFBVFPDTLRA");
+    if (CVC4::Configuration::isBuiltWithSymFPU())
+    {
+      TS_ASSERT_EQUALS(info.getLogicString(), "SEP_AUFBVFPDTLRA");
+    }
+    else
+    {
+      TS_ASSERT_EQUALS(info.getLogicString(), "SEP_AUFBVDTLRA");
+    }
 
     info = info.getUnlockedCopy();
-    TS_ASSERT( !info.isLocked() );
+    TS_ASSERT(!info.isLocked());
     info.disableQuantifiers();
     info.disableTheory(THEORY_BAGS);
     info.lock();
-    TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA");
+    if (CVC4::Configuration::isBuiltWithSymFPU())
+    {
+      TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA");
+    }
+    else
+    {
+      TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFBVDTLRA");
+    }
 
     info = info.getUnlockedCopy();
-    TS_ASSERT( !info.isLocked() );
+    TS_ASSERT(!info.isLocked());
     info.disableTheory(THEORY_BV);
     info.disableTheory(THEORY_DATATYPES);
     info.disableTheory(THEORY_BAGS);
     info.enableIntegers();
     info.disableReals();
     info.lock();
-    TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFFPLIA");
+    if (CVC4::Configuration::isBuiltWithSymFPU())
+    {
+      TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFFPLIA");
+    }
+    else
+    {
+      TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFLIA");
+    }
 
     info = info.getUnlockedCopy();
-    TS_ASSERT( !info.isLocked() );
+    TS_ASSERT(!info.isLocked());
     info.disableTheory(THEORY_ARITH);
     info.disableTheory(THEORY_UF);
     info.disableTheory(THEORY_FP);
     info.disableTheory(THEORY_SEP);
     info.disableTheory(THEORY_BAGS);
     info.lock();
-    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AX" );
-    TS_ASSERT( info.isPure( THEORY_ARRAYS ) );
-    TS_ASSERT( ! info.isQuantified() );
-
+    TS_ASSERT_EQUALS(info.getLogicString(), "QF_AX");
+    TS_ASSERT(info.isPure(THEORY_ARRAYS));
+    TS_ASSERT(!info.isQuantified());
     // check all-excluded logic
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index c5753e732..0fd7894fe 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -21,7 +21,9 @@ cvc4_add_unit_test_white(check_white util)
 cvc4_add_unit_test_black(configuration_black util)
 cvc4_add_unit_test_black(datatype_black util)
 cvc4_add_unit_test_black(exception_black util)
+if(CVC4_USE_SYMFPU)
 cvc4_add_unit_test_black(floatingpoint_black util)
+endif()
 cvc4_add_unit_test_black(integer_black util)
 cvc4_add_unit_test_white(integer_white util)
 cvc4_add_unit_test_black(output_black util)