Adding functions to the python API and testing them (#6477)

This PR adds some functions that are missing in the python API, along with unit tests for them.
Subsequent PR will include additional missing functions.

Also includes a yapf run to reformat the test file.

Co-authored-by: Makai Mann makaim@stanford.edu

3 files changed, 930 insertions, 746 deletions

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index e4c0eb915..b91a9e9c5 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -102,6 +102,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Kind getKind() except +
         Sort getSort() except +
         bint isNull() except +
+        bint isIndexed() except +
         T getIndices[T]() except +
         string toString() except +
 
@@ -182,6 +183,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term mkFalse() except +
         Term mkBoolean(bint val) except +
         Term mkPi() except +
+        Term mkInteger(const uint64_t i) except +
         Term mkInteger(const string& s) except +
         Term mkReal(const string& s) except +
         Term mkRegexpEmpty() except +
@@ -340,9 +342,10 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint operator==(const Term&) except +
         bint operator!=(const Term&) except +
         Term operator[](size_t idx) except +
+        uint64_t getId() except +
         Kind getKind() except +
         Sort getSort() except +
-        Term substitute(const vector[Term] es, const vector[Term] & reps) except +
+        Term substitute(const vector[Term] & es, const vector[Term] & reps) except +
         bint hasOp() except +
         Op getOp() except +
         bint isNull() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 11742ca08..f38a953ee 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -314,6 +314,9 @@ cdef class Op:
 
     def getKind(self):
         return kind(<int> self.cop.getKind())
+    
+    def isIndexed(self):
+        return self.cop.isIndexed()
 
     def isNull(self):
         return self.cop.isNull()
@@ -692,8 +695,11 @@ cdef class Solver:
 
     def mkInteger(self, val):
         cdef Term term = Term(self)
-        integer = int(val)
-        term.cterm = self.csolver.mkInteger("{}".format(integer).encode())
+        if isinstance(val, str):
+            term.cterm = self.csolver.mkInteger(<const string &> str(val).encode())
+        else:
+            assert(isinstance(val, int))
+            term.cterm = self.csolver.mkInteger((<int?> val))
         return term
 
     def mkReal(self, val, den=None):
@@ -1477,6 +1483,10 @@ cdef class Term:
     def __hash__(self):
         return ctermhash(self.cterm)
 
+
+    def getId(self):
+        return self.cterm.getId()
+
     def getKind(self):
         return kind(<int> self.cterm.getKind())
 
@@ -1485,20 +1495,33 @@ cdef class Term:
         sort.csort = self.cterm.getSort()
         return sort
 
-    def substitute(self, list es, list replacements):
+    def substitute(self, term_or_list_1, term_or_list_2):
+        # The resulting term after substitution
+        cdef Term term = Term(self.solver)
+        # lists for substitutions
         cdef vector[c_Term] ces
         cdef vector[c_Term] creplacements
-        cdef Term term = Term(self.solver)
-
-        if len(es) != len(replacements):
-            raise RuntimeError("Expecting list inputs to substitute to "
-                               "have the same length but got: "
-                               "{} and {}".format(len(es), len(replacements)))
-
-        for e, r in zip(es, replacements):
-            ces.push_back((<Term?> e).cterm)
-            creplacements.push_back((<Term?> r).cterm)
+        
+        # normalize the input parameters to be lists
+        if isinstance(term_or_list_1, list):
+            assert isinstance(term_or_list_2, list)
+            es = term_or_list_1
+            replacements = term_or_list_2
+            if len(es) != len(replacements):
+                raise RuntimeError("Expecting list inputs to substitute to "
+                                   "have the same length but got: "
+                                   "{} and {}".format(len(es), len(replacements)))
+
+            for e, r in zip(es, replacements):
+                ces.push_back((<Term?> e).cterm)
+                creplacements.push_back((<Term?> r).cterm)
 
+        else:
+            # add the single elements to the vectors
+            ces.push_back((<Term?> term_or_list_1).cterm)
+            creplacements.push_back((<Term?> term_or_list_2).cterm)
+        
+        # call the API substitute method with lists
         term.cterm = self.cterm.substitute(ces, creplacements)
         return term
 
diff --git a/test/python/unit/api/test_term.py b/test/python/unit/api/test_term.py
index ea4ec2427..91424c905 100644
--- a/test/python/unit/api/test_term.py
+++ b/test/python/unit/api/test_term.py
@@ -11,776 +11,934 @@
 # #############################################################################
 ##
 
-
-
 import pytest
 import pycvc5
 from pycvc5 import kinds
 from pycvc5 import Sort, Term
 
+
 @pytest.fixture
 def solver():
     return pycvc5.Solver()
 
 
 def test_eq(solver):
-  uSort = solver.mkUninterpretedSort("u")
-  x = solver.mkVar(uSort, "x")
-  y = solver.mkVar(uSort, "y")
-  z = Term(solver)
-
-  assert x == x
-  assert not x != x
-  assert not x == y
-  assert x != y
-  assert not (x == z)
-  assert x != z
+    uSort = solver.mkUninterpretedSort("u")
+    x = solver.mkVar(uSort, "x")
+    y = solver.mkVar(uSort, "y")
+    z = Term(solver)
+
+    assert x == x
+    assert not x != x
+    assert not x == y
+    assert x != y
+    assert not (x == z)
+    assert x != z
+
+
+def test_get_id(solver):
+    n = Term(solver)
+    with pytest.raises(RuntimeError):
+        n.getId()
+    x = solver.mkVar(solver.getIntegerSort(), "x")
+    x.getId()
+    y = x
+    assert x.getId() == y.getId()
+
+    z = solver.mkVar(solver.getIntegerSort(), "z")
+    assert x.getId() != z.getId()
+
 
 def test_get_kind(solver):
-  uSort = solver.mkUninterpretedSort("u")
-  intSort = solver.getIntegerSort()
-  boolSort = solver.getBooleanSort()
-  funSort1 = solver.mkFunctionSort(uSort, intSort)
-  funSort2 = solver.mkFunctionSort(intSort, boolSort)
-
-  n = Term(solver)
-  with pytest.raises(RuntimeError):
-      n.getKind()
-  x = solver.mkVar(uSort, "x")
-  x.getKind()
-  y = solver.mkVar(uSort, "y")
-  y.getKind()
-
-  f = solver.mkVar(funSort1, "f")
-  f.getKind()
-  p = solver.mkVar(funSort2, "p")
-  p.getKind()
-
-  zero = solver.mkInteger(0)
-  zero.getKind()
-
-  f_x = solver.mkTerm(kinds.ApplyUf, f, x)
-  f_x.getKind()
-  f_y = solver.mkTerm(kinds.ApplyUf, f, y)
-  f_y.getKind()
-  sum = solver.mkTerm(kinds.Plus, f_x, f_y)
-  sum.getKind()
-  p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
-  p_0.getKind()
-  p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y)
-  p_f_y.getKind()
-
-  # Sequence kinds do not exist internally, test that the API properly
-  # converts them back.
-  seqSort = solver.mkSequenceSort(intSort)
-  s = solver.mkConst(seqSort, "s")
-  ss = solver.mkTerm(kinds.SeqConcat, s, s)
-  assert ss.getKind() == kinds.SeqConcat
+    uSort = solver.mkUninterpretedSort("u")
+    intSort = solver.getIntegerSort()
+    boolSort = solver.getBooleanSort()
+    funSort1 = solver.mkFunctionSort(uSort, intSort)
+    funSort2 = solver.mkFunctionSort(intSort, boolSort)
+
+    n = Term(solver)
+    with pytest.raises(RuntimeError):
+        n.getKind()
+    x = solver.mkVar(uSort, "x")
+    x.getKind()
+    y = solver.mkVar(uSort, "y")
+    y.getKind()
+
+    f = solver.mkVar(funSort1, "f")
+    f.getKind()
+    p = solver.mkVar(funSort2, "p")
+    p.getKind()
+
+    zero = solver.mkInteger(0)
+    zero.getKind()
+
+    f_x = solver.mkTerm(kinds.ApplyUf, f, x)
+    f_x.getKind()
+    f_y = solver.mkTerm(kinds.ApplyUf, f, y)
+    f_y.getKind()
+    sum = solver.mkTerm(kinds.Plus, f_x, f_y)
+    sum.getKind()
+    p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
+    p_0.getKind()
+    p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y)
+    p_f_y.getKind()
+
+    # Sequence kinds do not exist internally, test that the API properly
+    # converts them back.
+    seqSort = solver.mkSequenceSort(intSort)
+    s = solver.mkConst(seqSort, "s")
+    ss = solver.mkTerm(kinds.SeqConcat, s, s)
+    assert ss.getKind() == kinds.SeqConcat
+
 
 def test_get_sort(solver):
