64f3da18a7
Phase 2.3: the first inference rule + the wrong=0 mechanism for proofs. - generate/proof_chain/rules.py: evaluate_modus_ponens / evaluate_proof_conclusion. Proof-layer dispatch (Option B) over proposition FORMULAS via the canonicalizer; never touches check_admissibility/_resolve_dep_units (proofs have no units). Disagreement rule = the select_self_verified twin: pool ALL admissible single-step MP derivations, require a unique canonical key == declared conclusion. Pooling (not filter-to-declared-first) is the soundness mechanism. - generate/logic_canonical.py: parse_top_implication (+ _unparse) — recovers an implication's syntactic antecedent/consequent (the ROBDD form doesn't preserve it). - Closed typed-reason set; the corpus's finer labels consolidate (6 disagreement refuse-labels -> conclusion_disagreement; 4 antecedent-flavor labels -> unestablished_antecedent — same redundancy, same mechanism-makes-one-distinction principle). - Honesty boundary (exact scope): guarantees a unique conclusion among SINGLE-STEP MP over the premises, NOT "uniquely entailed" by all strategies. Cross-check: all 24 GPT-5.5 adversarial corpus cases agree on OUTCOME against the real rule (no rule bug / no corpus outcome-misread); reasons consolidate as above. Mutation: filter-to-declared-first makes DISAGREE-007/010 wrongly admit -> pooling tests fail (pooling load-bearing). Drive-by fix (cleanup-as-you-find): merged ADR-0204 ProofNode.__post_init__ was dedented to module level -> all ProofNode validation was silently DEAD (smoke skips the dedicated test file; the smoke != full-suite hazard). Re-indented; validation restored. Additive (math lane untouched). Full binding-graph surface green; smoke 67.
590 lines
22 KiB
Python
590 lines
22 KiB
Python
"""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),
|
||
)
|