Run python tests during make check (#5226)

If building with python bindings, check the pytest is installed, and adds a command to run pytest after the existing make check tests. If built without python bindings, it just uses a null command. Note: the current semantics are such that the pytest tests will not run if the ctest run fails (unless you pass the correct flag to make to continue --ignore-errors I believe). I can look into changing this semantics if that would be preferred.

7 files changed, 908 insertions, 0 deletions

diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
index 34a18d9b2..59df71010 100644
--- a/test/api/CMakeLists.txt
+++ b/test/api/CMakeLists.txt
@@ -67,3 +67,9 @@ if (USE_EDITLINE)
     )
   endif()
 endif()
+
+
+# add Python bindings tests if building with Python bindings
+if (BUILD_BINDINGS_PYTHON)
+  add_subdirectory(python)
+endif()
diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt
new file mode 100644
index 000000000..300038ada
--- /dev/null
+++ b/test/api/python/CMakeLists.txt
@@ -0,0 +1,43 @@
+#####################
+## CMakeLists.txt
+## Top contributors (to current version):
+##   Makai Mann
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 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.
+##
+#-----------------------------------------------------------------------------#
+# Add Python bindings API tests
+
+# Check if the pytest Python module is installed.
+execute_process(
+  COMMAND
+  ${PYTHON_EXECUTABLE} -c "import pytest"
+  RESULT_VARIABLE
+    RET_PYTEST
+  ERROR_QUIET
+)
+
+if(RET_PYTEST)
+    message(FATAL_ERROR
+      "Could not find Python module pytest. Install via `pip install pytest'.")
+endif()
+
+macro(cvc4_add_python_api_test name filename)
+
+  #   we create test target 'api/<output_dir>/myapitest'
+  #   and run it with 'ctest -R "api/<output_dir>/myapitest"'.
+  add_test (NAME api/api/python/${name}
+    COMMAND ${PYTHON_EXECUTABLE} -m pytest ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
+    # directory for importing the python bindings
+    WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python)
+
+endmacro()
+
+cvc4_add_python_api_test(pytest_datatype_api test_datatype_api.py)
+cvc4_add_python_api_test(pytest_grammar test_grammar.py)
+cvc4_add_python_api_test(pytest_sort test_sort.py)
+cvc4_add_python_api_test(pytest_term test_term.py)
+cvc4_add_python_api_test(pytest_to_python_obj test_to_python_obj.py)
diff --git a/test/api/python/test_datatype_api.py b/test/api/python/test_datatype_api.py
new file mode 100644
index 000000000..c692416c6
--- /dev/null
+++ b/test/api/python/test_datatype_api.py
@@ -0,0 +1,181 @@
+#####################
+## test_datatype_api.py
+## Top contributors (to current version):
+##   Andres Noetzli, Makai Mann
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 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.
+##
+import pytest
+
+import pycvc4
+from pycvc4 import kinds
+
+
+def test_datatype_simply_rec():
+    solver = pycvc4.Solver()
+
+    # Create mutual datatypes corresponding to this definition block:
+    #
+    #   DATATYPE
+    #     wlist = leaf(data: list),
+    #     list = cons(car: wlist, cdr: list) | nil,
+    #     ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list))
+    #   END;
+
+    # Make unresolved types as placeholders
+    unres_wlist = solver.mkUninterpretedSort('wlist')
+    unres_list = solver.mkUninterpretedSort('list')
+    unres_ns = solver.mkUninterpretedSort('ns')
+    unres_types = set([unres_wlist, unres_list, unres_ns])
+
+    wlist = solver.mkDatatypeDecl('wlist')
+    leaf = solver.mkDatatypeConstructorDecl('leaf')
+    leaf.addSelector('data', unres_list)
+    wlist.addConstructor(leaf)
+
+    dlist = solver.mkDatatypeDecl('list')
+    cons = solver.mkDatatypeConstructorDecl('cons')
+    cons.addSelector('car', unres_wlist)
+    cons.addSelector('cdr', unres_list)
+    dlist.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dlist.addConstructor(nil)
+
+    ns = solver.mkDatatypeDecl('ns')
+    elem = solver.mkDatatypeConstructorDecl('elem')
+    elem.addSelector('ndata', solver.mkSetSort(unres_wlist))
+    ns.addConstructor(elem)
+    elem_array = solver.mkDatatypeConstructorDecl('elemArray')
+    elem_array.addSelector('ndata', solver.mkArraySort(unres_list, unres_list))
+    ns.addConstructor(elem_array)
+
+    # this is well-founded and has no nested recursion
+    dtdecls = [wlist, dlist, ns]
+    dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types)
+    assert len(dtsorts) == 3
+    assert dtsorts[0].getDatatype().isWellFounded()
+    assert dtsorts[1].getDatatype().isWellFounded()
+    assert dtsorts[2].getDatatype().isWellFounded()
+    assert not dtsorts[0].getDatatype().hasNestedRecursion()
+    assert not dtsorts[1].getDatatype().hasNestedRecursion()
+    assert not dtsorts[2].getDatatype().hasNestedRecursion()
+
+    # Create mutual datatypes corresponding to this definition block:
+    #   DATATYPE
+    #     ns2 = elem2(ndata: array(int,ns2)) | nil2
+    #   END;
+    unres_ns2 = solver.mkUninterpretedSort('ns2')
+    unres_types = set([unres_ns2])
+
+    ns2 = solver.mkDatatypeDecl('ns2')
+    elem2 = solver.mkDatatypeConstructorDecl('elem2')
+    elem2.addSelector('ndata',
+                      solver.mkArraySort(solver.getIntegerSort(), unres_ns2))
+    ns2.addConstructor(elem2)
+    nil2 = solver.mkDatatypeConstructorDecl('nil2')
+    ns2.addConstructor(nil2)
+
+    # this is not well-founded due to non-simple recursion
+    dtdecls = [ns2]
+    dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types)
+    assert len(dtsorts) == 1
+    assert dtsorts[0].getDatatype()[0][0].getRangeSort().isArray()
+    elem_sort = dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort()
+    assert elem_sort == dtsorts[0]
+    assert dtsorts[0].getDatatype().isWellFounded()
+    assert dtsorts[0].getDatatype().hasNestedRecursion()
+
+    # Create mutual datatypes corresponding to this definition block:
+    #  DATATYPE
+    #    list3 = cons3(car: ns3, cdr: list3) | nil3,
+    #    ns3 = elem3(ndata: set(list3))
+    #  END
+    unres_ns3 = solver.mkUninterpretedSort('ns3')
+    unres_list3 = solver.mkUninterpretedSort('list3')
+    unres_types = set([unres_ns3, unres_list3])
+
+    list3 = solver.mkDatatypeDecl('list3')
+    cons3 = solver.mkDatatypeConstructorDecl('cons3')
+    cons3.addSelector('car', unres_ns3)
+    cons3.addSelector('cdr', unres_list3)
+    list3.addConstructor(cons3)
+    nil3 = solver.mkDatatypeConstructorDecl('nil3')
+    list3.addConstructor(nil3)
+
+    ns3 = solver.mkDatatypeDecl('ns3')
+    elem3 = solver.mkDatatypeConstructorDecl('elem3')
+    elem3.addSelector('ndata', solver.mkSetSort(unres_list3))
+    ns3.addConstructor(elem3)
+
+    # both are well-founded and have nested recursion
+    dtdecls = [list3, ns3]
+    dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types)
+    assert len(dtsorts) == 2
+    assert dtsorts[0].getDatatype().isWellFounded()
+    assert dtsorts[1].getDatatype().isWellFounded()
+    assert dtsorts[0].getDatatype().hasNestedRecursion()
+    assert dtsorts[1].getDatatype().hasNestedRecursion()
+
+    # Create mutual datatypes corresponding to this definition block:
+    #  DATATYPE
+    #    list4 = cons(car: set(ns4), cdr: list4) | nil,
+    #    ns4 = elem(ndata: list4)
+    #  END
+    unres_ns4 = solver.mkUninterpretedSort('ns4')
+    unres_list4 = solver.mkUninterpretedSort('list4')
+    unres_types = set([unres_ns4, unres_list4])
+
+    list4 = solver.mkDatatypeDecl('list4')
+    cons4 = solver.mkDatatypeConstructorDecl('cons4')
+    cons4.addSelector('car', solver.mkSetSort(unres_ns4))
+    cons4.addSelector('cdr', unres_list4)
+    list4.addConstructor(cons4)
+    nil4 = solver.mkDatatypeConstructorDecl('nil4')
+    list4.addConstructor(nil4)
+
+    ns4 = solver.mkDatatypeDecl('ns4')
+    elem4 = solver.mkDatatypeConstructorDecl('elem3')
+    elem4.addSelector('ndata', unres_list4)
+    ns4.addConstructor(elem4)
+
+    # both are well-founded and have nested recursion
+    dtdecls = [list4, ns4]
+    dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types)
+    assert len(dtsorts) == 2
+    assert dtsorts[0].getDatatype().isWellFounded()
+    assert dtsorts[1].getDatatype().isWellFounded()
+    assert dtsorts[0].getDatatype().hasNestedRecursion()
+    assert dtsorts[1].getDatatype().hasNestedRecursion()
+
+    # Create mutual datatypes corresponding to this definition block:
+    #  DATATYPE
+    #    list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil
+    #  END
+    unres_list5 = solver.mkSortConstructorSort('list5', 1)
+    unres_types = set([unres_list5])
+
+    x = solver.mkParamSort('X')
+    v = [x]
+    list5 = solver.mkDatatypeDecl('list5', v)
+
+    args = [x]
+    ur_list_x = unres_list5.instantiate(args)
+    args = [ur_list_x]
+    ur_list_list_x = unres_list5.instantiate(args)
+
+    cons5 = solver.mkDatatypeConstructorDecl('cons5')
+    cons5.addSelector('car', x)
+    cons5.addSelector('cdr', ur_list_list_x)
+    list5.addConstructor(cons5)
+    nil5 = solver.mkDatatypeConstructorDecl('nil5')
+    list5.addConstructor(nil5)
+
+    # well-founded and has nested recursion
+    dtdecls = [list5]
+    dtsorts = solver.mkDatatypeSorts(dtdecls, unres_types)
+    assert len(dtsorts) == 1
+    assert dtsorts[0].getDatatype().isWellFounded()
+    assert dtsorts[0].getDatatype().hasNestedRecursion()
diff --git a/test/api/python/test_grammar.py b/test/api/python/test_grammar.py
new file mode 100644
index 000000000..5a0d5101f
--- /dev/null
+++ b/test/api/python/test_grammar.py
@@ -0,0 +1,128 @@
+#####################
+## test_grammar.py
+## Top contributors (to current version):
+##   Yoni Zohar, Makai Mann
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 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.
+##
+## Translated from test/unit/api/grammar_black.h
+##
+
+import pytest
+
+import pycvc4
+from pycvc4 import kinds
+
+def test_add_rule():
+  solver = pycvc4.Solver()
+  boolean = solver.getBooleanSort()
+  integer = solver.getIntegerSort()
+
+  nullTerm = pycvc4.Term(solver)
+  start = solver.mkVar(boolean)
+  nts = solver.mkVar(boolean)
+
+  # expecting no error
+  g = solver.mkSygusGrammar([], [start])
+
+  g.addRule(start, solver.mkBoolean(False))
+
+  # expecting errors
+  with pytest.raises(Exception):
+    g.addRule(nullTerm, solver.mkBoolean(false))
+  with pytest.raises(Exception):
+    g.addRule(start, nullTerm)
+  with pytest.raises(Exception):
+    g.addRule(nts, solver.mkBoolean(false))
+  with pytest.raises(Exception):
+    g.addRule(start, solver.mkInteger(0))
+
+  # expecting no errors
+  solver.synthFun("f", {}, boolean, g)
+
+  # expecting an error
+  with pytest.raises(Exception):
+    g.addRule(start, solver.mkBoolean(false))
+
+def test_add_rules():
+  solver = pycvc4.Solver()
+  boolean = solver.getBooleanSort()
+  integer = solver.getIntegerSort()
+
+  nullTerm = pycvc4.Term(solver)
+  start = solver.mkVar(boolean)
+  nts = solver.mkVar(boolean)
+
+  g = solver.mkSygusGrammar([], [start])
+
+  g.addRules(start, {solver.mkBoolean(False)})
+
+  #Expecting errors
+  with pytest.raises(Exception):
+    g.addRules(nullTerm, solver.mkBoolean(False))
+  with pytest.raises(Exception):
+    g.addRules(start, {nullTerm})
+  with pytest.raises(Exception):
+    g.addRules(nts, {solver.mkBoolean(False)})
+  with pytest.raises(Exception):
+    g.addRules(start, {solver.mkInteger(0)})
+  #Expecting no errors
+  solver.synthFun("f", {}, boolean, g)
+
+  #Expecting an error
+  with pytest.raises(Exception):
+    g.addRules(start, solver.mkBoolean(False))
+
+def testAddAnyConstant():
+  solver = pycvc4.Solver()
+  boolean = solver.getBooleanSort()
+
+  nullTerm = pycvc4.Term(solver)
+  start = solver.mkVar(boolean)
+  nts = solver.mkVar(boolean)
+
+  g = solver.mkSygusGrammar({}, {start})
+
+  g.addAnyConstant(start)
+  g.addAnyConstant(start)
+
+  with pytest.raises(Exception):
+    g.addAnyConstant(nullTerm)
+  with pytest.raises(Exception):
+    g.addAnyConstant(nts)
+
+  solver.synthFun("f", {}, boolean, g)
+
+  with pytest.raises(Exception):
+    g.addAnyConstant(start)
+
+
+def testAddAnyVariable():
+  solver = pycvc4.Solver()
+  boolean = solver.getBooleanSort()
+
+  nullTerm = pycvc4.Term(solver)
+  x = solver.mkVar(boolean)
+  start = solver.mkVar(boolean)
+  nts = solver.mkVar(boolean)
+
+  g1 = solver.mkSygusGrammar({x}, {start})
+  g2 = solver.mkSygusGrammar({}, {start})
+
+  g1.addAnyVariable(start)
+  g1.addAnyVariable(start)
+  g2.addAnyVariable(start)
+
+  with pytest.raises(Exception):
+    g1.addAnyVariable(nullTerm)
+  with pytest.raises(Exception):
+    g1.addAnyVariable(nts)
+
+  solver.synthFun("f", {}, boolean, g1)
+
+  with pytest.raises(Exception):
+    g1.addAnyVariable(start)
+
diff --git a/test/api/python/test_sort.py b/test/api/python/test_sort.py
new file mode 100644
index 000000000..cff92ca8d
--- /dev/null
+++ b/test/api/python/test_sort.py
@@ -0,0 +1,355 @@
+#####################
+## test_sort.py
+## Top contributors (to current version):
+##   Makai Mann, Andres Noetzli
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 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.
+##
+import pytest
+
+import pycvc4
+from pycvc4 import kinds
+
+
+def testGetDatatype():
+    solver = pycvc4.Solver()
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+
+    # expecting no Error
+    dtypeSort.getDatatype()
+
+    bvSort = solver.mkBitVectorSort(32)
+    with pytest.raises(Exception):
+        # expect an exception
+        bvSort.getDatatype()
+
+
+def testDatatypeSorts():
+    solver = pycvc4.Solver()
+    intSort = solver.getIntegerSort()
+    # create datatype sort to test
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", intSort)
+    cons.addSelectorSelf("tail")
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+    dt = dtypeSort.getDatatype()
+    assert not dtypeSort.isConstructor()
+
+    with pytest.raises(Exception):
+        dtypeSort.getConstructorCodomainSort()
+
+    with pytest.raises(Exception):
+        dtypeSort.getConstructorDomainSorts()
+
+    with pytest.raises(Exception):
+        dtypeSort.getConstructorArity()
+
+    # get constructor
+    dcons = dt[0]
+    consTerm = dcons.getConstructorTerm()
+    consSort = consTerm.getSort()
+    assert consSort.isConstructor()
+    assert not consSort.isTester()
+    assert not consSort.isSelector()
+    assert consSort.getConstructorArity() == 2
+    consDomSorts = consSort.getConstructorDomainSorts()
+    assert consDomSorts[0] == intSort
+    assert consDomSorts[1] == dtypeSort
+    assert consSort.getConstructorCodomainSort() == dtypeSort
+
+    # get tester
+    isConsTerm = dcons.getTesterTerm()
+    assert isConsTerm.getSort().isTester()
+
+    # get selector
+    dselTail = dcons[1]
+    tailTerm = dselTail.getSelectorTerm()
+    assert tailTerm.getSort().isSelector()
+
+
+def testInstantiate():
+    solver = pycvc4.Solver()
+    # instantiate parametric datatype, check should not fail
+    sort = solver.mkParamSort("T")
+    paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort)
+    paramCons = solver.mkDatatypeConstructorDecl("cons")
+    paramNil = solver.mkDatatypeConstructorDecl("nil")
+    paramCons.addSelector("head", sort)
+    paramDtypeSpec.addConstructor(paramCons)
+    paramDtypeSpec.addConstructor(paramNil)
+    paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec)
+    paramDtypeSort.instantiate([solver.getIntegerSort()])
+
+    # instantiate non-parametric datatype sort, check should fail
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+
+    with pytest.raises(Exception):
+        dtypeSort.instantiate([solver.getIntegerSort()])
+
+
+def testGetFunctionArity():
+    solver = pycvc4.Solver()
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
+                                            solver.getIntegerSort())
+    funSort.getFunctionArity()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getFunctionArity()
+
+
+def testGetFunctionDomainSorts():
+    solver = pycvc4.Solver()
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
+                                            solver.getIntegerSort())
+    funSort.getFunctionDomainSorts()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getFunctionDomainSorts()
+
+
+def testGetFunctionCodomainSort():
+    solver = pycvc4.Solver()
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
+                                            solver.getIntegerSort())
+    funSort.getFunctionCodomainSort()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getFunctionCodomainSort()
+
+def testGetArrayIndexSort():
+    solver = pycvc4.Solver()
+    elementSort = solver.mkBitVectorSort(32)
+    indexSort = solver.mkBitVectorSort(32)
+    arraySort = solver.mkArraySort(indexSort, elementSort)
+    arraySort.getArrayIndexSort()
+
+    with pytest.raises(Exception):
+        indexSort.getArrayIndexSort()
+
+def testGetArrayElementSort():
+    solver = pycvc4.Solver()
+    elementSort = solver.mkBitVectorSort(32)
+    indexSort = solver.mkBitVectorSort(32)
+    arraySort = solver.mkArraySort(indexSort, elementSort)
+    arraySort.getArrayElementSort()
+
+    with pytest.raises(Exception):
+        indexSort.getArrayElementSort()
+
+def testGetSetElementSort():
+    solver = pycvc4.Solver()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+    setSort.getSetElementSort()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getSetElementSort()
+
+def testGetSequenceElementSort():
+    solver = pycvc4.Solver()
+    seqSort = solver.mkSequenceSort(solver.getIntegerSort())
+    seqSort.getSequenceElementSort()
+    bvSort = solver.mkBitVectorSort(32)
+    assert not bvSort.isSequence()
+
+    with pytest.raises(Exception):
+        bvSort.getSetElementSort()
+
+def testGetUninterpretedSortName():
+    solver = pycvc4.Solver()
+    uSort = solver.mkUninterpretedSort("u")
+    uSort.getUninterpretedSortName()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getUninterpretedSortName()
+
+def testIsUninterpretedSortParameterized():
+    solver = pycvc4.Solver()
+    uSort = solver.mkUninterpretedSort("u")
+    uSort.isUninterpretedSortParameterized()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.isUninterpretedSortParameterized()
+
+def testGetUninterpretedSortParamSorts():
+    solver = pycvc4.Solver()
+    uSort = solver.mkUninterpretedSort("u")
+    uSort.getUninterpretedSortParamSorts()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getUninterpretedSortParamSorts()
+
+def testGetUninterpretedSortConstructorName():
+    solver = pycvc4.Solver()
+    sSort = solver.mkSortConstructorSort("s", 2)
+    sSort.getSortConstructorName()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getSortConstructorName()
+
+def testGetUninterpretedSortConstructorArity():
+    solver = pycvc4.Solver()
+    sSort = solver.mkSortConstructorSort("s", 2)
+    sSort.getSortConstructorArity()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getSortConstructorArity()
+
+def testGetBVSize():
+    solver = pycvc4.Solver()
+    bvSort = solver.mkBitVectorSort(32)
+    bvSort.getBVSize()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+
+    with pytest.raises(Exception):
+        setSort.getBVSize()
+
+def testGetFPExponentSize():
+    solver = pycvc4.Solver()
+
+    if solver.supportsFloatingPoint():
+        fpSort = solver.mkFloatingPointSort(4, 8)
+        fpSort.getFPExponentSize()
+        setSort = solver.mkSetSort(solver.getIntegerSort())
+
+        with pytest.raises(Exception):
+            setSort.getFPExponentSize()
+    else:
+        with pytest.raises(Exception):
+            solver.mkFloatingPointSort(4, 8)
+
+def testGetFPSignificandSize():
+    solver = pycvc4.Solver()
+
+    if solver.supportsFloatingPoint():
+        fpSort = solver.mkFloatingPointSort(4, 8)
+        fpSort.getFPSignificandSize()
+        setSort = solver.mkSetSort(solver.getIntegerSort())
+
+        with pytest.raises(Exception):
+            setSort.getFPSignificandSize()
+    else:
+        with pytest.raises(Exception):
+            solver.mkFloatingPointSort(4, 8)
+
+def testGetDatatypeParamSorts():
+    solver = pycvc4.Solver()
+    # create parametric datatype, check should not fail
+    sort = solver.mkParamSort("T")
+    paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort)
+    paramCons = solver.mkDatatypeConstructorDecl("cons")
+    paramNil = solver.mkDatatypeConstructorDecl("nil")
+    paramCons.addSelector("head", sort)
+    paramDtypeSpec.addConstructor(paramCons)
+    paramDtypeSpec.addConstructor(paramNil)
+    paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec)
+    paramDtypeSort.getDatatypeParamSorts()
+    # create non-parametric datatype sort, check should fail
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+
+    with pytest.raises(Exception):
+        dtypeSort.getDatatypeParamSorts()
+
+
+def testGetDatatypeArity():
+    solver = pycvc4.Solver()
+    # create datatype sort, check should not fail
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+    dtypeSort.getDatatypeArity()
+    # create bv sort, check should fail
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getDatatypeArity()
+
+def testGetTupleLength():
+    solver = pycvc4.Solver()
+    tupleSort = solver.mkTupleSort([solver.getIntegerSort(), solver.getIntegerSort()])
+    tupleSort.getTupleLength()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getTupleLength()
+
+def testGetTupleSorts():
+    solver = pycvc4.Solver()
+    tupleSort = solver.mkTupleSort([solver.getIntegerSort(), solver.getIntegerSort()])
+    tupleSort.getTupleSorts()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getTupleSorts()
+
+def testSortCompare():
+    solver = pycvc4.Solver()
+    boolSort = solver.getBooleanSort()
+    intSort = solver.getIntegerSort()
+    bvSort = solver.mkBitVectorSort(32)
+    bvSort2 = solver.mkBitVectorSort(32)
+    assert bvSort >= bvSort2
+    assert bvSort <= bvSort2
+    assert (intSort > boolSort) != (intSort < boolSort)
+    assert (intSort > bvSort or intSort == bvSort) == (intSort >= bvSort)
+
+def testSortSubtyping():
+    solver = pycvc4.Solver()
+    intSort = solver.getIntegerSort()
+    realSort = solver.getRealSort()
+    assert intSort.isSubsortOf(realSort)
+    assert not realSort.isSubsortOf(intSort)
+    assert intSort.isComparableTo(realSort)
+    assert realSort.isComparableTo(intSort)
+
+    arraySortII = solver.mkArraySort(intSort, intSort)
+    arraySortIR = solver.mkArraySort(intSort, realSort)
+    assert not arraySortII.isComparableTo(intSort)
+    # we do not support subtyping for arrays
+    assert not arraySortII.isComparableTo(arraySortIR)
+
+    setSortI = solver.mkSetSort(intSort)
+    setSortR = solver.mkSetSort(realSort)
+    # we don't support subtyping for sets
+    assert not setSortI.isComparableTo(setSortR)
+    assert not setSortI.isSubsortOf(setSortR)
+    assert not setSortR.isComparableTo(setSortI)
+    assert not setSortR.isSubsortOf(setSortI)
+
diff --git a/test/api/python/test_term.py b/test/api/python/test_term.py
new file mode 100644
index 000000000..a0c1b4681
--- /dev/null
+++ b/test/api/python/test_term.py
@@ -0,0 +1,124 @@
+#####################
+## test_term.py
+## Top contributors (to current version):
+##   Makai Mann, Andres Noetzli
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 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.
+##
+import pytest
+
+import pycvc4
+from pycvc4 import kinds
+
+
+def test_getitem():
+    solver = pycvc4.Solver()
+    intsort = solver.getIntegerSort()
+    x = solver.mkConst(intsort, 'x')
+    y = solver.mkConst(intsort, 'y')
+    xpy = solver.mkTerm(kinds.Plus, x, y)
+
+    assert xpy[0] == x
+    assert xpy[1] == y
+
+
+def test_get_kind():
+    solver = pycvc4.Solver()
+    intsort = solver.getIntegerSort()
+    x = solver.mkConst(intsort, 'x')
+    y = solver.mkConst(intsort, 'y')
+    xpy = solver.mkTerm(kinds.Plus, x, y)
+    assert xpy.getKind() == kinds.Plus
+
+    funsort = solver.mkFunctionSort(intsort, intsort)
+    f = solver.mkConst(funsort, 'f')
+    assert f.getKind() == kinds.Constant
+
+    fx = solver.mkTerm(kinds.ApplyUf, f, x)
+    assert fx.getKind() == kinds.ApplyUf
+
+    # 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_eq():
+    solver = pycvc4.Solver()
+    usort = solver.mkUninterpretedSort('u')
+    x = solver.mkConst(usort, 'x')
+    y = solver.mkConst(usort, 'y')
+    z = x
+
+    assert x == x
+    assert x == z
+    assert not (x != x)
+    assert x != y
+    assert y != z
+
+
+def test_get_sort():
+    solver = pycvc4.Solver()
+    intsort = solver.getIntegerSort()
+    bvsort8 = solver.mkBitVectorSort(8)
+
+    x = solver.mkConst(intsort, 'x')
+    y = solver.mkConst(intsort, 'y')
+
+    a = solver.mkConst(bvsort8, 'a')
+    b = solver.mkConst(bvsort8, 'b')
+
+    assert x.getSort() == intsort
+    assert solver.mkTerm(kinds.Plus, x, y).getSort() == intsort
+
+    assert a.getSort() == bvsort8
+    assert solver.mkTerm(kinds.BVConcat, a, b).getSort() == solver.mkBitVectorSort(16)
+
+def test_get_op():
+    solver = pycvc4.Solver()
+    intsort = solver.getIntegerSort()
+    funsort = solver.mkFunctionSort(intsort, intsort)
+
+    x = solver.mkConst(intsort, 'x')
+    f = solver.mkConst(funsort, 'f')
+
+    fx = solver.mkTerm(kinds.ApplyUf, f, x)
+
+    assert not x.hasOp()
+
+    try:
+        op = x.getOp()
+        assert False
+    except:
+        assert True
+
+    assert fx.hasOp()
+    assert fx.getOp().getKind() == kinds.ApplyUf
+    # equivalent check
+    assert fx.getOp() == solver.mkOp(kinds.ApplyUf)
+
+
+def test_const_sequence_elements():
+    solver = pycvc4.Solver()
+    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
+
+    # 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))
+    try:
+        su.getConstSequenceElements()
+        assert False
+    except:
+        assert True
diff --git a/test/api/python/test_to_python_obj.py b/test/api/python/test_to_python_obj.py
new file mode 100644
index 000000000..eb15e7469
--- /dev/null
+++ b/test/api/python/test_to_python_obj.py
@@ -0,0 +1,71 @@
+from fractions import Fraction
+import pytest
+
+import pycvc4
+from pycvc4 import kinds
+
+
+def testGetBool():
+    solver = pycvc4.Solver()
+    t = solver.mkTrue()
+    f = solver.mkFalse()
+    assert t.toPythonObj() == True
+    assert f.toPythonObj() == False
+
+
+def testGetInt():
+    solver = pycvc4.Solver()
+    two = solver.mkInteger(2)
+    assert two.toPythonObj() == 2
+
+
+def testGetReal():
+    solver = pycvc4.Solver()
+    half = solver.mkReal("1/2")
+    assert half.toPythonObj() == Fraction(1, 2)
+
+    neg34 = solver.mkReal("-3/4")
+    assert neg34.toPythonObj() == Fraction(-3, 4)
+
+    neg1 = solver.mkInteger("-1")
+    assert neg1.toPythonObj() == -1
+
+
+def testGetBV():
+    solver = pycvc4.Solver()
+    three = solver.mkBitVector(8, 3)
+    assert three.toPythonObj() == 3
+
+
+def testGetArray():
+    solver = pycvc4.Solver()
+    arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort())
+    zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0))
+    stores = solver.mkTerm(kinds.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2))
+    stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(2), solver.mkInteger(3))
+    stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(4), solver.mkInteger(5))
+
+    array_dict = stores.toPythonObj()
+
+    assert array_dict[1] == 2
+    assert array_dict[2] == 3
+    assert array_dict[4] == 5
+    # an index that wasn't stored at should give zero
+    assert array_dict[8] == 0
+
+
+def testGetSymbol():
+    solver = pycvc4.Solver()
+    solver.mkConst(solver.getBooleanSort(), "x")
+
+
+def testGetString():
+    solver = pycvc4.Solver()
+
+    s1 = '"test\n"😃\\u{a}'
+    t1 = solver.mkString(s1)
+    assert s1 == t1.toPythonObj()
+
+    s2 = '❤️CVC4❤️'
+    t2 = solver.mkString(s2)
+    assert s2 == t2.toPythonObj()