Reasoning (guardrail_solver.reasoning)

The explanation DAG, the SMT helpers, the forward derivation rules, puzzle solving, and Mermaid rendering. See How reasoning works for the narrative.

reasoning

The reasoning engine, re-exported as a stable public surface.

The engine lives in :mod:._python, with rendering split out into :mod:.renderers (.renderers.mermaid, .renderers.d3); this package keeps the public import path (guardrail_solver.reasoning.X) stable so a sibling backend can be slotted in behind it later without touching callers.

DEFAULT_REASONING_BACKEND module-attribute

DEFAULT_REASONING_BACKEND = ReasoningBackend()

DEFAULT_SOLVER_TIMEOUT_MS module-attribute

DEFAULT_SOLVER_TIMEOUT_MS = 30000

Z3_SEMANTICS module-attribute

Z3_SEMANTICS = Z3SemanticBackend(
    timeout_ms=DEFAULT_SOLVER_TIMEOUT_MS
)

ingest_puzzle module-attribute

ingest_puzzle = ingest

solve_puzzle module-attribute

solve_puzzle = PuzzleSolver()

CheckResult dataclass

A classification verdict plus the witnessing models and unsat cores.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class CheckResult:
    """A classification verdict plus the witnessing models and unsat cores."""

    status: Status
    true_model: ModelRef | None
    false_model: ModelRef | None
    true_core: tuple[BoolRef, ...]
    false_core: tuple[BoolRef, ...]

status instance-attribute

status

true_model instance-attribute

true_model

false_model instance-attribute

false_model

true_core instance-attribute

true_core

false_core instance-attribute

false_core

Consistent

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

class Consistent:
    pass

Derivation dataclass

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class Derivation:
    premise_ids: tuple[FactId, ...]
    rule: str

premise_ids instance-attribute

premise_ids

rule instance-attribute

rule

DerivationBackend

Bases: Protocol

Propose one round of derived facts from an immutable graph snapshot.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

class DerivationBackend(Protocol):
    """Propose one round of derived facts from an immutable graph snapshot."""

    def derive(
        self,
        input_: DerivationInput,
    ) -> Iterable[DerivationProposal]: ...

derive

derive(input_)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def derive(
    self,
    input_: DerivationInput,
) -> Iterable[DerivationProposal]: ...

DerivationId dataclass

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class DerivationId:
    value: str

    def __str__(self) -> str:
        return self.value

value instance-attribute

value

DerivationInput dataclass

Backend-free view constructible only from a consistent unsaturated graph.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class DerivationInput:
    """Backend-free view constructible only from a consistent unsaturated graph."""

    established: tuple[FactNode, ...]

established instance-attribute

established

DerivationNode dataclass

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class DerivationNode:
    id: DerivationId
    rule: str

id instance-attribute

id

rule instance-attribute

rule

DerivationProposal dataclass

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class DerivationProposal:
    conclusion: Prop[BoolRef]
    premises: tuple[FactId, ...]
    rule: str
    source: SourceSpan | None = None

conclusion instance-attribute

conclusion

premises instance-attribute

premises

rule instance-attribute

rule

source class-attribute instance-attribute

source = None

Entailment

Bases: Enum

A three-valued entailment verdict.

Deliberately a plain Enum, not IntEnum: a verdict must not be collapsible to bool — being three-valued is the whole point. Always compare with is (result is Entailment.PROVED); never use it in a boolean context, where "the solver gave up" would silently read as success.

The values form a conjunction lattice in which REFUTED is absorbing (one countermodel refutes the whole) and PROVED is the identity (an all-proved conjunction is proved), with UNDECIDED between. The ordering is expressed directly in :meth:conjunction, not smuggled into integer values.

• PROVED — the premises entail the conclusion (¬conclusion unsat).
• REFUTED — a countermodel exists (premises ∧ ¬conclusion sat); the entailment is definitely false, not merely unproven. The witnessing model lives on the SolveResult / classify path, not here.
• UNDECIDED — the solver could not decide (an encoding/theory limit).

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

class Entailment(Enum):
    """A three-valued entailment verdict.

    Deliberately a plain ``Enum``, not ``IntEnum``: a verdict must not be
    collapsible to ``bool`` — being three-valued is the whole point. Always
    compare with ``is`` (``result is Entailment.PROVED``); never use it in a
    boolean context, where "the solver gave up" would silently read as success.

    The values form a *conjunction lattice* in which ``REFUTED`` is **absorbing**
    (one countermodel refutes the whole) and ``PROVED`` is the **identity**
    (an all-proved conjunction is proved), with ``UNDECIDED`` between. The
    ordering is expressed directly in :meth:`conjunction`, not smuggled into
    integer values.

    - ``PROVED``    — the premises entail the conclusion (``¬conclusion`` unsat).
    - ``REFUTED``   — a countermodel exists (``premises ∧ ¬conclusion`` sat); the
                      entailment is *definitely false*, not merely unproven. The
                      witnessing model lives on the ``SolveResult`` / ``classify``
                      path, not here.
    - ``UNDECIDED`` — the solver could not decide (an encoding/theory limit).
    """

    REFUTED = "REFUTED"
    UNDECIDED = "UNDECIDED"
    PROVED = "PROVED"

    def meet(self, other: Entailment) -> Entailment:
        """Binary Kleene conjunction (∧) — the monoid op behind `conjunction`.

        ``REFUTED`` is absorbing, ``PROVED`` is the identity, ``UNDECIDED`` sits
        between. Raises on a non-``Entailment`` rather than returning
        ``NotImplemented`` (this is a plain method, not an operator dunder, so
        ``NotImplemented`` would silently leak as a value).
        """
        if not isinstance(other, Entailment):
            raise TypeError(f"meet expects an Entailment, got {other!r}")
        return next(x for x in Entailment if x in (self, other))

    @classmethod
    def conjunction(cls, results: Iterable[Entailment]) -> Entailment:
        """Fold ``meet`` over obligations that must *all* hold.

        ``REFUTED`` is the absorbing element, so this short-circuits: given a
        generator of solver calls, it stops at the first countermodel instead of
        running the rest. The empty conjunction is ``PROVED`` (vacuous truth).
        """
        return functools.reduce(
            cls.meet,
            takewhile_inclusive(lambda r: r is not cls.REFUTED, results),
            cls.PROVED,
        )

REFUTED class-attribute instance-attribute

REFUTED = 'REFUTED'

UNDECIDED class-attribute instance-attribute

UNDECIDED = 'UNDECIDED'

PROVED class-attribute instance-attribute

PROVED = 'PROVED'

meet

meet(other)

Binary Kleene conjunction (∧) — the monoid op behind conjunction.

REFUTED is absorbing, PROVED is the identity, UNDECIDED sits between. Raises on a non-Entailment rather than returning NotImplemented (this is a plain method, not an operator dunder, so NotImplemented would silently leak as a value).

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def meet(self, other: Entailment) -> Entailment:
    """Binary Kleene conjunction (∧) — the monoid op behind `conjunction`.

    ``REFUTED`` is absorbing, ``PROVED`` is the identity, ``UNDECIDED`` sits
    between. Raises on a non-``Entailment`` rather than returning
    ``NotImplemented`` (this is a plain method, not an operator dunder, so
    ``NotImplemented`` would silently leak as a value).
    """
    if not isinstance(other, Entailment):
        raise TypeError(f"meet expects an Entailment, got {other!r}")
    return next(x for x in Entailment if x in (self, other))

conjunction classmethod

conjunction(results)

Fold meet over obligations that must all hold.

REFUTED is the absorbing element, so this short-circuits: given a generator of solver calls, it stops at the first countermodel instead of running the rest. The empty conjunction is PROVED (vacuous truth).

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@classmethod
def conjunction(cls, results: Iterable[Entailment]) -> Entailment:
    """Fold ``meet`` over obligations that must *all* hold.

    ``REFUTED`` is the absorbing element, so this short-circuits: given a
    generator of solver calls, it stops at the first countermodel instead of
    running the rest. The empty conjunction is ``PROVED`` (vacuous truth).
    """
    return functools.reduce(
        cls.meet,
        takewhile_inclusive(lambda r: r is not cls.REFUTED, results),
        cls.PROVED,
    )

Evidence dataclass

Phantom evidence carried by a graph's static type.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

@dataclass(frozen=True)
class Evidence[ConsistencyT, SaturationT]:
    """Phantom evidence carried by a graph's static type."""

ExplanationBackend

Bases: Protocol

Propose explanation edges without mutating the fact graph.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

class ExplanationBackend(Protocol):
    """Propose explanation edges without mutating the fact graph."""

    def explain(
        self,
        input_: ExplanationInput,
        semantics: SemanticBackend,
    ) -> Iterable[ExplanationProposal]: ...

explain

explain(input_, semantics)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def explain(
    self,
    input_: ExplanationInput,
    semantics: SemanticBackend,
) -> Iterable[ExplanationProposal]: ...

ExplanationInput dataclass

Backend-free view constructible only from a consistent saturated graph.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class ExplanationInput:
    """Backend-free view constructible only from a consistent saturated graph."""

    established: tuple[FactNode, ...]
    checks: tuple[FactNode, ...]

established instance-attribute

established

checks instance-attribute

checks

ExplanationNode dataclass

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class ExplanationNode:
    id: DerivationId
    rule: str

id instance-attribute

id

rule instance-attribute

rule

ExplanationProposal dataclass

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class ExplanationProposal:
    check_id: FactId
    premises: tuple[FactId, ...]
    rule: str

check_id instance-attribute

check_id

premises instance-attribute

premises

rule instance-attribute

rule

FactGraph dataclass

Bases: Generic[StateT]

Facts, derivation steps, and checks in one typed provenance DAG.

Derivations are represented as:

premise fact -> derivation step -> conclusion fact

This preserves multi-premise rules and allows a single semantic fact to have several independent derivations without overloading edge labels or a single rule attribute on the conclusion fact.

Checks remain candidate propositions, not established facts. They cannot be premises; they are sinks. A known fact can point directly into a check when explain_check establishes an explicit explanation step.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class FactGraph(Generic[StateT]):
    """Facts, derivation steps, and checks in one typed provenance DAG.

    Derivations are represented as:

        premise fact -> derivation step -> conclusion fact

    This preserves multi-premise rules and allows a single semantic fact to have
    several independent derivations without overloading edge labels or a single
    ``rule`` attribute on the conclusion fact.

    Checks remain candidate propositions, not established facts. They cannot be
    premises; they are sinks. A known fact can point directly into a check when
    ``explain_check`` establishes an explicit explanation step.
    """

    dag: ProvenanceDag = field(default_factory=ProvenanceDag)
    by_expr: Mapping[str, FactId] = field(default_factory=dict)
    next_index: int = 1
    next_derivation_index: int = 1
    reasoning_backend: ReasoningBackend = field(
        default_factory=default_reasoning_backend,
        compare=False,
        repr=False,
    )

    @classmethod
    def empty(cls) -> FactGraph[Evidence[Unchecked, Unsaturated]]:
        return FactGraph()

    def with_reasoning_backend(
        self,
        backend: ReasoningBackend,
    ) -> FactGraph[StateT]:
        """Return an equal immutable graph using ``backend`` operationally."""
        return replace(self, reasoning_backend=backend)

    def _fresh_id(self) -> FactId:
        return FactId(f"f{self.next_index}")

    def _fresh_derivation_id(self) -> DerivationId:
        return DerivationId(f"d{self.next_derivation_index}")

    def fact(self, fact_id: FactId) -> FactNode:
        return self.dag.fact(fact_id)

    def derivation_step(self, derivation_id: DerivationId) -> DerivationNode:
        return self.dag.derivation(derivation_id)

    @property
    def nodes(self) -> Mapping[FactId, FactNode]:
        return self.dag.facts()

    @property
    def derivation_nodes(self) -> Mapping[DerivationId, DerivationNode]:
        return self.dag.derivation_nodes()

    @property
    def derivations(self) -> Mapping[FactId, tuple[Derivation, ...]]:
        return self.dag.derivations()

    def _insert_fact(
        self,
        node: FactNode,
        *,
        index_expression: bool,
    ) -> tuple[FactId, FactGraph[StateT]]:
        by_expr = (
            {**self.by_expr, expr_key(node.expr): node.id}
            if index_expression
            else self.by_expr
        )
        return node.id, replace(
            self,
            dag=self.dag.with_fact(node),
            by_expr=by_expr,
            next_index=self.next_index + 1,
        )

    def _with_given(
        self,
        *,
        expr: BoolRef,
        text: str | None,
        subject_name: str,
        source: SourceSpan | None,
    ) -> tuple[FactId, FactGraph[StateT], bool]:
        expr = as_bool_ref(simplify(expr))
        key = expr_key(expr)
        if key in self.by_expr:
            return self.by_expr[key], self, False
        fact_id, graph = self._insert_fact(
            FactNode(
                id=self._fresh_id(),
                kind=FactKind.GIVEN,
                expr=expr,
                text=text or render_fact(expr),
                subject=subject_name,
                source=source,
            ),
            index_expression=True,
        )
        return fact_id, graph, True

    def _with_check(
        self,
        *,
        expr: BoolRef,
        text: str | None,
        subject_name: str,
        check_label: str,
        source: SourceSpan | None,
    ) -> tuple[FactId, FactGraph[StateT]]:
        expr = as_bool_ref(simplify(expr))
        return self._insert_fact(
            FactNode(
                id=self._fresh_id(),
                kind=FactKind.CHECK,
                expr=expr,
                text=text or render_fact(expr),
                subject=subject_name,
                check_label=check_label,
                source=source,
            ),
            index_expression=False,
        )

    # The token returned by each add_* method carries the asserted Prop's
    # expression type as phantom evidence of what the caller put in. Note
    # that dedupe can hand back a token for a structurally equal fact that
    # was asserted under a different expression type, so this evidence is
    # about the claim, not the stored node — a typed recall() accessor must
    # wait for Phase 4's typed check surface.

    def add_given[E: Boolish_Bound](
        self: FactGraph[Evidence[Unchecked, Unsaturated]],
        prop_: Prop[E],
        *,
        subject_name: str,
        source: SourceSpan | None = None,
    ) -> tuple[FactToken[E], FactGraph[Evidence[Unchecked, Unsaturated]]]:
        fact_id, graph, _added = self._with_given(
            expr=as_z3_bool(prop_.expr),
            text=prop_.display_text,
            subject_name=subject_name,
            source=source,
        )
        return FactToken[E](fact_id), graph

    def add_check[E: Boolish_Bound](
        self,
        prop_: Prop[E],
        *,
        subject_name: str,
        check_label: str,
        source: SourceSpan | None = None,
    ) -> tuple[FactToken[E], FactGraph[StateT]]:
        fact_id, graph = self._with_check(
            expr=as_z3_bool(prop_.expr),
            text=prop_.display_text,
            subject_name=subject_name,
            check_label=check_label,
            source=source,
        )
        return FactToken[E](fact_id), graph

    def add_derived[E: Boolish_Bound](
        self: FactGraph[Evidence[Consistent, Unsaturated]],
        prop_: Prop[E],
        *,
        premises: Iterable[FactToken[Any]],
        rule: str,
        source: SourceSpan | None = None,
    ) -> tuple[
        FactToken[E],
        bool,
        FactGraph[Evidence[Consistent, Unsaturated]],
    ]:
        proposal = DerivationProposal(
            conclusion=Prop(expr=as_z3_bool(prop_.expr), text=prop_.text),
            premises=tuple(token.id for token in premises),
            rule=rule,
            source=source,
        )
        token, added, graph = self.apply_derivation(proposal)
        return FactToken[E](token.id), added, graph

    def apply_derivation(
        self: FactGraph[Evidence[Consistent, Unsaturated]],
        proposal: DerivationProposal,
    ) -> tuple[
        FactToken[BoolRef],
        bool,
        FactGraph[Evidence[Consistent, Unsaturated]],
    ]:
        if (
            entails(
                [node.expr for node in self._premise_nodes(proposal.premises)],
                as_z3_bool(proposal.conclusion.expr),
                backend=self.reasoning_backend.semantics,
            )
            is not Entailment.PROVED
        ):
            raise ValueError(
                "Invalid derivation: premises do not entail conclusion.\n"
                f"Rule: {proposal.rule}\n"
                f"Conclusion: {as_z3_bool(proposal.conclusion.expr)}"
            )
        return self._with_derivation(proposal)

    def _premise_nodes(self, premise_ids: Iterable[FactId]) -> tuple[FactNode, ...]:
        nodes: list[FactNode] = []
        for premise_id in premise_ids:
            if premise_id not in self.dag:
                raise KeyError(
                    f"Premise token does not belong to this graph: {premise_id}"
                )
            node = self.fact(premise_id)
            if node.kind is FactKind.CHECK:
                raise ValueError(f"Checks cannot be premises: {node.id}")
            nodes.append(node)
        return tuple(nodes)

    def apply_derivations(
        self: FactGraph[Evidence[Consistent, Unsaturated]],
        proposals: Iterable[DerivationProposal],
    ) -> tuple[bool, FactGraph[Evidence[Consistent, Unsaturated]]]:
        changed = False
        working = self
        for proposal in proposals:
            _token, added, working = working.apply_derivation(proposal)
            changed |= added
        return changed, working

    def _with_derivation(
        self,
        proposal: DerivationProposal,
    ) -> tuple[FactToken[BoolRef], bool, FactGraph[StateT]]:
        premise_ids = proposal.premises
        expr = as_bool_ref(simplify(as_z3_bool(proposal.conclusion.expr)))
        key = expr_key(expr)
        existing_fact_id = self.by_expr.get(key)
        if existing_fact_id is not None:
            if existing_fact_id in premise_ids or self.dag.has_derivation(
                conclusion_id=existing_fact_id,
                premise_ids=premise_ids,
                rule=proposal.rule,
            ):
                return FactToken[BoolRef](existing_fact_id), False, self
            derivation = DerivationNode(
                id=self._fresh_derivation_id(), rule=proposal.rule
            )
            return FactToken[BoolRef](existing_fact_id), False, replace(
                self,
                dag=self.dag.with_derivation(
                    derivation,
                    premises=premise_ids,
                    conclusion=existing_fact_id,
                ),
                next_derivation_index=self.next_derivation_index + 1,
            )

        fact_id = self._fresh_id()
        derivation = DerivationNode(id=self._fresh_derivation_id(), rule=proposal.rule)
        node = FactNode(
            id=fact_id,
            kind=FactKind.DERIVED,
            expr=expr,
            text=proposal.conclusion.display_text or render_fact(expr),
            source=proposal.source,
        )
        return FactToken[BoolRef](fact_id), True, replace(
            self,
            dag=self.dag.with_fact(
                node,
                derivation=derivation,
                premises=premise_ids,
            ),
            by_expr={**self.by_expr, key: fact_id},
            next_index=self.next_index + 1,
            next_derivation_index=self.next_derivation_index + 1,
        )

    def established_facts(self) -> tuple[FactNode, ...]:
        return tuple(
            node for node in self.nodes.values() if node.kind is not FactKind.CHECK
        )

    def base_exprs(self) -> list[BoolRef]:
        return [node.expr for node in self.established_facts()]

    def derivation_input(
        self: FactGraph[Evidence[Consistent, Unsaturated]],
    ) -> DerivationInput:
        return DerivationInput(established=self.established_facts())

    def explanation_input(
        self: FactGraph[Evidence[Consistent, Saturated]],
        checks: Iterable[FactToken[Any]],
    ) -> ExplanationInput:
        check_nodes = tuple(self.fact(token.id) for token in checks)
        for node in check_nodes:
            if node.kind is not FactKind.CHECK:
                raise ValueError(f"Not a check token: {node.id}")
        return ExplanationInput(
            established=self.established_facts(),
            checks=check_nodes,
        )

    def check_consistent[SaturationT](
        self: FactGraph[Evidence[Unchecked, SaturationT]],
    ) -> FactGraph[Evidence[Consistent, SaturationT]]:
        result = self.reasoning_backend.semantics.solve(self.base_exprs())
        if result.status is SolveStatus.UNSAT:
            lines = "\n".join(f"  {expr}" for expr in result.core)
            raise ValueError(f"Inconsistent givens:\n{lines}")
        if result.status in (SolveStatus.UNKNOWN, SolveStatus.TIMEOUT):
            raise ValueError("Solver could not determine consistency.")
        return cast(FactGraph[Evidence[Consistent, SaturationT]], self)

    def saturate(
        self: FactGraph[Evidence[Consistent, Unsaturated]],
    ) -> FactGraph[Evidence[Consistent, Saturated]]:
        working = self
        for _round in range(self.reasoning_backend.max_rounds):
            changed, working = working.apply_derivations(
                self.reasoning_backend.derivation.derive(working.derivation_input())
            )
            if not changed:
                return cast(FactGraph[Evidence[Consistent, Saturated]], working)
        raise RuntimeError("Derivation did not reach a fixed point.")

    def classify[SaturationT](
        self: FactGraph[Evidence[Consistent, SaturationT]],
        check: BoolRef,
    ) -> CheckResult:
        return classify(
            self.base_exprs(), check, backend=self.reasoning_backend.semantics
        )

    def verify_derivations(self) -> list[str]:
        """Re-check every stored derivation against the solver.

        Derivations are already entails-verified at insertion time in
        ``add_derived``; this is an opt-in audit for callers who want to
        re-establish that guarantee (e.g. over a deserialized graph), not
        something the solving pipeline runs per round.
        """
        errors: list[str] = []

        for conclusion_id, derivations in self.derivations.items():
            for derivation in derivations:
                premises = [
                    self.fact(premise_id).expr for premise_id in derivation.premise_ids
                ]
                conclusion = self.fact(conclusion_id).expr

                if entails(
                    premises,
                    conclusion,
                    backend=self.reasoning_backend.semantics,
                ) is not Entailment.PROVED:
                    errors.append(
                        f"Invalid derivation {conclusion_id}: {derivation.rule}"
                    )

        return errors

    def explanation_for(self, target: FactToken[Any]) -> list[str]:
        target_id = target.id

        if target_id not in self.dag:
            raise KeyError(f"Unknown fact id: {target_id}")

        lines: list[str] = []

        for node in self.dag.explanation_nodes(target_id):
            if isinstance(node, (DerivationNode, ExplanationNode)):
                lines.append(f"Using rule: {node.rule}")
                continue

            if node.kind == FactKind.GIVEN:
                lines.append(f"Given: {node.text}")

            elif node.kind == FactKind.DERIVED:
                lines.append(f"Therefore: {node.text}")

            else:
                lines.append(f"Check: {node.text}")

        return lines

    def explanation_subgraph_for(
        self,
        target: FactToken[Any],
    ) -> FactGraph[StateT]:
        """Return the minimal ancestor subgraph explaining ``target``.

        This is the graph-shaped counterpart to ``explanation_for``. It keeps
        the same immutable graph wrapper, but restricts the DAG to the target
        fact plus all graph nodes that feed into it, including derivation steps.
        """
        target_id = target.id

        if target_id not in self.dag:
            raise KeyError(f"Unknown fact id: {target_id}")

        sliced_dag = self.dag.slice_for(target_id)

        by_expr = {
            key: fact_id
            for key, fact_id in self.by_expr.items()
            if fact_id in sliced_dag
        }

        return replace(
            self,
            dag=sliced_dag,
            by_expr=by_expr,
        )

    def explain_check(
        self: FactGraph[Evidence[Consistent, Saturated]],
        check: FactToken[Any],
    ) -> tuple[bool, FactGraph[Evidence[Consistent, Saturated]]]:
        check_id = check.id
        if check_id not in self.dag:
            raise KeyError(f"Check token does not belong to this graph: {check_id}")
        check_node = self.fact(check_id)
        if check_node.kind is not FactKind.CHECK:
            raise ValueError(f"Not a check token: {check_id}")
        if self.dag.in_degree(check_id) > 0:
            return True, self

        return next(
            iter((True, self.apply_explanation(x)) for x in
                self.reasoning_backend.explanation.explain(
                    self.explanation_input((check,)),
                    self.reasoning_backend.semantics,
                )
            ),
            (False, self),
        )

    def apply_explanation(
        self,
        proposal: ExplanationProposal,
    ) -> FactGraph[StateT]:
        if proposal.check_id not in self.dag:
            raise KeyError(
                f"Check token does not belong to this graph: {proposal.check_id}"
            )
        check_node = self.fact(proposal.check_id)
        if check_node.kind is not FactKind.CHECK:
            raise ValueError(f"Not a check token: {proposal.check_id}")
        premises = self._premise_nodes(proposal.premises)
        if (
            entails(
                [premise.expr for premise in premises],
                check_node.expr,
                backend=self.reasoning_backend.semantics,
            )
            is not Entailment.PROVED
        ):
            raise ValueError("Explanation premises do not entail the check.")
        step = ExplanationNode(
            id=self._fresh_derivation_id(),
            rule=proposal.rule,
        )
        return replace(
            self,
            dag=self.dag.with_explanation(
                step,
                premises=proposal.premises,
                check=proposal.check_id,
            ),
            next_derivation_index=self.next_derivation_index + 1,
        )

dag class-attribute instance-attribute

dag = field(default_factory=ProvenanceDag)

by_expr class-attribute instance-attribute

by_expr = field(default_factory=dict)

next_index class-attribute instance-attribute

next_index = 1

next_derivation_index class-attribute instance-attribute

next_derivation_index = 1

reasoning_backend class-attribute instance-attribute

reasoning_backend = field(
    default_factory=default_reasoning_backend,
    compare=False,
    repr=False,
)

nodes property

nodes

derivation_nodes property

derivation_nodes

derivations property

derivations

empty classmethod

empty()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@classmethod
def empty(cls) -> FactGraph[Evidence[Unchecked, Unsaturated]]:
    return FactGraph()

with_reasoning_backend

with_reasoning_backend(backend)

Return an equal immutable graph using backend operationally.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def with_reasoning_backend(
    self,
    backend: ReasoningBackend,
) -> FactGraph[StateT]:
    """Return an equal immutable graph using ``backend`` operationally."""
    return replace(self, reasoning_backend=backend)

fact

fact(fact_id)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def fact(self, fact_id: FactId) -> FactNode:
    return self.dag.fact(fact_id)

derivation_step

derivation_step(derivation_id)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def derivation_step(self, derivation_id: DerivationId) -> DerivationNode:
    return self.dag.derivation(derivation_id)

add_given

add_given(prop_, *, subject_name, source=None)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def add_given[E: Boolish_Bound](
    self: FactGraph[Evidence[Unchecked, Unsaturated]],
    prop_: Prop[E],
    *,
    subject_name: str,
    source: SourceSpan | None = None,
) -> tuple[FactToken[E], FactGraph[Evidence[Unchecked, Unsaturated]]]:
    fact_id, graph, _added = self._with_given(
        expr=as_z3_bool(prop_.expr),
        text=prop_.display_text,
        subject_name=subject_name,
        source=source,
    )
    return FactToken[E](fact_id), graph

add_check

add_check(prop_, *, subject_name, check_label, source=None)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def add_check[E: Boolish_Bound](
    self,
    prop_: Prop[E],
    *,
    subject_name: str,
    check_label: str,
    source: SourceSpan | None = None,
) -> tuple[FactToken[E], FactGraph[StateT]]:
    fact_id, graph = self._with_check(
        expr=as_z3_bool(prop_.expr),
        text=prop_.display_text,
        subject_name=subject_name,
        check_label=check_label,
        source=source,
    )
    return FactToken[E](fact_id), graph

add_derived

add_derived(prop_, *, premises, rule, source=None)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def add_derived[E: Boolish_Bound](
    self: FactGraph[Evidence[Consistent, Unsaturated]],
    prop_: Prop[E],
    *,
    premises: Iterable[FactToken[Any]],
    rule: str,
    source: SourceSpan | None = None,
) -> tuple[
    FactToken[E],
    bool,
    FactGraph[Evidence[Consistent, Unsaturated]],
]:
    proposal = DerivationProposal(
        conclusion=Prop(expr=as_z3_bool(prop_.expr), text=prop_.text),
        premises=tuple(token.id for token in premises),
        rule=rule,
        source=source,
    )
    token, added, graph = self.apply_derivation(proposal)
    return FactToken[E](token.id), added, graph

apply_derivation

apply_derivation(proposal)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def apply_derivation(
    self: FactGraph[Evidence[Consistent, Unsaturated]],
    proposal: DerivationProposal,
) -> tuple[
    FactToken[BoolRef],
    bool,
    FactGraph[Evidence[Consistent, Unsaturated]],
]:
    if (
        entails(
            [node.expr for node in self._premise_nodes(proposal.premises)],
            as_z3_bool(proposal.conclusion.expr),
            backend=self.reasoning_backend.semantics,
        )
        is not Entailment.PROVED
    ):
        raise ValueError(
            "Invalid derivation: premises do not entail conclusion.\n"
            f"Rule: {proposal.rule}\n"
            f"Conclusion: {as_z3_bool(proposal.conclusion.expr)}"
        )
    return self._with_derivation(proposal)

apply_derivations

apply_derivations(proposals)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def apply_derivations(
    self: FactGraph[Evidence[Consistent, Unsaturated]],
    proposals: Iterable[DerivationProposal],
) -> tuple[bool, FactGraph[Evidence[Consistent, Unsaturated]]]:
    changed = False
    working = self
    for proposal in proposals:
        _token, added, working = working.apply_derivation(proposal)
        changed |= added
    return changed, working

established_facts

established_facts()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def established_facts(self) -> tuple[FactNode, ...]:
    return tuple(
        node for node in self.nodes.values() if node.kind is not FactKind.CHECK
    )

base_exprs

base_exprs()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def base_exprs(self) -> list[BoolRef]:
    return [node.expr for node in self.established_facts()]

derivation_input

derivation_input()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def derivation_input(
    self: FactGraph[Evidence[Consistent, Unsaturated]],
) -> DerivationInput:
    return DerivationInput(established=self.established_facts())

explanation_input

explanation_input(checks)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def explanation_input(
    self: FactGraph[Evidence[Consistent, Saturated]],
    checks: Iterable[FactToken[Any]],
) -> ExplanationInput:
    check_nodes = tuple(self.fact(token.id) for token in checks)
    for node in check_nodes:
        if node.kind is not FactKind.CHECK:
            raise ValueError(f"Not a check token: {node.id}")
    return ExplanationInput(
        established=self.established_facts(),
        checks=check_nodes,
    )

check_consistent

check_consistent()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def check_consistent[SaturationT](
    self: FactGraph[Evidence[Unchecked, SaturationT]],
) -> FactGraph[Evidence[Consistent, SaturationT]]:
    result = self.reasoning_backend.semantics.solve(self.base_exprs())
    if result.status is SolveStatus.UNSAT:
        lines = "\n".join(f"  {expr}" for expr in result.core)
        raise ValueError(f"Inconsistent givens:\n{lines}")
    if result.status in (SolveStatus.UNKNOWN, SolveStatus.TIMEOUT):
        raise ValueError("Solver could not determine consistency.")
    return cast(FactGraph[Evidence[Consistent, SaturationT]], self)

saturate

saturate()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def saturate(
    self: FactGraph[Evidence[Consistent, Unsaturated]],
) -> FactGraph[Evidence[Consistent, Saturated]]:
    working = self
    for _round in range(self.reasoning_backend.max_rounds):
        changed, working = working.apply_derivations(
            self.reasoning_backend.derivation.derive(working.derivation_input())
        )
        if not changed:
            return cast(FactGraph[Evidence[Consistent, Saturated]], working)
    raise RuntimeError("Derivation did not reach a fixed point.")

classify

classify(check)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def classify[SaturationT](
    self: FactGraph[Evidence[Consistent, SaturationT]],
    check: BoolRef,
) -> CheckResult:
    return classify(
        self.base_exprs(), check, backend=self.reasoning_backend.semantics
    )

verify_derivations

verify_derivations()

Re-check every stored derivation against the solver.

Derivations are already entails-verified at insertion time in add_derived; this is an opt-in audit for callers who want to re-establish that guarantee (e.g. over a deserialized graph), not something the solving pipeline runs per round.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def verify_derivations(self) -> list[str]:
    """Re-check every stored derivation against the solver.

    Derivations are already entails-verified at insertion time in
    ``add_derived``; this is an opt-in audit for callers who want to
    re-establish that guarantee (e.g. over a deserialized graph), not
    something the solving pipeline runs per round.
    """
    errors: list[str] = []

    for conclusion_id, derivations in self.derivations.items():
        for derivation in derivations:
            premises = [
                self.fact(premise_id).expr for premise_id in derivation.premise_ids
            ]
            conclusion = self.fact(conclusion_id).expr

            if entails(
                premises,
                conclusion,
                backend=self.reasoning_backend.semantics,
            ) is not Entailment.PROVED:
                errors.append(
                    f"Invalid derivation {conclusion_id}: {derivation.rule}"
                )

    return errors

explanation_for

explanation_for(target)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def explanation_for(self, target: FactToken[Any]) -> list[str]:
    target_id = target.id

    if target_id not in self.dag:
        raise KeyError(f"Unknown fact id: {target_id}")

    lines: list[str] = []

    for node in self.dag.explanation_nodes(target_id):
        if isinstance(node, (DerivationNode, ExplanationNode)):
            lines.append(f"Using rule: {node.rule}")
            continue

        if node.kind == FactKind.GIVEN:
            lines.append(f"Given: {node.text}")

        elif node.kind == FactKind.DERIVED:
            lines.append(f"Therefore: {node.text}")

        else:
            lines.append(f"Check: {node.text}")

    return lines

explanation_subgraph_for

explanation_subgraph_for(target)

Return the minimal ancestor subgraph explaining target.

This is the graph-shaped counterpart to explanation_for. It keeps the same immutable graph wrapper, but restricts the DAG to the target fact plus all graph nodes that feed into it, including derivation steps.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def explanation_subgraph_for(
    self,
    target: FactToken[Any],
) -> FactGraph[StateT]:
    """Return the minimal ancestor subgraph explaining ``target``.

    This is the graph-shaped counterpart to ``explanation_for``. It keeps
    the same immutable graph wrapper, but restricts the DAG to the target
    fact plus all graph nodes that feed into it, including derivation steps.
    """
    target_id = target.id

    if target_id not in self.dag:
        raise KeyError(f"Unknown fact id: {target_id}")

    sliced_dag = self.dag.slice_for(target_id)

    by_expr = {
        key: fact_id
        for key, fact_id in self.by_expr.items()
        if fact_id in sliced_dag
    }

    return replace(
        self,
        dag=sliced_dag,
        by_expr=by_expr,
    )

explain_check

explain_check(check)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def explain_check(
    self: FactGraph[Evidence[Consistent, Saturated]],
    check: FactToken[Any],
) -> tuple[bool, FactGraph[Evidence[Consistent, Saturated]]]:
    check_id = check.id
    if check_id not in self.dag:
        raise KeyError(f"Check token does not belong to this graph: {check_id}")
    check_node = self.fact(check_id)
    if check_node.kind is not FactKind.CHECK:
        raise ValueError(f"Not a check token: {check_id}")
    if self.dag.in_degree(check_id) > 0:
        return True, self

    return next(
        iter((True, self.apply_explanation(x)) for x in
            self.reasoning_backend.explanation.explain(
                self.explanation_input((check,)),
                self.reasoning_backend.semantics,
            )
        ),
        (False, self),
    )

apply_explanation

apply_explanation(proposal)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def apply_explanation(
    self,
    proposal: ExplanationProposal,
) -> FactGraph[StateT]:
    if proposal.check_id not in self.dag:
        raise KeyError(
            f"Check token does not belong to this graph: {proposal.check_id}"
        )
    check_node = self.fact(proposal.check_id)
    if check_node.kind is not FactKind.CHECK:
        raise ValueError(f"Not a check token: {proposal.check_id}")
    premises = self._premise_nodes(proposal.premises)
    if (
        entails(
            [premise.expr for premise in premises],
            check_node.expr,
            backend=self.reasoning_backend.semantics,
        )
        is not Entailment.PROVED
    ):
        raise ValueError("Explanation premises do not entail the check.")
    step = ExplanationNode(
        id=self._fresh_derivation_id(),
        rule=proposal.rule,
    )
    return replace(
        self,
        dag=self.dag.with_explanation(
            step,
            premises=proposal.premises,
            check=proposal.check_id,
        ),
        next_derivation_index=self.next_derivation_index + 1,
    )

FactGraphExplanationBackend dataclass

Use shared semantic equivalence to propose check explanations.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class FactGraphExplanationBackend:
    """Use shared semantic equivalence to propose check explanations."""

    def explain(
        self,
        input_: ExplanationInput,
        semantics: SemanticBackend,
    ) -> Iterable[ExplanationProposal]:
        for check_node in input_.checks:
            for node in input_.established:
                if equivalent(
                    node.expr, check_node.expr, backend=semantics
                ) is Entailment.PROVED:
                    yield ExplanationProposal(
                        check_id=check_node.id,
                        premises=(node.id,),
                        rule="check is equivalent to a known fact",
                    )
                    break

explain

explain(input_, semantics)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def explain(
    self,
    input_: ExplanationInput,
    semantics: SemanticBackend,
) -> Iterable[ExplanationProposal]:
    for check_node in input_.checks:
        for node in input_.established:
            if equivalent(
                node.expr, check_node.expr, backend=semantics
            ) is Entailment.PROVED:
                yield ExplanationProposal(
                    check_id=check_node.id,
                    premises=(node.id,),
                    rule="check is equivalent to a known fact",
                )
                break

FactId dataclass

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class FactId:
    value: str

    def __str__(self) -> str:
        return self.value

value instance-attribute

value

FactKind

Bases: str, Enum

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

class FactKind(str, Enum):
    GIVEN = "GIVEN"
    DERIVED = "DERIVED"
    CHECK = "CHECK"

GIVEN class-attribute instance-attribute

GIVEN = 'GIVEN'

DERIVED class-attribute instance-attribute

DERIVED = 'DERIVED'

CHECK class-attribute instance-attribute

CHECK = 'CHECK'

FactNode dataclass

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class FactNode:
    id: FactId
    kind: FactKind
    expr: BoolRef
    text: str
    subject: str | None = None
    check_label: str | None = None
    source: SourceSpan | None = None

id instance-attribute

id

kind instance-attribute

kind

expr instance-attribute

expr

text instance-attribute

text

subject class-attribute instance-attribute

subject = None

check_label class-attribute instance-attribute

check_label = None

source class-attribute instance-attribute

source = None

FactToken dataclass

Bases: Generic[ExprT]

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class FactToken(Generic[ExprT]):
    id: FactId

id instance-attribute

id

ForwardDerivationBackend dataclass

Current Python fixed-point rules behind the derivation interface.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class ForwardDerivationBackend:
    """Current Python fixed-point rules behind the derivation interface."""

    def derive(
        self,
        input_: DerivationInput,
    ) -> Iterable[DerivationProposal]:
        yield from _propose_simplified_equalities(input_)
        yield from _propose_offset_constants(input_)
        yield from _propose_equalities_from_shared_constants(input_)

derive

derive(input_)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def derive(
    self,
    input_: DerivationInput,
) -> Iterable[DerivationProposal]:
    yield from _propose_simplified_equalities(input_)
    yield from _propose_offset_constants(input_)
    yield from _propose_equalities_from_shared_constants(input_)

IngestedPuzzle dataclass

Bases: Generic[PuzzleT]

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class IngestedPuzzle(Generic[PuzzleT]):
    puzzle: PuzzleT
    graph: FactGraph[Evidence[Unchecked, Unsaturated]]
    check_tokens: dict[str, FactToken[Any]]

puzzle instance-attribute

puzzle

graph instance-attribute

graph

check_tokens instance-attribute

check_tokens

LinearOffset dataclass

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class LinearOffset:
    source: ArithRef
    offset: int

source instance-attribute

source

offset instance-attribute

offset

ProvenanceDag dataclass

Typed boundary around the heterogeneous provenance rustworkx DAG.

rustworkx has no freeze() equivalent, so immutability is by convention, not by runtime guard: every mutating method below builds a fresh .copy() (via to_rustworkx) and never touches self._graph or self._index_by_id in place.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class ProvenanceDag:
    """Typed boundary around the heterogeneous provenance rustworkx DAG.

    rustworkx has no ``freeze()`` equivalent, so immutability is by convention,
    not by runtime guard: every mutating method below builds a fresh
    ``.copy()`` (via ``to_rustworkx``) and never touches ``self._graph`` or
    ``self._index_by_id`` in place.
    """

    _graph: rx.PyDiGraph = field(default_factory=empty_rustworkx_digraph, repr=False)
    _index_by_id: Mapping[GraphNodeId, int] = field(default_factory=dict, repr=False)

    @classmethod
    def from_rustworkx(cls, graph: rx.PyDiGraph) -> ProvenanceDag:
        """Copy, validate, and adopt a raw interoperability graph."""
        copied = graph.copy()
        index_by_id: dict[GraphNodeId, int] = {}
        for idx in copied.node_indices():
            node_id = getattr(copied.get_node_data(idx), "id", None)
            if node_id is not None and node_id not in index_by_id:
                index_by_id[node_id] = idx
        result = cls(_graph=copied, _index_by_id=index_by_id)
        result.validate()
        return result

    def to_rustworkx(self) -> rx.PyDiGraph:
        """Return a mutable copy for explicit interoperability boundaries."""
        return self._graph.copy()

    def _replace_graph(
        self, graph: rx.PyDiGraph, index_by_id: Mapping[GraphNodeId, int]
    ) -> ProvenanceDag:
        return replace(self, _graph=graph, _index_by_id=index_by_id)

    def validate(self) -> None:
        """Establish the complete typed provenance topology at one boundary."""
        if not rx.is_directed_acyclic_graph(self._graph):
            raise ValueError("Provenance graph must be acyclic.")

        for idx in self._graph.node_indices():
            payload = self._graph.get_node_data(idx)
            if not isinstance(payload, (FactNode, DerivationNode, ExplanationNode)):
                raise TypeError(f"Unknown node payload: index {idx}")

        seen_ids: set[GraphNodeId] = set()
        for idx in self._graph.node_indices():
            node_id = self._graph.get_node_data(idx).id
            if node_id in seen_ids:
                raise ValueError(f"Duplicate node id: {node_id}")
            seen_ids.add(node_id)

        for source_idx, target_idx in self._graph.edge_list():
            source = self._graph.get_node_data(source_idx)
            target = self._graph.get_node_data(target_idx)
            source_is_fact = isinstance(source, FactNode)
            target_is_fact = isinstance(target, FactNode)
            if source_is_fact == target_is_fact:
                raise ValueError(
                    f"Invalid provenance edge: {source.id} -> {target.id}"
                )
            if source_is_fact and source.kind is FactKind.CHECK:
                raise ValueError(f"Checks cannot be premises: {source.id}")

        for idx in self._graph.node_indices():
            payload = self._graph.get_node_data(idx)
            if isinstance(payload, FactNode):
                continue

            successor_indices = self._graph.successor_indices(idx)
            if len(successor_indices) != 1 or not isinstance(
                self._graph.get_node_data(successor_indices[0]), FactNode
            ):
                raise ValueError(
                    f"Provenance steps need exactly one fact conclusion: {payload.id}"
                )
            conclusion = self._graph.get_node_data(successor_indices[0])
            if isinstance(payload, DerivationNode):
                if conclusion.kind is FactKind.CHECK:
                    raise ValueError(
                        f"Derivations cannot conclude checks: {payload.id}"
                    )
            elif conclusion.kind is not FactKind.CHECK:
                raise ValueError(f"Explanations must conclude checks: {payload.id}")

    def __contains__(self, node_id: object) -> bool:
        return node_id in self._index_by_id

    def _required_payload[PayloadT](
        self,
        node_id: GraphNodeId,
        payload_type: type[PayloadT],
        label: str,
    ) -> PayloadT:
        payload = self._graph.get_node_data(self._index_by_id[node_id])
        if not isinstance(payload, payload_type):
            raise TypeError(f"Not a {label} node: {node_id}")
        return payload

    def fact(self, fact_id: FactId) -> FactNode:
        return self._required_payload(fact_id, FactNode, "fact")

    def derivation(self, derivation_id: DerivationId) -> DerivationNode:
        return self._required_payload(derivation_id, DerivationNode, "derivation")

    def explanation(self, step_id: DerivationId) -> ExplanationNode:
        return self._required_payload(step_id, ExplanationNode, "explanation")

    def facts(self) -> Mapping[FactId, FactNode]:
        return {node.id: node for node in self.nodes() if isinstance(node, FactNode)}

    def derivation_nodes(self) -> Mapping[DerivationId, DerivationNode]:
        return {
            node.id: node for node in self.nodes() if isinstance(node, DerivationNode)
        }

    def nodes(self) -> Iterator[FactNode | DerivationNode | ExplanationNode]:
        for idx in self._graph.node_indices():
            yield cast(
                FactNode | DerivationNode | ExplanationNode,
                self._graph.get_node_data(idx),
            )

    def edges(self) -> Iterator[tuple[GraphNodeId, GraphNodeId]]:
        """Yield edges grouped by source in node-creation order.

        ``rx.PyDiGraph.edge_list()`` orders by raw edge-insertion time, which
        depends on incidental construction order rather than graph content —
        two structurally equivalent graphs built in a different sequence (or
        via a different backend) could yield edges differently, changing
        renderer output for no semantic reason. Iterating nodes in creation
        order, then each node's own successors, is canonical: it depends only
        on stable node identity (assigned once, at creation), not on when an
        edge happened to be added.
        """
        graph = self._graph
        for source_idx in graph.node_indices():
            source_id = cast(GraphNodeId, graph.get_node_data(source_idx).id)
            # rustworkx yields successors in reverse edge-insertion order;
            # reverse back for a stable, content-derived order.
            for target_idx in reversed(graph.successor_indices(source_idx)):
                yield source_id, cast(GraphNodeId, graph.get_node_data(target_idx).id)

    def in_degree(self, fact_id: FactId) -> int:
        return int(self._graph.in_degree(self._index_by_id[fact_id]))

    def has_edge(self, source: GraphNodeId, target: GraphNodeId) -> bool:
        source_idx = self._index_by_id.get(source)
        target_idx = self._index_by_id.get(target)
        if source_idx is None or target_idx is None:
            return False
        return self._graph.has_edge(source_idx, target_idx)

    def _fact_predecessors(self, node_id: GraphNodeId) -> Iterator[FactId]:
        graph = self._graph
        # rustworkx yields predecessors in reverse edge-insertion order;
        # reverse back so premise order matches the order they were added in.
        indices = reversed(graph.predecessor_indices(self._index_by_id[node_id]))
        return (
            graph.get_node_data(idx).id
            for idx in indices
            if isinstance(graph.get_node_data(idx), FactNode)
        )

    def explanation_node_ids(
        self,
        target_id: FactId,
    ) -> frozenset[GraphNodeId]:
        """Return the target and every provenance node contributing to it."""
        if target_id not in self._index_by_id:
            raise KeyError(f"Unknown fact id: {target_id}")

        ancestor_indices = rx.ancestors(self._graph, self._index_by_id[target_id])
        ancestor_ids = {self._graph.get_node_data(i).id for i in ancestor_indices}
        return frozenset(ancestor_ids | {target_id})

    def derivations(self) -> Mapping[FactId, tuple[Derivation, ...]]:
        result: dict[FactId, list[Derivation]] = {}
        for derivation_id, derivation in self.derivation_nodes().items():
            premise_ids = tuple(self._fact_predecessors(derivation_id))
            successor_indices = self._graph.successor_indices(
                self._index_by_id[derivation_id]
            )
            conclusion_id = cast(
                FactId, self._graph.get_node_data(next(iter(successor_indices))).id
            )
            result.setdefault(conclusion_id, []).append(
                Derivation(premise_ids=premise_ids, rule=derivation.rule)
            )
        return {fact_id: tuple(items) for fact_id, items in result.items()}

    def has_derivation(
        self,
        *,
        conclusion_id: FactId,
        premise_ids: tuple[FactId, ...],
        rule: str,
    ) -> bool:
        expected_premises = set(premise_ids)
        for predecessor_idx in self._graph.predecessor_indices(
            self._index_by_id[conclusion_id]
        ):
            predecessor = self._graph.get_node_data(predecessor_idx)
            if not isinstance(predecessor, DerivationNode):
                continue
            if predecessor.rule != rule:
                continue
            actual_premises = set(self._fact_predecessors(predecessor.id))
            if actual_premises == expected_premises:
                return True
        return False

    def with_fact(
        self,
        node: FactNode,
        *,
        derivation: DerivationNode | None = None,
        premises: tuple[FactId, ...] = (),
    ) -> ProvenanceDag:
        graph = self.to_rustworkx()
        index_by_id = dict(self._index_by_id)
        index_by_id[node.id] = graph.add_node(node)
        if derivation is not None:
            return self._with_step(
                derivation,
                premises=premises,
                conclusion=node.id,
                graph=graph,
                index_by_id=index_by_id,
            )
        return self._replace_graph(graph, index_by_id)

    def _with_step(
        self,
        step: DerivationNode | ExplanationNode,
        *,
        premises: tuple[FactId, ...],
        conclusion: FactId,
        graph: rx.PyDiGraph | None = None,
        index_by_id: Mapping[GraphNodeId, int] | None = None,
    ) -> ProvenanceDag:
        graph = self.to_rustworkx() if graph is None else graph
        index_by_id = dict(self._index_by_id if index_by_id is None else index_by_id)
        step_idx = graph.add_node(step)
        index_by_id[step.id] = step_idx
        for premise in premises:
            graph.add_edge(index_by_id[premise], step_idx, None)
        graph.add_edge(step_idx, index_by_id[conclusion], None)
        return self._replace_graph(graph, index_by_id)

    def with_derivation(
        self,
        derivation: DerivationNode,
        *,
        premises: tuple[FactId, ...],
        conclusion: FactId,
    ) -> ProvenanceDag:
        return self._with_step(
            derivation,
            premises=premises,
            conclusion=conclusion,
        )

    def with_explanation(
        self,
        explanation: ExplanationNode,
        *,
        premises: tuple[FactId, ...],
        check: FactId,
    ) -> ProvenanceDag:
        return self._with_step(
            explanation,
            premises=premises,
            conclusion=check,
        )

    def explanation_nodes(
        self, target_id: FactId
    ) -> Iterator[FactNode | DerivationNode | ExplanationNode]:
        relevant_ids = self.explanation_node_ids(target_id)
        relevant_indices = [self._index_by_id[node_id] for node_id in relevant_ids]
        sub = self._graph.subgraph(relevant_indices)
        for idx in rx.topological_sort(sub):
            payload = sub.get_node_data(idx)
            if isinstance(payload, FactNode):
                yield self.fact(payload.id)
            elif isinstance(payload, DerivationNode):
                yield self.derivation(payload.id)
            else:
                yield self.explanation(payload.id)

    def slice_for(self, target_id: FactId) -> ProvenanceDag:
        relevant_ids = self.explanation_node_ids(target_id)
        relevant_indices = [self._index_by_id[node_id] for node_id in relevant_ids]
        sub = self._graph.subgraph(relevant_indices)
        index_by_id = {
            sub.get_node_data(idx).id: idx for idx in sub.node_indices()
        }
        return self._replace_graph(sub, index_by_id)

