From bc316f21281b7ce492a86a67c81fd14963246fb8 Mon Sep 17 00:00:00 2001 From: Shay Date: Sat, 18 Jul 2026 12:40:31 -0700 Subject: [PATCH] =?UTF-8?q?feat(adr-0249):=20P3=20structural=20formula?= =?UTF-8?q?=E2=86=92CNF=20converter=20(deduction=20leg)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the deduction leg: propositional formula strings (as emitted by meaning_graph.to_deductive_logic, or any logic_canonical-parseable syntax) → corridor CNF PropositionalProblem + query Clause, consumable by propositional_entails. Structural, not truth-table (spike §4.1): reuses the production ROBDD parser (generate.logic_canonical — never re-implemented) for the AST, then the standard sound rewrite — eliminate iff/implies, NNF, distribute OR over AND — with constant folding, tautological-clause elimination, and a clause budget. The converter never enumerates assignments and never decides entailment; that stays the corridor's job. Soundness proved against the ROBDD oracle: for a 14-formula panel, the compiled CNF rendered back to a formula has the same canonicalize() identity as the source. End-to-end entailment through propositional_entails agrees with the ROBDD gold (evaluate_entailment) wrong=0 on consistent premises; ex-falso handled per the corridor's own contract (entailed + satisfiable_premises=False, where the ROBDD path returns REFUSED for inconsistent premises). Fail-closed: conjunctive/constant queries, formulas reducing to false, and CNF budget refuse with typed CnfCompileError; >5 atoms surfaces the corridor's HamiltonianCompileError(atom_count_out_of_range); out-of-regime propagates LogicRegimeError. Off-serving (A-04), import-guard pinned. 32/32 pins green. [Verification]: uv run python -m pytest tests/test_adr_0249_logic_cnf_compiler.py -q --- evals/logic_cnf_compiler.py | 221 ++++++++++++++++++++++ tests/test_adr_0249_logic_cnf_compiler.py | 154 +++++++++++++++ 2 files changed, 375 insertions(+) create mode 100644 evals/logic_cnf_compiler.py create mode 100644 tests/test_adr_0249_logic_cnf_compiler.py diff --git a/evals/logic_cnf_compiler.py b/evals/logic_cnf_compiler.py new file mode 100644 index 00000000..d91759fe --- /dev/null +++ b/evals/logic_cnf_compiler.py @@ -0,0 +1,221 @@ +"""evals.logic_cnf_compiler — structural formula → CNF PropositionalProblem (ADR-0249 P3). + +Closes the deduction leg of the reader→Hamiltonian compiler: turns propositional +formula strings (as emitted by ``generate.meaning_graph.to_deductive_logic``, or +any ``logic_canonical``-parseable syntax) into the corridor's CNF +``PropositionalProblem`` plus a query ``Clause``, consumable by +``propositional_entails``. + +Structural, not truth-table (spike §4.1): the formula is parsed with the +production ROBDD parser (``generate.logic_canonical`` — reused, never +re-implemented), then rewritten to CNF by the standard sound transform — +eliminate iff/implies, push negations to the literals (NNF), distribute OR over +AND — with constant folding, tautological-clause elimination, and a clause +budget. Equivalence to the source is provable against the ROBDD oracle +(``canonicalize``) and is pinned in tests. The converter never enumerates +assignments and never decides satisfiability or entailment — that is the +corridor's job; this only compiles the constraint shape. + +Off-serving (A-04): imports the serving-side logic parser for its grammar only, +lives in the eval quarantine, and is never imported by ``chat/runtime.py``. +""" +from __future__ import annotations + +from collections.abc import Sequence + +from core.physics.cognitive_lifecycle import Clause, PropositionalProblem +from generate.logic_canonical import ( + _Parser, + _reject_out_of_regime_text, + _reject_out_of_regime_tokens, + _tokenize, +) + +__all__ = [ + "CnfCompileError", + "formula_to_clauses", + "query_to_clause", + "compile_entailment", + "clauses_to_formula", +] + +# CNF as a frozenset of clauses; a clause is a frozenset of ``(atom, polarity)`` +# literals. Two sentinels: TRUE = no clauses (empty conjunction); FALSE = one +# empty clause (an unsatisfiable disjunction). +_TRUE: frozenset = frozenset() +_FALSE: frozenset = frozenset({frozenset()}) +_CLAUSE_BUDGET = 512 + + +class CnfCompileError(ValueError): + """Typed, fail-closed refusal for CNF compilation (spike §4.3). + + Parse/regime failures propagate as ``logic_canonical.LogicError`` / + ``LogicRegimeError``; atom-count and structural violations surface as the + corridor's ``HamiltonianCompileError`` when the ``PropositionalProblem`` is + built. This type covers the CNF-specific refusals only. + """ + + def __init__(self, reason: str, **disclosure: object) -> None: + self.reason = reason + self.disclosure = disclosure + detail = ", ".join(f"{k}={v!r}" for k, v in disclosure.items()) + super().__init__(f"{reason}({detail})" if detail else reason) + + +def _parse(formula: str): + """Mirror ``canonicalize``'s refusal-first front-matter, returning the AST.""" + _reject_out_of_regime_text(formula) + tokens = _tokenize(formula) + _reject_out_of_regime_tokens(tokens) + return _Parser(tokens).parse() + + +def _eliminate(ast: tuple) -> tuple: + """Remove ``iff`` and ``implies`` in favour of ``and``/``or``/``not``.""" + kind = ast[0] + if kind == "iff": + a, b = _eliminate(ast[1]), _eliminate(ast[2]) + return ("and", ("or", ("not", a), b), ("or", ("not", b), a)) + if kind == "implies": + return ("or", ("not", _eliminate(ast[1])), _eliminate(ast[2])) + if kind in ("and", "or"): + return (kind, _eliminate(ast[1]), _eliminate(ast[2])) + if kind == "not": + return ("not", _eliminate(ast[1])) + return ast # atom / const + + +def _nnf(ast: tuple) -> tuple: + """Push negations inward until they sit only on atoms (De Morgan).""" + kind = ast[0] + if kind == "not": + inner = ast[1] + ik = inner[0] + if ik == "not": + return _nnf(inner[1]) + if ik == "and": + return ("or", _nnf(("not", inner[1])), _nnf(("not", inner[2]))) + if ik == "or": + return ("and", _nnf(("not", inner[1])), _nnf(("not", inner[2]))) + if ik == "const": + return ("const", not inner[1]) + if ik == "atom": + return ("not", inner) + raise CnfCompileError("unparseable_negation", node=ik) + if kind in ("and", "or"): + return (kind, _nnf(ast[1]), _nnf(ast[2])) + return ast # atom / const + + +def _is_tautological(clause: frozenset) -> bool: + return any((atom, True) in clause and (atom, False) in clause for atom, _ in clause) + + +def _to_cnf(ast: tuple) -> frozenset: + """NNF AST → frozenset of clauses (constant-folded, tautologies dropped).""" + kind = ast[0] + if kind == "atom": + return frozenset({frozenset({(ast[1], True)})}) + if kind == "not": # NNF guarantees the operand is an atom + return frozenset({frozenset({(ast[1][1], False)})}) + if kind == "const": + return _TRUE if ast[1] else _FALSE + left, right = _to_cnf(ast[1]), _to_cnf(ast[2]) + if kind == "and": + if left == _FALSE or right == _FALSE: + return _FALSE + merged = left | right + if len(merged) > _CLAUSE_BUDGET: + raise CnfCompileError("cnf_budget_exceeded", clauses=len(merged)) + return frozenset(merged) + if kind == "or": + if left == _TRUE or right == _TRUE: + return _TRUE + if left == _FALSE: + return right + if right == _FALSE: + return left + out: set[frozenset] = set() + for clause_a in left: + for clause_b in right: + combined = clause_a | clause_b + if _is_tautological(combined): + continue # always-true clause drops from the conjunction + out.add(combined) + if len(out) > _CLAUSE_BUDGET: + raise CnfCompileError("cnf_budget_exceeded", clauses=len(out)) + return frozenset(out) if out else _TRUE + raise CnfCompileError("unparseable_node", node=kind) + + +def _sorted_clause(clause: frozenset) -> Clause: + return tuple(sorted(clause)) + + +def _cnf_of(formula: str) -> frozenset: + return _to_cnf(_nnf(_eliminate(_parse(formula)))) + + +def formula_to_clauses(formula: str) -> tuple[Clause, ...]: + """Structural CNF of ``formula`` as a deterministic tuple of clauses. + + A tautological formula yields ``()`` (no constraints); a formula that + reduces to ``false`` is refused (it cannot be a corridor clause set). + """ + cnf = _cnf_of(formula) + if cnf == _FALSE: + raise CnfCompileError("formula_reduces_to_false", formula=formula) + if cnf == _TRUE: + return () + return tuple(sorted((_sorted_clause(c) for c in cnf))) + + +def query_to_clause(query: str) -> Clause: + """A query must reduce to a single clause (a disjunction of literals). + + That is exactly the shape ``propositional_entails`` negates into unit + clauses. Conjunctive or constant queries are refused. + """ + cnf = _cnf_of(query) + if cnf in (_TRUE, _FALSE): + raise CnfCompileError("query_reduces_to_constant", query=query, value=(cnf == _TRUE)) + if len(cnf) != 1: + raise CnfCompileError("query_not_single_clause", query=query, clause_count=len(cnf)) + return _sorted_clause(next(iter(cnf))) + + +def compile_entailment( + premises: Sequence[str], query: str +) -> tuple[PropositionalProblem, Clause]: + """Compile ``premises ⊨ query`` into a corridor ``(PropositionalProblem, Clause)``. + + Run the result through ``propositional_entails`` to decide it. Raises + ``HamiltonianCompileError`` (``atom_count_out_of_range``) when the shared + atom set exceeds the corridor's ≤5-atom envelope — the honest boundary. + """ + premise_clauses: tuple[Clause, ...] = tuple( + clause for formula in premises for clause in formula_to_clauses(formula) + ) + query_clause = query_to_clause(query) + atoms = sorted( + {atom for clause in premise_clauses for atom, _ in clause} + | {atom for atom, _ in query_clause} + ) + problem = PropositionalProblem(atoms=tuple(atoms), clauses=premise_clauses) + return problem, query_clause + + +def clauses_to_formula(clauses: Sequence[Clause]) -> str: + """Render CNF clauses to a ``logic_canonical``-parseable string (``&``/``|``/``~``). + + Round-trips with ``formula_to_clauses`` under the ROBDD identity; ``()`` + (a tautology) renders to ``true``. + """ + if not clauses: + return "true" + rendered = [ + "(" + " | ".join(atom if pol else f"~{atom}" for atom, pol in clause) + ")" + for clause in clauses + ] + return " & ".join(rendered) diff --git a/tests/test_adr_0249_logic_cnf_compiler.py b/tests/test_adr_0249_logic_cnf_compiler.py new file mode 100644 index 00000000..5075dfd6 --- /dev/null +++ b/tests/test_adr_0249_logic_cnf_compiler.py @@ -0,0 +1,154 @@ +"""ADR-0249 P3 — structural formula→CNF converter pins (deduction leg). + +The converter turns propositional formula strings into the corridor's CNF +``PropositionalProblem`` + query ``Clause``. Two guarantees are pinned: + * soundness — the CNF is logically equivalent to the source, proved against + the production ROBDD oracle (``canonicalize``), never by truth table; + * agreement — end-to-end entailment through ``propositional_entails`` matches + the ROBDD gold (``evaluate_entailment``) with wrong=0 on consistent premises. +""" +from __future__ import annotations + +from pathlib import Path + +import pytest + +from core.physics.cognitive_lifecycle import ( + HamiltonianCompileError, + propositional_entails, +) +from generate.logic_canonical import LogicRegimeError, canonicalize +from generate.proof_chain.entail import Entailment, evaluate_entailment + +from evals.logic_cnf_compiler import ( + CnfCompileError, + clauses_to_formula, + compile_entailment, + formula_to_clauses, + query_to_clause, +) + +# Formulas that do NOT reduce to false (those are tested as refusals). +_SOUNDNESS_PANEL = [ + "P implies Q", + "P or Q", + "not P", + "P", + "(P implies Q) and (Q implies R)", + "not (P and Q)", + "not (P or Q)", + "P iff Q", + "(P or Q) and (not P or R)", + "P and not P", + "P or not P", + "not (P implies Q)", + "(a implies b) implies c", + "not (not P)", +] + + +@pytest.mark.parametrize("formula", _SOUNDNESS_PANEL) +def test_cnf_is_robdd_equivalent_to_source(formula: str) -> None: + # Structural soundness: the compiled CNF, rendered back to a formula, has + # the same ROBDD identity as the original. No assignment enumeration. + clauses = formula_to_clauses(formula) + rendered = clauses_to_formula(clauses) + assert canonicalize(formula).canonical_key == canonicalize(rendered).canonical_key + + +# --- End-to-end entailment agrees with the ROBDD gold (consistent premises) -- + +_ENTAILMENT_PANEL = [ + (("P implies Q", "P"), "Q"), + (("P implies Q", "P"), "not Q"), + (("P or Q",), "P"), + (("P implies Q", "Q implies R"), "P implies R"), + (("a implies b", "b implies c", "a"), "c"), + (("P or Q", "not P"), "Q"), + (("P or Q", "R"), "P or Q"), +] + + +@pytest.mark.parametrize(("premises", "query"), _ENTAILMENT_PANEL) +def test_entailment_agrees_with_robdd_gold_wrong_zero(premises, query) -> None: + problem, conclusion = compile_entailment(premises, query) + corridor = propositional_entails(problem, conclusion).entailed + gold = evaluate_entailment(tuple(premises), query).outcome is Entailment.ENTAILED + assert corridor == gold + + +def test_modus_ponens_entailed() -> None: + problem, conclusion = compile_entailment(("P implies Q", "P"), "Q") + verdict = propositional_entails(problem, conclusion) + assert verdict.entailed is True + assert verdict.satisfiable_premises is True + + +def test_ex_falso_entailed_with_unsatisfiable_premises_disclosed() -> None: + # Inconsistent premises classically entail everything; the corridor says so + # AND discloses that the premises are unsatisfiable (matches ADR-0243 §). + problem, conclusion = compile_entailment(("P", "not P"), "Q") + verdict = propositional_entails(problem, conclusion) + assert verdict.entailed is True + assert verdict.satisfiable_premises is False + + +# --- Clause shape + determinism --------------------------------------------- + + +def test_clause_literal_shape() -> None: + clauses = formula_to_clauses("P implies Q") # -> (~P | Q) + assert clauses == (( ("P", False), ("Q", True) ),) + (atom, polarity) = clauses[0][0] + assert isinstance(atom, str) and isinstance(polarity, bool) + + +def test_tautology_yields_no_clauses() -> None: + assert formula_to_clauses("P or not P") == () + + +def test_compilation_is_deterministic() -> None: + a, _ = compile_entailment(("P implies Q", "P"), "Q") + b, _ = compile_entailment(("P implies Q", "P"), "Q") + assert a.problem_id == b.problem_id + assert formula_to_clauses("(P or Q) and (not P or R)") == formula_to_clauses( + "(P or Q) and (not P or R)" + ) + + +# --- Fail-closed refusals ---------------------------------------------------- + + +def test_refuses_conjunctive_query() -> None: + with pytest.raises(CnfCompileError): + query_to_clause("P and Q") + + +def test_refuses_constant_query() -> None: + with pytest.raises(CnfCompileError): + query_to_clause("P or not P") + + +def test_refuses_formula_reducing_to_false() -> None: + with pytest.raises(CnfCompileError): + formula_to_clauses("false") + + +def test_refuses_over_five_atoms() -> None: + # Six distinct atoms exceed the corridor envelope → HamiltonianCompileError. + with pytest.raises(HamiltonianCompileError): + compile_entailment(("a or b", "c or d", "e or f"), "a") + + +def test_out_of_regime_propagates() -> None: + with pytest.raises(LogicRegimeError): + formula_to_clauses("forall x P(x)") + + +# --- Off-serving guard (A-04) ------------------------------------------------ + + +def test_compiler_is_not_serve_wired() -> None: + source = Path("evals/logic_cnf_compiler.py").read_text() + assert "import chat" not in source + assert "from chat" not in source