From 71da294cb63afd1d9e35a40b02290d775a3fd149 Mon Sep 17 00:00:00 2001 From: Christopher Toth Date: Sun, 27 Sep 2026 12:47:52 -0600 Subject: [PATCH] test: bound ASPIC property-test theories and pin the #102 argument budget The ASPIC strict/defeasible rule generators drew antecedents with replacement. A seed like ~q, ~q -> p, plus its positional transpositions, multiplied arguments to 18,850 (~306M attacks) on a 4-premise theory; once saved in a local Hypothesis database it replayed into the 600s timeout on every run. - Rule generators draw distinct antecedents in canonical order. - knowledge_base and well_defined_knowledge_base reject theories whose argument set (built without contrariness, an upper bound) exceeds 2,000, so no saved example can replay a blow-up. - The #102 theory is pinned with a deterministic operational contract (<= 200 arguments, <= 20,000 attack pairs counted from per-conclusion argument counts without compute_attacks), xfail(strict=True) until the production fix lands; it fails in about 0.5s instead of timing out. Refs #102 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01V4tAVyyKcs1sYcsEzL7Bzg --- tests/structured/aspic/test_aspic.py | 52 ++++++- .../aspic/test_aspic_argument_budget.py | 135 ++++++++++++++++++ 2 files changed, 182 insertions(+), 5 deletions(-) create mode 100644 tests/structured/aspic/test_aspic_argument_budget.py diff --git a/tests/structured/aspic/test_aspic.py b/tests/structured/aspic/test_aspic.py index a5d2846..69b0868 100644 --- a/tests/structured/aspic/test_aspic.py +++ b/tests/structured/aspic/test_aspic.py @@ -290,6 +290,44 @@ def test_asymmetric_contrary_generates_one_way_attack(self): # ── Phase 2: Rule strategies ───────────────────────────────────── +def _distinct_antecedents( + draw, literals: list[Literal], count: int +) -> tuple[Literal, ...]: + """Draw ``count`` distinct antecedents in canonical order. + + Repeated antecedents (``~q, ~q -> p``) and their positional + transpositions multiply arguments combinatorially: issue #102 found a + 4-premise theory with 18,850 arguments and ~306M attacks. Distinct, + sorted antecedents keep generated theories small. + """ + chosen = draw( + st.lists(st.sampled_from(literals), min_size=count, max_size=count, unique=True) + ) + return tuple(sorted(chosen, key=repr)) + + +# Property tests discard theories with more arguments than this, so a saved +# Hypothesis example cannot replay a combinatorial blow-up (issue #102). +MAX_GENERATED_ARGUMENTS = 2000 + + +def _assume_bounded_arguments( + language: frozenset[Literal], + strict: frozenset[Rule], + defeasible: frozenset[Rule], + kb: KnowledgeBase, +) -> None: + """Reject theories whose argument set exceeds MAX_GENERATED_ARGUMENTS. + + Built with an empty contrariness function: no argument is filtered as + c-inconsistent, so this count bounds the real argument set from above. + """ + unfiltered = ArgumentationSystem( + language, ContrarinessFn(frozenset()), frozenset(strict), frozenset(defeasible) + ) + assume(len(build_arguments(unfiltered, kb)) <= MAX_GENERATED_ARGUMENTS) + + @st.composite def strict_rules(draw, language, contrariness, max_rules=4): """Generate strict rules over L with transposition closure. @@ -308,7 +346,7 @@ def strict_rules(draw, language, contrariness, max_rules=4): seed_rules: list[Rule] = [] for _ in range(n_rules): n_ante = draw(st.integers(min_value=1, max_value=min(2, len(L_list)))) - antecedents = tuple(draw(st.sampled_from(L_list)) for _ in range(n_ante)) + antecedents = _distinct_antecedents(draw, L_list, n_ante) consequent = draw(st.sampled_from(L_list)) # Filter: consequent must not appear in antecedents if consequent in antecedents: @@ -337,7 +375,7 @@ def strict_seed_rules(draw, language, contrariness, max_rules=4): seed_rules: list[Rule] = [] for _ in range(n_rules): n_ante = draw(st.integers(min_value=1, max_value=min(2, len(L_list)))) - antecedents = tuple(draw(st.sampled_from(L_list)) for _ in range(n_ante)) + antecedents = _distinct_antecedents(draw, L_list, n_ante) consequent = draw(st.sampled_from(L_list)) if consequent in antecedents: continue @@ -432,7 +470,7 @@ def defeasible_rules(draw, language, max_rules=4): rules: list[Rule] = [] for i in range(n_rules): n_ante = draw(st.integers(min_value=1, max_value=min(2, len(L_list)))) - antecedents = tuple(draw(st.sampled_from(L_list)) for _ in range(n_ante)) + antecedents = _distinct_antecedents(draw, L_list, n_ante) consequent = draw(st.sampled_from(L_list)) # Filter: consequent must not appear in antecedents if consequent in antecedents: @@ -932,7 +970,9 @@ def knowledge_base(draw, language, strict_rules, defeasible_rules): # Ensure K_n and K_p are disjoint K_n = K_n - K_p - return KnowledgeBase(axioms=K_n, premises=K_p) + kb = KnowledgeBase(axioms=K_n, premises=K_p) + _assume_bounded_arguments(language, strict_rules, defeasible_rules, kb) + return kb @st.composite @@ -975,7 +1015,9 @@ def well_defined_knowledge_base( # This keeps the rationality-postulate generators on genuinely well-defined # c-SAF inputs even when Hypothesis shrinks toward edge cases. assume(is_c_consistent(K_n | K_p, strict_rules, contrariness)) - return KnowledgeBase(axioms=K_n, premises=K_p) + kb = KnowledgeBase(axioms=K_n, premises=K_p) + _assume_bounded_arguments(language, strict_rules, defeasible_rules, kb) + return kb # ── Phase 3: Argument construction property tests ───────────────── diff --git a/tests/structured/aspic/test_aspic_argument_budget.py b/tests/structured/aspic/test_aspic_argument_budget.py new file mode 100644 index 0000000..d5f647a --- /dev/null +++ b/tests/structured/aspic/test_aspic_argument_budget.py @@ -0,0 +1,135 @@ +"""Operational contract for ASPIC+ argument multiplication (issue #102). + +Per this repository's AGENTS.md, a performance-shaped defect gets a +deterministic budget that fails fast instead of timing out. The attack count +is computed from per-conclusion argument counts (every argument concluding a +conflicting literal attacks each rebuttable or underminable sub-argument, +Modgil & Prakken 2018, Def 8, p.11) without calling ``compute_attacks``. +""" + +from __future__ import annotations + +from collections import Counter + +import pytest + +from argumentation.structured.aspic.aspic import ( + Argument, + ArgumentationSystem, + ContrarinessFn, + GroundAtom, + KnowledgeBase, + Literal, + PremiseArg, + Rule, + build_arguments, + conc, + is_firm, + is_strict, + sub, + top_rule, +) + +ARGUMENT_BUDGET = 200 +ATTACK_PAIR_BUDGET = 20_000 + + +def _attack_pair_count( + system: ArgumentationSystem, arguments: frozenset[Argument] +) -> int: + by_conclusion = Counter(conc(argument) for argument in arguments) + contrariness = system.contrariness + + def attackers_of(target: Literal) -> int: + return sum( + count + for literal, count in by_conclusion.items() + if contrariness.is_contradictory(literal, target) + or contrariness.is_contrary(literal, target) + ) + + pairs = 0 + for argument in arguments: + for sub_argument in sub(argument): + if is_firm(sub_argument) and is_strict(sub_argument): + continue + if isinstance(sub_argument, PremiseArg) and not sub_argument.is_axiom: + pairs += attackers_of(sub_argument.premise) + rule = top_rule(sub_argument) + if rule is not None and rule.kind == "defeasible": + pairs += attackers_of(conc(sub_argument)) + return pairs + + +def _issue_102_theory() -> tuple[ArgumentationSystem, KnowledgeBase]: + """The Hypothesis-shrunk theory from #102: 4 ordinary premises, 11 strict + rules (including ``~q, ~q -> p`` and permuted duplicates) and 3 + defeasible rules.""" + p, q, r, s = (Literal(GroundAtom(name)) for name in "pqrs") + not_p, not_q, not_r, not_s = (atom.contrary for atom in (p, q, r, s)) + strict = frozenset( + Rule(body, head, "strict") + for body, head in [ + ((p,), not_s), + ((q, not_r), s), + ((q, not_s), r), + ((s,), not_p), + ((not_p, not_q), q), + ((not_q, not_p), q), + ((not_q, not_q), p), + ((not_r, q), s), + ((not_r, not_s), not_q), + ((not_s, q), r), + ((not_s, not_r), not_q), + ] + ) + defeasible = frozenset( + { + Rule((r, q), not_r, "defeasible", "d0"), + Rule((s,), q, "defeasible", "d3"), + Rule((not_p,), not_s, "defeasible", "d1"), + } + ) + system = ArgumentationSystem( + frozenset({p, q, r, s, not_p, not_q, not_r, not_s}), + ContrarinessFn(frozenset((atom, atom.contrary) for atom in (p, q, r, s))), + strict, + defeasible, + ) + return system, KnowledgeBase( + axioms=frozenset(), premises=frozenset({q, s, not_p, not_r}) + ) + + +@pytest.mark.xfail( + strict=True, + reason="#102: argument multiplication; 18,850 arguments and ~306M attacks " + "until rule canonicalisation (option A) lands", +) +def test_issue_102_theory_stays_within_argument_and_attack_budget() -> None: + """Refs #102: the theory must build at most 200 arguments and at most + 20,000 attack pairs (98 and 7,226 under antecedent-set rules).""" + system, kb = _issue_102_theory() + + arguments = build_arguments(system, kb) + + assert len(arguments) <= ARGUMENT_BUDGET + assert _attack_pair_count(system, arguments) <= ATTACK_PAIR_BUDGET + + +def test_small_theory_within_budget_control() -> None: + """Control: a theory with distinct antecedents (q, ~r -> s; s => q) is + well inside the budget.""" + q, r, s = (Literal(GroundAtom(name)) for name in "qrs") + system = ArgumentationSystem( + frozenset({q, r, s, q.contrary, r.contrary, s.contrary}), + ContrarinessFn(frozenset((atom, atom.contrary) for atom in (q, r, s))), + frozenset({Rule((q, r.contrary), s, "strict")}), + frozenset({Rule((s,), q, "defeasible", "d3")}), + ) + kb = KnowledgeBase(axioms=frozenset(), premises=frozenset({q, r.contrary})) + + arguments = build_arguments(system, kb) + + assert len(arguments) <= ARGUMENT_BUDGET + assert _attack_pair_count(system, arguments) <= ATTACK_PAIR_BUDGET