-  bvSort = solver.mkBitVectorSort(8)
-  intSort = solver.getIntegerSort()
-  boolSort = solver.getBooleanSort()
-  funSort1 = solver.mkFunctionSort(bvSort, intSort)
-  funSort2 = solver.mkFunctionSort(intSort, boolSort)
-
-  n = Term(solver)
-  with pytest.raises(RuntimeError):
-      n.getSort()
-  x = solver.mkVar(bvSort, "x")
-  x.getSort()
-  assert x.getSort() == bvSort
-  y = solver.mkVar(bvSort, "y")
-  y.getSort()
-  assert y.getSort() == bvSort
-
-  f = solver.mkVar(funSort1, "f")
-  f.getSort()
-  assert f.getSort() == funSort1
-  p = solver.mkVar(funSort2, "p")
-  p.getSort()
-  assert p.getSort() == funSort2
-
-  zero = solver.mkInteger(0)
-  zero.getSort()
-  assert zero.getSort() == intSort
-
-  f_x = solver.mkTerm(kinds.ApplyUf, f, x)
-  f_x.getSort()
-  assert f_x.getSort() == intSort
-  f_y = solver.mkTerm(kinds.ApplyUf, f, y)
-  f_y.getSort()
-  assert f_y.getSort() == intSort
-  sum = solver.mkTerm(kinds.Plus, f_x, f_y)
-  sum.getSort()
-  assert sum.getSort() == intSort
-  p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
-  p_0.getSort()
-  assert p_0.getSort() == boolSort
-  p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y)
-  p_f_y.getSort()
-  assert p_f_y.getSort() == boolSort
+    bvSort = solver.mkBitVectorSort(8)
+    intSort = solver.getIntegerSort()
+    boolSort = solver.getBooleanSort()
+    funSort1 = solver.mkFunctionSort(bvSort, intSort)
+    funSort2 = solver.mkFunctionSort(intSort, boolSort)
+
+    n = Term(solver)
+    with pytest.raises(RuntimeError):
+        n.getSort()
+    x = solver.mkVar(bvSort, "x")
+    x.getSort()
+    assert x.getSort() == bvSort
+    y = solver.mkVar(bvSort, "y")
+    y.getSort()
+    assert y.getSort() == bvSort
+
+    f = solver.mkVar(funSort1, "f")
+    f.getSort()
+    assert f.getSort() == funSort1
+    p = solver.mkVar(funSort2, "p")
+    p.getSort()
+    assert p.getSort() == funSort2
+
+    zero = solver.mkInteger(0)
+    zero.getSort()
+    assert zero.getSort() == intSort
+
+    f_x = solver.mkTerm(kinds.ApplyUf, f, x)
+    f_x.getSort()
+    assert f_x.getSort() == intSort
+    f_y = solver.mkTerm(kinds.ApplyUf, f, y)
+    f_y.getSort()
+    assert f_y.getSort() == intSort
+    sum = solver.mkTerm(kinds.Plus, f_x, f_y)
+    sum.getSort()
+    assert sum.getSort() == intSort
+    p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
+    p_0.getSort()
+    assert p_0.getSort() == boolSort
+    p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y)
+    p_f_y.getSort()
+    assert p_f_y.getSort() == boolSort
+
+
+def test_get_op(solver):
+    intsort = solver.getIntegerSort()
+    bvsort = solver.mkBitVectorSort(8)
+    arrsort = solver.mkArraySort(bvsort, intsort)
+    funsort = solver.mkFunctionSort(intsort, bvsort)
+
+    x = solver.mkConst(intsort, "x")
+    a = solver.mkConst(arrsort, "a")
+    b = solver.mkConst(bvsort, "b")
+
+    assert not x.hasOp()
+    with pytest.raises(RuntimeError):
+        x.getOp()
+
+    ab = solver.mkTerm(kinds.Select, a, b)
+    ext = solver.mkOp(kinds.BVExtract, 4, 0)
+    extb = solver.mkTerm(ext, b)
+
+    assert ab.hasOp()
+    assert not ab.getOp().isIndexed()
+    # can compare directly to a Kind (will invoke constructor)
+    assert extb.hasOp()
+    assert extb.getOp().isIndexed()
+    assert extb.getOp() == ext
+
+    f = solver.mkConst(funsort, "f")
+    fx = solver.mkTerm(kinds.ApplyUf, f, x)
+
+    assert not f.hasOp()
+    with pytest.raises(RuntimeError):
+        f.getOp()
+    assert fx.hasOp()
+    children = [c for c in fx]
+    # testing rebuild from op and children
+    assert fx == solver.mkTerm(fx.getOp(), children)
+
+    # Test Datatypes Ops
+    sort = solver.mkParamSort("T")
+    listDecl = solver.mkDatatypeDecl("paramlist", sort)
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    cons.addSelector("head", sort)
+    cons.addSelectorSelf("tail")
+    listDecl.addConstructor(cons)
+    listDecl.addConstructor(nil)
+    listSort = solver.mkDatatypeSort(listDecl)
+    intListSort = listSort.instantiate([solver.getIntegerSort()])
+    c = solver.mkConst(intListSort, "c")
+    list1 = listSort.getDatatype()
+    # list datatype constructor and selector operator terms
+    consOpTerm = list1.getConstructorTerm("cons")
+    nilOpTerm = list1.getConstructorTerm("nil")
+    headOpTerm = list1["cons"].getSelectorTerm("head")
+    tailOpTerm = list1["cons"].getSelectorTerm("tail")
+
+    nilTerm = solver.mkTerm(kinds.ApplyConstructor, nilOpTerm)
+    consTerm = solver.mkTerm(kinds.ApplyConstructor, consOpTerm,
+                             solver.mkInteger(0), nilTerm)
+    headTerm = solver.mkTerm(kinds.ApplySelector, headOpTerm, consTerm)
+    tailTerm = solver.mkTerm(kinds.ApplySelector, tailOpTerm, consTerm)
+
+    assert nilTerm.hasOp()
+    assert consTerm.hasOp()
+    assert headTerm.hasOp()
+    assert tailTerm.hasOp()
+
+    # Test rebuilding
+    children = [c for c in headTerm]
+    assert headTerm == solver.mkTerm(headTerm.getOp(), children)
+
 
 def test_is_null(solver):
-  x = Term(solver)
-  assert x.isNull()
-  x = solver.mkVar(solver.mkBitVectorSort(4), "x")
-  assert not x.isNull()
+    x = Term(solver)
+    assert x.isNull()
+    x = solver.mkVar(solver.mkBitVectorSort(4), "x")
+    assert not x.isNull()
+
 
 def test_not_term(solver):
-  bvSort = solver.mkBitVectorSort(8)
-  intSort = solver.getIntegerSort()
-  boolSort = solver.getBooleanSort()
-  funSort1 = solver.mkFunctionSort(bvSort, intSort)
-  funSort2 = solver.mkFunctionSort(intSort, boolSort)
-
-  with pytest.raises(RuntimeError):
-      Term(solver).notTerm()
-  b = solver.mkTrue()
-  b.notTerm()
-  x = solver.mkVar(solver.mkBitVectorSort(8), "x")
-  with pytest.raises(RuntimeError):
-      x.notTerm()
-  f = solver.mkVar(funSort1, "f")
-  with pytest.raises(RuntimeError):
-      f.notTerm()
-  p = solver.mkVar(funSort2, "p")
-  with pytest.raises(RuntimeError):
-      p.notTerm()
-  zero = solver.mkInteger(0)
-  with pytest.raises(RuntimeError):
-      zero.notTerm()
-  f_x = solver.mkTerm(kinds.ApplyUf, f, x)
-  with pytest.raises(RuntimeError):
-      f_x.notTerm()
-  sum = solver.mkTerm(kinds.Plus, f_x, f_x)
-  with pytest.raises(RuntimeError):
-      sum.notTerm()
-  p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
-  p_0.notTerm()
-  p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
-  p_f_x.notTerm()
+    bvSort = solver.mkBitVectorSort(8)
+    intSort = solver.getIntegerSort()
+    boolSort = solver.getBooleanSort()
+    funSort1 = solver.mkFunctionSort(bvSort, intSort)
+    funSort2 = solver.mkFunctionSort(intSort, boolSort)
+
+    with pytest.raises(RuntimeError):
+        Term(solver).notTerm()
+    b = solver.mkTrue()
+    b.notTerm()
+    x = solver.mkVar(solver.mkBitVectorSort(8), "x")
+    with pytest.raises(RuntimeError):
+        x.notTerm()
+    f = solver.mkVar(funSort1, "f")
+    with pytest.raises(RuntimeError):
+        f.notTerm()
+    p = solver.mkVar(funSort2, "p")
+    with pytest.raises(RuntimeError):
+        p.notTerm()
+    zero = solver.mkInteger(0)
+    with pytest.raises(RuntimeError):
+        zero.notTerm()
+    f_x = solver.mkTerm(kinds.ApplyUf, f, x)
+    with pytest.raises(RuntimeError):
+        f_x.notTerm()
+    sum = solver.mkTerm(kinds.Plus, f_x, f_x)
+    with pytest.raises(RuntimeError):
+        sum.notTerm()
+    p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
+    p_0.notTerm()
+    p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
+    p_f_x.notTerm()
+
 
 def test_and_term(solver):
