Move `toPythonObj` tests to the new API unit test directory (#6656)

This is the last test file that we move from the old directory to the new one, and so the old directory is deleted.

diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
index b340ec8ba36e3a5492dfefe81370d955cee58b05..e9fd47261e2263d06a3bab4279ec1220b7572c0d 100644 (file)
--- a/test/api/CMakeLists.txt
+++ b/test/api/CMakeLists.txt
@@ -72,9 +72,3 @@ 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
deleted file mode 100644 (file)
index 4e77c0e..0000000
--- a/test/api/python/CMakeLists.txt
+++ /dev/null
@@ -1,41 +0,0 @@
-###############################################################################
-# Top contributors (to current version):
-#   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.
-# #############################################################################
-#
-# The build system configuration.
-##
-
-# 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(cvc5_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()
-
-cvc5_add_python_api_test(pytest_to_python_obj test_to_python_obj.py)

diff --git a/test/api/python/test_to_python_obj.py b/test/api/python/test_to_python_obj.py
deleted file mode 100644 (file)
index 2ba685d..0000000
--- a/test/api/python/test_to_python_obj.py
+++ /dev/null
@@ -1,118 +0,0 @@
-###############################################################################
-# Top contributors (to current version):
-#   Makai Mann, Andres Noetzli, Mudathir Mohamed
-#
-# 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.
-# #############################################################################
-##
-
-from fractions import Fraction
-import pytest
-
-import pycvc5
-from pycvc5 import kinds
-
-
-def testGetBool():
-    solver = pycvc5.Solver()
-    t = solver.mkTrue()
-    f = solver.mkFalse()
-    assert t.toPythonObj() == True
-    assert f.toPythonObj() == False
-
-
-def testGetInt():
-    solver = pycvc5.Solver()
-    two = solver.mkInteger(2)
-    assert two.toPythonObj() == 2
-
-
-def testGetReal():
-    solver = pycvc5.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 = pycvc5.Solver()
-    three = solver.mkBitVector(8, 3)
-    assert three.toPythonObj() == 3
-
-
-def testGetArray():
-    solver = pycvc5.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 = pycvc5.Solver()
-    solver.mkConst(solver.getBooleanSort(), "x")
-
-
-def testGetString():
-    solver = pycvc5.Solver()
-
-    s1 = '"test\n"😃\\u{a}'
-    t1 = solver.mkString(s1)
-    assert s1 == t1.toPythonObj()
-
-    s2 = '❤️cvc5❤️'
-    t2 = solver.mkString(s2)
-    assert s2 == t2.toPythonObj()
-
-
-def testGetValueInt():
-    solver = pycvc5.Solver()
-    solver.setOption("produce-models", "true")
-
-    intsort = solver.getIntegerSort()
-    x = solver.mkConst(intsort, "x")
-    solver.assertFormula(solver.mkTerm(kinds.Equal, x, solver.mkInteger(6)))
-
-    r = solver.checkSat()
-    assert r.isSat()
-
-    xval = solver.getValue(x)
-    assert xval.toPythonObj() == 6
-
-
-def testGetValueReal():
-    solver = pycvc5.Solver()
-    solver.setOption("produce-models", "true")
-
-    realsort = solver.getRealSort()
-    x = solver.mkConst(realsort, "x")
-    y = solver.mkConst(realsort, "y")
-    solver.assertFormula(solver.mkTerm(kinds.Equal, x, solver.mkReal("6")))
-    solver.assertFormula(solver.mkTerm(kinds.Equal, y, solver.mkReal("8.33")))
-
-    r = solver.checkSat()
-    assert r.isSat()
-
-    xval = solver.getValue(x)
-    yval = solver.getValue(y)
-    assert xval.toPythonObj() == Fraction("6")
-    assert yval.toPythonObj() == float(Fraction("8.33"))

diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt
index 88fd817f2eeba102297b8e62beb7c9b36a309b76..54134b5103488d8ceb7cb34e308978c8b6e1eacc 100644 (file)
--- a/test/python/CMakeLists.txt
+++ b/test/python/CMakeLists.txt
@@ -32,3 +32,4 @@ cvc5_add_python_api_test(pytest_sort unit/api/test_sort.py)
 cvc5_add_python_api_test(pytest_term unit/api/test_term.py)
 cvc5_add_python_api_test(pytest_datatype_api unit/api/test_datatype_api.py)
 cvc5_add_python_api_test(pytest_grammar unit/api/test_grammar.py)
+cvc5_add_python_api_test(pytest_to_python_obj unit/api/test_to_python_obj.py)

diff --git a/test/python/unit/api/test_to_python_obj.py b/test/python/unit/api/test_to_python_obj.py
new file mode 100644 (file)
index 0000000..2ba685d
--- /dev/null
+++ b/test/python/unit/api/test_to_python_obj.py
@@ -0,0 +1,118 @@
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann, Andres Noetzli, Mudathir Mohamed
+#
+# 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.
+# #############################################################################
+##
+
+from fractions import Fraction
+import pytest
+
+import pycvc5
+from pycvc5 import kinds
+
+
+def testGetBool():
+    solver = pycvc5.Solver()
+    t = solver.mkTrue()
+    f = solver.mkFalse()
+    assert t.toPythonObj() == True
+    assert f.toPythonObj() == False
+
+
+def testGetInt():
+    solver = pycvc5.Solver()
+    two = solver.mkInteger(2)
+    assert two.toPythonObj() == 2
+
+
+def testGetReal():
+    solver = pycvc5.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 = pycvc5.Solver()
+    three = solver.mkBitVector(8, 3)
+    assert three.toPythonObj() == 3
+
+
+def testGetArray():
+    solver = pycvc5.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 = pycvc5.Solver()
+    solver.mkConst(solver.getBooleanSort(), "x")
+
+
+def testGetString():
+    solver = pycvc5.Solver()
+
+    s1 = '"test\n"😃\\u{a}'
+    t1 = solver.mkString(s1)
+    assert s1 == t1.toPythonObj()
+
+    s2 = '❤️cvc5❤️'
+    t2 = solver.mkString(s2)
+    assert s2 == t2.toPythonObj()
+
+
+def testGetValueInt():
+    solver = pycvc5.Solver()
+    solver.setOption("produce-models", "true")
+
+    intsort = solver.getIntegerSort()
+    x = solver.mkConst(intsort, "x")
+    solver.assertFormula(solver.mkTerm(kinds.Equal, x, solver.mkInteger(6)))
+
+    r = solver.checkSat()
+    assert r.isSat()
+
+    xval = solver.getValue(x)
+    assert xval.toPythonObj() == 6
+
+
+def testGetValueReal():
+    solver = pycvc5.Solver()
+    solver.setOption("produce-models", "true")
+
+    realsort = solver.getRealSort()
+    x = solver.mkConst(realsort, "x")
+    y = solver.mkConst(realsort, "y")
+    solver.assertFormula(solver.mkTerm(kinds.Equal, x, solver.mkReal("6")))
+    solver.assertFormula(solver.mkTerm(kinds.Equal, y, solver.mkReal("8.33")))
+
+    r = solver.checkSat()
+    assert r.isSat()
+
+    xval = solver.getValue(x)
+    yval = solver.getValue(y)
+    assert xval.toPythonObj() == Fraction("6")
+    assert yval.toPythonObj() == float(Fraction("8.33"))