From e682d696a978a04b9541184ae1c798086c3115a3 Mon Sep 17 00:00:00 2001
From: Raine-Yang-UofT <raine.yang@mail.utoronto.ca>
Date: Tue, 31 Dec 2024 20:39:29 -0400
Subject: [PATCH] fix: handle exclude z3 in collection stage

Fix regex for matching z3-related modules
Exclude z3 tests in test_examples
---
 tests/conftest.py      | 34 ++++++++++++----------------------
 tests/test_examples.py | 16 +++++++++++++++-
 2 files changed, 27 insertions(+), 23 deletions(-)

diff --git a/tests/conftest.py b/tests/conftest.py
index 9d2a8f4c4..f0921e45a 100644
--- a/tests/conftest.py
+++ b/tests/conftest.py
@@ -6,16 +6,17 @@
 import python_ta.contracts
 
 Z3_RELATED_TESTS = {
-    r"tests/test_z3_constraints\.py",
-    r"tests/test_edge_feasibility\.py",
-    r"tests/test_impossible_condition_checker\.py",
-    r"tests/test_redundant_condition_checker\.py",
-    r"tests/test_z3_parser\.py",
-    r".*TestInconsistentReturnCheckerZ3Option.*",
-    r".*TestMissingReturnCheckerZ3Option.*",
-    r".*TestOneIterationCheckerZ3Option.*",
-    r".*TestPossiblyUndefinedCheckerZ3Option.*",
-    r".*TestRedundantAssignmentCheckerZ3Option.*",
+    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.*",
 }
 
 
@@ -60,16 +61,5 @@ def pytest_ignore_collect(path, config):
 
     # Convert path to string for pattern matching
     path_str = str(path)
+    print(path_str)
     return any(re.search(pattern, path_str) for pattern in Z3_RELATED_TESTS)
-
-
-def pytest_collection_modifyitems(config, items):
-    """Modify collected test items to exclude certain tests based on configuration."""
-    if not config.getoption("--exclude-z3"):
-        return
-
-    skip_marker = pytest.mark.skip(reason="Only run when z3-solver is installed")
-    for item in items:
-        # Check if the test's nodeid matches any Z3-related patterns
-        if any(re.search(pattern, item.nodeid) for pattern in Z3_RELATED_TESTS):
-            item.add_marker(skip_marker)
diff --git a/tests/test_examples.py b/tests/test_examples.py
index c38e4d8c3..4cc3429ac 100644
--- a/tests/test_examples.py
+++ b/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))