-  bvSort = solver.mkBitVectorSort(8)
-  intSort = solver.getIntegerSort()
-  boolSort = solver.getBooleanSort()
-  funSort1 = solver.mkFunctionSort(bvSort, intSort)
-  funSort2 = solver.mkFunctionSort(intSort, boolSort)
-
-  b = solver.mkTrue()
-  with pytest.raises(RuntimeError):
-      Term(solver).andTerm(b)
-  with pytest.raises(RuntimeError):
-      b.andTerm(Term(solver))
-  b.andTerm(b)
-  x = solver.mkVar(solver.mkBitVectorSort(8), "x")
-  with pytest.raises(RuntimeError):
-      x.andTerm(b)
-  with pytest.raises(RuntimeError):
-      x.andTerm(x)
-  f = solver.mkVar(funSort1, "f")
-  with pytest.raises(RuntimeError):
-      f.andTerm(b)
-  with pytest.raises(RuntimeError):
-      f.andTerm(x)
-  with pytest.raises(RuntimeError):
-      f.andTerm(f)
-  p = solver.mkVar(funSort2, "p")
-  with pytest.raises(RuntimeError):
-      p.andTerm(b)
-  with pytest.raises(RuntimeError):
-      p.andTerm(x)
-  with pytest.raises(RuntimeError):
-      p.andTerm(f)
-  with pytest.raises(RuntimeError):
-      p.andTerm(p)
-  zero = solver.mkInteger(0)
-  with pytest.raises(RuntimeError):
-      zero.andTerm(b)
-  with pytest.raises(RuntimeError):
-      zero.andTerm(x)
-  with pytest.raises(RuntimeError):
-      zero.andTerm(f)
-  with pytest.raises(RuntimeError):
-      zero.andTerm(p)
-  with pytest.raises(RuntimeError):
-      zero.andTerm(zero)
-  f_x = solver.mkTerm(kinds.ApplyUf, f, x)
-  with pytest.raises(RuntimeError):
-      f_x.andTerm(b)
-  with pytest.raises(RuntimeError):
-      f_x.andTerm(x)
-  with pytest.raises(RuntimeError):
-      f_x.andTerm(f)
-  with pytest.raises(RuntimeError):
-      f_x.andTerm(p)
-  with pytest.raises(RuntimeError):
-      f_x.andTerm(zero)
-  with pytest.raises(RuntimeError):
-      f_x.andTerm(f_x)
-  sum = solver.mkTerm(kinds.Plus, f_x, f_x)
-  with pytest.raises(RuntimeError):
-      sum.andTerm(b)
-  with pytest.raises(RuntimeError):
-      sum.andTerm(x)
-  with pytest.raises(RuntimeError):
-      sum.andTerm(f)
-  with pytest.raises(RuntimeError):
-      sum.andTerm(p)
-  with pytest.raises(RuntimeError):
-      sum.andTerm(zero)
-  with pytest.raises(RuntimeError):
-      sum.andTerm(f_x)
-  with pytest.raises(RuntimeError):
-      sum.andTerm(sum)
-  p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
-  p_0.andTerm(b)
-  with pytest.raises(RuntimeError):
-      p_0.andTerm(x)
-  with pytest.raises(RuntimeError):
-      p_0.andTerm(f)
-  with pytest.raises(RuntimeError):
-      p_0.andTerm(p)
-  with pytest.raises(RuntimeError):
-      p_0.andTerm(zero)
-  with pytest.raises(RuntimeError):
-      p_0.andTerm(f_x)
-  with pytest.raises(RuntimeError):
-      p_0.andTerm(sum)
-  p_0.andTerm(p_0)
-  p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
-  p_f_x.andTerm(b)
-  with pytest.raises(RuntimeError):
-      p_f_x.andTerm(x)
-  with pytest.raises(RuntimeError):
-      p_f_x.andTerm(f)
-  with pytest.raises(RuntimeError):
-      p_f_x.andTerm(p)
-  with pytest.raises(RuntimeError):
-      p_f_x.andTerm(zero)
-  with pytest.raises(RuntimeError):
-      p_f_x.andTerm(f_x)
-  with pytest.raises(RuntimeError):
-      p_f_x.andTerm(sum)
-  p_f_x.andTerm(p_0)
-  p_f_x.andTerm(p_f_x)
+    bvSort = solver.mkBitVectorSort(8)
+    intSort = solver.getIntegerSort()
+    boolSort = solver.getBooleanSort()
+    funSort1 = solver.mkFunctionSort(bvSort, intSort)
+    funSort2 = solver.mkFunctionSort(intSort, boolSort)
+
+    b = solver.mkTrue()
+    with pytest.raises(RuntimeError):
+        Term(solver).andTerm(b)
+    with pytest.raises(RuntimeError):
+        b.andTerm(Term(solver))
+    b.andTerm(b)
+    x = solver.mkVar(solver.mkBitVectorSort(8), "x")
+    with pytest.raises(RuntimeError):
+        x.andTerm(b)
+    with pytest.raises(RuntimeError):
+        x.andTerm(x)
+    f = solver.mkVar(funSort1, "f")
+    with pytest.raises(RuntimeError):
+        f.andTerm(b)
+    with pytest.raises(RuntimeError):
+        f.andTerm(x)
+    with pytest.raises(RuntimeError):
+        f.andTerm(f)
+    p = solver.mkVar(funSort2, "p")
+    with pytest.raises(RuntimeError):
+        p.andTerm(b)
+    with pytest.raises(RuntimeError):
+        p.andTerm(x)
+    with pytest.raises(RuntimeError):
+        p.andTerm(f)
+    with pytest.raises(RuntimeError):
+        p.andTerm(p)
+    zero = solver.mkInteger(0)
+    with pytest.raises(RuntimeError):
+        zero.andTerm(b)
+    with pytest.raises(RuntimeError):
+        zero.andTerm(x)
+    with pytest.raises(RuntimeError):
+        zero.andTerm(f)
+    with pytest.raises(RuntimeError):
+        zero.andTerm(p)
+    with pytest.raises(RuntimeError):
+        zero.andTerm(zero)
+    f_x = solver.mkTerm(kinds.ApplyUf, f, x)
+    with pytest.raises(RuntimeError):
+        f_x.andTerm(b)
+    with pytest.raises(RuntimeError):
+        f_x.andTerm(x)
+    with pytest.raises(RuntimeError):
+        f_x.andTerm(f)
+    with pytest.raises(RuntimeError):
+        f_x.andTerm(p)
+    with pytest.raises(RuntimeError):
+        f_x.andTerm(zero)
+    with pytest.raises(RuntimeError):
+        f_x.andTerm(f_x)
+    sum = solver.mkTerm(kinds.Plus, f_x, f_x)
+    with pytest.raises(RuntimeError):
+        sum.andTerm(b)
+    with pytest.raises(RuntimeError):
+        sum.andTerm(x)
+    with pytest.raises(RuntimeError):
+        sum.andTerm(f)
+    with pytest.raises(RuntimeError):
+        sum.andTerm(p)
+    with pytest.raises(RuntimeError):
+        sum.andTerm(zero)
+    with pytest.raises(RuntimeError):
+        sum.andTerm(f_x)
+    with pytest.raises(RuntimeError):
+        sum.andTerm(sum)
+    p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
+    p_0.andTerm(b)
+    with pytest.raises(RuntimeError):
+        p_0.andTerm(x)
+    with pytest.raises(RuntimeError):
+        p_0.andTerm(f)
+    with pytest.raises(RuntimeError):
+        p_0.andTerm(p)
+    with pytest.raises(RuntimeError):
+        p_0.andTerm(zero)
+    with pytest.raises(RuntimeError):
+        p_0.andTerm(f_x)
+    with pytest.raises(RuntimeError):
+        p_0.andTerm(sum)
+    p_0.andTerm(p_0)
+    p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
+    p_f_x.andTerm(b)
+    with pytest.raises(RuntimeError):
+        p_f_x.andTerm(x)
+    with pytest.raises(RuntimeError):
+        p_f_x.andTerm(f)
+    with pytest.raises(RuntimeError):
+        p_f_x.andTerm(p)
+    with pytest.raises(RuntimeError):
+        p_f_x.andTerm(zero)
+    with pytest.raises(RuntimeError):
+        p_f_x.andTerm(f_x)
+    with pytest.raises(RuntimeError):
+        p_f_x.andTerm(sum)
+    p_f_x.andTerm(p_0)
+    p_f_x.andTerm(p_f_x)
+
 
 def test_or_term(solver):
