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 /examples | |
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 'examples')
-rw-r--r-- | examples/api/python/CMakeLists.txt | 15 | ||||
-rw-r--r-- | examples/api/python/exceptions.py | 34 | ||||
-rwxr-xr-x | examples/api/python/floating_point.py | 9 | ||||
-rw-r--r-- | examples/api/python/sygus-fun.py | 6 |
4 files changed, 42 insertions, 22 deletions
diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt index e3966fa2d..0da960513 100644 --- a/examples/api/python/CMakeLists.txt +++ b/examples/api/python/CMakeLists.txt @@ -1,9 +1,22 @@ set(EXAMPLES_API_PYTHON + bitvectors_and_arrays + bitvectors + combination + datatypes exceptions + extract + floating_point + helloworld + linear_arith sequences + sets + strings + sygus-fun + sygus-grammar + sygus-inv ) -find_package(PythonInterp REQUIRED) +find_package(PythonInterp ${CVC4_BINDINGS_PYTHON_VERSION} REQUIRED) # Find Python bindings in the corresponding python-*/site-packages directory. # Lookup Python module directory and store path in PYTHON_MODULE_PATH. diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py index 780f75bf7..27f068011 100644 --- a/examples/api/python/exceptions.py +++ b/examples/api/python/exceptions.py @@ -16,40 +16,40 @@ ## A simple demonstration of catching CVC4 execptions with the legacy Python ## API. -import CVC4 +import pycvc4 +from pycvc4 import kinds import sys def main(): - em = CVC4.ExprManager() - smt = CVC4.SmtEngine(em) + slv = pycvc4.Solver() - smt.setOption("produce-models", CVC4.SExpr("true")) + slv.setOption("produce-models", "true") # Setting an invalid option try: - smt.setOption("non-existing", CVC4.SExpr("true")) + slv.setOption("non-existing", "true") return 1 - except CVC4.Exception as e: - print(e.toString()) + except: + pass # Creating a term with an invalid type try: - integer = em.integerType() - x = em.mkVar("x", integer) - invalidExpr = em.mkExpr(CVC4.AND, x, x) - smt.checkSat(invalidExpr) + integer = slv.getIntegerSort() + x = slv.mkConst("x", integer) + invalidTerm = em.mkTerm(AND, x, x) + slv.checkSat(invalidTerm) return 1 - except CVC4.Exception as e: - print(e.toString()) + except: + pass # Asking for a model after unsat result try: - smt.checkSat(em.mkBoolConst(False)) - smt.getModel() + slv.checkSat(slv.mkBoolean(False)) + slv.getModel() return 1 - except CVC4.Exception as e: - print(e.toString()) + except: + pass return 0 diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index c92666c0b..6fb595e34 100755 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -20,8 +20,15 @@ from pycvc4 import kinds if __name__ == "__main__": slv = pycvc4.Solver() + + if not slv.supportsFloatingPoint(): + # CVC4 must be built with SymFPU to support the theory of + # floating-point numbers + print("CVC4 was not built with floating-point support.") + exit() + slv.setOption("produce-models", "true") - slv.setLogic("FP") + slv.setLogic("QF_FP") # single 32-bit precision fp32 = slv.mkFloatingPointSort(8, 24) diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py index 0f53bd343..25090bd8f 100644 --- a/examples/api/python/sygus-fun.py +++ b/examples/api/python/sygus-fun.py @@ -53,7 +53,7 @@ if __name__ == "__main__": leq = slv.mkTerm(kinds.Leq, start, start) # create the grammar object - g = slv.mkSygusGrammar({x, y}, {start, start_bool}) + g = slv.mkSygusGrammar([x, y], [start, start_bool]) # bind each non-terminal to its rules g.addRules(start, {zero, one, x, y, plus, minus, ite}) @@ -61,8 +61,8 @@ if __name__ == "__main__": # declare the functions-to-synthesize. Optionally, provide the grammar # constraints - max = slv.synthFun("max", {x, y}, integer, g) - min = slv.synthFun("min", {x, y}, integer) + max = slv.synthFun("max", [x, y], integer, g) + min = slv.synthFun("min", [x, y], integer) # declare universal variables. varX = slv.mkSygusVar(integer, "x") |