From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Thu, 25 Mar 2021 18:04:54 +0000 (-0700)
Subject: Do not use Configuration class in API black tests. (#6205)
X-Git-Tag: cvc5-1.0.0~2030
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f9e3d2dccd5018e07df1c2cd323c5e192b020819;p=cvc5.git

Do not use Configuration class in API black tests. (#6205)
---

diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 6b6a0fa0f..ed7edf633 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -14,7 +14,6 @@
  ** Black box testing of the Solver class of the  C++ API.
  **/
 
-#include "base/configuration.h"
 #include "test_api.h"
 
 namespace CVC4 {
@@ -379,7 +378,7 @@ TEST_F(TestApiBlackSolver, mkBoolean)
 
 TEST_F(TestApiBlackSolver, mkRoundingMode)
 {
-  if (CVC4::Configuration::isBuiltWithSymFPU())
+  if (d_solver.supportsFloatingPoint())
   {
     ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
   }
@@ -422,7 +421,7 @@ TEST_F(TestApiBlackSolver, mkFloatingPoint)
   Term t1 = d_solver.mkBitVector(8);
   Term t2 = d_solver.mkBitVector(4);
   Term t3 = d_solver.mkInteger(2);
-  if (CVC4::Configuration::isBuiltWithSymFPU())
+  if (d_solver.supportsFloatingPoint())
   {
     ASSERT_NO_THROW(d_solver.mkFloatingPoint(3, 5, t1));
   }
@@ -436,7 +435,7 @@ TEST_F(TestApiBlackSolver, mkFloatingPoint)
   ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException);
   ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException);
 
-  if (CVC4::Configuration::isBuiltWithSymFPU())
+  if (d_solver.supportsFloatingPoint())
   {
     Solver slv;
     ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC4ApiException);
@@ -482,7 +481,7 @@ TEST_F(TestApiBlackSolver, mkFalse)
 
 TEST_F(TestApiBlackSolver, mkNaN)
 {
-  if (CVC4::Configuration::isBuiltWithSymFPU())
+  if (d_solver.supportsFloatingPoint())
   {
     ASSERT_NO_THROW(d_solver.mkNaN(3, 5));
   }
@@ -494,7 +493,7 @@ TEST_F(TestApiBlackSolver, mkNaN)
 
 TEST_F(TestApiBlackSolver, mkNegZero)
 {
-  if (CVC4::Configuration::isBuiltWithSymFPU())
+  if (d_solver.supportsFloatingPoint())
   {
     ASSERT_NO_THROW(d_solver.mkNegZero(3, 5));
   }
@@ -506,7 +505,7 @@ TEST_F(TestApiBlackSolver, mkNegZero)
 
 TEST_F(TestApiBlackSolver, mkNegInf)
 {
-  if (CVC4::Configuration::isBuiltWithSymFPU())
+  if (d_solver.supportsFloatingPoint())
   {
     ASSERT_NO_THROW(d_solver.mkNegInf(3, 5));
   }
@@ -518,7 +517,7 @@ TEST_F(TestApiBlackSolver, mkNegInf)
 
 TEST_F(TestApiBlackSolver, mkPosInf)
 {
-  if (CVC4::Configuration::isBuiltWithSymFPU())
+  if (d_solver.supportsFloatingPoint())
   {
     ASSERT_NO_THROW(d_solver.mkPosInf(3, 5));
   }
@@ -530,7 +529,7 @@ TEST_F(TestApiBlackSolver, mkPosInf)
 
 TEST_F(TestApiBlackSolver, mkPosZero)
 {
-  if (CVC4::Configuration::isBuiltWithSymFPU())
+  if (d_solver.supportsFloatingPoint())
   {
     ASSERT_NO_THROW(d_solver.mkPosZero(3, 5));
   }
diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp
index 625af9342..8e7eb00ec 100644
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/sort_black.cpp
@@ -14,7 +14,6 @@
  ** Black box testing of the guards of the C++ API functions.
  **/
 
-#include "base/configuration.h"
 #include "test_api.h"
 
 namespace CVC4 {
@@ -95,8 +94,11 @@ TEST_F(TestApiBlackSort, isRegExp)
 
 TEST_F(TestApiBlackSort, isRoundingMode)
 {
-  ASSERT_TRUE(d_solver.getRoundingModeSort().isRoundingMode());
-  ASSERT_NO_THROW(Sort().isRoundingMode());
+  if (d_solver.supportsFloatingPoint())
+  {
+    ASSERT_TRUE(d_solver.getRoundingModeSort().isRoundingMode());
+    ASSERT_NO_THROW(Sort().isRoundingMode());
+  }
 }
 
 TEST_F(TestApiBlackSort, isBitVector)
@@ -107,8 +109,11 @@ TEST_F(TestApiBlackSort, isBitVector)
 
 TEST_F(TestApiBlackSort, isFloatingPoint)
 {
-  ASSERT_TRUE(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint());
-  ASSERT_NO_THROW(Sort().isFloatingPoint());
+  if (d_solver.supportsFloatingPoint())
+  {
+    ASSERT_TRUE(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint());
+    ASSERT_NO_THROW(Sort().isFloatingPoint());
+  }
 }
 
 TEST_F(TestApiBlackSort, isDatatype)
@@ -471,7 +476,7 @@ TEST_F(TestApiBlackSort, getBVSize)
 
 TEST_F(TestApiBlackSort, getFPExponentSize)
 {
-  if (CVC4::Configuration::isBuiltWithSymFPU())
+  if (d_solver.supportsFloatingPoint())
   {
     Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
     ASSERT_NO_THROW(fpSort.getFPExponentSize());
@@ -482,7 +487,7 @@ TEST_F(TestApiBlackSort, getFPExponentSize)
 
 TEST_F(TestApiBlackSort, getFPSignificandSize)
 {
-  if (CVC4::Configuration::isBuiltWithSymFPU())
+  if (d_solver.supportsFloatingPoint())
   {
     Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
     ASSERT_NO_THROW(fpSort.getFPSignificandSize());