-  bvSort = solver.mkBitVectorSort(8)
-  intSort = solver.getIntegerSort()
-  boolSort = solver.getBooleanSort()
-  funSort1 = solver.mkFunctionSort(bvSort, intSort)
-  funSort2 = solver.mkFunctionSort(intSort, boolSort)
-
-  b = solver.mkTrue()
-  with pytest.raises(RuntimeError):
-      Term(solver).orTerm(b)
-  with pytest.raises(RuntimeError):
-      b.orTerm(Term(solver))
-  b.orTerm(b)
-  x = solver.mkVar(solver.mkBitVectorSort(8), "x")
-  with pytest.raises(RuntimeError):
-      x.orTerm(b)
-  with pytest.raises(RuntimeError):
-      x.orTerm(x)
-  f = solver.mkVar(funSort1, "f")
-  with pytest.raises(RuntimeError):
-      f.orTerm(b)
-  with pytest.raises(RuntimeError):
-      f.orTerm(x)
-  with pytest.raises(RuntimeError):
-      f.orTerm(f)
-  p = solver.mkVar(funSort2, "p")
-  with pytest.raises(RuntimeError):
-      p.orTerm(b)
-  with pytest.raises(RuntimeError):
-      p.orTerm(x)
-  with pytest.raises(RuntimeError):
-      p.orTerm(f)
-  with pytest.raises(RuntimeError):
-      p.orTerm(p)
-  zero = solver.mkInteger(0)
-  with pytest.raises(RuntimeError):
-      zero.orTerm(b)
-  with pytest.raises(RuntimeError):
-      zero.orTerm(x)
-  with pytest.raises(RuntimeError):
-      zero.orTerm(f)
-  with pytest.raises(RuntimeError):
-      zero.orTerm(p)
-  with pytest.raises(RuntimeError):
-      zero.orTerm(zero)
-  f_x = solver.mkTerm(kinds.ApplyUf, f, x)
-  with pytest.raises(RuntimeError):
-      f_x.orTerm(b)
-  with pytest.raises(RuntimeError):
-      f_x.orTerm(x)
-  with pytest.raises(RuntimeError):
-      f_x.orTerm(f)
-  with pytest.raises(RuntimeError):
-      f_x.orTerm(p)
-  with pytest.raises(RuntimeError):
-      f_x.orTerm(zero)
-  with pytest.raises(RuntimeError):
-      f_x.orTerm(f_x)
-  sum = solver.mkTerm(kinds.Plus, f_x, f_x)
-  with pytest.raises(RuntimeError):
-      sum.orTerm(b)
-  with pytest.raises(RuntimeError):
-      sum.orTerm(x)
-  with pytest.raises(RuntimeError):
-      sum.orTerm(f)
-  with pytest.raises(RuntimeError):
-      sum.orTerm(p)
-  with pytest.raises(RuntimeError):
-      sum.orTerm(zero)
-  with pytest.raises(RuntimeError):
-      sum.orTerm(f_x)
-  with pytest.raises(RuntimeError):
-      sum.orTerm(sum)
-  p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
-  p_0.orTerm(b)
-  with pytest.raises(RuntimeError):
-      p_0.orTerm(x)
-  with pytest.raises(RuntimeError):
-      p_0.orTerm(f)
-  with pytest.raises(RuntimeError):
-      p_0.orTerm(p)
-  with pytest.raises(RuntimeError):
-      p_0.orTerm(zero)
-  with pytest.raises(RuntimeError):
-      p_0.orTerm(f_x)
-  with pytest.raises(RuntimeError):
-      p_0.orTerm(sum)
-  p_0.orTerm(p_0)
-  p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
-  p_f_x.orTerm(b)
-  with pytest.raises(RuntimeError):
-      p_f_x.orTerm(x)
-  with pytest.raises(RuntimeError):
-      p_f_x.orTerm(f)
-  with pytest.raises(RuntimeError):
-      p_f_x.orTerm(p)
-  with pytest.raises(RuntimeError):
-      p_f_x.orTerm(zero)
-  with pytest.raises(RuntimeError):
-      p_f_x.orTerm(f_x)
-  with pytest.raises(RuntimeError):
-      p_f_x.orTerm(sum)
-  p_f_x.orTerm(p_0)
-  p_f_x.orTerm(p_f_x)
+    bvSort = solver.mkBitVectorSort(8)
+    intSort = solver.getIntegerSort()
+    boolSort = solver.getBooleanSort()
+    funSort1 = solver.mkFunctionSort(bvSort, intSort)
+    funSort2 = solver.mkFunctionSort(intSort, boolSort)
+
+    b = solver.mkTrue()
+    with pytest.raises(RuntimeError):
+        Term(solver).orTerm(b)
+    with pytest.raises(RuntimeError):
+        b.orTerm(Term(solver))
+    b.orTerm(b)
+    x = solver.mkVar(solver.mkBitVectorSort(8), "x")
+    with pytest.raises(RuntimeError):
+        x.orTerm(b)
+    with pytest.raises(RuntimeError):
+        x.orTerm(x)
+    f = solver.mkVar(funSort1, "f")
+    with pytest.raises(RuntimeError):
+        f.orTerm(b)
+    with pytest.raises(RuntimeError):
+        f.orTerm(x)
+    with pytest.raises(RuntimeError):
+        f.orTerm(f)
+    p = solver.mkVar(funSort2, "p")
+    with pytest.raises(RuntimeError):
+        p.orTerm(b)
+    with pytest.raises(RuntimeError):
+        p.orTerm(x)
+    with pytest.raises(RuntimeError):
+        p.orTerm(f)
+    with pytest.raises(RuntimeError):
+        p.orTerm(p)
+    zero = solver.mkInteger(0)
+    with pytest.raises(RuntimeError):
+        zero.orTerm(b)
+    with pytest.raises(RuntimeError):
+        zero.orTerm(x)
+    with pytest.raises(RuntimeError):
+        zero.orTerm(f)
+    with pytest.raises(RuntimeError):
+        zero.orTerm(p)
+    with pytest.raises(RuntimeError):
+        zero.orTerm(zero)
+    f_x = solver.mkTerm(kinds.ApplyUf, f, x)
+    with pytest.raises(RuntimeError):
+        f_x.orTerm(b)
+    with pytest.raises(RuntimeError):
+        f_x.orTerm(x)
+    with pytest.raises(RuntimeError):
+        f_x.orTerm(f)
+    with pytest.raises(RuntimeError):
+        f_x.orTerm(p)
+    with pytest.raises(RuntimeError):
+        f_x.orTerm(zero)
+    with pytest.raises(RuntimeError):
+        f_x.orTerm(f_x)
+    sum = solver.mkTerm(kinds.Plus, f_x, f_x)
+    with pytest.raises(RuntimeError):
+        sum.orTerm(b)
+    with pytest.raises(RuntimeError):
+        sum.orTerm(x)
+    with pytest.raises(RuntimeError):
+        sum.orTerm(f)
+    with pytest.raises(RuntimeError):
+        sum.orTerm(p)
+    with pytest.raises(RuntimeError):
+        sum.orTerm(zero)
+    with pytest.raises(RuntimeError):
+        sum.orTerm(f_x)
+    with pytest.raises(RuntimeError):
+        sum.orTerm(sum)
+    p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
+    p_0.orTerm(b)
+    with pytest.raises(RuntimeError):
+        p_0.orTerm(x)
+    with pytest.raises(RuntimeError):
+        p_0.orTerm(f)
+    with pytest.raises(RuntimeError):
+        p_0.orTerm(p)
+    with pytest.raises(RuntimeError):
+        p_0.orTerm(zero)
+    with pytest.raises(RuntimeError):
+        p_0.orTerm(f_x)
+    with pytest.raises(RuntimeError):
+        p_0.orTerm(sum)
+    p_0.orTerm(p_0)
+    p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
+    p_f_x.orTerm(b)
+    with pytest.raises(RuntimeError):
+        p_f_x.orTerm(x)
+    with pytest.raises(RuntimeError):
+        p_f_x.orTerm(f)
+    with pytest.raises(RuntimeError):
+        p_f_x.orTerm(p)
+    with pytest.raises(RuntimeError):
+        p_f_x.orTerm(zero)
+    with pytest.raises(RuntimeError):
+        p_f_x.orTerm(f_x)
+    with pytest.raises(RuntimeError):
+        p_f_x.orTerm(sum)
+    p_f_x.orTerm(p_0)
+    p_f_x.orTerm(p_f_x)
+
 
 def test_xor_term(solver):
