Projects a ShotTx.Prover.Branch onto a ShotDs.Data.Problem for external
model-finding.
The projection ships the branch's :frontier as axioms and its :defs as
TPTP definition entries. Types are auto-derived from constants referenced
by the axioms via ShotDs.Data.Problem.new/1; constants that only appear in
:defs are added afterwards so their type declarations are not lost.
The resulting %Problem{} has no conjecture — the intended TPTP payload
is "here are some axioms, find me a model," which is exactly what
nitpick[satisfy] consumes.
Summary
Functions
Builds a ShotDs.Data.Problem from a branch. Sorted axiom order gives
deterministic TPTP output for golden testing.
Functions
@spec to_problem(ShotTx.Prover.Branch.t()) :: ShotDs.Data.Problem.t()
Builds a ShotDs.Data.Problem from a branch. Sorted axiom order gives
deterministic TPTP output for golden testing.