summaryrefslogtreecommitdiff
path: root/CMakeLists.txt
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2020-09-01 23:37:14 -0700
committerGitHub <noreply@github.com>2020-09-01 23:37:14 -0700
commit3830d80ce312e8633b9de6311b809bd9418ddd4a (patch)
treecd4e78eac884e92dfd2b1e12560166fe6e439ae6 /CMakeLists.txt
parent8ad308b23c705e73507a42d2425289e999d47f86 (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 'CMakeLists.txt')
-rw-r--r--CMakeLists.txt1
1 files changed, 1 insertions, 0 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 5b1d1e292..02933762b 100644
--- 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()
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback