Python API: bugfix + translating tests from cpp unit tests (#6559)

This PR fixes an issue in the python API for datatypes, and also introduces tests translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/datatype_api_black.cpp

The next PR will translate more tests and will also introduce missing functions in the python API for datatypes.

2 files changed, 0 insertions, 185 deletions

diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt
index 7f05bf130..4e77c0ead 100644
--- a/test/api/python/CMakeLists.txt
+++ b/test/api/python/CMakeLists.txt
@@ -38,5 +38,4 @@ macro(cvc5_add_python_api_test name filename)
 
 endmacro()
 
-cvc5_add_python_api_test(pytest_datatype_api test_datatype_api.py)
 cvc5_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
deleted file mode 100644
index 06f4e0f3d..000000000
--- a/test/api/python/test_datatype_api.py
+++ /dev/null
@@ -1,184 +0,0 @@
-###############################################################################
-# Top contributors (to current version):
-#   Andres Noetzli, Makai Mann
-#
-# This file is part of the cvc5 project.
-#
-# Copyright (c) 2009-2021 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 pycvc5
-from pycvc5 import kinds
-
-
-def test_datatype_simply_rec():
-    solver = pycvc5.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()