Reads and writes the SZS result lines that ATP systems emit around their output.
iex> Tptp.Szs.status("% SZS status Theorem for PUZ001+1\n")
{:ok, :theorem, "PUZ001+1", nil}The convention
A system reports its result on a single comment line:
% SZS status <value> for <problem>
% SZS status <value> for <problem> : <free text>and delimits any output offered in support of that result:
% SZS output start <dataform> for <problem>
...
% SZS output end <dataform> for <problem>Two properties make this worth a module rather than a regular expression at each
call site. The status value is drawn from a closed vocabulary,
Tptp.Szs.Ontology, so a misspelling can be reported rather than propagated. And
the lines are interleaved with the remainder of a prover's output, including its
banner, its own comments and possibly several candidate answers, so locating the
status requires scanning rather than matching.
Selection
status/1 returns the last status line in the output. A system refining its
answer emits the refinement afterwards, and a system abandoning the attempt emits
GaveUp last; in both cases the final line is the result the system asserts.
statuses/1 returns all of them in order.
Atom creation
Every status and dataform name resolves through the tables in
Tptp.Szs.Ontology, whose atoms exist at compile time. Prover output is
untrusted input, and an unrecognised value is returned as {:error, word} with
the word as a binary rather than converted to an atom.
Summary
Types
A delimited output block: its dataform, the problem, and the lines between the
start and end markers with the markers removed.
A parsed SZS status line: the value, the problem it is about, and any trailing
free text after the :.
A status line whose value is not in the ontology, kept verbatim.
Functions
Every delimited output block, in order.
Wrap a body in output start / output end markers.
The status a system reported, taken from the last status line it printed.
Write a status line.
Every status line in the output, in the order they appear.
Whether the output reports a success-ontology value.
The last status, reduced to a plain value.
Types
@type block() :: %{dataform: Tptp.Szs.Ontology.t(), problem: binary(), body: binary()}
A delimited output block: its dataform, the problem, and the lines between the
start and end markers with the markers removed.
@type status() :: {:ok, Tptp.Szs.Ontology.t(), binary(), binary() | nil}
A parsed SZS status line: the value, the problem it is about, and any trailing
free text after the :.
A status line whose value is not in the ontology, kept verbatim.
Functions
Every delimited output block, in order.
A start with no matching end is dropped rather than guessed at: a truncated
block is exactly the case where guessing hands a consumer half a derivation and
calls it whole.
iex> output = "% SZS output start Proof for X\nfof(a,axiom,p).\n% SZS output end Proof for X\n"
iex> Tptp.Szs.blocks(output)
[%{dataform: :proof, problem: "X", body: "fof(a,axiom,p)."}]@spec output_block(Tptp.Szs.Ontology.t(), binary(), binary()) :: binary()
Wrap a body in output start / output end markers.
iex> Tptp.Szs.output_block(:proof, "X", "fof(a,axiom,p).")
"% SZS output start Proof for X\nfof(a,axiom,p).\n% SZS output end Proof for X"The status a system reported, taken from the last status line it printed.
iex> Tptp.Szs.status("% SZS status Theorem for X\n% SZS status GaveUp for X : ran out\n")
{:ok, :gave_up, "X", "ran out"}
iex> Tptp.Szs.status("nothing to see here")
:none
iex> Tptp.Szs.status("% SZS status Nonsense for X")
{:error, "Nonsense", "X", nil}@spec status_line(Tptp.Szs.Ontology.t(), binary(), binary() | nil) :: binary()
Write a status line.
iex> Tptp.Szs.status_line(:theorem, "PUZ001+1")
"% SZS status Theorem for PUZ001+1"
iex> Tptp.Szs.status_line(:gave_up, "PUZ001+1", "no strategy left")
"% SZS status GaveUp for PUZ001+1 : no strategy left"Every status line in the output, in the order they appear.
iex> Tptp.Szs.statuses("% SZS status Theorem for A\n% SZS status Timeout for B\n")
[{:ok, :theorem, "A", nil}, {:ok, :timeout, "B", nil}]Whether the output reports a success-ontology value.
iex> Tptp.Szs.success?("% SZS status Unsatisfiable for X")
true
iex> Tptp.Szs.success?("% SZS status Timeout for X")
false
iex> Tptp.Szs.success?("")
false@spec value(binary()) :: {:ok, Tptp.Szs.Ontology.t()} | {:error, binary()} | :none
The last status, reduced to a plain value.
iex> Tptp.Szs.value("% SZS status CounterSatisfiable for X")
{:ok, :counter_satisfiable}
iex> Tptp.Szs.value("% SZS status Nonsense for X")
{:error, "Nonsense"}
iex> Tptp.Szs.value("")
:none