From 12824efa0807f3c3a652dfc78342ba608faff10d Mon Sep 17 00:00:00 2001 From: Christopher Toth Date: Sun, 27 Sep 2026 02:00:24 -0600 Subject: [PATCH 1/2] fix: accept differing valid witnesses in the solver differential helper The helper required identical single-extension witnesses and acceptance certificates, so native {a} and SAT {c}, both stage extensions, were reported as a semantic disagreement. Witnesses are choices: differing ones now agree when each is an extension in reference_extensions (and, for acceptance, contains or omits the query as required). Answers and extension existence must still match, and differing witnesses without a reference set fail with an explicit message. Closes #73 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01V4tAVyyKcs1sYcsEzL7Bzg --- .../solving/solver_differential.py | 74 ++++++++- .../test_solver_differential_witnesses.py | 152 ++++++++++++++++++ 2 files changed, 222 insertions(+), 4 deletions(-) create mode 100644 tests/solving/test_solver_differential_witnesses.py 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", + ) From 11877bd1a28bb241a6e08d653f33b3a99233d5c7 Mon Sep 17 00:00:00 2001 From: Christopher Toth Date: Sun, 27 Sep 2026 02:04:35 -0600 Subject: [PATCH 2/2] test: drop the wall-clock deadline from ABA shape property tests These properties check shape invariants, not speed, but ran under Hypothesis's 200 ms deadline while some generated frameworks take several hundred ms (observed 251-286 ms failures, 0-611 ms typical runtimes), so they failed with DeadlineExceeded under load. The module now uses one settings object with deadline=None and the same max_examples=40; the global Hypothesis default is unchanged. Closes #95 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01V4tAVyyKcs1sYcsEzL7Bzg --- .../aba/test_aba_shape_properties.py | 28 +++++++++++-------- 1 file changed, 17 insertions(+), 11 deletions(-) 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: