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.

What the reader accepts

The writers, status_line/3 and output_block/3, emit the form above, leaving out for <problem> when the problem is nil. The readers accept three departures from it that occur in practice:

• # in place of % as the comment character. E writes # SZS status Theorem.
• No for <problem>, as in the same line from E. The problem is then nil.
• Anything before the comment character on the same line. StarExec prefixes each line of a job's output with a pair of elapsed times, as in 0.00/0.03\t# SZS status Theorem.

The value and dataform are not relaxed: each is looked up in Tptp.Szs.Ontology as written. Anything after the problem other than a : <free text> suffix means the line is not a status line. The SystemOnTPTP summary line, ... <system> says <value> ..., is not an SZS status line and is not read here.

iex> Tptp.Szs.status("# SZS status Theorem\n")
{:ok, :theorem, nil, nil}

iex> Tptp.Szs.status("0.00/0.03\t# SZS status CounterSatisfiable\n")
{:ok, :counter_satisfiable, nil, nil}

iex> Tptp.Szs.status("% RESULT: SOT_x - Vampire---5.0 says Theorem - CPU = 0.01\n")
:none

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.