core-labs/core
core-labs/core
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

feat(adr-0249): P3 structural formula→CNF converter (deduction leg)

Browse source 
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
This commit is contained in:
Shay 2026-07-18 12:40:31 -07:00
parent 2575d0d937
commit bc316f2128
2 changed files with 375 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

221
evals/logic_cnf_compiler.py Normal file
View file

@ -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)

154
tests/test_adr_0249_logic_cnf_compiler.py Normal file
View file

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