diff --git a/tests/test_pi_star_logic.py b/tests/test_pi_star_logic.py new file mode 100644 index 0000000..31fd50b --- /dev/null +++ b/tests/test_pi_star_logic.py @@ -0,0 +1,276 @@ +"""logic-kernel@v1 π* tests. + +Propositional-logic CNF canonicalizer. KATs mirror the docstring's +equivalence-class examples: commutativity, associativity, IMPL/IFF/ +XOR rewrites, De Morgan, double negation, distribution, tautology / +contradiction collapse, idempotence. Plus negative cones (>8 atoms, +unrecognized tokens, unconsumed tokens, empty, non-bytes) and round- +trip idempotence. + +Backfills the test-coverage gap for arborist/pi_star/logic.py +identified during the 2026-05-10 zero-coverage sweep. +""" + +from __future__ import annotations + +import pytest + +from arborist.pi_star import get +from arborist.pi_star.protocol import ( + PiStarError, + assert_round_trip, + equivalence_class_id, +) + + +@pytest.fixture +def ps(): + return get("logic-kernel@v1") + + +def _canon(ps, expr: str) -> bytes: + return ps.canonicalize(expr.encode("utf-8")) + + +# --- registry presence + metadata ------------------------------------ + + +def test_registry_contains_logic_kernel(): + ps = get("logic-kernel@v1") + assert ps.name == "logic-kernel" + assert ps.version == "v1" + assert ps.domain == "logic" + + +# --- atom + literal serialization ------------------------------------ + + +def test_single_atom(ps): + assert _canon(ps, "A") == b"A" + + +def test_negated_atom(ps): + assert _canon(ps, "NOT A") == b"NOT A" + + +def test_true_literal(ps): + assert _canon(ps, "TRUE") == b"TRUE" + + +def test_false_literal(ps): + assert _canon(ps, "FALSE") == b"FALSE" + + +# --- equivalence classes preserved ----------------------------------- + + +@pytest.mark.parametrize( + "a,b", + [ + # commutativity of AND / OR + ("A AND B", "B AND A"), + ("A OR B", "B OR A"), + # associativity + ("(A AND B) AND C", "A AND (B AND C)"), + ("(A OR B) OR C", "A OR (B OR C)"), + # IMPL rewrite + ("A IMPL B", "NOT A OR B"), + # IFF rewrite + ("A IFF B", "(NOT A OR B) AND (NOT B OR A)"), + # XOR rewrite + ("A XOR B", "(A OR B) AND (NOT A OR NOT B)"), + # De Morgan + ("NOT (A AND B)", "NOT A OR NOT B"), + ("NOT (A OR B)", "NOT A AND NOT B"), + # double negation + ("NOT NOT A", "A"), + # distribution + ("A OR (B AND C)", "(A OR B) AND (A OR C)"), + # idempotence + ("A AND A", "A"), + ("A OR A", "A"), + ], +) +def test_equivalent_inputs_collapse(ps, a, b): + assert _canon(ps, a) == _canon(ps, b) + + +@pytest.mark.parametrize( + "a,b", + [ + ("A IMPL B", "NOT A OR B"), + ("NOT NOT A", "A"), + ("A OR (B AND C)", "(A OR B) AND (A OR C)"), + ], +) +def test_equivalence_class_id_matches(ps, a, b): + assert equivalence_class_id(ps, a.encode()) == equivalence_class_id( + ps, b.encode() + ) + + +# --- tautology / contradiction collapse ------------------------------ + + +def test_tautology_collapses_to_true(ps): + assert _canon(ps, "A OR NOT A") == b"TRUE" + + +def test_false_literal_collapses_to_false(ps): + """Direct FALSE input → empty clause → 'FALSE'.""" + assert _canon(ps, "FALSE") == b"FALSE" + + +def test_and_with_false_collapses_to_false(ps): + """A AND FALSE yields an empty clause that surfaces as 'FALSE'.""" + assert _canon(ps, "A AND FALSE") == b"FALSE" + + +def test_a_and_not_a_is_not_simplified(ps): + """v1 kernel only catches WITHIN-clause tautologies + empty clauses. + + `A AND NOT A` is two separate clauses ({A}, {NOT A}); neither + contains both polarities, so the within-clause tautology drop + doesn't fire, and neither is the empty clause. Documented limit + of the v1 algorithm — sat-solving multi-clause contradictions is + out of scope. + """ + assert _canon(ps, "A AND NOT A") == b"A AND NOT A" + + +def test_complex_tautology(ps): + # (A IMPL B) OR (B IMPL A) is a classical tautology. + assert _canon(ps, "(A IMPL B) OR (B IMPL A)") == b"TRUE" + + +# --- equivalence classes kept distinct ------------------------------- + + +@pytest.mark.parametrize( + "a,b", + [ + ("A AND B", "A AND C"), # different atom sets + ("A AND B", "A OR B"), # logically distinct + ("A", "NOT A"), + ("A IMPL B", "B IMPL A"), + ("TRUE", "FALSE"), + ], +) +def test_distinct_inputs_stay_distinct(ps, a, b): + assert _canon(ps, a) != _canon(ps, b) + + +# --- round-trip idempotence ------------------------------------------ + + +@pytest.mark.parametrize( + "expr", + [ + "A", + "NOT A", + "A AND B", + "A OR B", + "(A OR B) AND (NOT A OR C)", + "A IMPL B", + "TRUE", + "FALSE", + ], +) +def test_round_trip(ps, expr): + canonical = _canon(ps, expr) + # Re-canonicalizing the canonical form yields the same bytes. + assert ps.canonicalize(canonical) == canonical + + +def test_round_trip_via_helper(ps): + """assert_round_trip exercises the protocol contract.""" + assert_round_trip(ps, b"A AND B") + assert_round_trip(ps, b"TRUE") + assert_round_trip(ps, b"FALSE") + + +# --- determinism + sort order ---------------------------------------- + + +def test_clauses_sorted_lexically(ps): + """Clause order is canonical regardless of input order.""" + a = _canon(ps, "C AND A AND B") + b = _canon(ps, "A AND B AND C") + assert a == b == b"A AND B AND C" + + +def test_literals_sorted_within_clause(ps): + """Literals inside a disjunction are sorted by (name, negated).""" + assert _canon(ps, "C OR A OR B") == b"(A OR B OR C)" + + +def test_dedupe_repeated_clauses(ps): + """Duplicate AND clauses collapse.""" + assert _canon(ps, "(A OR B) AND (A OR B)") == _canon(ps, "A OR B") + + +# --- invalid-input cone ---------------------------------------------- + + +def test_empty_raises(ps): + with pytest.raises(PiStarError, match="empty"): + ps.canonicalize(b"") + with pytest.raises(PiStarError, match="empty"): + ps.canonicalize(b" ") + + +def test_non_bytes_raises(ps): + with pytest.raises(PiStarError, match="expects bytes"): + ps.canonicalize("A AND B") # type: ignore[arg-type] + + +def test_unrecognized_multichar_token_raises(ps): + """Multi-letter tokens that aren't AND/OR/NOT/XOR/IMPL/IFF/T/F raise.""" + with pytest.raises(PiStarError, match="unrecognized token"): + ps.canonicalize(b"foo AND bar") + + +def test_unexpected_char_raises(ps): + with pytest.raises(PiStarError, match="unexpected char"): + ps.canonicalize(b"A + B") + + +def test_too_many_atoms_raises(ps): + """v1 caps at 8 atoms (`_MAX_ATOMS`).""" + expr = " AND ".join("ABCDEFGHI") # 9 atoms + with pytest.raises(PiStarError, match="caps atoms"): + ps.canonicalize(expr.encode()) + + +def test_exactly_max_atoms_allowed(ps): + """8 atoms is the boundary — must succeed.""" + expr = " AND ".join("ABCDEFGH") # 8 atoms + out = ps.canonicalize(expr.encode()) + assert out == b"A AND B AND C AND D AND E AND F AND G AND H" + + +def test_unbalanced_paren_raises(ps): + with pytest.raises(PiStarError): + ps.canonicalize(b"(A AND B") + + +def test_unconsumed_tokens_raise(ps): + """Trailing garbage after a complete expression is rejected.""" + with pytest.raises(PiStarError): + ps.canonicalize(b"A AND B C") + + +def test_dangling_operator_raises(ps): + with pytest.raises(PiStarError): + ps.canonicalize(b"A AND") + + +# --- determinism ----------------------------------------------------- + + +def test_repeated_canonicalize_is_stable(ps): + expr = b"(A IMPL B) AND (C IFF D) OR NOT E" + a = ps.canonicalize(expr) + b = ps.canonicalize(expr) + c = ps.canonicalize(expr) + assert a == b == c