"""ADR-0201 — Propositional canonicalizer (the ``proof_chain`` keystone). Boolean-logic twin of :mod:`generate.math_symbolic_normalizer` / :mod:`generate.math_symbolic_equivalence`. Where the algebra side normalizes an expression to a canonical *polynomial string* and compares by byte-equality, this module canonicalizes a propositional formula to a **Reduced Ordered Binary Decision Diagram (ROBDD)** under a fixed (sorted) variable ordering and emits a canonical *string* serialization of the reduced diagram. Why ROBDD, not CNF/DNF: for a fixed variable ordering the ROBDD is canonical — two formulas are logically equivalent **iff** their reduced diagrams are isomorphic. CNF/DNF are merely normal (standardized shape), not canonical, and have no poly-time equivalence-preserving transform. The reduced diagram collapses logically-irrelevant variables, so ``P`` and ``P ∧ (Q ∨ ¬Q)`` produce the same key. ``wrong == 0`` discipline (mirrors the sibling): the canonicalizer **refuses** rather than guesses. Out-of-grammar input raises :class:`LogicError`; a diagram that would exceed the node budget raises :class:`LogicBudgetError` (a subclass, so callers catching :class:`LogicError` refuse on both) rather than churning. There is no approximate path — an answer is either the exact canonical form or a refusal. Honesty boundary: this is **propositional** logic only (finite Boolean variables — decidable, canonical). It does NOT canonicalize quantifiers/predicate logic and must not be used to claim ``wrong == 0`` for first-order reasoning. Hand-rolled (no external BDD library) to stay in CORE's idiom: deterministic by construction, fully inspectable, zero opaque dependencies — the same posture as the hand-rolled symbolic normalizer. """ from __future__ import annotations import re from dataclasses import dataclass from typing import Final # --------------------------------------------------------------------------- # Errors (twin of math_symbolic_normalizer.SymbolicError) # --------------------------------------------------------------------------- class LogicError(ValueError): """Raised when a formula cannot be canonicalized. Refusal-first; never coerces a malformed or out-of-regime input into a guess.""" class LogicBudgetError(LogicError): """Raised when the ROBDD would exceed the node budget (the exponential-blowup guard). A subclass of :class:`LogicError` so callers that refuse on ``LogicError`` refuse on budget-exceeded too — the proof-domain analog of the math gate refusing rather than churning.""" class LogicRegimeError(LogicError): """Raised when the input is outside the decidable **propositional** regime — quantified or predicate logic (ADR-0201.1; the typed refusal ADR-0202 §3 names). A subclass of :class:`LogicError` so callers that refuse on ``LogicError`` refuse here too, but it carries the typed :data:`OUT_OF_DECIDABLE_REGIME` reason so the regime boundary is distinguishable from a generic malformed-formula grammar error. Crucially, the boundary is enforced **by design** (see :func:`_reject_out_of_regime_text` / :func:`_reject_out_of_regime_tokens`), not by the tokenizer incidentally choking on an out-of-grammar character — the latter is the by-luck-not-by-design refusal the ``wrong == 0`` discipline rejects.""" # --------------------------------------------------------------------------- # Public defaults # --------------------------------------------------------------------------- DEFAULT_MAX_NODES: Final[int] = 100_000 """Default cap on reduced-diagram nodes. Bounded proof-step propositions relate a handful of atoms; this is generous for that regime and refuses on adversarial blowup rather than hanging.""" # Terminal node ids. 0 = constant false, 1 = constant true. Non-terminal ids >= 2. _FALSE: Final[int] = 0 _TRUE: Final[int] = 1 # --------------------------------------------------------------------------- # Tokenizer # --------------------------------------------------------------------------- # Multi-character / unicode operator spellings, longest first so the scanner is # unambiguous. Each maps to a canonical token kind. _OPERATOR_SPELLINGS: Final[tuple[tuple[str, str], ...]] = ( ("<->", "IFF"), ("↔", "IFF"), ("≡", "IFF"), ("->", "IMPLIES"), ("→", "IMPLIES"), ("⊃", "IMPLIES"), ("∧", "AND"), ("&&", "AND"), ("&", "AND"), ("∨", "OR"), ("||", "OR"), ("|", "OR"), ("¬", "NOT"), ("~", "NOT"), ("!", "NOT"), ("(", "LPAREN"), (")", "RPAREN"), ) # Keyword operators / constants (matched on word boundaries, case-insensitive). _KEYWORDS: Final[dict[str, str]] = { "and": "AND", "or": "OR", "not": "NOT", "implies": "IMPLIES", "iff": "IFF", "true": "TRUE", "false": "FALSE", } def _is_ident_start(ch: str) -> bool: return ch.isalpha() or ch == "_" def _is_ident_char(ch: str) -> bool: return ch.isalnum() or ch == "_" def _tokenize(text: str) -> list[tuple[str, str]]: """Scan ``text`` into ``(kind, lexeme)`` tokens. Raises :class:`LogicError` on any character that is not part of the propositional grammar.""" tokens: list[tuple[str, str]] = [] pos = 0 n = len(text) while pos < n: ch = text[pos] if ch.isspace(): pos += 1 continue # Symbolic operators (longest spelling first). matched = False for spelling, kind in _OPERATOR_SPELLINGS: if text.startswith(spelling, pos): tokens.append((kind, spelling)) pos += len(spelling) matched = True break if matched: continue # Identifiers / keywords. if _is_ident_start(ch): start = pos pos += 1 while pos < n and _is_ident_char(text[pos]): pos += 1 word = text[start:pos] kind = _KEYWORDS.get(word.lower()) if kind is not None: tokens.append((kind, word)) else: tokens.append(("ATOM", word)) continue raise LogicError(f"unexpected character {ch!r} at position {pos}") return tokens # --------------------------------------------------------------------------- # Parser (recursive descent — twin of math_symbolic_normalizer._Parser) # # Precedence, lowest to highest: IFF < IMPLIES < OR < AND < NOT < atom/paren. # IMPLIES is right-associative; the rest left-associative (associativity is # semantically irrelevant under ROBDD but a fixed parse keeps errors crisp). # # The AST is a nested tuple, e.g. ('and', ('atom','P'), ('not',('atom','Q'))). # --------------------------------------------------------------------------- _Ast = tuple class _Parser: def __init__(self, tokens: list[tuple[str, str]]) -> None: self._tokens = tokens self._pos = 0 def _peek(self) -> tuple[str, str] | None: return None if self._pos >= len(self._tokens) else self._tokens[self._pos] def _consume(self) -> tuple[str, str]: if self._pos >= len(self._tokens): raise LogicError("unexpected end of formula") tok = self._tokens[self._pos] self._pos += 1 return tok def parse(self) -> _Ast: if not self._tokens: raise LogicError("empty formula") ast = self._iff() if self._pos != len(self._tokens): raise LogicError(f"unexpected trailing token {self._tokens[self._pos]!r}") return ast def _iff(self) -> _Ast: node = self._implies() while (tok := self._peek()) is not None and tok[0] == "IFF": self._consume() node = ("iff", node, self._implies()) return node def _implies(self) -> _Ast: node = self._or() if (tok := self._peek()) is not None and tok[0] == "IMPLIES": self._consume() # right-associative: recurse into _implies for the RHS node = ("implies", node, self._implies()) return node def _or(self) -> _Ast: node = self._and() while (tok := self._peek()) is not None and tok[0] == "OR": self._consume() node = ("or", node, self._and()) return node def _and(self) -> _Ast: node = self._not() while (tok := self._peek()) is not None and tok[0] == "AND": self._consume() node = ("and", node, self._not()) return node def _not(self) -> _Ast: tok = self._peek() if tok is not None and tok[0] == "NOT": self._consume() return ("not", self._not()) return self._atom() def _atom(self) -> _Ast: tok = self._consume() kind, lexeme = tok if kind == "ATOM": return ("atom", lexeme) if kind == "TRUE": return ("const", True) if kind == "FALSE": return ("const", False) if kind == "LPAREN": inner = self._iff() close = self._consume() if close[0] != "RPAREN": raise LogicError(f"expected ')'; got {close[1]!r}") return inner raise LogicError(f"unexpected token {lexeme!r}") def _collect_atoms(ast: _Ast) -> set[str]: kind = ast[0] if kind == "atom": return {ast[1]} if kind == "const": return set() if kind == "not": return _collect_atoms(ast[1]) # binary return _collect_atoms(ast[1]) | _collect_atoms(ast[2]) _BINARY_OPS: Final[dict[str, str]] = {"and": "&", "or": "|", "implies": "->", "iff": "<->"} def _unparse(ast: _Ast) -> str: """Render an AST back to a fully-parenthesized formula string. Used to hand a sub-formula (e.g. an implication's antecedent/consequent) back to :func:`canonicalize`. Parenthesized everywhere so re-parsing is unambiguous.""" kind = ast[0] if kind == "atom": return ast[1] if kind == "const": return "true" if ast[1] else "false" if kind == "not": return f"(~{_unparse(ast[1])})" return f"({_unparse(ast[1])} {_BINARY_OPS[kind]} {_unparse(ast[2])})" def parse_top_implication(formula: str) -> tuple[str, str] | None: """If ``formula``'s top-level connective is ``->``, return ``(antecedent, consequent)`` as formula strings; else ``None``. Modus ponens needs the syntactic antecedent/consequent of an implication premise — the ROBDD form does not preserve which side is which (``P->Q`` and ``~P|Q`` share one diagram), so this works at the parse layer. Raises :class:`LogicError` / :class:`LogicRegimeError` on malformed / out-of-regime input, consistent with :func:`canonicalize`.""" _reject_out_of_regime_text(formula) tokens = _tokenize(formula) _reject_out_of_regime_tokens(tokens) ast = _Parser(tokens).parse() if ast[0] == "implies": return _unparse(ast[1]), _unparse(ast[2]) return None # --------------------------------------------------------------------------- # ROBDD manager (hand-rolled, minimal: mk + apply + negate + unique table) # --------------------------------------------------------------------------- class _Bdd: """A single-formula ROBDD builder. Variables are addressed by index into a fixed (sorted) ordering; ``var_count`` is the terminal sentinel level.""" __slots__ = ("var_count", "max_nodes", "_nodes", "_unique", "_and_c", "_or_c", "_neg_c") def __init__(self, var_count: int, max_nodes: int) -> None: self.var_count = var_count self.max_nodes = max_nodes # node id -> (var_index, low_id, high_id); ids 0/1 are terminals (absent here). self._nodes: list[tuple[int, int, int]] = [] self._unique: dict[tuple[int, int, int], int] = {} self._and_c: dict[tuple[int, int], int] = {} self._or_c: dict[tuple[int, int], int] = {} self._neg_c: dict[int, int] = {} def _var(self, node: int) -> int: # Terminals sit "below" every variable: use var_count as +inf sentinel. if node <= _TRUE: return self.var_count return self._nodes[node - 2][0] def _low(self, node: int) -> int: return self._nodes[node - 2][1] def _high(self, node: int) -> int: return self._nodes[node - 2][2] def mk(self, var: int, low: int, high: int) -> int: """Make-or-reuse a node, applying the two reduction rules. This is the only node-creation site, so the budget is enforced here.""" if low == high: return low # redundant-node rule key = (var, low, high) existing = self._unique.get(key) if existing is not None: return existing # shared-subgraph rule (hash-cons) if len(self._nodes) >= self.max_nodes: raise LogicBudgetError( f"ROBDD exceeded node budget ({self.max_nodes}); refusing rather " f"than churn" ) node_id = len(self._nodes) + 2 self._nodes.append(key) self._unique[key] = node_id return node_id def var_node(self, var: int) -> int: """The diagram for a bare variable: if var then true else false.""" return self.mk(var, _FALSE, _TRUE) def negate(self, f: int) -> int: if f == _FALSE: return _TRUE if f == _TRUE: return _FALSE cached = self._neg_c.get(f) if cached is not None: return cached result = self.mk(self._var(f), self.negate(self._low(f)), self.negate(self._high(f))) self._neg_c[f] = result return result def conj(self, f: int, g: int) -> int: if f == _FALSE or g == _FALSE: return _FALSE if f == _TRUE: return g if g == _TRUE: return f if f == g: return f key = (f, g) if f <= g else (g, f) # commutative -> canonical cache key cached = self._and_c.get(key) if cached is not None: return cached result = self._apply(self.conj, f, g) self._and_c[key] = result return result def disj(self, f: int, g: int) -> int: if f == _TRUE or g == _TRUE: return _TRUE if f == _FALSE: return g if g == _FALSE: return f if f == g: return f key = (f, g) if f <= g else (g, f) cached = self._or_c.get(key) if cached is not None: return cached result = self._apply(self.disj, f, g) self._or_c[key] = result return result def _apply(self, op, f: int, g: int) -> int: """Shannon expansion on the top variable of ``f``/``g`` (Bryant apply).""" v = min(self._var(f), self._var(g)) f0, f1 = self._cofactor(f, v) g0, g1 = self._cofactor(g, v) return self.mk(v, op(f0, g0), op(f1, g1)) def _cofactor(self, f: int, v: int) -> tuple[int, int]: if self._var(f) == v: return self._low(f), self._high(f) return f, f # v does not occur at the top of f def compile(self, ast: _Ast, index_of: dict[str, int]) -> int: kind = ast[0] if kind == "atom": return self.var_node(index_of[ast[1]]) if kind == "const": return _TRUE if ast[1] else _FALSE if kind == "not": return self.negate(self.compile(ast[1], index_of)) left = self.compile(ast[1], index_of) right = self.compile(ast[2], index_of) if kind == "and": return self.conj(left, right) if kind == "or": return self.disj(left, right) if kind == "implies": return self.disj(self.negate(left), right) if kind == "iff": # (a -> b) ∧ (b -> a) return self.conj(self.disj(self.negate(left), right), self.disj(self.negate(right), left)) raise LogicError(f"unknown AST node {kind!r}") # pragma: no cover def serialize(self, root: int, names: tuple[str, ...]) -> str: """Canonical, construction-order-independent serialization of the reduced diagram reachable from ``root``. Post-order DFS (low subtree fully before high subtree) assigns canonical indices; nodes reference variable *names* so diagrams over different atoms never collide, while terminals collapse (every tautology -> 'T', every contradiction -> 'F'). Because the diagram is reduced and the ordering fixed, isomorphic diagrams emit identical strings.""" if root == _TRUE: return "T" if root == _FALSE: return "F" order: dict[int, int] = {} lines: list[str] = [] def ref(node: int) -> str: if node == _TRUE: return "T" if node == _FALSE: return "F" return f"@{order[node]}" def visit(node: int) -> None: if node in order or node <= _TRUE: return visit(self._low(node)) visit(self._high(node)) idx = len(order) order[node] = idx lines.append( f"{idx}:{names[self._var(node)]}?{ref(self._high(node))}:{ref(self._low(node))}" ) visit(root) return ";".join(lines) def support(self, root: int) -> set[int]: """The set of variable indices that occur in the reduced diagram — i.e. the atoms that survive reduction (irrelevant ones are absent).""" seen: set[int] = set() out: set[int] = set() def visit(node: int) -> None: if node <= _TRUE or node in seen: return seen.add(node) out.add(self._var(node)) visit(self._low(node)) visit(self._high(node)) visit(root) return out # --------------------------------------------------------------------------- # Public API (twin of math_symbolic_equivalence) # --------------------------------------------------------------------------- @dataclass(frozen=True, slots=True) class CanonicalProposition: """The canonical form of a propositional formula. ``canonical_key`` is the byte-equality discriminator — two formulas are logically equivalent iff their keys are equal. ``atoms`` are the variables that *survive* reduction (logically-irrelevant ones are dropped), so it can be a strict subset of the atoms written in the input.""" canonical_key: str atoms: tuple[str, ...] is_tautology: bool is_contradiction: bool # --------------------------------------------------------------------------- # Out-of-regime detection (ADR-0201.1) # # Propositional logic is the only regime with a canonical form + decidable # equivalence. Quantified / predicate input must REFUSE with the typed # `out_of_decidable_regime` reason (ADR-0202 §3) — by DESIGN, recognized as # out-of-regime, not by accident of the tokenizer choking on an out-of-grammar # character. These checks run BEFORE the generic grammar error so the regime # boundary is principled, typed, and inspectable. # --------------------------------------------------------------------------- OUT_OF_DECIDABLE_REGIME: Final[str] = "out_of_decidable_regime" # Quantifier markers: ASCII keywords (word-boundary, case-insensitive) and the # logic symbols ∀ / ∃. Their presence means first-order/predicate reasoning, # which has no ROBDD canonical form and is undecidable in general. `forall` and # `exists` are therefore reserved — not usable as atom ids. _QUANTIFIER_WORD_RE: Final[re.Pattern[str]] = re.compile(r"\b(forall|exists)\b", re.IGNORECASE) _QUANTIFIER_SYMBOLS: Final[frozenset[str]] = frozenset({"∀", "∃"}) # ∀ ∃ def _reject_out_of_regime_text(formula: str) -> None: """Refuse raw input that carries a quantifier marker. Runs before tokenizing so quantifier symbols (∀/∃) and the ``forall x. …`` / ``exists x. …`` shape refuse with the typed regime reason rather than a generic 'unexpected character' grammar error from the trailing ``.``/predicate syntax.""" for sym in sorted(_QUANTIFIER_SYMBOLS): if sym in formula: raise LogicRegimeError(f"{OUT_OF_DECIDABLE_REGIME}: quantifier symbol {sym!r}") match = _QUANTIFIER_WORD_RE.search(formula) if match is not None: raise LogicRegimeError(f"{OUT_OF_DECIDABLE_REGIME}: quantifier {match.group(0)!r}") def _reject_out_of_regime_tokens(tokens: list[tuple[str, str]]) -> None: """Refuse predicate-application shape — an atom immediately applied to an argument list, e.g. ``rains(x)``. In the propositional grammar an atom is never followed by ``(`` (grouping only follows an operator or opens an expression), so ``ATOM (`` is a predicate, not a well-formed propositional formula. Runs before the parser's generic trailing-token error so the regime boundary is the reason that surfaces. (Keyword operators such as ``not`` are NOT ``ATOM`` tokens, so ``not (P)`` is unaffected.)""" for (kind, lexeme), (next_kind, _next_lexeme) in zip(tokens, tokens[1:]): if kind == "ATOM" and next_kind == "LPAREN": raise LogicRegimeError( f"{OUT_OF_DECIDABLE_REGIME}: predicate application {lexeme!r}(…)" ) def canonicalize(formula: str, *, max_nodes: int = DEFAULT_MAX_NODES) -> CanonicalProposition: """Canonicalize ``formula`` to its ROBDD identity under the sorted-atom ordering. Refusal-first: * :class:`LogicRegimeError` (``out_of_decidable_regime``) if the input is quantified / predicate logic — checked *before* grammar, so the regime boundary is principled, not an incidental tokenizer failure; * :class:`LogicError` on out-of-grammar (malformed propositional) input; * :class:`LogicBudgetError` if the diagram exceeds ``max_nodes``. """ _reject_out_of_regime_text(formula) tokens = _tokenize(formula) _reject_out_of_regime_tokens(tokens) ast = _Parser(tokens).parse() declared = tuple(sorted(_collect_atoms(ast))) # fixed variable ordering index_of = {name: i for i, name in enumerate(declared)} bdd = _Bdd(var_count=len(declared), max_nodes=max_nodes) root = bdd.compile(ast, index_of) key = bdd.serialize(root, declared) # Atoms that actually occur in the reduced diagram (irrelevant ones dropped). support_idx = bdd.support(root) surviving = tuple(name for i, name in enumerate(declared) if i in support_idx) return CanonicalProposition( canonical_key=key, atoms=surviving, is_tautology=(root == _TRUE), is_contradiction=(root == _FALSE), )