diff --git a/src/argumentation/solving/solver_differential.py b/src/argumentation/solving/solver_differential.py index f0aa9e9..159227b 100644 --- a/src/argumentation/solving/solver_differential.py +++ b/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")) diff --git a/tests/solving/test_solver_differential_witnesses.py b/tests/solving/test_solver_differential_witnesses.py new file mode 100644 index 0000000..7922a83 --- /dev/null +++ b/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", + ) diff --git a/tests/structured/aba/test_aba_shape_properties.py b/tests/structured/aba/test_aba_shape_properties.py index 982312b..0a6a51c 100644 --- a/tests/structured/aba/test_aba_shape_properties.py +++ b/tests/structured/aba/test_aba_shape_properties.py @@ -14,9 +14,15 @@ ) 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) @@ -24,7 +30,7 @@ def test_renaming_preserves_every_shape_field(framework: ABAFramework) -> None: @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,7 +133,7 @@ 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: @@ -135,7 +141,7 @@ def test_p_acyclicity_matches_independent_dependency_graph( @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: