Add Python bindings using Cython -- see below for more details (#2879)

9 files changed, 762 insertions, 0 deletions

diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py
new file mode 100755
index 000000000..773974cc7
--- /dev/null
+++ b/examples/api/python/bitvectors.py
@@ -0,0 +1,121 @@
+#!/usr/bin/env python
+
+#####################
+#! \file bitvectors.py
+ ## \verbatim
+ ## Top contributors (to current version):
+ ##   Makai Mann
+ ## This file is part of the CVC4 project.
+ ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ## in the top-level source directory) and their institutional affiliations.
+ ## All rights reserved.  See the file COPYING in the top-level source
+ ## directory for licensing information.\endverbatim
+ ##
+ ## \brief A simple demonstration of the solving capabilities of the CVC4
+ ## bit-vector solver through the Python API. This is a direct translation
+ ## of bitvectors-new.cpp.
+import pycvc4
+from pycvc4 import kinds
+
+if __name__ == "__main__":
+    slv = pycvc4.Solver()
+    slv.setLogic("QF_BV") # Set the logic
+    # The following example has been adapted from the book A Hacker's Delight by
+    # Henry S. Warren.
+    #
+    # Given a variable x that can only have two values, a or b. We want to
+    # assign to x a value other than the current one. The straightforward code
+    # to do that is:
+    #
+    #(0) if (x == a ) x = b;
+    #    else x = a;
+    #
+    # Two more efficient yet equivalent methods are:
+    #
+    #(1) x = a xor b xor x;
+    #
+    #(2) x = a + b - x;
+    #
+    # We will use CVC4 to prove that the three pieces of code above are all
+    # equivalent by encoding the problem in the bit-vector theory.
+
+    # Creating a bit-vector type of width 32
+    bitvector32 = slv.mkBitVectorSort(32)
+
+    # Variables
+    x = slv.mkConst(bitvector32, "x")
+    a = slv.mkConst(bitvector32, "a")
+    b = slv.mkConst(bitvector32, "b")
+
+    # First encode the assumption that x must be equal to a or b
+    x_eq_a = slv.mkTerm(kinds.Equal, x, a)
+    x_eq_b = slv.mkTerm(kinds.Equal, x, b)
+    assumption = slv.mkTerm(kinds.Or, x_eq_a, x_eq_b)
+
+    # Assert the assumption
+    slv.assertFormula(assumption)
+
+    # Introduce a new variable for the new value of x after assignment.
+    # x after executing code (0)
+    new_x = slv.mkConst(bitvector32, "new_x")
+    # x after executing code (1) or (2)
+    new_x_ = slv.mkConst(bitvector32, "new_x_")
+
+    # Encoding code (0)
+    # new_x = x == a ? b : a
+    ite = slv.mkTerm(kinds.Ite, x_eq_a, b, a)
+    assignment0 = slv.mkTerm(kinds.Equal, new_x, ite)
+
+    # Assert the encoding of code (0)
+    print("Asserting {} to CVC4".format(assignment0))
+    slv.assertFormula(assignment0)
+    print("Pushing a new context.")
+    slv.push()
+
+    # Encoding code (1)
+    # new_x_ = a xor b xor x
+    a_xor_b_xor_x = slv.mkTerm(kinds.BVXor, a, b, x)
+    assignment1 = slv.mkTerm(kinds.Equal, new_x_, a_xor_b_xor_x)
+
+    # Assert encoding to CVC4 in current context
+    print("Asserting {} to CVC4".format(assignment1))
+    slv.assertFormula(assignment1)
+    new_x_eq_new_x_ = slv.mkTerm(kinds.Equal, new_x, new_x_)
+
+    print("Checking validity assuming:", new_x_eq_new_x_)
+    print("Expect valid.")
+    print("CVC4:", slv.checkValidAssuming(new_x_eq_new_x_))
+    print("Popping context.")
+    slv.pop()
+
+    # Encoding code (2)
+    # new_x_ = a + b - x
+    a_plus_b = slv.mkTerm(kinds.BVPlus, a, b)
+    a_plus_b_minus_x = slv.mkTerm(kinds.BVSub, a_plus_b, x)
+    assignment2 = slv.mkTerm(kinds.Equal, new_x_, a_plus_b_minus_x)
+
+    # Assert encoding to CVC4 in current context
+    print("Asserting {} to CVC4".format(assignment2))
+    slv.assertFormula(assignment2)
+
+    print("Checking validity assuming:", new_x_eq_new_x_)
+    print("Expect valid.")
+    print("CVC4:", slv.checkValidAssuming(new_x_eq_new_x_))
+
+
+    x_neq_x = slv.mkTerm(kinds.Equal, x, x).notTerm()
+    v = [new_x_eq_new_x_, x_neq_x]
+    print("Check Validity Assuming: ", v)
+    print("Expect invalid.")
+    print("CVC4:", slv.checkValidAssuming(v))
+
+    # Assert that a is odd
+    extract_op = slv.mkOp(kinds.BVExtract, 0, 0)
+    lsb_of_a = slv.mkTerm(extract_op, a)
+    print("Sort of {} is {}".format(lsb_of_a, lsb_of_a.getSort()))
+    a_odd = slv.mkTerm(kinds.Equal, lsb_of_a, slv.mkBitVector(1, 1))
+    print("Assert", a_odd)
+    print("Check satisifiability")
+    slv.assertFormula(a_odd)
+    print("Expect sat")
+    print("CVC4:", slv.checkSat())
diff --git a/examples/api/python/bitvectors_and_arrays.py b/examples/api/python/bitvectors_and_arrays.py
new file mode 100755
index 000000000..7e3d8f478
--- /dev/null
+++ b/examples/api/python/bitvectors_and_arrays.py
@@ -0,0 +1,91 @@
+#!/usr/bin/env python
+
+#####################
+#! \file bitvectors_and_arrays.py
+ ## \verbatim
+ ## Top contributors (to current version):
+ ##   Makai Mann
+ ## This file is part of the CVC4 project.
+ ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ## in the top-level source directory) and their institutional affiliations.
+ ## All rights reserved.  See the file COPYING in the top-level source
+ ## directory for licensing information.\endverbatim
+ ##
+ ## \brief A simple demonstration of the solving capabilities of the CVC4
+ ## bit-vector and array solvers through the Python API. This is a direct
+ ## translation of bitvectors_and_arrays-new.cpp.
+import pycvc4
+from pycvc4 import kinds
+
+import math
+
+if __name__ == "__main__":
+    slv = pycvc4.Solver()
+    slv.setOption("produce-models", "true")
+    slv.setOption("output-language", "smtlib")
+    slv.setLogic("QF_AUFBV")
+
+    # Consider the following code (where size is some previously defined constant):
+    #
+    #
+    #   Assert (current_array[0] > 0);
+    #   for (unsigned i = 1; i < k; ++i) {
+    #     current_array[i] = 2 * current_array[i - 1];
+    #     Assert (current_array[i-1] < current_array[i]);
+    #     }
+    #
+    # We want to check whether the assertion in the body of the for loop holds
+    # throughout the loop.
+
+    # Setting up the problem parameters
+    k = 4
+    index_size = int(math.ceil(math.log(k, 2)))
+
+    # Sorts
+    elementSort = slv.mkBitVectorSort(32)
+    indexSort = slv.mkBitVectorSort(index_size)
+    arraySort = slv.mkArraySort(indexSort, elementSort)
+
+    # Variables
+    current_array = slv.mkConst(arraySort, "current_array")
+
+    # Making a bit-vector constant
+    zero = slv.mkBitVector(index_size, 0)
+
+    # Test making a constant array
+    constarr0 = slv.mkConstArray(arraySort, slv.mkBitVector(32, 0))
+
+    # Asserting that current_array[0] > 0
+    current_array0 = slv.mkTerm(kinds.Select, current_array, zero)
+    current_array0_gt_0 = slv.mkTerm(kinds.BVSgt,
+                                     current_array0,
+                                     slv.mkBitVector(32, 0))
+    slv.assertFormula(current_array0_gt_0)
+
+    # Building the assertions in the loop unrolling
+    index = slv.mkBitVector(index_size, 0)
+    old_current = slv.mkTerm(kinds.Select, current_array, index)
+    two = slv.mkBitVector(32, 2)
+
+    assertions = []
+    for i in range(1, k):
+        index = slv.mkBitVector(index_size, i)
+        new_current = slv.mkTerm(kinds.BVMult, two, old_current)
+        # current[i] = 2*current[i-1]
+        current_array = slv.mkTerm(kinds.Store, current_array, index, new_current)
+        # current[i-1] < current[i]
+        current_slt_new_current = slv.mkTerm(kinds.BVSlt, old_current, new_current)
+        assertions.append(current_slt_new_current)
+        old_current = slv.mkTerm(kinds.Select, current_array, index)
+
+    query = slv.mkTerm(kinds.Not, slv.mkTerm(kinds.And, assertions))
+
+    print("Asserting {} to CVC4".format(query))
+    slv.assertFormula(query)
+    print("Expect sat.")
+    print("CVC4:", slv.checkSatAssuming(slv.mkTrue()))
+
+    # Getting the model
+    print("The satisfying model is: ")
+    print(" current_array =", slv.getValue(current_array))
+    print(" current_array[0]", slv.getValue(current_array0))
diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
new file mode 100755
index 000000000..1b488d7d5
--- /dev/null
+++ b/examples/api/python/combination.py
@@ -0,0 +1,99 @@
+#!/usr/bin/env python
+
+#####################
+#! \file combination.py
+ ## \verbatim
+ ## Top contributors (to current version):
+ ##   Makai Mann
+ ## This file is part of the CVC4 project.
+ ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ## in the top-level source directory) and their institutional affiliations.
+ ## All rights reserved.  See the file COPYING in the top-level source
+ ## directory for licensing information.\endverbatim
+ ##
+ ## \brief A simple demonstration of the solving capabilities of the CVC4
+ ## combination solver through the Python API. This is a direct translation
+ ## of combination-new.cpp.
+import pycvc4
+from pycvc4 import kinds
+
+def prefixPrintGetValue(slv, t, level=0):
+    print("slv.getValue({}): {}".format(t, slv.getValue(t)))
+    for c in t:
+        prefixPrintGetValue(slv, c, level + 1)
+
+if __name__ == "__main__":
+    slv = pycvc4.Solver()
+    slv.setOption("produce-models", "true")  # Produce Models
+    slv.setOption("output-language", "cvc4") # Set the output-language to CVC's
+    slv.setOption("default-dag-thresh", "0") # Disable dagifying the output
+    slv.setOption("output-language", "smt2") # use smt-lib v2 as output language
+    slv.setLogic("QF_UFLIRA")
+
+    # Sorts
+    u = slv.mkUninterpretedSort("u")
+    integer = slv.getIntegerSort()
+    boolean = slv.getBooleanSort()
+    uToInt = slv.mkFunctionSort(u, integer)
+    intPred = slv.mkFunctionSort(integer, boolean)
+
+    # Variables
+    x = slv.mkConst(u, "x")
+    y = slv.mkConst(u, "y")
+
+    # Functions
+    f = slv.mkConst(uToInt, "f")
+    p = slv.mkConst(intPred, "p")
+
+    # Constants
+    zero = slv.mkReal(0)
+    one = slv.mkReal(1)
+
+    # Terms
+    f_x = slv.mkTerm(kinds.ApplyUf, f, x)
+    f_y = slv.mkTerm(kinds.ApplyUf, f, y)
+    sum_ = slv.mkTerm(kinds.Plus, f_x, f_y)
+    p_0 = slv.mkTerm(kinds.ApplyUf, p, zero)
+    p_f_y = slv.mkTerm(kinds.ApplyUf, p, f_y)
+
+    # Construct the assertions
+    assertions = slv.mkTerm(kinds.And,
+                            [
+                                slv.mkTerm(kinds.Leq, zero, f_x), # 0 <= f(x)
+                                slv.mkTerm(kinds.Leq, zero, f_y), # 0 <= f(y)
+                                slv.mkTerm(kinds.Leq, sum_, one), # f(x) + f(y) <= 1
+                                p_0.notTerm(), # not p(0)
+                                p_f_y # p(f(y))
+                            ])
+
+    slv.assertFormula(assertions)
+
+    print("Given the following assertions:", assertions, "\n")
+    print("Prove x /= y is valid.\nCVC4: ",
+          slv.checkValidAssuming(slv.mkTerm(kinds.Distinct, x, y)), "\n")
+
+    print("Call checkSat to show that the assertions are satisfiable")
+    print("CVC4:", slv.checkSat(), "\n")
+
+    print("Call slv.getValue(...) on terms of interest")
+    print("slv.getValue({}): {}".format(f_x, slv.getValue(f_x)))
+    print("slv.getValue({}): {}".format(f_y, slv.getValue(f_y)))
+    print("slv.getValue({}): {}".format(sum_, slv.getValue(sum_)))
+    print("slv.getValue({}): {}".format(p_0, slv.getValue(p_0)))
+    print("slv.getValue({}): {}".format(p_f_y, slv.getValue(p_f_y)), "\n")
+
+    print("Alternatively, iterate over assertions and call"
+          " slv.getValue(...) on all terms")
+    prefixPrintGetValue(slv, assertions)
+
+    print("Alternatively, print the model", "\n")
+    slv.printModel()
+
+    print()
+    print("You can also use nested loops to iterate over terms")
+    for a in assertions:
+        print("term:", a)
+        for t in a:
+            print(" + child: ", t)
+
+    print()
diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
new file mode 100755
index 000000000..c5eda1741
--- /dev/null
+++ b/examples/api/python/datatypes.py
@@ -0,0 +1,137 @@
+#!/usr/bin/env python
+
+#####################
+#! \file datatypes.py
+ ## \verbatim
+ ## Top contributors (to current version):
+ ##   Makai Mann
+ ## This file is part of the CVC4 project.
+ ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ## in the top-level source directory) and their institutional affiliations.
+ ## All rights reserved.  See the file COPYING in the top-level source
+ ## directory for licensing information.\endverbatim
+ ##
+ ## \brief A simple demonstration of the solving capabilities of the CVC4
+ ## datatypes solver through the Python API. This is a direct translation
+ ## of datatypes-new.cpp.
+
+import pycvc4
+from pycvc4 import kinds
+
+def test(slv, consListSort):
+    # Now our old "consListSpec" is useless--the relevant information
+    # has been copied out, so we can throw that spec away.  We can get
+    # the complete spec for the datatype from the DatatypeSort, and
+    # this Datatype object has constructor symbols (and others) filled in.
+
+    consList = consListSort.getDatatype()
+
+    # t = cons 0 nil
+    #
+    # Here, consList["cons"] gives you the DatatypeConstructor.  To get
+    # the constructor symbol for application, use .getConstructor("cons"),
+    # which is equivalent to consList["cons"].getConstructor().  Note that
+    # "nil" is a constructor too
+
+    t = slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("cons"),
+                   slv.mkReal(0),
+                   slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("nil")))
+
+    print("t is {}\nsort of cons is {}\n sort of nil is {}".format(
+        t,
+        consList.getConstructorTerm("cons").getSort(),
+        consList.getConstructorTerm("nil").getSort()))
+
+    # t2 = head(cons 0 nil), and of course this can be evaluated
+    #
+    # Here we first get the DatatypeConstructor for cons (with
+    # consList["cons"]) in order to get the "head" selector symbol
+    # to apply.
+
+    t2 = slv.mkTerm(kinds.ApplySelector, consList["cons"].getSelectorTerm("head"), t)
+
+    print("t2 is {}\nsimplify(t2) is {}\n\n".format(t2, slv.simplify(t2)))
+
+    # You can also iterate over a Datatype to get all its constructors,
+    # and over a DatatypeConstructor to get all its "args" (selectors)
+    for i in consList:
+        print("ctor:", i)
+        for j in i:
+            print(" + args:", j)
+        print()
+
+    # You can also define parameterized datatypes.
+    # This example builds a simple parameterized list of sort T, with one
+    # constructor "cons".
+    sort = slv.mkParamSort("T")
+    paramConsListSpec = slv.mkDatatypeDecl("paramlist", sort)
+    paramCons = pycvc4.DatatypeConstructorDecl("cons")
+    paramNil = pycvc4.DatatypeConstructorDecl("nil")
+    paramHead = pycvc4.DatatypeSelectorDecl("head", sort)
+    paramTail = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort())
+    paramCons.addSelector(paramHead)
+    paramCons.addSelector(paramTail)
+    paramConsListSpec.addConstructor(paramCons)
+    paramConsListSpec.addConstructor(paramNil)
+
+    paramConsListSort = slv.mkDatatypeSort(paramConsListSpec)
+    paramConsIntListSort = paramConsListSort.instantiate([slv.getIntegerSort()])
+    paramConsList = paramConsListSort.getDatatype()
+
+    a = slv.mkConst(paramConsIntListSort, "a")
+    print("term {} is of sort {}".format(a, a.getSort()))
+
+    head_a = slv.mkTerm(kinds.ApplySelector, paramConsList["cons"].getSelectorTerm("head"), a)
+    print("head_a is {} of sort {}".format(head_a, head_a.getSort()))
+    print("sort of cons is", paramConsList.getConstructorTerm("cons").getSort())
+
+    assertion = slv.mkTerm(kinds.Gt, head_a, slv.mkReal(50))
+    print("Assert", assertion)
+    slv.assertFormula(assertion)
+    print("Expect sat.")
+    print("CVC4:", slv.checkSat())
+
+
+if __name__ == "__main__":
+    slv = pycvc4.Solver()
+
+    # This example builds a simple "cons list" of integers, with
+    # two constructors, "cons" and "nil."
+
+    # Building a datatype consists of two steps.
+    # First, the datatype is specified.
+    # Second, it is "resolved" to an actual sort, at which point function
+    # symbols are assigned to its constructors, selectors, and testers.
+
+    consListSpec = slv.mkDatatypeDecl("list") # give the datatype a name
+    cons = pycvc4.DatatypeConstructorDecl("cons")
+    head = pycvc4.DatatypeSelectorDecl("head", slv.getIntegerSort())
+    tail = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort())
+    cons.addSelector(head)
+    cons.addSelector(tail)
+    consListSpec.addConstructor(cons)
+    nil = pycvc4.DatatypeConstructorDecl("nil")
+    consListSpec.addConstructor(nil)
+
+    print("spec is {}".format(consListSpec))
+
+    # Keep in mind that "DatatypeDecl" is the specification class for
+    # datatypes---"DatatypeDecl" is not itself a CVC4 Sort.
+    # Now that our Datatype is fully specified, we can get a Sort for it.
+    # This step resolves the "SelfSort" reference and creates
+    # symbols for all the constructors, etc.
+
+    consListSort = slv.mkDatatypeSort(consListSpec)
+    test(slv, consListSort)
+
+    print("### Alternatively, use declareDatatype")
+
+    cons2 = pycvc4.DatatypeConstructorDecl("cons")
+    head2 = pycvc4.DatatypeSelectorDecl("head", slv.getIntegerSort())
+    tail2 = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort())
+    cons2.addSelector(head2)
+    cons2.addSelector(tail2)
+    nil2 = pycvc4.DatatypeConstructorDecl("nil")
+    ctors = [cons2, nil2]
+    consListSort2 = slv.declareDatatype("list2", ctors)
+    test(slv, consListSort2)
diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py
new file mode 100755
index 000000000..1bfdf652a
--- /dev/null
+++ b/examples/api/python/extract.py
@@ -0,0 +1,51 @@
+#!/usr/bin/env python
+
+#####################
+#! \file extract.py
+ ## \verbatim
+ ## Top contributors (to current version):
+ ##   Makai Mann
+ ## This file is part of the CVC4 project.
+ ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ## in the top-level source directory) and their institutional affiliations.
+ ## All rights reserved.  See the file COPYING in the top-level source
+ ## directory for licensing information.\endverbatim
+ ##
+ ## \brief A simple demonstration of the solving capabilities of the CVC4
+ ## bit-vector solver through the Python API. This is a direct translation
+ ## of extract-new.cpp.
+
+from pycvc4 import Solver
+from pycvc4.kinds import BVExtract, Equal
+
+if __name__ == "__main__":
+    slv = Solver()
+    slv.setLogic("QF_BV")
+
+    bitvector32 = slv.mkBitVectorSort(32)
+
+    x = slv.mkConst(bitvector32, "a")
+
+    ext_31_1 = slv.mkOp(BVExtract, 31, 1)
+    x_31_1 = slv.mkTerm(ext_31_1, x)
+
+    ext_30_0 = slv.mkOp(BVExtract, 30, 0)
+    x_30_0 = slv.mkTerm(ext_30_0, x)
+
+    ext_31_31 = slv.mkOp(BVExtract, 31, 31)
+    x_31_31 = slv.mkTerm(ext_31_31, x)
+
+    ext_0_0 = slv.mkOp(BVExtract, 0, 0)
+    x_0_0 = slv.mkTerm(ext_0_0, x)
+
+    # test getting indices
+    assert ext_30_0.getIndices() == (30, 0)
+
+    eq = slv.mkTerm(Equal, x_31_1, x_30_0)
+    print("Asserting:", eq)
+    slv.assertFormula(eq)
+
+    eq2 = slv.mkTerm(Equal, x_31_31, x_0_0)
+    print("Check validity assuming:", eq2)
+    print("Expect valid")
+    print("CVC4:", slv.checkValidAssuming(eq2))
diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py
new file mode 100755
index 000000000..472cf945b
--- /dev/null
+++ b/examples/api/python/helloworld.py
@@ -0,0 +1,21 @@
+#!/usr/bin/env python
+
+#####################
+#! \file helloworld.py
+## \verbatim
+## Top contributors (to current version):
+##   Makai Mann
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+## in the top-level source directory) and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.\endverbatim
+##
+## \brief A very simple CVC4 tutorial example, adapted from helloworld-new.cpp
+import pycvc4
+from pycvc4 import kinds
+
+if __name__ == "__main__":
+    slv = pycvc4.Solver()
+    helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!")
+    print(helloworld, "is", slv.checkValidAssuming(helloworld))
diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py
new file mode 100755
index 000000000..6ae6427b1
--- /dev/null
+++ b/examples/api/python/linear_arith.py
@@ -0,0 +1,70 @@
+#!/usr/bin/env python
+
+#####################
+#! \file linear_arith.py
+## \verbatim
+## Top contributors (to current version):
+##   Makai Mann
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+## in the top-level source directory) and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.\endverbatim
+##
+## \brief A simple demonstration of the solving capabilities of the CVC4
+## linear arithmetic solver through the Python API. This is a direct
+## translation of linear_arith-new.cpp.
+import pycvc4
+from pycvc4 import kinds
+
+if __name__ == "__main__":
+    slv = pycvc4.Solver()
+    slv.setLogic("QF_LIRA")
+
+    # Prove that if given x (Integer) and y (Real) and some constraints
+    # then the maximum value of y - x is 2/3
+
+    # Sorts
+    real = slv.getRealSort()
+    integer = slv.getIntegerSort()
+
+    # Variables
+    x = slv.mkConst(integer, "x")
+    y = slv.mkConst(real, "y")
+
+    # Constants
+    three = slv.mkReal(3)
+    neg2 = slv.mkReal(-2)
+    two_thirds = slv.mkReal(2, 3)
+
+    # Terms
+    three_y = slv.mkTerm(kinds.Mult, three, y)
+    diff = slv.mkTerm(kinds.Minus, y, x)
+
+    # Formulas
+    x_geq_3y = slv.mkTerm(kinds.Geq, x, three_y)
+    x_leq_y = slv.mkTerm(kinds.Leq, x ,y)
+    neg2_lt_x = slv.mkTerm(kinds.Lt, neg2, x)
+
+    assertions = slv.mkTerm(kinds.And, x_geq_3y, x_leq_y, neg2_lt_x)
+
+    print("Given the assertions", assertions)
+    slv.assertFormula(assertions)
+
+    slv.push()
+    diff_leq_two_thirds = slv.mkTerm(kinds.Leq, diff, two_thirds)
+    print("Prove that", diff_leq_two_thirds, "with CVC4")
+    print("CVC4 should report VALID")
+    print("Result from CVC4 is:",
+          slv.checkValidAssuming(diff_leq_two_thirds))
+    slv.pop()
+
+    print()
+
+    slv.push()
+    diff_is_two_thirds = slv.mkTerm(kinds.Equal, diff, two_thirds)
+    slv.assertFormula(diff_is_two_thirds)
+    print("Show that the assertions are consistent with\n", diff_is_two_thirds, "with CVC4")
+    print("CVC4 should report SAT")
+    print("Result from CVC4 is:", slv.checkSat())
+    slv.pop()
diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py
new file mode 100755
index 000000000..584880b2b
--- /dev/null
+++ b/examples/api/python/sets.py
@@ -0,0 +1,85 @@
+#!/usr/bin/env python
+
+#####################
+#! \file sets.py
+## \verbatim
+## Top contributors (to current version):
+##   Makai Mann
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+## in the top-level source directory) and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.\endverbatim
+##
+## \brief A simple demonstration of the solving capabilities of the CVC4
+## sets solver through the Python API. This is a direct translation
+## of sets-new.cpp.
+import pycvc4
+from pycvc4 import kinds
+
+if __name__ == "__main__":
+    slv = pycvc4.Solver()
+
+    # Optionally, set the logic. We need at least UF for equality predicate,
+    # integers (LIA) and sets (FS).
+    slv.setLogic("QF_UFLIAFS")
+
+    # Produce models
+    slv.setOption("produce-models", "true")
+    slv.setOption("output-language", "smt2")
+
+    integer = slv.getIntegerSort()
+    set_ = slv.mkSetSort(integer)
+
+    # Verify union distributions over intersection
+    # (A union B) intersection C = (A intersection C) union (B intersection C)
+
+    A = slv.mkConst(set_, "A")
+    B = slv.mkConst(set_, "B")
+    C = slv.mkConst(set_, "C")
+
+    unionAB = slv.mkTerm(kinds.Union, A, B)
+    lhs = slv.mkTerm(kinds.Intersection, unionAB, C)
+
+    intersectionAC = slv.mkTerm(kinds.Intersection, A, C)
+    intersectionBC = slv.mkTerm(kinds.Intersection, B, C)
+    rhs = slv.mkTerm(kinds.Union, intersectionAC, intersectionBC)
+
+    theorem = slv.mkTerm(kinds.Equal, lhs, rhs)
+
+    print("CVC4 reports: {} is {}".format(theorem,
+                                          slv.checkValidAssuming(theorem)))
+
+    # Verify emptset is a subset of any set
+
+    A = slv.mkConst(set_, "A")
+    emptyset = slv.mkEmptySet(set_)
+
+    theorem = slv.mkTerm(kinds.Subset, emptyset, A)
+
+    print("CVC4 reports: {} is {}".format(theorem,
+                                          slv.checkValidAssuming(theorem)))
+
+    # Find me an element in 1, 2 intersection 2, 3, if there is one.
+
+    one = slv.mkReal(1)
+    two = slv.mkReal(2)
+    three = slv.mkReal(3)
+
+    singleton_one = slv.mkTerm(kinds.Singleton, one)
+    singleton_two = slv.mkTerm(kinds.Singleton, two)
+    singleton_three = slv.mkTerm(kinds.Singleton, three)
+    one_two = slv.mkTerm(kinds.Union, singleton_one, singleton_two)
+    two_three = slv.mkTerm(kinds.Union, singleton_two, singleton_three)
+    intersection = slv.mkTerm(kinds.Intersection, one_two, two_three)
+
+    x = slv.mkConst(integer, "x")
+
+    e = slv.mkTerm(kinds.Member, x, intersection)
+
+    result = slv.checkSatAssuming(e)
+
+    print("CVC4 reports: {} is {}".format(e, result))
+
+    if result:
+        print("For instance, {} is a member".format(slv.getValue(x)))
diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py
new file mode 100755
index 000000000..5c8e91997
--- /dev/null
+++ b/examples/api/python/strings.py
@@ -0,0 +1,87 @@
+#!/usr/bin/env python
+
+#####################
+#! \file strings.py
+## \verbatim
+## Top contributors (to current version):
+##   Makai Mann
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+## in the top-level source directory) and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.\endverbatim
+##
+## \brief A simple demonstration of the solving capabilities of the CVC4
+## strings solver through the Python API. This is a direct translation
+## of strings-new.cpp.
+import pycvc4
+from pycvc4 import kinds
+
+if __name__ == "__main__":
+    slv = pycvc4.Solver()
+    # Set the logic
+    slv.setLogic("S")
+    # Produce models
+    slv.setOption("produce-models", "true")
+    # The option strings-exp is needed
+    slv.setOption("strings-exp", "true")
+    # Set output language to SMTLIB2
+    slv.setOption("output-language", "smt2")
+
+    # String type
+    string = slv.getStringSort()
+
+    # std::string
+    str_ab = "ab"
+    # String constants
+    ab  = slv.mkString(str_ab)
+    abc = slv.mkString("abc")
+    # String variables
+    x = slv.mkConst(string, "x")
+    y = slv.mkConst(string, "y")
+    z = slv.mkConst(string, "z")
+
+    # String concatenation: x.ab.y
+    lhs = slv.mkTerm(kinds.StringConcat, x, ab, y)
+    # String concatenation: abc.z
+    rhs = slv.mkTerm(kinds.StringConcat, abc, z)
+    # x.ab.y = abc.z
+    formula1 = slv.mkTerm(kinds.Equal, lhs, rhs)
+
+    # Length of y: |y|
+    leny = slv.mkTerm(kinds.StringLength, y)
+    # |y| >= 0
+    formula2 = slv.mkTerm(kinds.Geq, leny, slv.mkReal(0))
+
+    # Regular expression: (ab[c-e]*f)|g|h
+    r = slv.mkTerm(kinds.RegexpUnion,
+                   slv.mkTerm(kinds.RegexpConcat,
+                              slv.mkTerm(kinds.StringToRegexp, slv.mkString("ab")),
+                              slv.mkTerm(kinds.RegexpStar,
+                                         slv.mkTerm(kinds.RegexpRange, slv.mkString("c"), slv.mkString("e"))),
+                            slv.mkTerm(kinds.StringToRegexp, slv.mkString("f"))),
+                 slv.mkTerm(kinds.StringToRegexp, slv.mkString("g")),
+                 slv.mkTerm(kinds.StringToRegexp, slv.mkString("h")))
+
+    # String variables
+    s1 = slv.mkConst(string, "s1")
+    s2 = slv.mkConst(string, "s2")
+    # String concatenation: s1.s2
+    s = slv.mkTerm(kinds.StringConcat, s1, s2)
+
+    # s1.s2 in (ab[c-e]*f)|g|h
+    formula3 = slv.mkTerm(kinds.StringInRegexp, s, r)
+
+    # Make a query
+    q = slv.mkTerm(kinds.And,
+                   formula1,
+                   formula2,
+                   formula3)
+
+    # check sat
+    result = slv.checkSatAssuming(q)
+    print("CVC4 reports:", q, "is", result)
+
+    if result:
+        print("x = ", slv.getValue(x))
+        print(" s1.s2 =", slv.getValue(s))