arborist/tests/test_pi_star_logic.py

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