-  bvSort = solver.mkBitVectorSort(8)
-  intSort = solver.getIntegerSort()
-  boolSort = solver.getBooleanSort()
-  funSort1 = solver.mkFunctionSort(bvSort, intSort)
-  funSort2 = solver.mkFunctionSort(intSort, boolSort)
-
-  b = solver.mkTrue()
-  with pytest.raises(RuntimeError):
-      Term(solver).xorTerm(b)
-  with pytest.raises(RuntimeError):
-      b.xorTerm(Term(solver))
-  b.xorTerm(b)
-  x = solver.mkVar(solver.mkBitVectorSort(8), "x")
-  with pytest.raises(RuntimeError):
-      x.xorTerm(b)
-  with pytest.raises(RuntimeError):
-      x.xorTerm(x)
-  f = solver.mkVar(funSort1, "f")
-  with pytest.raises(RuntimeError):
-      f.xorTerm(b)
-  with pytest.raises(RuntimeError):
-      f.xorTerm(x)
-  with pytest.raises(RuntimeError):
-      f.xorTerm(f)
-  p = solver.mkVar(funSort2, "p")
-  with pytest.raises(RuntimeError):
-      p.xorTerm(b)
-  with pytest.raises(RuntimeError):
-      p.xorTerm(x)
-  with pytest.raises(RuntimeError):
-      p.xorTerm(f)
-  with pytest.raises(RuntimeError):
-      p.xorTerm(p)
-  zero = solver.mkInteger(0)
-  with pytest.raises(RuntimeError):
-      zero.xorTerm(b)
-  with pytest.raises(RuntimeError):
-      zero.xorTerm(x)
-  with pytest.raises(RuntimeError):
-      zero.xorTerm(f)
-  with pytest.raises(RuntimeError):
-      zero.xorTerm(p)
-  with pytest.raises(RuntimeError):
-      zero.xorTerm(zero)
-  f_x = solver.mkTerm(kinds.ApplyUf, f, x)
-  with pytest.raises(RuntimeError):
-      f_x.xorTerm(b)
-  with pytest.raises(RuntimeError):
-      f_x.xorTerm(x)
-  with pytest.raises(RuntimeError):
-      f_x.xorTerm(f)
-  with pytest.raises(RuntimeError):
-      f_x.xorTerm(p)
-  with pytest.raises(RuntimeError):
-      f_x.xorTerm(zero)
-  with pytest.raises(RuntimeError):
-      f_x.xorTerm(f_x)
-  sum = solver.mkTerm(kinds.Plus, f_x, f_x)
-  with pytest.raises(RuntimeError):
-      sum.xorTerm(b)
-  with pytest.raises(RuntimeError):
-      sum.xorTerm(x)
-  with pytest.raises(RuntimeError):
-      sum.xorTerm(f)
-  with pytest.raises(RuntimeError):
-      sum.xorTerm(p)
-  with pytest.raises(RuntimeError):
-      sum.xorTerm(zero)
-  with pytest.raises(RuntimeError):
-      sum.xorTerm(f_x)
-  with pytest.raises(RuntimeError):
-      sum.xorTerm(sum)
-  p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
-  p_0.xorTerm(b)
-  with pytest.raises(RuntimeError):
-      p_0.xorTerm(x)
-  with pytest.raises(RuntimeError):
-      p_0.xorTerm(f)
-  with pytest.raises(RuntimeError):
-      p_0.xorTerm(p)
-  with pytest.raises(RuntimeError):
-      p_0.xorTerm(zero)
-  with pytest.raises(RuntimeError):
-      p_0.xorTerm(f_x)
-  with pytest.raises(RuntimeError):
-      p_0.xorTerm(sum)
-  p_0.xorTerm(p_0)
-  p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
-  p_f_x.xorTerm(b)
-  with pytest.raises(RuntimeError):
-      p_f_x.xorTerm(x)
-  with pytest.raises(RuntimeError):
-      p_f_x.xorTerm(f)
-  with pytest.raises(RuntimeError):
-      p_f_x.xorTerm(p)
-  with pytest.raises(RuntimeError):
-      p_f_x.xorTerm(zero)
-  with pytest.raises(RuntimeError):
-      p_f_x.xorTerm(f_x)
-  with pytest.raises(RuntimeError):
-      p_f_x.xorTerm(sum)
-  p_f_x.xorTerm(p_0)
-  p_f_x.xorTerm(p_f_x)
+    bvSort = solver.mkBitVectorSort(8)
+    intSort = solver.getIntegerSort()
+    boolSort = solver.getBooleanSort()
+    funSort1 = solver.mkFunctionSort(bvSort, intSort)
+    funSort2 = solver.mkFunctionSort(intSort, boolSort)
+
+    b = solver.mkTrue()
+    with pytest.raises(RuntimeError):
+        Term(solver).xorTerm(b)
+    with pytest.raises(RuntimeError):
+        b.xorTerm(Term(solver))
+    b.xorTerm(b)
+    x = solver.mkVar(solver.mkBitVectorSort(8), "x")
+    with pytest.raises(RuntimeError):
+        x.xorTerm(b)
+    with pytest.raises(RuntimeError):
+        x.xorTerm(x)
+    f = solver.mkVar(funSort1, "f")
+    with pytest.raises(RuntimeError):
+        f.xorTerm(b)
+    with pytest.raises(RuntimeError):
+        f.xorTerm(x)
+    with pytest.raises(RuntimeError):
+        f.xorTerm(f)
+    p = solver.mkVar(funSort2, "p")
+    with pytest.raises(RuntimeError):
+        p.xorTerm(b)
+    with pytest.raises(RuntimeError):
+        p.xorTerm(x)
+    with pytest.raises(RuntimeError):
+        p.xorTerm(f)
+    with pytest.raises(RuntimeError):
+        p.xorTerm(p)
+    zero = solver.mkInteger(0)
+    with pytest.raises(RuntimeError):
+        zero.xorTerm(b)
+    with pytest.raises(RuntimeError):
+        zero.xorTerm(x)
+    with pytest.raises(RuntimeError):
+        zero.xorTerm(f)
+    with pytest.raises(RuntimeError):
+        zero.xorTerm(p)
+    with pytest.raises(RuntimeError):
+        zero.xorTerm(zero)
+    f_x = solver.mkTerm(kinds.ApplyUf, f, x)
+    with pytest.raises(RuntimeError):
+        f_x.xorTerm(b)
+    with pytest.raises(RuntimeError):
+        f_x.xorTerm(x)
+    with pytest.raises(RuntimeError):
+        f_x.xorTerm(f)
+    with pytest.raises(RuntimeError):
+        f_x.xorTerm(p)
+    with pytest.raises(RuntimeError):
+        f_x.xorTerm(zero)
+    with pytest.raises(RuntimeError):
+        f_x.xorTerm(f_x)
+    sum = solver.mkTerm(kinds.Plus, f_x, f_x)
+    with pytest.raises(RuntimeError):
+        sum.xorTerm(b)
+    with pytest.raises(RuntimeError):
+        sum.xorTerm(x)
+    with pytest.raises(RuntimeError):
+        sum.xorTerm(f)
+    with pytest.raises(RuntimeError):
+        sum.xorTerm(p)
+    with pytest.raises(RuntimeError):
+        sum.xorTerm(zero)
+    with pytest.raises(RuntimeError):
+        sum.xorTerm(f_x)
+    with pytest.raises(RuntimeError):
+        sum.xorTerm(sum)
+    p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
+    p_0.xorTerm(b)
+    with pytest.raises(RuntimeError):
+        p_0.xorTerm(x)
+    with pytest.raises(RuntimeError):
+        p_0.xorTerm(f)
+    with pytest.raises(RuntimeError):
+        p_0.xorTerm(p)
+    with pytest.raises(RuntimeError):
+        p_0.xorTerm(zero)
+    with pytest.raises(RuntimeError):
+        p_0.xorTerm(f_x)
+    with pytest.raises(RuntimeError):
+        p_0.xorTerm(sum)
+    p_0.xorTerm(p_0)
+    p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
+    p_f_x.xorTerm(b)
+    with pytest.raises(RuntimeError):
+        p_f_x.xorTerm(x)
+    with pytest.raises(RuntimeError):
+        p_f_x.xorTerm(f)
+    with pytest.raises(RuntimeError):
+        p_f_x.xorTerm(p)
+    with pytest.raises(RuntimeError):
+        p_f_x.xorTerm(zero)
+    with pytest.raises(RuntimeError):
+        p_f_x.xorTerm(f_x)
+    with pytest.raises(RuntimeError):
+        p_f_x.xorTerm(sum)
+    p_f_x.xorTerm(p_0)
+    p_f_x.xorTerm(p_f_x)
+
 
 def test_eq_term(solver):
