[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.

1 files changed, 16 insertions, 2 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index c14bed6aa..6c39bfb91 100644
--- 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()