[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, 7 insertions, 1 deletions

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 9805f602e..878815811 100644
--- 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);
   }
 }