Accept valid differing solver witnesses; drop ABA shape property deadline

src/argumentation/solving/solver_differential.py

@@ -2,6 +2,7 @@
 
 from __future__ import annotations
 
+from collections.abc import Collection
 from dataclasses import dataclass
 import json
 from pathlib import Path
@@ -52,8 +53,20 @@ def assert_solver_results_agree(
     task: SolverTask,
     expected: SolverResult,
     actual: SolverResult,
+    *,
+    reference_extensions: Collection[frozenset[object]] | None = None,
+    query: object | None = None,
 ) -> None:
-    """Assert two solver results are comparable and semantically equal."""
+    """Assert two solver results are comparable and semantically equal.
+
+    Single-extension witnesses and acceptance certificates are choices: a
+    solver may return any extension of the semantics, and any extension that
+    contains (credulous witness) or omits (skeptical counterexample) the
+    query. Differing choices therefore agree when each is valid against
+    ``reference_extensions``, the full extension set of the semantics.
+    Identical choices need no reference; differing ones cannot be judged
+    without it. Acceptance certificates are validated with ``query``.
+    """
     if task == "enumeration":
         if isinstance(expected, SingleExtensionSolverSuccess) or isinstance(
             actual, SingleExtensionSolverSuccess
@@ -82,7 +95,13 @@ def assert_solver_results_agree(
             raise AssertionError(
                 "single-extension comparison requires two single-extension successes"
             )
-        assert expected.extension == actual.extension
+        if (expected.extension is None) != (actual.extension is None):
+            raise AssertionError("solvers disagree on whether an extension exists")
+        _validate_certificates(
+            "single-extension witness",
+            _present(expected.extension, actual.extension),
+            reference_extensions,
+        )
         return
     if task == "acceptance":
         if not isinstance(expected, AcceptanceSolverSuccess) or not isinstance(
@@ -92,12 +111,59 @@ def assert_solver_results_agree(
                 "acceptance comparison requires two acceptance successes"
             )
         assert expected.answer is actual.answer
-        assert expected.witness == actual.witness
-        assert expected.counterexample == actual.counterexample
+        witnesses = _present(expected.witness, actual.witness)
+        counterexamples = _present(expected.counterexample, actual.counterexample)
+        _validate_certificates("credulous witness", witnesses, reference_extensions)
+        _validate_certificates(
+            "skeptical counterexample", counterexamples, reference_extensions
+        )
+        if reference_extensions is not None and (witnesses or counterexamples):
+            if query is None:
+                raise AssertionError("acceptance certificates need the query")
+            for witness in witnesses:
+                if query not in witness:
+                    raise AssertionError(
+                        f"credulous witness {sorted(map(repr, witness))} "
+                        f"does not contain the query {query!r}"
+                    )
+            for counterexample in counterexamples:
+                if query in counterexample:
+                    raise AssertionError(
+                        f"skeptical counterexample {sorted(map(repr, counterexample))} "
+                        f"contains the query {query!r}"
+                    )
         return
     raise ValueError(f"unsupported solver differential task: {task}")
 
 
+def _present(
+    *certificates: frozenset[object] | None,
+) -> tuple[frozenset[object], ...]:
+    return tuple(certificate for certificate in certificates if certificate is not None)
+
+
+def _validate_certificates(
+    label: str,
+    certificates: tuple[frozenset[object], ...],
+    reference_extensions: Collection[frozenset[object]] | None,
+) -> None:
+    """Require each certificate to be an extension, or all to be identical."""
+    if reference_extensions is None:
+        if len(set(certificates)) > 1:
+            raise AssertionError(
+                f"differing {label}s {certificates!r} cannot be validated "
+                "without reference_extensions"
+            )
+        return
+    reference = {frozenset(extension) for extension in reference_extensions}
+    for certificate in certificates:
+        if frozenset(certificate) not in reference:
+            raise AssertionError(
+                f"{label} {sorted(map(repr, certificate))} is not an extension "
+                "of the reference semantics"
+            )
+
+
 def load_benchmark_manifest(path: Path) -> tuple[BenchmarkCase, ...]:
     """Load a tiny benchmark manifest fixture without touching solver binaries."""
     payload = json.loads(path.read_text(encoding="utf-8"))

tests/solving/test_solver_differential_witnesses.py

@@ -0,0 +1,152 @@
+"""Differential comparison must accept any valid witness, not one fixed choice.
+
+Stage extensions are conflict-free sets with subset-maximal range (Dvorak et
+al. 2014, Def 3; papers/Dvorak_2014_ComplexitySensitiveDecisionProcedures/
+notes.md). A single-extension solver may return any of them, and a credulous
+witness may be any extension containing the query.
+"""
+
+from __future__ import annotations
+
+import pytest
+
+from argumentation.core.dung import ArgumentationFramework
+from argumentation.solving.solver import (
+    AcceptanceSolverSuccess,
+    SingleExtensionSolverSuccess,
+    solve_dung_extensions,
+    solve_dung_single_extension,
+)
+from argumentation.solving.solver_differential import assert_solver_results_agree
+
+# b attacks itself, a attacks c, c attacks b: the stage extensions are {a}
+# (range {a, c}) and {c} (range {b, c}).
+STAGE_FRAMEWORK = ArgumentationFramework(
+    frozenset("abc"), frozenset({("b", "b"), ("a", "c"), ("c", "b")})
+)
+
+
+def _stage_extensions() -> tuple[frozenset[str], ...]:
+    result = solve_dung_extensions(STAGE_FRAMEWORK, semantics="stage", backend="native")
+    return tuple(result.extensions)  # type: ignore[union-attr]
+
+
+def test_single_extension_accepts_different_valid_witnesses() -> None:
+    """Issue #73: native and SAT may pick different stage extensions."""
+    reference = _stage_extensions()
+    assert set(reference) == {frozenset({"a"}), frozenset({"c"})}
+
+    assert_solver_results_agree(
+        "single-extension",
+        SingleExtensionSolverSuccess(frozenset({"a"})),
+        SingleExtensionSolverSuccess(frozenset({"c"})),
+        reference_extensions=reference,
+    )
+
+
+def test_single_extension_solvers_agree_on_issue_framework() -> None:
+    """Issue #73 reproduction with the real backends."""
+    native = solve_dung_single_extension(
+        STAGE_FRAMEWORK, semantics="stage", backend="native"
+    )
+    sat = solve_dung_single_extension(STAGE_FRAMEWORK, semantics="stage", backend="sat")
+
+    assert_solver_results_agree(
+        "single-extension", native, sat, reference_extensions=_stage_extensions()
+    )
+
+
+def test_single_extension_rejects_witness_that_is_not_an_extension() -> None:
+    """Issue #73 control: {b} is not conflict-free (b attacks b), so it is
+    no stage extension and the comparison must still fail."""
+    with pytest.raises(AssertionError, match="not an extension"):
+        assert_solver_results_agree(
+            "single-extension",
+            SingleExtensionSolverSuccess(frozenset({"a"})),
+            SingleExtensionSolverSuccess(frozenset({"b"})),
+            reference_extensions=_stage_extensions(),
+        )
+
+
+def test_single_extension_differing_witnesses_need_reference() -> None:
+    """Issue #73: without reference extensions, differing witnesses cannot be
+    validated, so the helper says so instead of reporting a disagreement."""
+    with pytest.raises(AssertionError, match="reference_extensions"):
+        assert_solver_results_agree(
+            "single-extension",
+            SingleExtensionSolverSuccess(frozenset({"a"})),
+            SingleExtensionSolverSuccess(frozenset({"c"})),
+        )
+
+
+def test_single_extension_rejects_existence_disagreement() -> None:
+    """Issue #73 control: one solver finding no extension is a real disagreement."""
+    with pytest.raises(AssertionError, match="whether an extension exists"):
+        assert_solver_results_agree(
+            "single-extension",
+            SingleExtensionSolverSuccess(frozenset({"a"})),
+            SingleExtensionSolverSuccess(None),
+            reference_extensions=_stage_extensions(),
+        )
+
+
+def test_single_extension_identical_witnesses_need_no_reference() -> None:
+    """Issue #73 control: identical witnesses agree as before."""
+    assert_solver_results_agree(
+        "single-extension",
+        SingleExtensionSolverSuccess(frozenset({"a"})),
+        SingleExtensionSolverSuccess(frozenset({"a"})),
+    )
+
+
+def test_acceptance_accepts_different_valid_credulous_witnesses() -> None:
+    """Issue #73: any extension containing the query is a valid credulous
+    witness, so {a, d} and {c, d} both certify that d is accepted."""
+    reference = (frozenset({"a", "d"}), frozenset({"c", "d"}))
+
+    assert_solver_results_agree(
+        "acceptance",
+        AcceptanceSolverSuccess(answer=True, witness=frozenset({"a", "d"})),
+        AcceptanceSolverSuccess(answer=True, witness=frozenset({"c", "d"})),
+        reference_extensions=reference,
+        query="d",
+    )
+
+
+def test_acceptance_accepts_different_valid_skeptical_counterexamples() -> None:
+    """Issue #73: any extension omitting the query refutes skeptical acceptance."""
+    reference = (frozenset({"a"}), frozenset({"c"}), frozenset({"a", "d"}))
+
+    assert_solver_results_agree(
+        "acceptance",
+        AcceptanceSolverSuccess(answer=False, counterexample=frozenset({"a"})),
+        AcceptanceSolverSuccess(answer=False, counterexample=frozenset({"c"})),
+        reference_extensions=reference,
+        query="d",
+    )
+
+
+def test_acceptance_rejects_witness_without_query() -> None:
+    """Issue #73 control: a credulous witness must contain the query."""
+    reference = (frozenset({"a"}), frozenset({"c", "d"}))
+
+    with pytest.raises(AssertionError, match="does not contain the query"):
+        assert_solver_results_agree(
+            "acceptance",
+            AcceptanceSolverSuccess(answer=True, witness=frozenset({"c", "d"})),
+            AcceptanceSolverSuccess(answer=True, witness=frozenset({"a"})),
+            reference_extensions=reference,
+            query="d",
+        )
+
+
+def test_acceptance_rejects_different_answers() -> None:
+    """Issue #73 control: the answers themselves must still agree."""
+    with pytest.raises(AssertionError):
+        assert_solver_results_agree(
+            "acceptance",
+            AcceptanceSolverSuccess(answer=True, witness=frozenset({"a"})),
+            AcceptanceSolverSuccess(answer=False, counterexample=frozenset({"c"})),
+            reference_extensions=(frozenset({"a"}), frozenset({"c"})),
+            query="a",
+        )

tests/structured/aba/test_aba_shape_properties.py

@@ -14,17 +14,23 @@
 )
 from tools.aba_shape_benchmark import compute_aba_shape, shape_buckets
 
+# These properties check shape invariants, not speed. Some generated
+# frameworks legitimately take several hundred ms, so Hypothesis's 200 ms
+# wall-clock deadline only produced load-dependent DeadlineExceeded flakes
+# (issue #95). The global Hypothesis default is left unchanged.
+_SHAPE_PROPERTY_SETTINGS = settings(max_examples=40, deadline=None)
+
 
 @given(flat_aba_frameworks())
-@settings(max_examples=40)
+@_SHAPE_PROPERTY_SETTINGS
 def test_renaming_preserves_every_shape_field(framework: ABAFramework) -> None:
     renamed, _ = renamed_framework(framework)
 
     assert compute_aba_shape(renamed) == compute_aba_shape(framework)
 
 
 @given(flat_aba_frameworks())
-@settings(max_examples=40)
+@_SHAPE_PROPERTY_SETTINGS
 def test_renaming_preserves_bucketed_shape_fields(framework: ABAFramework) -> None:
     renamed, _ = renamed_framework(framework)
     solver_class = "aba/single-extension/preferred"
@@ -36,7 +42,7 @@ def test_renaming_preserves_bucketed_shape_fields(framework: ABAFramework) -> No
 
 
 @given(flat_aba_specs())
-@settings(max_examples=40)
+@_SHAPE_PROPERTY_SETTINGS
 def test_permuting_rules_preserves_shape(spec) -> None:
     forward = spec.to_framework()
     reversed_rules = ABAFramework(
@@ -50,7 +56,7 @@ def test_permuting_rules_preserves_shape(spec) -> None:
 
 
 @given(flat_aba_specs())
-@settings(max_examples=40)
+@_SHAPE_PROPERTY_SETTINGS
 def test_permuting_contrary_declarations_preserves_shape(spec) -> None:
     framework = spec.to_framework()
     reversed_contrary = dict(reversed(tuple(spec.contrary.items())))
@@ -65,7 +71,7 @@ def test_permuting_contrary_declarations_preserves_shape(spec) -> None:
 
 
 @given(flat_aba_frameworks())
-@settings(max_examples=40)
+@_SHAPE_PROPERTY_SETTINGS
 def test_adding_unreachable_rule_preserves_grounded_and_acyclic_fields(
     framework: ABAFramework,
 ) -> None:
@@ -86,7 +92,7 @@ def test_adding_unreachable_rule_preserves_grounded_and_acyclic_fields(
 
 
 @given(flat_aba_frameworks(max_rules=6))
-@settings(max_examples=40)
+@_SHAPE_PROPERTY_SETTINGS
 def test_duplicate_semantic_rule_changes_density_not_boolean_shape(
     framework: ABAFramework,
 ) -> None:
@@ -110,7 +116,7 @@ def test_duplicate_semantic_rule_changes_density_not_boolean_shape(
 
 
 @given(flat_aba_frameworks())
-@settings(max_examples=40)
+@_SHAPE_PROPERTY_SETTINGS
 def test_removing_zero_body_facts_cannot_increase_closure_size(
     framework: ABAFramework,
 ) -> None:
@@ -127,15 +133,15 @@ def test_removing_zero_body_facts_cannot_increase_closure_size(
 
 
 @given(flat_aba_frameworks())
-@settings(max_examples=40)
+@_SHAPE_PROPERTY_SETTINGS
 def test_p_acyclicity_matches_independent_dependency_graph(
     framework: ABAFramework,
 ) -> None:
     assert compute_aba_shape(framework).p_acyclic is _paper_p_acyclic(framework)
 
 
 @given(flat_aba_frameworks())
-@settings(max_examples=40)
+@_SHAPE_PROPERTY_SETTINGS
 def test_scc_count_and_size_match_independent_graph(framework: ABAFramework) -> None:
     components = _independent_sccs(framework)
     shape = compute_aba_shape(framework)
@@ -147,7 +153,7 @@ def test_scc_count_and_size_match_independent_graph(framework: ABAFramework) ->
 
 
 @given(flat_aba_specs())
-@settings(max_examples=40)
+@_SHAPE_PROPERTY_SETTINGS
 def test_contrary_target_in_degree_is_invariant_under_order_and_renaming(spec) -> None:
     framework = spec.to_framework()
     permuted = ABAFramework(
@@ -168,7 +174,7 @@ def test_contrary_target_in_degree_is_invariant_under_order_and_renaming(spec) -
 
 
 @given(flat_aba_frameworks())
-@settings(max_examples=40)
+@_SHAPE_PROPERTY_SETTINGS
 def test_closure_growth_is_monotone_when_adding_assumptions(
     framework: ABAFramework,
 ) -> None: