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 53563f8333fdab057b4c55ad0893f665b9e02af0..e9f0e04ea172e0b3eb2466c75b8c4218e870e055 100644 (file)
--- 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 7990d9e54d7b69e0ae61b3be25d42bda69a2ec57..055ff41cc2e6bc7216b4404301103be9837a5c72 100644 (file)
--- 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 c5753e732f6ee4d3ae9399e05c776633903e3895..0fd7894fed92fa8deeca926cf3e7864c3cf76f65 100644 (file)
--- 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)