-  bvSort = solver.mkBitVectorSort(8)
-  intSort = solver.getIntegerSort()
-  boolSort = solver.getBooleanSort()
-  funSort1 = solver.mkFunctionSort(bvSort, intSort)
-  funSort2 = solver.mkFunctionSort(intSort, boolSort)
-
-  b = solver.mkTrue()
-  with pytest.raises(RuntimeError):
-      Term(solver).eqTerm(b)
-  with pytest.raises(RuntimeError):
-      b.eqTerm(Term(solver))
-  b.eqTerm(b)
-  x = solver.mkVar(solver.mkBitVectorSort(8), "x")
-  with pytest.raises(RuntimeError):
-      x.eqTerm(b)
-  x.eqTerm(x)
-  f = solver.mkVar(funSort1, "f")
-  with pytest.raises(RuntimeError):
-      f.eqTerm(b)
-  with pytest.raises(RuntimeError):
-      f.eqTerm(x)
-  f.eqTerm(f)
-  p = solver.mkVar(funSort2, "p")
-  with pytest.raises(RuntimeError):
-      p.eqTerm(b)
-  with pytest.raises(RuntimeError):
-      p.eqTerm(x)
-  with pytest.raises(RuntimeError):
-      p.eqTerm(f)
-  p.eqTerm(p)
-  zero = solver.mkInteger(0)
-  with pytest.raises(RuntimeError):
-      zero.eqTerm(b)
-  with pytest.raises(RuntimeError):
-      zero.eqTerm(x)
-  with pytest.raises(RuntimeError):
-      zero.eqTerm(f)
-  with pytest.raises(RuntimeError):
-      zero.eqTerm(p)
-  zero.eqTerm(zero)
-  f_x = solver.mkTerm(kinds.ApplyUf, f, x)
-  with pytest.raises(RuntimeError):
-      f_x.eqTerm(b)
-  with pytest.raises(RuntimeError):
-      f_x.eqTerm(x)
-  with pytest.raises(RuntimeError):
-      f_x.eqTerm(f)
-  with pytest.raises(RuntimeError):
-      f_x.eqTerm(p)
-  f_x.eqTerm(zero)
-  f_x.eqTerm(f_x)
-  sum = solver.mkTerm(kinds.Plus, f_x, f_x)
-  with pytest.raises(RuntimeError):
-      sum.eqTerm(b)
-  with pytest.raises(RuntimeError):
-      sum.eqTerm(x)
-  with pytest.raises(RuntimeError):
-      sum.eqTerm(f)
-  with pytest.raises(RuntimeError):
-      sum.eqTerm(p)
-  sum.eqTerm(zero)
-  sum.eqTerm(f_x)
-  sum.eqTerm(sum)
-  p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
-  p_0.eqTerm(b)
-  with pytest.raises(RuntimeError):
-      p_0.eqTerm(x)
-  with pytest.raises(RuntimeError):
-      p_0.eqTerm(f)
-  with pytest.raises(RuntimeError):
-      p_0.eqTerm(p)
-  with pytest.raises(RuntimeError):
-      p_0.eqTerm(zero)
-  with pytest.raises(RuntimeError):
-      p_0.eqTerm(f_x)
-  with pytest.raises(RuntimeError):
-      p_0.eqTerm(sum)
-  p_0.eqTerm(p_0)
-  p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
-  p_f_x.eqTerm(b)
-  with pytest.raises(RuntimeError):
-      p_f_x.eqTerm(x)
-  with pytest.raises(RuntimeError):
-      p_f_x.eqTerm(f)
-  with pytest.raises(RuntimeError):
-      p_f_x.eqTerm(p)
-  with pytest.raises(RuntimeError):
-      p_f_x.eqTerm(zero)
-  with pytest.raises(RuntimeError):
-      p_f_x.eqTerm(f_x)
-  with pytest.raises(RuntimeError):
-      p_f_x.eqTerm(sum)
-  p_f_x.eqTerm(p_0)
-  p_f_x.eqTerm(p_f_x)
+    bvSort = solver.mkBitVectorSort(8)
+    intSort = solver.getIntegerSort()
+    boolSort = solver.getBooleanSort()
+    funSort1 = solver.mkFunctionSort(bvSort, intSort)
+    funSort2 = solver.mkFunctionSort(intSort, boolSort)
+
+    b = solver.mkTrue()
+    with pytest.raises(RuntimeError):
+        Term(solver).eqTerm(b)
+    with pytest.raises(RuntimeError):
+        b.eqTerm(Term(solver))
+    b.eqTerm(b)
+    x = solver.mkVar(solver.mkBitVectorSort(8), "x")
+    with pytest.raises(RuntimeError):
+        x.eqTerm(b)
+    x.eqTerm(x)
+    f = solver.mkVar(funSort1, "f")
+    with pytest.raises(RuntimeError):
+        f.eqTerm(b)
+    with pytest.raises(RuntimeError):
+        f.eqTerm(x)
+    f.eqTerm(f)
+    p = solver.mkVar(funSort2, "p")
+    with pytest.raises(RuntimeError):
+        p.eqTerm(b)
+    with pytest.raises(RuntimeError):
+        p.eqTerm(x)
+    with pytest.raises(RuntimeError):
+        p.eqTerm(f)
+    p.eqTerm(p)
+    zero = solver.mkInteger(0)
+    with pytest.raises(RuntimeError):
+        zero.eqTerm(b)
+    with pytest.raises(RuntimeError):
+        zero.eqTerm(x)
+    with pytest.raises(RuntimeError):
+        zero.eqTerm(f)
+    with pytest.raises(RuntimeError):
+        zero.eqTerm(p)
+    zero.eqTerm(zero)
+    f_x = solver.mkTerm(kinds.ApplyUf, f, x)
+    with pytest.raises(RuntimeError):
+        f_x.eqTerm(b)
+    with pytest.raises(RuntimeError):
+        f_x.eqTerm(x)
+    with pytest.raises(RuntimeError):
+        f_x.eqTerm(f)
+    with pytest.raises(RuntimeError):
+        f_x.eqTerm(p)
+    f_x.eqTerm(zero)
+    f_x.eqTerm(f_x)
+    sum = solver.mkTerm(kinds.Plus, f_x, f_x)
+    with pytest.raises(RuntimeError):
+        sum.eqTerm(b)
+    with pytest.raises(RuntimeError):
+        sum.eqTerm(x)
+    with pytest.raises(RuntimeError):
+        sum.eqTerm(f)
+    with pytest.raises(RuntimeError):
+        sum.eqTerm(p)
+    sum.eqTerm(zero)
+    sum.eqTerm(f_x)
+    sum.eqTerm(sum)
+    p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
+    p_0.eqTerm(b)
+    with pytest.raises(RuntimeError):
+        p_0.eqTerm(x)
+    with pytest.raises(RuntimeError):
+        p_0.eqTerm(f)
+    with pytest.raises(RuntimeError):
+        p_0.eqTerm(p)
+    with pytest.raises(RuntimeError):
+        p_0.eqTerm(zero)
+    with pytest.raises(RuntimeError):
+        p_0.eqTerm(f_x)
+    with pytest.raises(RuntimeError):
+        p_0.eqTerm(sum)
+    p_0.eqTerm(p_0)
+    p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
+    p_f_x.eqTerm(b)
+    with pytest.raises(RuntimeError):
+        p_f_x.eqTerm(x)
+    with pytest.raises(RuntimeError):
+        p_f_x.eqTerm(f)
+    with pytest.raises(RuntimeError):
+        p_f_x.eqTerm(p)
+    with pytest.raises(RuntimeError):
+        p_f_x.eqTerm(zero)
+    with pytest.raises(RuntimeError):
+        p_f_x.eqTerm(f_x)
+    with pytest.raises(RuntimeError):
+        p_f_x.eqTerm(sum)
+    p_f_x.eqTerm(p_0)
+    p_f_x.eqTerm(p_f_x)
+
 
 def test_imp_term(solver):