from_rustworkx classmethod

from_rustworkx(graph)

Copy, validate, and adopt a raw interoperability graph.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@classmethod
def from_rustworkx(cls, graph: rx.PyDiGraph) -> ProvenanceDag:
    """Copy, validate, and adopt a raw interoperability graph."""
    copied = graph.copy()
    index_by_id: dict[GraphNodeId, int] = {}
    for idx in copied.node_indices():
        node_id = getattr(copied.get_node_data(idx), "id", None)
        if node_id is not None and node_id not in index_by_id:
            index_by_id[node_id] = idx
    result = cls(_graph=copied, _index_by_id=index_by_id)
    result.validate()
    return result

to_rustworkx

to_rustworkx()

Return a mutable copy for explicit interoperability boundaries.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def to_rustworkx(self) -> rx.PyDiGraph:
    """Return a mutable copy for explicit interoperability boundaries."""
    return self._graph.copy()

validate

validate()

Establish the complete typed provenance topology at one boundary.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def validate(self) -> None:
    """Establish the complete typed provenance topology at one boundary."""
    if not rx.is_directed_acyclic_graph(self._graph):
        raise ValueError("Provenance graph must be acyclic.")

    for idx in self._graph.node_indices():
        payload = self._graph.get_node_data(idx)
        if not isinstance(payload, (FactNode, DerivationNode, ExplanationNode)):
            raise TypeError(f"Unknown node payload: index {idx}")

    seen_ids: set[GraphNodeId] = set()
    for idx in self._graph.node_indices():
        node_id = self._graph.get_node_data(idx).id
        if node_id in seen_ids:
            raise ValueError(f"Duplicate node id: {node_id}")
        seen_ids.add(node_id)

    for source_idx, target_idx in self._graph.edge_list():
        source = self._graph.get_node_data(source_idx)
        target = self._graph.get_node_data(target_idx)
        source_is_fact = isinstance(source, FactNode)
        target_is_fact = isinstance(target, FactNode)
        if source_is_fact == target_is_fact:
            raise ValueError(
                f"Invalid provenance edge: {source.id} -> {target.id}"
            )
        if source_is_fact and source.kind is FactKind.CHECK:
            raise ValueError(f"Checks cannot be premises: {source.id}")

    for idx in self._graph.node_indices():
        payload = self._graph.get_node_data(idx)
        if isinstance(payload, FactNode):
            continue

        successor_indices = self._graph.successor_indices(idx)
        if len(successor_indices) != 1 or not isinstance(
            self._graph.get_node_data(successor_indices[0]), FactNode
        ):
            raise ValueError(
                f"Provenance steps need exactly one fact conclusion: {payload.id}"
            )
        conclusion = self._graph.get_node_data(successor_indices[0])
        if isinstance(payload, DerivationNode):
            if conclusion.kind is FactKind.CHECK:
                raise ValueError(
                    f"Derivations cannot conclude checks: {payload.id}"
                )
        elif conclusion.kind is not FactKind.CHECK:
            raise ValueError(f"Explanations must conclude checks: {payload.id}")

fact

fact(fact_id)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def fact(self, fact_id: FactId) -> FactNode:
    return self._required_payload(fact_id, FactNode, "fact")

derivation

derivation(derivation_id)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def derivation(self, derivation_id: DerivationId) -> DerivationNode:
    return self._required_payload(derivation_id, DerivationNode, "derivation")

explanation

explanation(step_id)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def explanation(self, step_id: DerivationId) -> ExplanationNode:
    return self._required_payload(step_id, ExplanationNode, "explanation")

facts

facts()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def facts(self) -> Mapping[FactId, FactNode]:
    return {node.id: node for node in self.nodes() if isinstance(node, FactNode)}

derivation_nodes

derivation_nodes()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def derivation_nodes(self) -> Mapping[DerivationId, DerivationNode]:
    return {
        node.id: node for node in self.nodes() if isinstance(node, DerivationNode)
    }

nodes

nodes()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def nodes(self) -> Iterator[FactNode | DerivationNode | ExplanationNode]:
    for idx in self._graph.node_indices():
        yield cast(
            FactNode | DerivationNode | ExplanationNode,
            self._graph.get_node_data(idx),
        )

edges

edges()

Yield edges grouped by source in node-creation order.

rx.PyDiGraph.edge_list() orders by raw edge-insertion time, which depends on incidental construction order rather than graph content — two structurally equivalent graphs built in a different sequence (or via a different backend) could yield edges differently, changing renderer output for no semantic reason. Iterating nodes in creation order, then each node's own successors, is canonical: it depends only on stable node identity (assigned once, at creation), not on when an edge happened to be added.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def edges(self) -> Iterator[tuple[GraphNodeId, GraphNodeId]]:
    """Yield edges grouped by source in node-creation order.

    ``rx.PyDiGraph.edge_list()`` orders by raw edge-insertion time, which
    depends on incidental construction order rather than graph content —
    two structurally equivalent graphs built in a different sequence (or
    via a different backend) could yield edges differently, changing
    renderer output for no semantic reason. Iterating nodes in creation
    order, then each node's own successors, is canonical: it depends only
    on stable node identity (assigned once, at creation), not on when an
    edge happened to be added.
    """
    graph = self._graph
    for source_idx in graph.node_indices():
        source_id = cast(GraphNodeId, graph.get_node_data(source_idx).id)
        # rustworkx yields successors in reverse edge-insertion order;
        # reverse back for a stable, content-derived order.
        for target_idx in reversed(graph.successor_indices(source_idx)):
            yield source_id, cast(GraphNodeId, graph.get_node_data(target_idx).id)

in_degree

in_degree(fact_id)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def in_degree(self, fact_id: FactId) -> int:
    return int(self._graph.in_degree(self._index_by_id[fact_id]))

has_edge

has_edge(source, target)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def has_edge(self, source: GraphNodeId, target: GraphNodeId) -> bool:
    source_idx = self._index_by_id.get(source)
    target_idx = self._index_by_id.get(target)
    if source_idx is None or target_idx is None:
        return False
    return self._graph.has_edge(source_idx, target_idx)

explanation_node_ids

explanation_node_ids(target_id)

Return the target and every provenance node contributing to it.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def explanation_node_ids(
    self,
    target_id: FactId,
) -> frozenset[GraphNodeId]:
    """Return the target and every provenance node contributing to it."""
    if target_id not in self._index_by_id:
        raise KeyError(f"Unknown fact id: {target_id}")

    ancestor_indices = rx.ancestors(self._graph, self._index_by_id[target_id])
    ancestor_ids = {self._graph.get_node_data(i).id for i in ancestor_indices}
    return frozenset(ancestor_ids | {target_id})

derivations

derivations()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def derivations(self) -> Mapping[FactId, tuple[Derivation, ...]]:
    result: dict[FactId, list[Derivation]] = {}
    for derivation_id, derivation in self.derivation_nodes().items():
        premise_ids = tuple(self._fact_predecessors(derivation_id))
        successor_indices = self._graph.successor_indices(
            self._index_by_id[derivation_id]
        )
        conclusion_id = cast(
            FactId, self._graph.get_node_data(next(iter(successor_indices))).id
        )
        result.setdefault(conclusion_id, []).append(
            Derivation(premise_ids=premise_ids, rule=derivation.rule)
        )
    return {fact_id: tuple(items) for fact_id, items in result.items()}

has_derivation

has_derivation(*, conclusion_id, premise_ids, rule)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def has_derivation(
    self,
    *,
    conclusion_id: FactId,
    premise_ids: tuple[FactId, ...],
    rule: str,
) -> bool:
    expected_premises = set(premise_ids)
    for predecessor_idx in self._graph.predecessor_indices(
        self._index_by_id[conclusion_id]
    ):
        predecessor = self._graph.get_node_data(predecessor_idx)
        if not isinstance(predecessor, DerivationNode):
            continue
        if predecessor.rule != rule:
            continue
        actual_premises = set(self._fact_predecessors(predecessor.id))
        if actual_premises == expected_premises:
            return True
    return False

with_fact

with_fact(node, *, derivation=None, premises=())

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def with_fact(
    self,
    node: FactNode,
    *,
    derivation: DerivationNode | None = None,
    premises: tuple[FactId, ...] = (),
) -> ProvenanceDag:
    graph = self.to_rustworkx()
    index_by_id = dict(self._index_by_id)
    index_by_id[node.id] = graph.add_node(node)
    if derivation is not None:
        return self._with_step(
            derivation,
            premises=premises,
            conclusion=node.id,
            graph=graph,
            index_by_id=index_by_id,
        )
    return self._replace_graph(graph, index_by_id)

with_derivation

with_derivation(derivation, *, premises, conclusion)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def with_derivation(
    self,
    derivation: DerivationNode,
    *,
    premises: tuple[FactId, ...],
    conclusion: FactId,
) -> ProvenanceDag:
    return self._with_step(
        derivation,
        premises=premises,
        conclusion=conclusion,
    )

with_explanation

with_explanation(explanation, *, premises, check)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def with_explanation(
    self,
    explanation: ExplanationNode,
    *,
    premises: tuple[FactId, ...],
    check: FactId,
) -> ProvenanceDag:
    return self._with_step(
        explanation,
        premises=premises,
        conclusion=check,
    )

explanation_nodes

explanation_nodes(target_id)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def explanation_nodes(
    self, target_id: FactId
) -> Iterator[FactNode | DerivationNode | ExplanationNode]:
    relevant_ids = self.explanation_node_ids(target_id)
    relevant_indices = [self._index_by_id[node_id] for node_id in relevant_ids]
    sub = self._graph.subgraph(relevant_indices)
    for idx in rx.topological_sort(sub):
        payload = sub.get_node_data(idx)
        if isinstance(payload, FactNode):
            yield self.fact(payload.id)
        elif isinstance(payload, DerivationNode):
            yield self.derivation(payload.id)
        else:
            yield self.explanation(payload.id)

slice_for

slice_for(target_id)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def slice_for(self, target_id: FactId) -> ProvenanceDag:
    relevant_ids = self.explanation_node_ids(target_id)
    relevant_indices = [self._index_by_id[node_id] for node_id in relevant_ids]
    sub = self._graph.subgraph(relevant_indices)
    index_by_id = {
        sub.get_node_data(idx).id: idx for idx in sub.node_indices()
    }
    return self._replace_graph(sub, index_by_id)

PuzzleSolver dataclass

Configured callable that solves puzzles with one reasoning backend.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class PuzzleSolver:
    """Configured callable that solves puzzles with one reasoning backend."""

    backend: ReasoningBackend = DEFAULT_REASONING_BACKEND

    def ingest[PuzzleT](self, puzzle: PuzzleT) -> IngestedPuzzle[PuzzleT]:
        """Parse a puzzle without attaching this solver's backend."""
        if not is_dataclass(puzzle):
            raise TypeError(f"Expected dataclass puzzle schema, got {puzzle!r}")

        graph = FactGraph.empty()
        check_tokens: dict[str, FactToken[Any]] = {}

        for field_info in fields(cast(Any, puzzle)):
            subject_name = field_info.name
            block = getattr(puzzle, subject_name)

            if not isinstance(block, SubjectFacts):
                raise TypeError(
                    f"Puzzle field {subject_name!r} is not SubjectFacts: {block!r}"
                )

            if block.given is not None:
                bound_given = block.given.bind(subject_name)
                _given_token, graph = graph.add_given(
                    bound_given,
                    subject_name=subject_name,
                )

            for check_label, check_prop in block.checks.items():
                bound_check = check_prop.bind(subject_name)
                check_token, graph = graph.add_check(
                    bound_check,
                    subject_name=subject_name,
                    check_label=check_label,
                )
                check_tokens[check_label] = check_token

        return IngestedPuzzle(
            puzzle=puzzle,
            graph=graph,
            check_tokens=check_tokens,
        )

    def __call__[PuzzleT](self, puzzle: PuzzleT) -> SolvedPuzzle[PuzzleT]:
        """Ingest, check consistency, saturate, and attach checks."""
        ingested = self.ingest(puzzle)
        graph = ingested.graph.with_reasoning_backend(self.backend)
        saturated = graph.check_consistent().saturate()
        final_graph = saturated
        proposals = self.backend.explanation.explain(
            saturated.explanation_input(ingested.check_tokens.values()),
            self.backend.semantics,
        )
        for proposal in proposals:
            final_graph = final_graph.apply_explanation(proposal)

        return SolvedPuzzle(
            puzzle=ingested.puzzle,
            graph=final_graph,
            check_tokens=ingested.check_tokens,
        )

backend class-attribute instance-attribute

backend = DEFAULT_REASONING_BACKEND

ingest

ingest(puzzle)

Parse a puzzle without attaching this solver's backend.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def ingest[PuzzleT](self, puzzle: PuzzleT) -> IngestedPuzzle[PuzzleT]:
    """Parse a puzzle without attaching this solver's backend."""
    if not is_dataclass(puzzle):
        raise TypeError(f"Expected dataclass puzzle schema, got {puzzle!r}")

    graph = FactGraph.empty()
    check_tokens: dict[str, FactToken[Any]] = {}

    for field_info in fields(cast(Any, puzzle)):
        subject_name = field_info.name
        block = getattr(puzzle, subject_name)

        if not isinstance(block, SubjectFacts):
            raise TypeError(
                f"Puzzle field {subject_name!r} is not SubjectFacts: {block!r}"
            )

        if block.given is not None:
            bound_given = block.given.bind(subject_name)
            _given_token, graph = graph.add_given(
                bound_given,
                subject_name=subject_name,
            )

        for check_label, check_prop in block.checks.items():
            bound_check = check_prop.bind(subject_name)
            check_token, graph = graph.add_check(
                bound_check,
                subject_name=subject_name,
                check_label=check_label,
            )
            check_tokens[check_label] = check_token

    return IngestedPuzzle(
        puzzle=puzzle,
        graph=graph,
        check_tokens=check_tokens,
    )

ReasoningBackend dataclass

Composite, graph-independent reasoning capabilities.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class ReasoningBackend:
    """Composite, graph-independent reasoning capabilities."""

    semantics: SemanticBackend = Z3_SEMANTICS
    derivation: DerivationBackend = ForwardDerivationBackend()
    explanation: ExplanationBackend = FactGraphExplanationBackend()
    max_rounds: int = 20

    def __enter__(self) -> ReasoningBackend:
        return self

    def __exit__(
        self,
        exc_type: type[BaseException] | None,
        exc_value: BaseException | None,
        traceback: object | None,
    ) -> None:
        return None

semantics class-attribute instance-attribute

semantics = Z3_SEMANTICS

derivation class-attribute instance-attribute

derivation = ForwardDerivationBackend()

explanation class-attribute instance-attribute

explanation = FactGraphExplanationBackend()

max_rounds class-attribute instance-attribute

max_rounds = 20

Saturated

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

class Saturated:
    pass

SemanticBackend

Bases: Protocol

One complete decision primitive from which logical queries are derived.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

class SemanticBackend(Protocol):
    """One complete decision primitive from which logical queries are derived."""

    def solve(self, assertions: Sequence[BoolRef]) -> SolveResult: ...

solve

solve(assertions)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def solve(self, assertions: Sequence[BoolRef]) -> SolveResult: ...

SolveResult dataclass

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class SolveResult:
    status: SolveStatus
    model: ModelRef | None = None
    core: tuple[BoolRef, ...] = ()

status instance-attribute

status

model class-attribute instance-attribute

model = None

core class-attribute instance-attribute

core = ()

SolveStatus

Bases: str, Enum

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

class SolveStatus(str, Enum):
    SAT = "SAT"
    UNSAT = "UNSAT"
    UNKNOWN = "UNKNOWN"
    #: The solver hit its resource budget (timeout/rlimit). Kept distinct from
    #: UNKNOWN so a resource exhaustion is never mistaken for a theory verdict.
    TIMEOUT = "TIMEOUT"

SAT class-attribute instance-attribute

SAT = 'SAT'

UNSAT class-attribute instance-attribute

UNSAT = 'UNSAT'

UNKNOWN class-attribute instance-attribute

UNKNOWN = 'UNKNOWN'

TIMEOUT class-attribute instance-attribute

TIMEOUT = 'TIMEOUT'

SolvedPuzzle dataclass

Bases: Generic[PuzzleT]

A puzzle after ingestion, consistency check, saturation, and attach.

graph is the final explanation DAG; check_tokens maps each check label to the fact recording that candidate proposition.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class SolvedPuzzle(Generic[PuzzleT]):
    """A puzzle after ingestion, consistency check, saturation, and attach.

    ``graph`` is the final explanation DAG; ``check_tokens`` maps each check
    label to the fact recording that candidate proposition.
    """

    puzzle: PuzzleT
    graph: FactGraph[Evidence[Consistent, Saturated]]
    check_tokens: dict[str, FactToken[Any]]

puzzle instance-attribute

puzzle

graph instance-attribute

graph

check_tokens instance-attribute

check_tokens

SourceSpan dataclass

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class SourceSpan:
    uri: str
    start_line: int
    start_col: int
    end_line: int
    end_col: int

uri instance-attribute

uri

start_line instance-attribute

start_line

start_col instance-attribute

start_col

end_line instance-attribute

end_line

end_col instance-attribute

end_col

Unchecked

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

class Unchecked:
    pass

Unsaturated

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

class Unsaturated:
    pass

Z3SemanticBackend dataclass

Default semantic backend using Z3's solver and unsat cores.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class Z3SemanticBackend:
    """Default semantic backend using Z3's solver and unsat cores."""

    solver_factory: Callable[[], Any] = field(default=Solver, repr=False)
    timeout_ms: int | None = None

    def solve(self, assertions: Sequence[BoolRef]) -> SolveResult:
        return check_with_core(
            assertions,
            BoolVal(True),
            solver_factory=self.solver_factory,
            timeout_ms=self.timeout_ms,
        )

solver_factory class-attribute instance-attribute

solver_factory = field(default=Solver, repr=False)

timeout_ms class-attribute instance-attribute

timeout_ms = None

solve

solve(assertions)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def solve(self, assertions: Sequence[BoolRef]) -> SolveResult:
    return check_with_core(
        assertions,
        BoolVal(True),
        solver_factory=self.solver_factory,
        timeout_ms=self.timeout_ms,
    )

all_equivalent

all_equivalent(*predicates, backend=None)

Are all predicates provably equivalent to one another?

Entailment is a preorder, so mutual equivalence of a set is "every element lies in one strongly-connected component". Establishing that does not require all N·(N−1) ordered pairs: because the PROVED fragment of entailment is transitive (A⊨B ∧ B⊨C ⟹ A⊨C — a theorem, independent of the solver), a single covering cycle p₀ ⊨ p₁ ⊨ … ⊨ p₀ proves it in N solver calls rather than N². conjunction short-circuits on the first REFUTED link, so a definite mismatch costs even less.

Fewer than two predicates are vacuously equivalent (PROVED), with no solver call. equivalent is the binary case.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def all_equivalent(
    *predicates: BoolRef,
    backend: SemanticBackend | None = None,
) -> Entailment:
    """Are all ``predicates`` provably equivalent to one another?

    Entailment is a *preorder*, so mutual equivalence of a set is "every element
    lies in one strongly-connected component". Establishing that does **not**
    require all ``N·(N−1)`` ordered pairs: because the ``PROVED`` fragment of
    entailment is *transitive* (``A⊨B ∧ B⊨C ⟹ A⊨C`` — a theorem, independent of
    the solver), a single covering **cycle** ``p₀ ⊨ p₁ ⊨ … ⊨ p₀`` proves it in
    ``N`` solver calls rather than ``N²``. ``conjunction`` short-circuits on the
    first ``REFUTED`` link, so a definite mismatch costs even less.

    Fewer than two predicates are vacuously equivalent (``PROVED``), with no
    solver call. ``equivalent`` is the binary case.
    """
    if len(predicates) < 2:
        return Entailment.PROVED

    cycle = zip(predicates, (*predicates[1:], predicates[0]), strict=True)
    return Entailment.conjunction(
        entails([left], right, backend=backend) for left, right in cycle
    )

arith_key

arith_key(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def arith_key(expr: ArithRef) -> str:
    return simplify(expr).sexpr()

as_bool_ref

as_bool_ref(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def as_bool_ref(expr: object) -> BoolRef:
    return cast(BoolRef, expr)

as_int

as_int(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def as_int(expr: object) -> int | None:
    if is_int_value(expr):
        return cast(IntNumRef, expr).as_long()
    return None

check_with_core

check_with_core(
    base, extra, *, solver_factory=Solver, timeout_ms=None
)

Low-level Z3 solve retaining a model, unsat core, or unknown result.

timeout_ms bounds the solve: a query that exceeds it returns SolveStatus.TIMEOUT rather than running unbounded, so a small but solver-expensive request cannot exhaust the service.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def check_with_core(
    base: Sequence[BoolRef],
    extra: BoolRef,
    *,
    solver_factory: Callable[[], Any] = Solver,
    timeout_ms: int | None = None,
) -> SolveResult:
    """Low-level Z3 solve retaining a model, unsat core, or unknown result.

    ``timeout_ms`` bounds the solve: a query that exceeds it returns
    ``SolveStatus.TIMEOUT`` rather than running unbounded, so a small but
    solver-expensive request cannot exhaust the service.
    """
    solver = solver_factory()
    if timeout_ms is not None:
        solver.set("timeout", timeout_ms)
    tracked: dict[str, BoolRef] = {}

    for i, expr in enumerate([*base, extra]):
        key = Bool(f"a{i}")
        tracked[str(key)] = expr
        solver.assert_and_track(expr, key)

    result = solver.check()

    if result == sat:
        return SolveResult(SolveStatus.SAT, model=solver.model())

    if result == unsat:
        return SolveResult(
            SolveStatus.UNSAT,
            core=tuple(tracked[str(k)] for k in solver.unsat_core()),
        )

    return SolveResult(_unknown_status(solver.reason_unknown()))

classify

classify(base, check, *, backend=None)

Classify check against base as VERIFIED/FALSIFIED/UNKNOWN/…

Runs the solver twice — once asserting the check, once its negation — and maps the (satisfiable, refutable) pair to a :class:Status. This is the engine puzzle mode and the workflow coverage analysis both build on.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def classify(
    base: Sequence[BoolRef],
    check: BoolRef,
    *,
    backend: SemanticBackend | None = None,
) -> CheckResult:
    """Classify ``check`` against ``base`` as VERIFIED/FALSIFIED/UNKNOWN/…

    Runs the solver twice — once asserting the check, once its negation — and
    maps the ``(satisfiable, refutable)`` pair to a :class:`Status`. This is the
    engine puzzle mode and the workflow coverage analysis both build on.
    """
    semantics = _semantic_backend(backend)
    yes = semantics.solve([*base, check])
    no = semantics.solve([*base, Not(check)])

    status = (
        Status.UNDECIDED
        if {yes.status, no.status} & {SolveStatus.UNKNOWN, SolveStatus.TIMEOUT}
        else {
            (SolveStatus.SAT, SolveStatus.UNSAT): Status.VERIFIED,
            (SolveStatus.UNSAT, SolveStatus.SAT): Status.FALSIFIED,
            (SolveStatus.SAT, SolveStatus.SAT): Status.UNKNOWN,
            (SolveStatus.UNSAT, SolveStatus.UNSAT): Status.INCONSISTENT_BASE,
        }[(yes.status, no.status)]
    )

    return CheckResult(
        status=status,
        true_model=yes.model,
        false_model=no.model,
        true_core=yes.core,
        false_core=no.core,
    )

classify_check

classify_check(base, check)

Classify a proposition with the default reasoning backend.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def classify_check(
    base: Sequence[BoolRef],
    check: BoolRef,
) -> CheckResult:
    """Classify a proposition with the default reasoning backend."""
    return classify(base, check, backend=DEFAULT_REASONING_BACKEND.semantics)

empty_rustworkx_digraph

empty_rustworkx_digraph()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def empty_rustworkx_digraph() -> rx.PyDiGraph:
    return rx.PyDiGraph()

entails

entails(premises, conclusion, *, backend=None)

Classify whether premises entail conclusion without losing unknown.

A SAT result for premises ∧ ¬conclusion is a countermodel, so it maps to REFUTED (definitely not entailed), not a mere proof failure.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def entails(
    premises: Sequence[BoolRef],
    conclusion: BoolRef,
    *,
    backend: SemanticBackend | None = None,
) -> Entailment:
    """Classify whether ``premises`` entail ``conclusion`` without losing unknown.

    A ``SAT`` result for ``premises ∧ ¬conclusion`` is a *countermodel*, so it
    maps to ``REFUTED`` (definitely not entailed), not a mere proof failure.
    """
    status = _semantic_backend(backend).solve([*premises, Not(conclusion)]).status
    return {
        SolveStatus.UNSAT: Entailment.PROVED,
        SolveStatus.SAT: Entailment.REFUTED,
        SolveStatus.UNKNOWN: Entailment.UNDECIDED,
        SolveStatus.TIMEOUT: Entailment.UNDECIDED,
    }[status]

equality_sides

equality_sides(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def equality_sides(expr: BoolRef) -> tuple[ArithRef, ArithRef] | None:
    expr = as_bool_ref(simplify(expr))

    if not is_eq(expr):
        return None

    lhs, rhs = expr.children()
    return cast(ArithRef, simplify(lhs)), cast(ArithRef, simplify(rhs))

equivalent

equivalent(a, b, *, backend=None)

Logical equivalence of two predicates.

The binary case of :func:all_equivalent — the 2-cycle a ⊨ b ⊨ a.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def equivalent(
    a: BoolRef,
    b: BoolRef,
    *,
    backend: SemanticBackend | None = None,
) -> Entailment:
    """Logical equivalence of two predicates.

    The binary case of :func:`all_equivalent` — the 2-cycle ``a ⊨ b ⊨ a``.
    """
    return all_equivalent(a, b, backend=backend)

expr_key

expr_key(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def expr_key(expr: BoolRef) -> str:
    return simplify(expr).sexpr()

is_eq

is_eq(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def is_eq(expr: BoolRef) -> bool:
    return is_app_of(expr, Z3_OP_EQ)

linear_offset

linear_offset(expr)

Parse simplify(expr) as source + offset for a single symbolic source.

Only addition needs handling: Z3's simplify normalises subtraction into addition of negated terms. Anything else (pure constants, multiple symbolic terms) returns None, and callers simply derive nothing from it.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def linear_offset(expr: ArithRef) -> LinearOffset | None:
    """Parse `simplify(expr)` as `source + offset` for a single symbolic source.

    Only addition needs handling: Z3's `simplify` normalises subtraction into
    addition of negated terms. Anything else (pure constants, multiple
    symbolic terms) returns None, and callers simply derive nothing from it.
    """
    expr = cast(ArithRef, simplify(expr))

    if is_int_value(expr):
        return None

    if expr.num_args() == 0:
        return LinearOffset(expr, 0)

    if expr.decl().kind() == Z3_OP_ADD:
        symbolic: list[ArithRef] = []
        offset = 0

        for child in expr.children():
            arg = cast(ArithRef, simplify(child))
            value = as_int(arg)

            if value is None:
                symbolic.append(arg)
            else:
                offset += value

        if len(symbolic) == 1:
            return LinearOffset(symbolic[0], offset)

    return None

parse_constant_equality

parse_constant_equality(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def parse_constant_equality(expr: BoolRef) -> tuple[ArithRef, int] | None:
    sides = equality_sides(expr)

    if sides is None:
        return None

    lhs, rhs = sides

    rhs_value = as_int(rhs)
    if rhs_value is not None:
        return lhs, rhs_value

    lhs_value = as_int(lhs)
    if lhs_value is not None:
        return rhs, lhs_value

    return None

parse_offset_equality

parse_offset_equality(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def parse_offset_equality(expr: BoolRef) -> tuple[ArithRef, ArithRef, int] | None:
    sides = equality_sides(expr)

    if sides is None:
        return None

    lhs, rhs = sides

    parsed_rhs = linear_offset(rhs)
    if parsed_rhs is not None and as_int(lhs) is None:
        return lhs, parsed_rhs.source, parsed_rhs.offset

    parsed_lhs = linear_offset(lhs)
    if parsed_lhs is not None and as_int(rhs) is None:
        return rhs, parsed_lhs.source, parsed_lhs.offset

    return None

print_core

print_core(core)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def print_core(core: Sequence[BoolRef]) -> None:
    for expr in core:
        print(f"    {expr}")

print_model

print_model(model, subject_names)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def print_model(model: ModelRef, subject_names: Sequence[str]) -> None:
    rows: list[tuple[int, str]] = []

    for subject_name in subject_names:
        z3_value = Int(f"{subject_name}.departure")
        value = cast(IntNumRef, model.eval(z3_value, model_completion=True)).as_long()
        rows.append((value, subject_name))

    for value, subject_name in sorted(rows):
        print(f"    {fmt_time(value)}  {subject_name.capitalize()}")

render_arith

render_arith(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def render_arith(expr: ArithRef) -> str:
    return str(expr)

render_fact

render_fact(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def render_fact(expr: BoolRef) -> str:
    constant = parse_constant_equality(expr)
    if constant is not None:
        var, value = constant
        return f"{render_arith(var)} is {fmt_time(value)}."

    offset = parse_offset_equality(expr)
    if offset is not None:
        target, source, minutes = offset

        if minutes < 0:
            return (
                f"{render_arith(target)} is {-minutes} minutes before "
                f"{render_arith(source)}."
            )
        if minutes > 0:
            return (
                f"{render_arith(target)} is {minutes} minutes after "
                f"{render_arith(source)}."
            )
        return f"{render_arith(target)} is the same time as {render_arith(source)}."

    return str(expr)

to_wire_explanation_dag

to_wire_explanation_dag(dag)

Project dag into the portable, z3-free explanation-DAG wire form.

A faithful, order-stable read: node/edge order matches dag.nodes() / dag.edges() exactly, so two equivalent DAGs always project to the same wire form regardless of graph backend.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def to_wire_explanation_dag(dag: ProvenanceDag) -> WireExplanationDag:
    """Project ``dag`` into the portable, z3-free explanation-DAG wire form.

    A faithful, order-stable read: node/edge order matches ``dag.nodes()`` /
    ``dag.edges()`` exactly, so two equivalent DAGs always project to the
    same wire form regardless of graph backend.
    """
    return WireExplanationDag(
        nodes=tuple(_wire_node(node) for node in dag.nodes()),
        edges=tuple(
            WireProvenanceEdge(source=str(source), target=str(target))
            for source, target in dag.edges()
        ),
    )

graph_to_d3_html

graph_to_d3_html(
    graph, *, element_id="reasoning-d3", library="cytoscape"
)

Render a FactGraph explanation DAG as a self-contained HTML snippet.

Returns a <div> plus inline <script> that loads the chosen library from a CDN and draws the graph client-side. See D3Library and the module docstring for the trade-off between the two styles.

Parameters:

Name	Type	Description	Default
graph	FactGraph[Any]	The graph to render.	required
element_id	str	The HTML id attribute for the container div element.	'reasoning-d3'
library	D3Library	The chosen rendering library.	'cytoscape'

Returns:

Type	Description
str	Self-contained HTML snippet string.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/d3.py

def graph_to_d3_html(
    graph: FactGraph[Any],
    *,
    element_id: str = "reasoning-d3",
    library: D3Library = "cytoscape",
) -> str:
    """Render a [FactGraph][guardrail_solver.reasoning.FactGraph] explanation DAG as a self-contained HTML snippet.

    Returns a `<div>` plus inline `<script>` that loads the chosen
    `library` from a CDN and draws the graph client-side. See
    `D3Library` and the module docstring
    for the trade-off between the two styles.

    Args:
        graph: The graph to render.
        element_id: The HTML id attribute for the container div element.
        library: The chosen rendering library.

    Returns:
        Self-contained HTML snippet string.
    """
    payload = graph_to_d3_payload(graph, library=library)

    if library == "cytoscape":
        return _cytoscape_html(payload, element_id)

    return _d3_html(payload, element_id)

graph_to_d3_payload

graph_to_d3_payload(graph, *, library='cytoscape')

Build the JSON-able payload (meta/nodes/links) for a graph.

library picks the payload shape to build (see D3Library and the module docstring): "cytoscape" (the default) omits per-node positions (Cytoscape computes them client-side); "d3" includes a fixed x/y/width per node computed here in Python.

The name is kept as d3_payload for backwards compatibility with existing callers.

Parameters:

Name	Type	Description	Default
graph	FactGraph[Any]	The FactGraph to build the payload for.	required
library	D3Library	The chosen rendering library.	'cytoscape'

Returns:

Type	Description
dict[str, Any]	A dictionary containing the keys "meta", "nodes", and "links" with graph representation data.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/d3.py

def graph_to_d3_payload(
    graph: FactGraph[Any],
    *,
    library: D3Library = "cytoscape",
) -> dict[str, Any]:
    """Build the JSON-able payload (`meta`/`nodes`/`links`) for a graph.

    `library` picks the payload shape to build (see `D3Library`
    and the module docstring): `"cytoscape"` (the default) omits per-node
    positions (Cytoscape computes them client-side); `"d3"` includes a
    fixed `x`/`y`/`width` per node computed here in Python.

    The name is kept as `d3_payload` for backwards compatibility with
    existing callers.

    Args:
        graph: The [FactGraph][guardrail_solver.reasoning.FactGraph] to build the payload for.
        library: The chosen rendering library.

    Returns:
        A dictionary containing the keys "meta", "nodes", and "links" with graph representation data.
    """
    all_nodes = tuple(graph.dag.nodes())
    fact_and_derivation_nodes = [
        node
        for node in all_nodes
        if isinstance(node, (FactNode, DerivationNode))
    ]

    if library == "cytoscape":
        return _cytoscape_payload(graph, all_nodes, fact_and_derivation_nodes)

    return _d3_payload(graph, all_nodes, fact_and_derivation_nodes)

graph_to_mermaid

graph_to_mermaid(
    graph,
    *,
    focus=None,
    grouping="flat",
    include_config=True,
    include_clicks=True
)

Render a FactGraph using semantic rows.

Rows are: - Givens - Reasoning - Derived facts - Checks

Nodes are arranged left-to-right within their semantic row where the layout engine allows it. grouping picks how rows and the focus/peripheral split are conveyed visually — see MermaidGrouping and the module docstring for the trade-off between the two styles.

When focus is supplied, the focused fact and all provenance ancestors are the vivid, prominent group; unrelated graph material is muted and placed beneath it.

Derivations remain explicit

premise fact -> reasoning step -> conclusion fact

Explanation steps are collapsed

known fact -. rule .-> check

Parameters:

Name	Type	Description	Default
graph	FactGraph[Any]	The FactGraph to render.	required
focus	MermaidFocus	The node/fact to focus on.	None
grouping	MermaidGrouping	The grouping/layout style.	'flat'
include_config	bool	Whether to include default Mermaid config markers.	True
include_clicks	bool	Whether to include hyperlink actions for clickable nodes.	True

Returns:

Type	Description
str	The generated Mermaid graph string.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/mermaid.py

def graph_to_mermaid(
    graph: FactGraph[Any],
    *,
    focus: MermaidFocus = None,
    grouping: MermaidGrouping = "flat",
    include_config: bool = True,
    include_clicks: bool = True,
) -> str:
    """Render a [FactGraph][guardrail_solver.reasoning.FactGraph] using semantic rows.

    Rows are:
    - Givens
    - Reasoning
    - Derived facts
    - Checks

    Nodes are arranged left-to-right within their semantic row where the
    layout engine allows it. `grouping` picks how rows and the
    focus/peripheral split are conveyed visually — see `MermaidGrouping`
    and the module docstring for the trade-off between the two styles.

    When `focus` is supplied, the focused fact and all provenance ancestors
    are the vivid, prominent group; unrelated graph material is muted and
    placed beneath it.

    Derivations remain explicit:
        premise fact -> reasoning step -> conclusion fact

    Explanation steps are collapsed:
        known fact -. rule .-> check

    Args:
        graph: The [FactGraph][guardrail_solver.reasoning.FactGraph] to render.
        focus: The node/fact to focus on.
        grouping: The grouping/layout style.
        include_config: Whether to include default Mermaid config markers.
        include_clicks: Whether to include hyperlink actions for clickable nodes.

    Returns:
        The generated Mermaid graph string.
    """
    target_id = _focus_fact_id(focus)

    if target_id is not None and target_id not in graph.dag:
        raise KeyError(
            f"Mermaid focus does not belong to this graph: {target_id}"
        )

    all_nodes = tuple(graph.dag.nodes())
    all_node_ids = frozenset(node.id for node in all_nodes)

    relevant_ids = (
        graph.dag.explanation_node_ids(target_id)
        if target_id is not None
        else all_node_ids
    )
    peripheral_ids = all_node_ids - relevant_ids

    relevant_nodes = tuple(
        node
        for node in all_nodes
        if node.id in relevant_ids
    )
    peripheral_nodes = tuple(
        node
        for node in all_nodes
        if node.id in peripheral_ids
    )

    relevant_rows = partition_rows(relevant_nodes)
    peripheral_rows = partition_rows(peripheral_nodes)

    relevant_facts = tuple(
        node
        for node in relevant_nodes
        if isinstance(node, FactNode)
    )
    peripheral_facts = tuple(
        node
        for node in peripheral_nodes
        if isinstance(node, FactNode)
    )

    relevant_steps = tuple(
        node
        for node in relevant_nodes
        if isinstance(node, (DerivationNode, ExplanationNode))
    )
    peripheral_steps = tuple(
        node
        for node in peripheral_nodes
        if isinstance(node, (DerivationNode, ExplanationNode))
    )

    predecessors: dict[GraphNodeId, list[GraphNodeId]] = {}
    successors: dict[GraphNodeId, list[GraphNodeId]] = {}

    for source_id, target_node_id in graph.dag.edges():
        predecessors.setdefault(target_node_id, []).append(source_id)
        successors.setdefault(source_id, []).append(target_node_id)

    lines: list[str] = []

    if include_config:
        lines.append(
            _MERMAID_INIT_DIRECTIVE_FLAT
            if grouping == "flat"
            else _MERMAID_INIT_DIRECTIVE_SUBGRAPH
        )

    lines.append("flowchart TB")
    lines.append("")

    focus_title = "Explanation"

    if target_id is not None:
        target = graph.fact(target_id)

        if (
            target.kind is FactKind.CHECK
            and target.check_label is not None
        ):
            focus_title = f"Explanation for Check {target.check_label}"

    focus_anchors: tuple[tuple[str, GraphNodeId], ...] = ()
    peripheral_anchors: tuple[tuple[str, GraphNodeId], ...] = ()
    focus_row_ids: tuple[str, ...] = ()
    peripheral_row_ids: tuple[str, ...] = ()

    if grouping == "flat":
        lines.append(
            mermaid_label_declaration("explanation_label", focus_title)
        )
        focus_anchors = _render_semantic_rows_flat(
            lines,
            rows=relevant_rows,
            include_subject=True,
            muted=False,
            indent="    ",
        )

        if peripheral_ids:
            lines.append("")
            lines.append(
                mermaid_label_declaration(
                    "peripheral_label", "Other facts and checks"
                )
            )
            peripheral_anchors = _render_semantic_rows_flat(
                lines,
                rows=peripheral_rows,
                include_subject=True,
                muted=True,
                indent="    ",
            )
    else:
        lines.append(
            f'    subgraph explanation_region["{mermaid_escape(focus_title)}"]'
        )
        focus_row_ids = _render_semantic_rows_subgraph(
            lines,
            rows=relevant_rows,
            include_subject=True,
            muted=False,
            indent="        ",
        )
        lines.append("    end")

        if peripheral_ids:
            lines.append("")
            lines.append(
                '    subgraph peripheral_region["Other facts and checks"]'
            )
            peripheral_row_ids = _render_semantic_rows_subgraph(
                lines,
                rows=peripheral_rows,
                include_subject=True,
                muted=True,
                indent="        ",
            )
            lines.append("    end")

    lines.append("")

    edge_indices: dict[Literal["focus", "muted", "invisible"], list[int]] = {
        "focus": [],
        "muted": [],
        "invisible": [],
    }
    link_index = 0

    def append_edge(
        declaration: str,
        *,
        edge_class: Literal["focus", "muted", "invisible"],
    ) -> None:
        nonlocal link_index

        lines.append(f"    {declaration}")
        edge_indices[edge_class].append(link_index)
        link_index += 1

    # Explicit derivation edges:
    #
    #     premise -> reasoning -> conclusion
    for node in (*relevant_steps, *peripheral_steps):
        if not isinstance(node, DerivationNode):
            continue

        step_id = mermaid_derivation_id(node.id)
        focused_step = node.id in relevant_ids

        for premise_id in predecessors.get(node.id, ()):
            append_edge(
                f"{mermaid_graph_node_id(premise_id)} "
                f'-->|"uses"| {step_id}',
                edge_class=(
                    "focus"
                    if focused_step and premise_id in relevant_ids
                    else "muted"
                ),
            )

        for conclusion_id in successors.get(node.id, ()):
            append_edge(
                f'{step_id} -->|"derives"| '
                f"{mermaid_graph_node_id(conclusion_id)}",
                edge_class=(
                    "focus"
                    if focused_step and conclusion_id in relevant_ids
                    else "muted"
                ),
            )

    # Collapsed explanation edges:
    #
    #     established fact -. rule .-> check
    for node in (*relevant_steps, *peripheral_steps):
        if not isinstance(node, ExplanationNode):
            continue

        edge_label = mermaid_escape(node.rule)

        for premise_id in predecessors.get(node.id, ()):
            for conclusion_id in successors.get(node.id, ()):
                append_edge(
                    f"{mermaid_graph_node_id(premise_id)} "
                    f'-. "{edge_label}" .-> '
                    f"{mermaid_graph_node_id(conclusion_id)}",
                    edge_class=(
                        "focus"
                        if (
                            premise_id in relevant_ids
                            and conclusion_id in relevant_ids
                        )
                        else "muted"
                    ),
                )

    # Keep nodes within each semantic row arranged left-to-right.
    #
    # These invisible edges constrain layout only; they do not represent
    # provenance.
    for row in (
        *_row_node_ids(relevant_rows),
        *_row_node_ids(peripheral_rows),
    ):
        for earlier, later in zip(
            row,
            row[1:],
            strict=False,
        ):
            append_edge(
                f"{mermaid_graph_node_id(earlier)} "
                f"~~~ {mermaid_graph_node_id(later)}",
                edge_class="invisible",
            )

    if grouping == "flat":
        # Anchor each row's floating label beside its first node.
        for label_id, first_node_id in (*focus_anchors, *peripheral_anchors):
            append_edge(
                f"{label_id} ~~~ {mermaid_graph_node_id(first_node_id)}",
                edge_class="invisible",
            )

    # Keep semantic rows in top-to-bottom order even where adjacent categories
    # have no direct provenance edge.
    for rows in (relevant_rows, peripheral_rows):
        non_empty_rows = tuple(
            row
            for row in _row_node_ids(rows)
            if row
        )

        for upper_row, lower_row in zip(
            non_empty_rows,
            non_empty_rows[1:],
            strict=False,
        ):
            append_edge(
                f"{mermaid_graph_node_id(upper_row[0])} "
                f"~~~ {mermaid_graph_node_id(lower_row[0])}",
                edge_class="invisible",
            )

    if grouping == "flat":
        # Anchor each section label above its own first row.
        if focus_anchors:
            append_edge(
                f"explanation_label ~~~ {focus_anchors[0][0]}",
                edge_class="invisible",
            )
        if peripheral_anchors:
            append_edge(
                f"peripheral_label ~~~ {peripheral_anchors[0][0]}",
                edge_class="invisible",
            )

    # Keep the peripheral section below the focused explanation.
    if relevant_facts and peripheral_facts:
        focus_anchor = target_id or relevant_facts[-1].id
        peripheral_anchor = peripheral_facts[0].id

        append_edge(
            f"{mermaid_node_id(focus_anchor)} "
            f"~~~ {mermaid_node_id(peripheral_anchor)}",
            edge_class="invisible",
        )

    lines.append("")
    lines.extend(
        f"    classDef {name} {style};" for name, style in _FOCUS_CLASS_DEFS
    )
    lines.append("")
    lines.extend(
        f"    classDef {name} {style};" for name, style in _MUTED_CLASS_DEFS
    )

    lines.append("")

    if grouping == "flat":
        _append_class_assignment(lines, ("explanation_label",), "sectionLabel")
        if peripheral_anchors:
            _append_class_assignment(
                lines, ("peripheral_label",), "mutedSectionLabel"
            )

    for rows, anchors, prefix in (
        (relevant_rows, focus_anchors, "focus"),
        (peripheral_rows, peripheral_anchors, "muted"),
    ):
        # Only the focus region can contain the target check; the
        # peripheral region never does, so nothing is excluded there.
        excluded_check_id = target_id if prefix == "focus" else None

        _append_class_assignment(
            lines,
            (mermaid_node_id(node.id) for node in rows.givens),
            f"{prefix}Given",
        )
        _append_class_assignment(
            lines,
            (mermaid_derivation_id(node.id) for node in rows.reasoning),
            f"{prefix}Reasoning",
        )
        _append_class_assignment(
            lines,
            (mermaid_node_id(node.id) for node in rows.derived),
            f"{prefix}Derived",
        )
        _append_class_assignment(
            lines,
            (
                mermaid_node_id(node.id)
                for node in rows.checks
                if node.id != excluded_check_id
            ),
            f"{prefix}Check",
        )

        if grouping == "flat":
            _append_class_assignment(
                lines,
                (label_id for label_id, _ in anchors),
                "rowLabel" if prefix == "focus" else "mutedRowLabel",
            )

        if prefix == "focus" and target_id is not None:
            target = graph.fact(target_id)

            target_class = {
                FactKind.GIVEN: "focusGiven",
                FactKind.DERIVED: "focusDerived",
                FactKind.CHECK: "targetCheck",
            }[target.kind]

            _append_class_assignment(
                lines,
                (mermaid_node_id(target_id),),
                target_class,
            )

    if grouping == "subgraph":
        lines.extend(
            [
                "",
                "    style explanation_region "
                "fill:#FFFFFF,stroke:#455A64,stroke-width:2px;",
            ]
        )

        if peripheral_ids:
            lines.append(
                "    style peripheral_region "
                "fill:#FAFAFA,stroke:#D5D5D5,stroke-width:1px,"
                "stroke-dasharray:5 5;"
            )

        for row_id in focus_row_ids:
            lines.append(
                f"    style {row_id} "
                "fill:#FCFDFE,stroke:#C6D0D7,stroke-width:1px;"
            )

        for row_id in peripheral_row_ids:
            lines.append(
                f"    style {row_id} "
                "fill:#FCFCFC,stroke:#E0E0E0,stroke-width:1px;"
            )

    lines.append("")

    link_styles: tuple[
        tuple[Literal["focus", "muted", "invisible"], str], ...
    ] = (
        ("focus", "stroke:#37474F,stroke-width:3px,opacity:1"),
        ("muted", "stroke:#C5C5C5,stroke-width:1px,opacity:0.42"),
        ("invisible", "stroke:transparent,stroke-width:0px,opacity:0"),
    )
    for edge_class, style in link_styles:
        _append_link_style(lines, edge_indices[edge_class], style)

    if include_clicks:
        clickable_facts = tuple(
            fact
            for fact in graph.nodes.values()
            if fact.source is not None
        )

        if clickable_facts:
            lines.append("")

        for fact in clickable_facts:
            assert fact.source is not None
            lines.append(
                f"    click {mermaid_node_id(fact.id)} "
                f'"{mermaid_escape(mermaid_source_url(fact.source))}" '
                f'"Go to source"'
            )

    return "\n".join(lines)

graph_to_mermaid_markdown

graph_to_mermaid_markdown(
    graph,
    *,
    focus=None,
    grouping="flat",
    include_config=True,
    include_clicks=True
)

Render a FactGraph as a fenced Mermaid Markdown block.

Parameters:

Name	Type	Description	Default
graph	FactGraph[Any]	The FactGraph to render.	required
focus	MermaidFocus	The node/fact to focus on.	None
grouping	MermaidGrouping	The grouping/layout style.	'flat'
include_config	bool	Whether to include default Mermaid config markers.	True
include_clicks	bool	Whether to include hyperlink actions for clickable nodes.	True

Returns:

Type	Description
str	The fenced Mermaid Markdown block string.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/mermaid.py

def graph_to_mermaid_markdown(
    graph: FactGraph[Any],
    *,
    focus: MermaidFocus = None,
    grouping: MermaidGrouping = "flat",
    include_config: bool = True,
    include_clicks: bool = True,
) -> str:
    """Render a [FactGraph][guardrail_solver.reasoning.FactGraph] as a fenced Mermaid Markdown block.

    Args:
        graph: The [FactGraph][guardrail_solver.reasoning.FactGraph] to render.
        focus: The node/fact to focus on.
        grouping: The grouping/layout style.
        include_config: Whether to include default Mermaid config markers.
        include_clicks: Whether to include hyperlink actions for clickable nodes.

    Returns:
        The fenced Mermaid Markdown block string.
    """
    mermaid = graph_to_mermaid(
        graph,
        focus=focus,
        grouping=grouping,
        include_config=include_config,
        include_clicks=include_clicks,
    )
    return f"```mermaid\n{mermaid}\n```"

mermaid_fact_declaration

mermaid_fact_declaration(node, *, include_subject)

Declare a fact using Mermaid's native Markdown wrapping.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/mermaid.py

def mermaid_fact_declaration(
    node: FactNode,
    *,
    include_subject: bool,
) -> str:
    """Declare a fact using Mermaid's native Markdown wrapping."""
    node_id = mermaid_node_id(node.id)
    label = mermaid_fact_label(
        node,
        include_subject=include_subject,
    )

    if node.kind is FactKind.GIVEN:
        return f'{node_id}["`{label}`"]'

    # mermaid_fact_label (above) already raised for any kind other than
    # GIVEN/DERIVED/CHECK, via mermaid_fact_heading's own exhaustiveness check.
    return f'{node_id}("`{label}`")'

mermaid_fact_label

mermaid_fact_label(node, *, include_subject)

Render a natively wrapping label without internal provenance ids.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/mermaid.py

def mermaid_fact_label(
    node: FactNode,
    *,
    include_subject: bool,
) -> str:
    """Render a natively wrapping label without internal provenance ids."""
    parts = [f"**{mermaid_fact_heading(node)}**"]

    if include_subject and node.subject is not None:
        parts.append(node.subject.capitalize())

    parts.append(node.text)

    return mermaid_markdown_label(parts)

mermaid_graph_node_id

mermaid_graph_node_id(node_id)

Return the Mermaid id corresponding to a provenance graph node.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/mermaid.py

def mermaid_graph_node_id(node_id: GraphNodeId) -> str:
    """Return the Mermaid id corresponding to a provenance graph node."""
    if isinstance(node_id, FactId):
        return mermaid_node_id(node_id)

    if isinstance(node_id, DerivationId):
        return mermaid_derivation_id(node_id)

    raise TypeError(f"Unknown graph node id: {node_id!r}")