Refactor CI tests to separate z3 tests (#1126)

Configure CI matrix with "base" and "z3-solver". z3 is installed only for z3-solver config.

.github/workflows/test.yml

@@ -13,6 +13,7 @@ jobs:
     strategy:
       matrix:
         python-version: ["3.9", "3.10", "3.11", "3.12", "3.13"]
+        dependency: ["base", "z3-solver"]
 
     steps:
       - uses: actions/[email protected]
@@ -38,11 +39,29 @@ jobs:
       - name: Install dependencies
         run: |
           python -m pip install --upgrade pip setuptools wheel
-          pip install -e .[dev,cfg,z3]
+          pip install -e .[dev,cfg]
+          if [ "${{ matrix.dependency }}" == "z3-solver" ]; then
+            pip install .[z3]
+          fi
       - name: Run tests
         run: |
-          pytest -vv --cov python_ta --cov-config=.coveragerc --cov-report lcov --ignore=tests/test_type_constraints --ignore=tests/test_type_inference tests --ignore=tests/test_debug/test_accumulation_table.py --ignore=tests/test_debug/test_recursion_table.py --ignore=tests/test_debug/test_snapshot_tracer.py
-          pytest -vv tests/test_debug/test_accumulation_table.py tests/test_debug/test_recursion_table.py tests/test_debug/test_snapshot_tracer.py
+          if [ "${{ matrix.dependency }}" == "z3-solver" ]; then
+            pytest -vv --cov python_ta --cov-config=.coveragerc --cov-report lcov \
+            --ignore=tests/test_type_constraints \
+            --ignore=tests/test_type_inference \
+            --ignore=tests/test_debug/test_accumulation_table.py \
+            --ignore=tests/test_debug/test_recursion_table.py \
+            --ignore=tests/test_debug/test_snapshot_tracer.py
+            pytest -vv tests/test_debug/test_accumulation_table.py tests/test_debug/test_recursion_table.py tests/test_debug/test_snapshot_tracer.py
+          else
+            pytest -vv --cov python_ta --cov-config=.coveragerc --cov-report lcov --exclude-z3 \
+            --ignore=tests/test_type_constraints \
+            --ignore=tests/test_type_inference \
+            --ignore=tests/test_debug/test_accumulation_table.py \
+            --ignore=tests/test_debug/test_recursion_table.py \
+            --ignore=tests/test_debug/test_snapshot_tracer.py
+            pytest -vv tests/test_debug/test_accumulation_table.py tests/test_debug/test_recursion_table.py tests/test_debug/test_snapshot_tracer.py
+          fi
       - name: Upload test coverage to coveralls.io
         uses: coverallsapp/[email protected]
         env:

CHANGELOG.md

@@ -18,6 +18,8 @@ and adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
 ### 🔧 Internal changes
 
+- Configured CI tests to run on environments with and without `z3` dependency.
+
 ## [2.9.1] - 2024-12-09
 
 ### 🐛 Bug fixes

tests/conftest.py

@@ -1,9 +1,24 @@
+import re
 from http.server import HTTPServer
 
 import pytest
 
 import python_ta.contracts
 
+Z3_RELATED_TESTS = {
+    r".*test_z3_constraints.*",
+    r".*test_edge_feasibility.*",
+    r".*test_impossible_condition_checker.*",
+    r".*test_redundant_condition_checker.*",
+    r".*test_z3_parser.*",
+    r".*test_z3_visitor.*",
+    r".*test_inconsistent_returns.*",
+    r".*test_missing_return_statements.*",
+    r".*test_one_iteration_checker.*",
+    r".*test_possibly_undefined_checker.*",
+    r".*test_redundant_assignment_checker.*",
+}
+
 
 @pytest.fixture()
 def disable_contract_checking():
@@ -27,3 +42,39 @@ def prevent_webbrowser_and_httpserver(mocker):
     code running when running Pytest to avoid CI timeouts, and unexpected browser popups."""
     mocker.patch("webbrowser.open", return_value=None)
     mocker.patch.object(HTTPServer, "handle_request", return_value=None)
+
+
+def pytest_addoption(parser):
+    """Custom command-line options to enable/disable exclusion of certain tests"""
+    parser.addoption(
+        "--exclude-z3",
+        action="store_true",
+        default=False,
+        help="Exclude test cases the require z3 dependency.",
+    )
+
+
+def pytest_ignore_collect(path, config):
+    """Return True to prevent collecting a test file or directory.
+    Note: this function must return None for test cases not intended to exclude. Otherwise, it will interfere
+    with other configurations such as --exclude flag.
+
+    Refer to the following docstring in Pytest source code:
+
+    Return ``True`` to ignore this path for collection.
+
+    Return ``None`` to let other plugins ignore the path for collection.
+
+    Returning ``False`` will forcefully *not* ignore this path for collection,
+    without giving a chance for other plugins to ignore this path.
+    https://github.com/pytest-dev/pytest/blob/main/src/_pytest/hookspec.py
+    """
+    if config.getoption("--exclude-z3"):
+        # Convert path to string for pattern matching
+        path_str = str(path)
+        if any(re.search(pattern, path_str) for pattern in Z3_RELATED_TESTS):
+            return True
+        else:
+            return None
+
+    return None

tests/test_examples.py

@@ -38,6 +38,9 @@
     "e9950_forbidden_python_syntax.py",
 ]
 
+# The following tests require z3-solver as dependency
+Z3_RELATED_TESTS = ["r9900_redundant_condition.py", "r9901_impossible_condition.py"]
+
 
 def get_file_paths(paths: Union[str, list[str]]) -> list[str]:
     """
@@ -54,10 +57,21 @@ def get_file_paths(paths: Union[str, list[str]]) -> list[str]:
     if isinstance(paths, str):
         paths = [paths]
 
+    # check if z3 dependency is available
+    z3_dependency_available = True
+    try:
+        import z3
+    except ImportError:
+        z3_dependency_available = False
+
     for path in paths:
         for root, _, files in os.walk(path, topdown=True):
             for filename in files:
-                if filename not in IGNORED_TESTS and filename.endswith(".py"):
+                if (
+                    filename not in IGNORED_TESTS
+                    and filename.endswith(".py")
+                    and (z3_dependency_available or filename not in Z3_RELATED_TESTS)
+                ):
                     full_path = os.path.join(root, filename)
                     rel_path = os.path.relpath(full_path, path)
                     test_files.append(os.path.join(path, rel_path))