diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-09-01 23:37:14 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-01 23:37:14 -0700 |
| commit | 3830d80ce312e8633b9de6311b809bd9418ddd4a (patch) | |
| tree | cd4e78eac884e92dfd2b1e12560166fe6e439ae6 /cmake | |
| parent | 8ad308b23c705e73507a42d2425289e999d47f86 (diff) | |
[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.
Diffstat (limited to 'cmake')
| -rw-r--r-- | cmake/CVC4Config.cmake.in | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/cmake/CVC4Config.cmake.in b/cmake/CVC4Config.cmake.in index 76535762d..7f6a80995 100644 --- 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) |