[API] Fix Python Examples (#4943)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 2 Sep 2020 06:37:14 +0000 (23:37 -0700)
committerGitHub <noreply@github.com>
Wed, 2 Sep 2020 06:37:14 +0000 (23:37 -0700)
commit3830d80ce312e8633b9de6311b809bd9418ddd4a
treecd4e78eac884e92dfd2b1e12560166fe6e439ae6
parent8ad308b23c705e73507a42d2425289e999d47f86
[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.
16 files changed:
CMakeLists.txt
cmake/CVC4Config.cmake.in
examples/api/python/CMakeLists.txt
examples/api/python/exceptions.py
examples/api/python/floating_point.py
examples/api/python/sygus-fun.py
src/api/cvc4cpp.cpp
src/api/cvc4cpp.h
src/api/python/cvc4.pxd
src/api/python/cvc4.pxi
src/parser/smt2/smt2.cpp
src/theory/logic_info.cpp
test/regress/regress1/quantifiers/issue3481-unsat1.smt2
test/regress/regress1/quantifiers/issue3481.smt2
test/unit/api/python/test_sort.py
test/unit/api/solver_black.h