[API] Fix Python Examples (#4943)

When testing the API examples, Python examples were not included. This
commit changes that and fixes multiple minor issues that came up once
the tests were enabled:

- It adds `Solver::supportsFloatingPoint()` as an API method that
  returns whether CVC4 is configured to support floating-point numbers
  or not (this is useful for failing gracefully when floating-point
  support is not available, e.g. in the case of our floating-point
  example).
- It updates the `expections.py` example to use the new API.
- It fixes the `sygus-fun.py` example. The example was passing a _set_
  of non-terminals to `Solver::mkSygusGrammar()` but the order in which
  the non-terminals are passed in matters because the first non-terminal
  is considered to be the starting terminal. The commit also updates the
  documentation of that function.
- It fixes the Python API for datatypes. The `__getitem__` function had
  a typo and the `datatypes.py` example was crashing as a result.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 5b1d1e2921059212252d6efd9d7ff844b98e216a..02933762b846111f09436aa3a5aa158e8d534acb 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -571,6 +571,7 @@ add_subdirectory(src)
 add_subdirectory(test)
 
 if(BUILD_BINDINGS_PYTHON)
+  set(BUILD_BINDINGS_PYTHON_VERSION ${PYTHON_VERSION_MAJOR})
   add_subdirectory(src/api/python)
 endif()
 

diff --git a/cmake/CVC4Config.cmake.in b/cmake/CVC4Config.cmake.in
index 76535762d2a58438410fd4087c5d05702828a018..7f6a80995569da0fd09e1b1b4fbae0279c8f3e83 100644 (file)
--- a/cmake/CVC4Config.cmake.in
+++ b/cmake/CVC4Config.cmake.in
@@ -1,7 +1,8 @@
 @PACKAGE_INIT@
 
-set(CVC4_BINDINGS_JAVA @BUILD_SWIG_BINDINGS_JAVA@)
-set(CVC4_BINDINGS_PYTHON @BUILD_SWIG_BINDINGS_PYTHON@)
+set(CVC4_BINDINGS_JAVA @BUILD_BINDINGS_JAVA@)
+set(CVC4_BINDINGS_PYTHON @BUILD_BINDINGS_PYTHON@)
+set(CVC4_BINDINGS_PYTHON_VERSION @BUILD_BINDINGS_PYTHON_VERSION@)
 
 if(NOT TARGET CVC4::cvc4)
   include(${CMAKE_CURRENT_LIST_DIR}/CVC4Targets.cmake)

diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt
index e3966fa2d9e53008fb27d8178e0871af6b2acbc5..0da960513ab0d00ec877e77cb8374614d66b471b 100644 (file)
--- a/examples/api/python/CMakeLists.txt
+++ b/examples/api/python/CMakeLists.txt
@@ -1,9 +1,22 @@
 set(EXAMPLES_API_PYTHON
+  bitvectors_and_arrays
+  bitvectors
+  combination
+  datatypes
   exceptions
+  extract
+  floating_point
+  helloworld
+  linear_arith
   sequences
+  sets
+  strings
+  sygus-fun
+  sygus-grammar
+  sygus-inv
 )
 
-find_package(PythonInterp REQUIRED)
+find_package(PythonInterp ${CVC4_BINDINGS_PYTHON_VERSION} REQUIRED)
 
 # Find Python bindings in the corresponding python-*/site-packages directory.
 # Lookup Python module directory and store path in PYTHON_MODULE_PATH.

diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py
index 780f75bf709d29a855074475c779a52da18da81a..27f0680119561595d7dde70c9d6f0c5fe948ecc2 100644 (file)
--- a/examples/api/python/exceptions.py
+++ b/examples/api/python/exceptions.py
@@ -16,40 +16,40 @@
 ## A simple demonstration of catching CVC4 execptions with the legacy Python
 ## API.
 
-import CVC4
+import pycvc4
+from pycvc4 import kinds
 import sys
 
 
 def main():
-    em = CVC4.ExprManager()
-    smt = CVC4.SmtEngine(em)
+    slv = pycvc4.Solver()
 
-    smt.setOption("produce-models", CVC4.SExpr("true"))
+    slv.setOption("produce-models", "true")
 
     # Setting an invalid option
     try:
-        smt.setOption("non-existing", CVC4.SExpr("true"))
+        slv.setOption("non-existing", "true")
         return 1
-    except CVC4.Exception as e:
-        print(e.toString())
+    except:
+        pass
 
     # Creating a term with an invalid type
     try:
-        integer = em.integerType()
-        x = em.mkVar("x", integer)
-        invalidExpr = em.mkExpr(CVC4.AND, x, x)
-        smt.checkSat(invalidExpr)
+        integer = slv.getIntegerSort()
+        x = slv.mkConst("x", integer)
+        invalidTerm = em.mkTerm(AND, x, x)
+        slv.checkSat(invalidTerm)
         return 1
-    except CVC4.Exception as e:
-        print(e.toString())
+    except:
+        pass
 
     # Asking for a model after unsat result
     try:
-        smt.checkSat(em.mkBoolConst(False))
-        smt.getModel()
+        slv.checkSat(slv.mkBoolean(False))
+        slv.getModel()
         return 1
-    except CVC4.Exception as e:
-        print(e.toString())
+    except:
+        pass
 
     return 0
 

diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py
index c92666c0b69963396354b00fb4e2238aab8d39a7..6fb595e34095ee466a59b0d9a3cd68a78684678f 100755 (executable)
--- a/examples/api/python/floating_point.py
+++ b/examples/api/python/floating_point.py
@@ -20,8 +20,15 @@ from pycvc4 import kinds
 
 if __name__ == "__main__":
     slv = pycvc4.Solver()
+
+    if not slv.supportsFloatingPoint():
+        # CVC4 must be built with SymFPU to support the theory of
+        # floating-point numbers
+        print("CVC4 was not built with floating-point support.")
+        exit()
+
     slv.setOption("produce-models", "true")
-    slv.setLogic("FP")
+    slv.setLogic("QF_FP")
 
     # single 32-bit precision
     fp32 = slv.mkFloatingPointSort(8, 24)

diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py
index 0f53bd343405efd9c67c24acad186f3546a59bf5..25090bd8f3626fa00602654131fb8e04e9126ebc 100644 (file)
--- a/examples/api/python/sygus-fun.py
+++ b/examples/api/python/sygus-fun.py
@@ -53,7 +53,7 @@ if __name__ == "__main__":
   leq = slv.mkTerm(kinds.Leq, start, start)
 
   # create the grammar object
-  g = slv.mkSygusGrammar({x, y}, {start, start_bool})
+  g = slv.mkSygusGrammar([x, y], [start, start_bool])
 
   # bind each non-terminal to its rules
   g.addRules(start, {zero, one, x, y, plus, minus, ite})
@@ -61,8 +61,8 @@ if __name__ == "__main__":
 
   # declare the functions-to-synthesize. Optionally, provide the grammar
   # constraints
-  max = slv.synthFun("max", {x, y}, integer, g)
-  min = slv.synthFun("min", {x, y}, integer)
+  max = slv.synthFun("max", [x, y], integer, g)
+  min = slv.synthFun("min", [x, y], integer)
 
   # declare universal variables.
   varX = slv.mkSygusVar(integer, "x")

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index c14bed6aaffbdd6296aed023ce38eddafaee1fcc..6c39bfb912faeeb0816c580c2aab7ec88fa63db8 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3240,6 +3240,14 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
       << " children (the one under construction has " << nchildren << ")";
 }
 
