diff options
Diffstat (limited to 'examples/api')
-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") |