Bound ASPIC property-test theories and pin the #102 argument budget

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 ─────────────────

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