From: yoni206 <yoni206@users.noreply.github.com>
Date: Mon, 5 Apr 2021 13:30:19 +0000 (-0700)
Subject: A proposal for python api unit tests (#6255)
X-Git-Tag: cvc5-1.0.0~1975
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6c2779e52f1301d99b874897f902e31d4a8cc208;p=cvc5.git

A proposal for python api unit tests (#6255)

This PR introduces two unit tests for the python api, translated directly from the unit tests for the cpp api.
The goal is to get feedback in order to reach some kind of a pattern/style for python API tests.
Also, i'd be happy to hear if there is any specific cpp api unit test I should translate for this initial attempt (e.g., a test that is more representative or might raise difficulties). For now i just picked the first two solver tests.
---

diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index 35d640869..4913a35c1 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -43,3 +43,8 @@ if(ENABLE_UNIT_TESTING)
     add_subdirectory(java)
   endif()
 endif()
+
+# add Python bindings tests if building with Python bindings
+if (BUILD_BINDINGS_PYTHON)
+  add_subdirectory(python)
+endif()
diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt
new file mode 100644
index 000000000..675f6a7c5
--- /dev/null
+++ b/test/python/CMakeLists.txt
@@ -0,0 +1,44 @@
+#####################
+## CMakeLists.txt
+## Top contributors (to current version):
+##   Makai Mann and Yoni Zohar
+## This file is part of the CVC4 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.
+##
+#-----------------------------------------------------------------------------#
+# 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 pytest for Python "
+      "version ${PYTHON_VERSION_MAJOR}.${PYTHON_VERSION_MINOR}. "
+      "Make sure to install pytest for this Python version "
+      "via \n`${PYTHON_EXECUTABLE} -m pip install pytest'.\nNote: You need to "
+      "have pip installed for this Python version.")
+endif()
+
+macro(cvc4_add_python_api_test name filename)
+
+  #   we create test target 'python/unit/api/myapitest'
+  #   and run it with 'ctest -R "python/unit/api/myapitest"'.
+  add_test (NAME python/unit/api/${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()
+
+# add specific test files
+cvc4_add_python_api_test(pytest_solver unit/api/test_solver.py)
diff --git a/test/python/unit/api/__init__.py b/test/python/unit/api/__init__.py
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
new file mode 100644
index 000000000..4ab0427c1
--- /dev/null
+++ b/test/python/unit/api/test_solver.py
@@ -0,0 +1,36 @@
+#####################
+## test_solver.py
+## Top contributors (to current version):
+##   Yoni Zohar
+## This file is part of the CVC4 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 pycvc4
+import sys
+
+from pycvc4 import kinds
+
+@pytest.fixture
+def solver():
+    return pycvc4.Solver()
+
+def test_recoverable_exception(solver):
+    solver.setOption("produce-models", "true")
+    x = solver.mkConst(solver.getBooleanSort(), "x")
+    solver.assertFormula(x.eqTerm(x).notTerm())
+    with pytest.raises(RuntimeError):
+        c = solver.getValue(x)
+
+def test_supports_floating_point(solver):
+    if solver.supportsFloatingPoint():
+      try:
+          solver.mkRoundingMode(pycvc4.RoundNearestTiesToEven)
+      except RuntimeError:
+          pytest.fail()
+    else:
+        with pytest.raises(RuntimeError):
+          solver.mkRoundingMode(pycvc4.RoundNearestTiesToEven)