-  bvSort = solver.mkBitVectorSort(8)
-  intSort = solver.getIntegerSort()
-  boolSort = solver.getBooleanSort()
-  funSort1 = solver.mkFunctionSort(bvSort, intSort)
-  funSort2 = solver.mkFunctionSort(intSort, boolSort)
-
-  b = solver.mkTrue()
-  with pytest.raises(RuntimeError):
-      Term(solver).impTerm(b)
-  with pytest.raises(RuntimeError):
-      b.impTerm(Term(solver))
-  b.impTerm(b)
-  x = solver.mkVar(solver.mkBitVectorSort(8), "x")
-  with pytest.raises(RuntimeError):
-      x.impTerm(b)
-  with pytest.raises(RuntimeError):
-      x.impTerm(x)
-  f = solver.mkVar(funSort1, "f")
-  with pytest.raises(RuntimeError):
-      f.impTerm(b)
-  with pytest.raises(RuntimeError):
-      f.impTerm(x)
-  with pytest.raises(RuntimeError):
-      f.impTerm(f)
-  p = solver.mkVar(funSort2, "p")
-  with pytest.raises(RuntimeError):
-      p.impTerm(b)
-  with pytest.raises(RuntimeError):
-      p.impTerm(x)
-  with pytest.raises(RuntimeError):
-      p.impTerm(f)
-  with pytest.raises(RuntimeError):
-      p.impTerm(p)
-  zero = solver.mkInteger(0)
-  with pytest.raises(RuntimeError):
-      zero.impTerm(b)
-  with pytest.raises(RuntimeError):
-      zero.impTerm(x)
-  with pytest.raises(RuntimeError):
-      zero.impTerm(f)
-  with pytest.raises(RuntimeError):
-      zero.impTerm(p)
-  with pytest.raises(RuntimeError):
-      zero.impTerm(zero)
-  f_x = solver.mkTerm(kinds.ApplyUf, f, x)
-  with pytest.raises(RuntimeError):
-      f_x.impTerm(b)
-  with pytest.raises(RuntimeError):
-      f_x.impTerm(x)
-  with pytest.raises(RuntimeError):
-      f_x.impTerm(f)
-  with pytest.raises(RuntimeError):
-      f_x.impTerm(p)
-  with pytest.raises(RuntimeError):
-      f_x.impTerm(zero)
-  with pytest.raises(RuntimeError):
-      f_x.impTerm(f_x)
-  sum = solver.mkTerm(kinds.Plus, f_x, f_x)
-  with pytest.raises(RuntimeError):
-      sum.impTerm(b)
-  with pytest.raises(RuntimeError):
-      sum.impTerm(x)
-  with pytest.raises(RuntimeError):
-      sum.impTerm(f)
-  with pytest.raises(RuntimeError):
-      sum.impTerm(p)
-  with pytest.raises(RuntimeError):
-      sum.impTerm(zero)
-  with pytest.raises(RuntimeError):
-      sum.impTerm(f_x)
-  with pytest.raises(RuntimeError):
-      sum.impTerm(sum)
-  p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
-  p_0.impTerm(b)
-  with pytest.raises(RuntimeError):
-      p_0.impTerm(x)
-  with pytest.raises(RuntimeError):
-      p_0.impTerm(f)
-  with pytest.raises(RuntimeError):
-      p_0.impTerm(p)
-  with pytest.raises(RuntimeError):
-      p_0.impTerm(zero)
-  with pytest.raises(RuntimeError):
-      p_0.impTerm(f_x)
-  with pytest.raises(RuntimeError):
-      p_0.impTerm(sum)
-  p_0.impTerm(p_0)
-  p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
-  p_f_x.impTerm(b)
-  with pytest.raises(RuntimeError):
-      p_f_x.impTerm(x)
-  with pytest.raises(RuntimeError):
-      p_f_x.impTerm(f)
-  with pytest.raises(RuntimeError):
-      p_f_x.impTerm(p)
-  with pytest.raises(RuntimeError):
-      p_f_x.impTerm(zero)
-  with pytest.raises(RuntimeError):
-      p_f_x.impTerm(f_x)
-  with pytest.raises(RuntimeError):
-      p_f_x.impTerm(sum)
-  p_f_x.impTerm(p_0)
-  p_f_x.impTerm(p_f_x)
+    bvSort = solver.mkBitVectorSort(8)
+    intSort = solver.getIntegerSort()
+    boolSort = solver.getBooleanSort()
+    funSort1 = solver.mkFunctionSort(bvSort, intSort)
+    funSort2 = solver.mkFunctionSort(intSort, boolSort)
+
+    b = solver.mkTrue()
+    with pytest.raises(RuntimeError):
+        Term(solver).impTerm(b)
+    with pytest.raises(RuntimeError):
+        b.impTerm(Term(solver))
+    b.impTerm(b)
+    x = solver.mkVar(solver.mkBitVectorSort(8), "x")
+    with pytest.raises(RuntimeError):
+        x.impTerm(b)
+    with pytest.raises(RuntimeError):
+        x.impTerm(x)
+    f = solver.mkVar(funSort1, "f")
+    with pytest.raises(RuntimeError):
+        f.impTerm(b)
+    with pytest.raises(RuntimeError):
+        f.impTerm(x)
+    with pytest.raises(RuntimeError):
+        f.impTerm(f)
+    p = solver.mkVar(funSort2, "p")
+    with pytest.raises(RuntimeError):
+        p.impTerm(b)
+    with pytest.raises(RuntimeError):
+        p.impTerm(x)
+    with pytest.raises(RuntimeError):
+        p.impTerm(f)
+    with pytest.raises(RuntimeError):
+        p.impTerm(p)
+    zero = solver.mkInteger(0)
+    with pytest.raises(RuntimeError):
+        zero.impTerm(b)
+    with pytest.raises(RuntimeError):
+        zero.impTerm(x)
+    with pytest.raises(RuntimeError):
+        zero.impTerm(f)
+    with pytest.raises(RuntimeError):
+        zero.impTerm(p)
+    with pytest.raises(RuntimeError):
+        zero.impTerm(zero)
+    f_x = solver.mkTerm(kinds.ApplyUf, f, x)
+    with pytest.raises(RuntimeError):
+        f_x.impTerm(b)
+    with pytest.raises(RuntimeError):
+        f_x.impTerm(x)
+    with pytest.raises(RuntimeError):
+        f_x.impTerm(f)
+    with pytest.raises(RuntimeError):
+        f_x.impTerm(p)
+    with pytest.raises(RuntimeError):
+        f_x.impTerm(zero)
+    with pytest.raises(RuntimeError):
+        f_x.impTerm(f_x)
+    sum = solver.mkTerm(kinds.Plus, f_x, f_x)
+    with pytest.raises(RuntimeError):
+        sum.impTerm(b)
+    with pytest.raises(RuntimeError):
+        sum.impTerm(x)
+    with pytest.raises(RuntimeError):
+        sum.impTerm(f)
+    with pytest.raises(RuntimeError):
+        sum.impTerm(p)
+    with pytest.raises(RuntimeError):
+        sum.impTerm(zero)
+    with pytest.raises(RuntimeError):
+        sum.impTerm(f_x)
+    with pytest.raises(RuntimeError):
+        sum.impTerm(sum)
+    p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
+    p_0.impTerm(b)
+    with pytest.raises(RuntimeError):
+        p_0.impTerm(x)
+    with pytest.raises(RuntimeError):
+        p_0.impTerm(f)
+    with pytest.raises(RuntimeError):
+        p_0.impTerm(p)
+    with pytest.raises(RuntimeError):
+        p_0.impTerm(zero)
+    with pytest.raises(RuntimeError):
+        p_0.impTerm(f_x)
+    with pytest.raises(RuntimeError):
+        p_0.impTerm(sum)
+    p_0.impTerm(p_0)
+    p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
+    p_f_x.impTerm(b)
+    with pytest.raises(RuntimeError):
+        p_f_x.impTerm(x)
+    with pytest.raises(RuntimeError):
+        p_f_x.impTerm(f)
+    with pytest.raises(RuntimeError):
+        p_f_x.impTerm(p)
+    with pytest.raises(RuntimeError):
+        p_f_x.impTerm(zero)
+    with pytest.raises(RuntimeError):
+        p_f_x.impTerm(f_x)
+    with pytest.raises(RuntimeError):
+        p_f_x.impTerm(sum)
+    p_f_x.impTerm(p_0)
+    p_f_x.impTerm(p_f_x)
+
 
 def test_ite_term(solver):
