Merge branch 'master' into fixCMSBuildPRfixCMSBuildPR

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")