+/* Solver Configuration                                                       */
+/* -------------------------------------------------------------------------- */
+
+bool Solver::supportsFloatingPoint() const
+{
+  return Configuration::isBuiltWithSymFPU();
+}
+
 /* Sorts Handling                                                             */
 /* -------------------------------------------------------------------------- */
 
@@ -3285,9 +3293,11 @@ Sort Solver::getStringSort(void) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Sort Solver::getRoundingmodeSort(void) const
+Sort Solver::getRoundingModeSort(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
+      << "Expected CVC4 to be compiled with SymFPU support";
   return Sort(this, d_exprMgr->roundingModeType());
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3323,6 +3333,8 @@ Sort Solver::mkBitVectorSort(uint32_t size) const
 Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
+      << "Expected CVC4 to be compiled with SymFPU support";
   CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0";
   CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0";
 
@@ -3803,6 +3815,8 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
 Term Solver::mkRoundingMode(RoundingMode rm) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
+      << "Expected CVC4 to be compiled with SymFPU support";
   return mkValHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -5396,7 +5410,7 @@ Term Solver::synthFunHelper(const std::string& symbol,
   {
     CVC4_API_CHECK(g->d_ntSyms[0].d_node->getType().toType() == *sort.d_type)
         << "Invalid Start symbol for Grammar g, Expected Start's sort to be "
-        << *sort.d_type;
+        << *sort.d_type << " but found " << g->d_ntSyms[0].d_node->getType();
   }
 
   Type funType = varTypes.empty()

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 0c322d7dae54157de8da86335674fbaffca5b97c..d92660920b95b0f20d7c35fc7f414fbddd86e262 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2152,6 +2152,12 @@ class CVC4_PUBLIC Solver
   Solver(const Solver&) = delete;
   Solver& operator=(const Solver&) = delete;
 
+  /* .................................................................... */
+  /* Solver Configuration                                                 */
+  /* .................................................................... */
+
+  bool supportsFloatingPoint() const;
+
   /* .................................................................... */
   /* Sorts Handling                                                       */
   /* .................................................................... */
@@ -2184,7 +2190,7 @@ class CVC4_PUBLIC Solver
   /**
    * @return sort RoundingMode
    */
-  Sort getRoundingmodeSort() const;
+  Sort getRoundingModeSort() const;
 
   /**
    * @return sort String
@@ -3169,7 +3175,9 @@ class CVC4_PUBLIC Solver
   Term mkSygusVar(Sort sort, const std::string& symbol = std::string()) const;
 
   /**
-   * Create a Sygus grammar.
+   * Create a Sygus grammar. The first non-terminal is treated as the starting
+   * non-terminal, so the order of non-terminals matters.
+   *
    * @param boundVars the parameters to corresponding synth-fun/synth-inv
    * @param ntSymbols the pre-declaration of the non-terminal symbols
    * @return the grammar

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 16d64b85e3afaaccc37a76b915cbd385faa9b58f..841fbb44d489aa1582ffad40bbf054da46afd96f 100644 (file)
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -116,11 +116,12 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
 
     cdef cppclass Solver:
         Solver(Options*) except +
+        bint supportsFloatingPoint() except +
         Sort getBooleanSort() except +
         Sort getIntegerSort() except +
         Sort getRealSort() except +
         Sort getRegExpSort() except +
-        Sort getRoundingmodeSort() except +
+        Sort getRoundingModeSort() except +
         Sort getStringSort() except +
         Sort mkArraySort(Sort indexSort, Sort elemSort) except +
         Sort mkBitVectorSort(uint32_t size) except +

diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index a51307d213875a6dbc14d7b1ac622eb142615c63..3caead057f835431cead6c8dfca0a37edab1df85 100644 (file)
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -21,7 +21,8 @@ from cvc4 cimport Grammar as c_Grammar
 from cvc4 cimport Sort as c_Sort
 from cvc4 cimport SortHashFunction as c_SortHashFunction
 from cvc4 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
-from cvc4 cimport ROUND_TOWARD_ZERO, ROUND_NEAREST_TIES_TO_AWAY
+from cvc4 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO
+from cvc4 cimport ROUND_NEAREST_TIES_TO_AWAY
 from cvc4 cimport Term as c_Term
 from cvc4 cimport TermHashFunction as c_TermHashFunction
 
@@ -88,7 +89,7 @@ cdef class Datatype:
         if isinstance(index, int) and index >= 0:
             dc.cdc = self.cd[(<int?> index)]
         elif isinstance(index, str):
-            dc.cdc = self.cd[(<const string &> name.encode())]
+            dc.cdc = self.cd[(<const string &> index.encode())]
         else:
             raise ValueError("Expecting a non-negative integer or string")
         return dc
@@ -395,6 +396,9 @@ cdef class Solver:
     def __dealloc__(self):
         del self.csolver
 
+    def supportsFloatingPoint(self):
+        return self.csolver.supportsFloatingPoint()
+
     def getBooleanSort(self):
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.getBooleanSort()
@@ -415,9 +419,9 @@ cdef class Solver:
         sort.csort = self.csolver.getRegExpSort()
         return sort
 
-    def getRoundingmodeSort(self):
+    def getRoundingModeSort(self):
         cdef Sort sort = Sort(self)
-        sort.csort = self.csolver.getRoundingmodeSort()
+        sort.csort = self.csolver.getRoundingModeSort()
         return sort
 
     def getStringSort(self):
@@ -1457,6 +1461,7 @@ cdef class Term:
 cdef __rounding_modes = {
     <int> ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven",
     <int> ROUND_TOWARD_POSITIVE: "RoundTowardPositive",
+    <int> ROUND_TOWARD_NEGATIVE: "RoundTowardNegative",
     <int> ROUND_TOWARD_ZERO: "RoundTowardZero",
     <int> ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway"
 }

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 1e5d2155a0ed1fafec20b3bb825f8c067b950efa..c4899c8a87e735a96904a348d8818b1fdf83606a 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -718,7 +718,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
   }
 
   if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
-    defineType("RoundingMode", d_solver->getRoundingmodeSort());
+    defineType("RoundingMode", d_solver->getRoundingModeSort());
     defineType("Float16", d_solver->mkFloatingPointSort(5, 11));
     defineType("Float32", d_solver->mkFloatingPointSort(8, 24));
     defineType("Float64", d_solver->mkFloatingPointSort(11, 53));

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 9805f602e1254baccb5b54b4a3248c07ff64c16c..87881581120a10a84399404ce2493d30bdb384ca 100644 (file)
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -23,6 +23,7 @@
 #include <string>
 
 #include "base/check.h"
+#include "base/configuration.h"
 #include "expr/kind.h"
 
 using namespace std;
@@ -43,7 +44,12 @@ LogicInfo::LogicInfo()
       d_higherOrder(true),
       d_locked(false)
 {
-  for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
+  for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id)
+  {
+    if (id == THEORY_FP && !Configuration::isBuiltWithSymFPU())
+    {
+      continue;
+    }
     enableTheory(id);
   }
 }

diff --git a/test/regress/regress1/quantifiers/issue3481-unsat1.smt2 b/test/regress/regress1/quantifiers/issue3481-unsat1.smt2
index fb7ff54857562de7f76a54507589871b618e45f3..9cf535dc7b496ea90c69ee7f8b75eb238ad1a220 100644 (file)
--- a/test/regress/regress1/quantifiers/issue3481-unsat1.smt2
+++ b/test/regress/regress1/quantifiers/issue3481-unsat1.smt2
@@ -2,7 +2,7 @@
 ; EXPECT: unsat
 
 ;; produced by cvc4_16.drv ;;
-(set-logic AUFBVFPDTNIRA)
+(set-logic AUFBVDTNIRA)
 (set-info :smt-lib-version 2.6)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part

diff --git a/test/regress/regress1/quantifiers/issue3481.smt2 b/test/regress/regress1/quantifiers/issue3481.smt2
index fe8c84d628eaf51cf41c08f42e5e4d380274b472..3d9bfe981b322c1bb7fa9c195892350c1d42cb9a 100644 (file)
--- a/test/regress/regress1/quantifiers/issue3481.smt2
+++ b/test/regress/regress1/quantifiers/issue3481.smt2
@@ -3,7 +3,7 @@
 
 ;; produced by cvc4_16.drv ;;
 (set-info :smt-lib-version 2.6)
-(set-logic AUFBVFPDTNIRA)
+(set-logic AUFBVDTNIRA)
 ;;; generated by SMT-LIB2 driver
 ;;; SMT-LIB2 driver: bit-vectors, common part
 ;;; SMT-LIB2: integer arithmetic

diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
index cd40fc8077b73495f2d2354503b3105e4f5a5847..5fdb49f48adcd78d7902bff60d958bac8165e067 100644 (file)
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -223,21 +223,31 @@ def testGetBVSize():
 
 def testGetFPExponentSize():
     solver = pycvc4.Solver()
-    fpSort = solver.mkFloatingPointSort(4, 8)
-    fpSort.getFPExponentSize()
-    setSort = solver.mkSetSort(solver.getIntegerSort())
 
-    with pytest.raises(Exception):
-        setSort.getFPExponentSize()
+    if solver.supportsFloatingPoint():
+        fpSort = solver.mkFloatingPointSort(4, 8)
+        fpSort.getFPExponentSize()
+        setSort = solver.mkSetSort(solver.getIntegerSort())
+
+        with pytest.raises(Exception):
+            setSort.getFPExponentSize()
+    else:
+        with pytest.raises(Exception):
+            solver.mkFloatingPointSort(4, 8)
 
 def testGetFPSignificandSize():
     solver = pycvc4.Solver()
-    fpSort = solver.mkFloatingPointSort(4, 8)
-    fpSort.getFPSignificandSize()
-    setSort = solver.mkSetSort(solver.getIntegerSort())
 
-    with pytest.raises(Exception):
-        setSort.getFPSignificandSize()
+    if solver.supportsFloatingPoint():
+        fpSort = solver.mkFloatingPointSort(4, 8)
+        fpSort.getFPSignificandSize()
+        setSort = solver.mkSetSort(solver.getIntegerSort())
+
+        with pytest.raises(Exception):
+            setSort.getFPSignificandSize()
+    else:
+        with pytest.raises(Exception):
+            solver.mkFloatingPointSort(4, 8)
 
 def testGetDatatypeParamSorts():
     solver = pycvc4.Solver()

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 9837d6b00db986a8bcadd3d2310e694e2a727319..11dbbb7aec88bde18ffdd26d1d24dff707e3ca43 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -27,12 +27,14 @@ class SolverBlack : public CxxTest::TestSuite
   void setUp() override;
   void tearDown() override;
 
+  void testSupportsFloatingPoint();
+
   void testGetBooleanSort();
   void testGetIntegerSort();
   void testGetNullSort();
   void testGetRealSort();
   void testGetRegExpSort();
-  void testGetRoundingmodeSort();
+  void testGetRoundingModeSort();
   void testGetStringSort();
 
   void testMkArraySort();
@@ -169,6 +171,20 @@ void SolverBlack::setUp() { d_solver.reset(new Solver()); }
 
 void SolverBlack::tearDown() { d_solver.reset(nullptr); }
 
+void SolverBlack::testSupportsFloatingPoint()
+{
+  if (d_solver->supportsFloatingPoint())
+  {
+    TS_ASSERT_THROWS_NOTHING(
+        d_solver->mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN));
+  }
+  else
+  {
+    TS_ASSERT_THROWS(d_solver->mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN),
+                     CVC4ApiException&);
+  }
+}
+
 void SolverBlack::testGetBooleanSort()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->getBooleanSort());
@@ -199,9 +215,16 @@ void SolverBlack::testGetStringSort()
   TS_ASSERT_THROWS_NOTHING(d_solver->getStringSort());
 }
 
-void SolverBlack::testGetRoundingmodeSort()
+void SolverBlack::testGetRoundingModeSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver->getRoundingmodeSort());
+  if (d_solver->supportsFloatingPoint())
+  {
+    TS_ASSERT_THROWS_NOTHING(d_solver->getRoundingModeSort());
+  }
+  else
+  {
+    TS_ASSERT_THROWS(d_solver->getRoundingModeSort(), CVC4ApiException&);
+  }
 }
 
 void SolverBlack::testMkArraySort()
@@ -210,15 +233,20 @@ void SolverBlack::testMkArraySort()
   Sort intSort = d_solver->getIntegerSort();
   Sort realSort = d_solver->getRealSort();
   Sort bvSort = d_solver->mkBitVectorSort(32);
-  Sort fpSort = d_solver->mkFloatingPointSort(3, 5);
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, boolSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(intSort, intSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, realSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, bvSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(fpSort, fpSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, intSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, bvSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, fpSort));
+
+  if (d_solver->supportsFloatingPoint())
+  {
+    Sort fpSort = d_solver->mkFloatingPointSort(3, 5);
+    TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(fpSort, fpSort));
+    TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, fpSort));
+  }
+
   Solver slv;
   TS_ASSERT_THROWS(slv.mkArraySort(boolSort, boolSort), CVC4ApiException&);
 }
@@ -231,9 +259,16 @@ void SolverBlack::testMkBitVectorSort()
 
 void SolverBlack::testMkFloatingPointSort()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPointSort(4, 8));
-  TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(0, 8), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 0), CVC4ApiException&);
+  if (d_solver->supportsFloatingPoint())
+  {
+    TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPointSort(4, 8));
+    TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(0, 8), CVC4ApiException&);
+    TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 0), CVC4ApiException&);
+  }
+  else
+  {
+    TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 8), CVC4ApiException&);
+  }
 }
 
 void SolverBlack::testMkDatatypeSort()
@@ -480,8 +515,16 @@ void SolverBlack::testMkBoolean()
 
 void SolverBlack::testMkRoundingMode()
 {
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    TS_ASSERT_THROWS_NOTHING(
+        d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
+  }
+  else
+  {
+    TS_ASSERT_THROWS(d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO),
+                     CVC4ApiException&);
+  }
 }
 
 void SolverBlack::testMkUninterpretedConst()