-  bvSort = solver.mkBitVectorSort(8)
-  intSort = solver.getIntegerSort()
-  boolSort = solver.getBooleanSort()
-  funSort1 = solver.mkFunctionSort(bvSort, intSort)
-  funSort2 = solver.mkFunctionSort(intSort, boolSort)
-
-  b = solver.mkTrue()
-  with pytest.raises(RuntimeError):
-      Term(solver).iteTerm(b, b)
-  with pytest.raises(RuntimeError):
-      b.iteTerm(Term(solver), b)
-  with pytest.raises(RuntimeError):
-      b.iteTerm(b, Term(solver))
-  b.iteTerm(b, b)
-  x = solver.mkVar(solver.mkBitVectorSort(8), "x")
-  b.iteTerm(x, x)
-  b.iteTerm(b, b)
-  with pytest.raises(RuntimeError):
-      b.iteTerm(x, b)
-  with pytest.raises(RuntimeError):
-      x.iteTerm(x, x)
-  with pytest.raises(RuntimeError):
-      x.iteTerm(x, b)
-  f = solver.mkVar(funSort1, "f")
-  with pytest.raises(RuntimeError):
-      f.iteTerm(b, b)
-  with pytest.raises(RuntimeError):
-      x.iteTerm(b, x)
-  p = solver.mkVar(funSort2, "p")
-  with pytest.raises(RuntimeError):
-      p.iteTerm(b, b)
-  with pytest.raises(RuntimeError):
-      p.iteTerm(x, b)
-  zero = solver.mkInteger(0)
-  with pytest.raises(RuntimeError):
-      zero.iteTerm(x, x)
-  with pytest.raises(RuntimeError):
-      zero.iteTerm(x, b)
-  f_x = solver.mkTerm(kinds.ApplyUf, f, x)
-  with pytest.raises(RuntimeError):
-      f_x.iteTerm(b, b)
-  with pytest.raises(RuntimeError):
-      f_x.iteTerm(b, x)
-  sum = solver.mkTerm(kinds.Plus, f_x, f_x)
-  with pytest.raises(RuntimeError):
-      sum.iteTerm(x, x)
-  with pytest.raises(RuntimeError):
-      sum.iteTerm(b, x)
-  p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
-  p_0.iteTerm(b, b)
-  p_0.iteTerm(x, x)
-  with pytest.raises(RuntimeError):
-      p_0.iteTerm(x, b)
-  p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
-  p_f_x.iteTerm(b, b)
-  p_f_x.iteTerm(x, x)
-  with pytest.raises(RuntimeError):
-      p_f_x.iteTerm(x, b)
+    bvSort = solver.mkBitVectorSort(8)
+    intSort = solver.getIntegerSort()
+    boolSort = solver.getBooleanSort()
+    funSort1 = solver.mkFunctionSort(bvSort, intSort)
+    funSort2 = solver.mkFunctionSort(intSort, boolSort)
+
+    b = solver.mkTrue()
+    with pytest.raises(RuntimeError):
+        Term(solver).iteTerm(b, b)
+    with pytest.raises(RuntimeError):
+        b.iteTerm(Term(solver), b)
+    with pytest.raises(RuntimeError):
+        b.iteTerm(b, Term(solver))
+    b.iteTerm(b, b)
+    x = solver.mkVar(solver.mkBitVectorSort(8), "x")
+    b.iteTerm(x, x)
+    b.iteTerm(b, b)
+    with pytest.raises(RuntimeError):
+        b.iteTerm(x, b)
+    with pytest.raises(RuntimeError):
+        x.iteTerm(x, x)
+    with pytest.raises(RuntimeError):
+        x.iteTerm(x, b)
+    f = solver.mkVar(funSort1, "f")
+    with pytest.raises(RuntimeError):
+        f.iteTerm(b, b)
+    with pytest.raises(RuntimeError):
+        x.iteTerm(b, x)
+    p = solver.mkVar(funSort2, "p")
+    with pytest.raises(RuntimeError):
+        p.iteTerm(b, b)
+    with pytest.raises(RuntimeError):
+        p.iteTerm(x, b)
+    zero = solver.mkInteger(0)
+    with pytest.raises(RuntimeError):
+        zero.iteTerm(x, x)
+    with pytest.raises(RuntimeError):
+        zero.iteTerm(x, b)
+    f_x = solver.mkTerm(kinds.ApplyUf, f, x)
+    with pytest.raises(RuntimeError):
+        f_x.iteTerm(b, b)
+    with pytest.raises(RuntimeError):
+        f_x.iteTerm(b, x)
+    sum = solver.mkTerm(kinds.Plus, f_x, f_x)
+    with pytest.raises(RuntimeError):
+        sum.iteTerm(x, x)
+    with pytest.raises(RuntimeError):
+        sum.iteTerm(b, x)
+    p_0 = solver.mkTerm(kinds.ApplyUf, p, zero)
+    p_0.iteTerm(b, b)
+    p_0.iteTerm(x, x)
+    with pytest.raises(RuntimeError):
+        p_0.iteTerm(x, b)
+    p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x)
+    p_f_x.iteTerm(b, b)
+    p_f_x.iteTerm(x, x)
+    with pytest.raises(RuntimeError):
+        p_f_x.iteTerm(x, b)
+
 
 def test_term_assignment(solver):
-  t1 = solver.mkInteger(1)
-  t2 = t1
-  t2 = solver.mkInteger(2)
-  assert t1 == solver.mkInteger(1)
+    t1 = solver.mkInteger(1)
+    t2 = t1
+    t2 = solver.mkInteger(2)
+    assert t1 == solver.mkInteger(1)
+
+
+def test_substitute(solver):
+    x = solver.mkConst(solver.getIntegerSort(), "x")
+    one = solver.mkInteger(1)
+    ttrue = solver.mkTrue()
+    xpx = solver.mkTerm(kinds.Plus, x, x)
+    onepone = solver.mkTerm(kinds.Plus, one, one)
+
+    assert xpx.substitute(x, one) == onepone
+    assert onepone.substitute(one, x) == xpx
+    # incorrect due to type
+    with pytest.raises(RuntimeError):
+        xpx.substitute(one, ttrue)
+
+    # simultaneous substitution
+    y = solver.mkConst(solver.getIntegerSort(), "y")
+    xpy = solver.mkTerm(kinds.Plus, x, y)
+    xpone = solver.mkTerm(kinds.Plus, y, one)
+    es = []
+    rs = []
+    es.append(x)
+    rs.append(y)
+    es.append(y)
+    rs.append(one)
+    assert xpy.substitute(es, rs) == xpone
+
+    # incorrect substitution due to arity
+    rs.pop()
+    with pytest.raises(RuntimeError):
+        xpy.substitute(es, rs)
+
+    # incorrect substitution due to types
+    rs.append(ttrue)
+    with pytest.raises(RuntimeError):
+        xpy.substitute(es, rs)
+
+    # null cannot substitute
+    tnull = Term(solver)
+    with pytest.raises(RuntimeError):
+        tnull.substitute(one, x)
+    with pytest.raises(RuntimeError):
+        xpx.substitute(tnull, x)
+    with pytest.raises(RuntimeError):
+        xpx.substitute(x, tnull)
+    rs.pop()
+    rs.append(tnull)
+    with pytest.raises(RuntimeError):
+        xpy.substitute(es, rs)
+    es.clear()
+    rs.clear()
+    es.append(x)
+    rs.append(y)
+    with pytest.raises(RuntimeError):
+        tnull.substitute(es, rs)
+    es.append(tnull)
+    rs.append(one)
+    with pytest.raises(RuntimeError):
+        xpx.substitute(es, rs)
+
 
 def test_const_array(solver):
-  intsort = solver.getIntegerSort()
-  arrsort = solver.mkArraySort(intsort, intsort)
-  a = solver.mkConst(arrsort, "a")
-  one = solver.mkInteger(1)
-  constarr = solver.mkConstArray(arrsort, one)
-
-  assert constarr.getKind() == kinds.ConstArray
-  assert constarr.getConstArrayBase() == one
-  with pytest.raises(RuntimeError):
-      a.getConstArrayBase()
-
-  arrsort =       solver.mkArraySort(solver.getRealSort(), solver.getRealSort())
-  zero_array = solver.mkConstArray(arrsort, solver.mkReal(0))
-  stores = solver.mkTerm(
-      kinds.Store, zero_array, solver.mkReal(1), solver.mkReal(2))
-  stores =       solver.mkTerm(kinds.Store, stores, solver.mkReal(2), solver.mkReal(3))
-  stores =       solver.mkTerm(kinds.Store, stores, solver.mkReal(4), solver.mkReal(5))
+    intsort = solver.getIntegerSort()
+    arrsort = solver.mkArraySort(intsort, intsort)
+    a = solver.mkConst(arrsort, "a")
+    one = solver.mkInteger(1)
+    constarr = solver.mkConstArray(arrsort, one)
+
+    assert constarr.getKind() == kinds.ConstArray
+    assert constarr.getConstArrayBase() == one
+    with pytest.raises(RuntimeError):
+        a.getConstArrayBase()
+
+    arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort())
+    zero_array = solver.mkConstArray(arrsort, solver.mkReal(0))
+    stores = solver.mkTerm(kinds.Store, zero_array, solver.mkReal(1),
+                           solver.mkReal(2))
+    stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(2),
+                           solver.mkReal(3))
+    stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(4),
+                           solver.mkReal(5))
+
 
 def test_const_sequence_elements(solver):
-  realsort = solver.getRealSort()
-  seqsort = solver.mkSequenceSort(realsort)
-  s = solver.mkEmptySequence(seqsort)
+    realsort = solver.getRealSort()
+    seqsort = solver.mkSequenceSort(realsort)
+    s = solver.mkEmptySequence(seqsort)
+
+    assert s.getKind() == kinds.ConstSequence
+    # empty sequence has zero elements
+    cs = s.getConstSequenceElements()
+    assert len(cs) == 0
 
-  assert s.getKind() == kinds.ConstSequence
-  # empty sequence has zero elements
-  cs = s.getConstSequenceElements()
-  assert len(cs) == 0
+    # A seq.unit app is not a constant sequence (regardless of whether it is
+    # applied to a constant).
+    su = solver.mkTerm(kinds.SeqUnit, solver.mkReal(1))
+    with pytest.raises(RuntimeError):
+        su.getConstSequenceElements()
 
-  # A seq.unit app is not a constant sequence (regardless of whether it is
-  # applied to a constant).
-  su = solver.mkTerm(kinds.SeqUnit, solver.mkReal(1))
-  with pytest.raises(RuntimeError):
-      su.getConstSequenceElements()
 
 def test_term_scoped_to_string(solver):
-  intsort = solver.getIntegerSort()
-  x = solver.mkConst(intsort, "x")
-  assert str(x) == "x"
-  solver2 = pycvc5.Solver()
-  assert str(x) == "x"
+    intsort = solver.getIntegerSort()
+    x = solver.mkConst(intsort, "x")
+    assert str(x) == "x"
+    solver2 = pycvc5.Solver()
+    assert str(x) == "x"