# `Tptp.Szs` [🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/szs.ex#L1) 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 for % SZS status for : and delimits any output offered in support of that result: % SZS output start for ... % SZS output end for 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 ` 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 `, 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 `: ` suffix means the line is not a status line. The SystemOnTPTP summary line, `... says ...`, 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. # `block` ```elixir @type block() :: %{ dataform: Tptp.Szs.Ontology.t(), problem: binary() | nil, body: binary() } ``` A delimited output block: its dataform, the problem (`nil` when the markers name none), and the lines between the `start` and `end` markers with the markers removed. The body is verbatim, including any per-line prefix such as StarExec's. # `status` ```elixir @type status() :: {:ok, Tptp.Szs.Ontology.t(), binary() | nil, binary() | nil} ``` A parsed SZS status line: the value, the problem it is about (`nil` when the line names none), and any trailing free text after the `:`. # `unknown` ```elixir @type unknown() :: {:error, binary(), binary() | nil, binary() | nil} ``` A status line whose value is not in the ontology, kept verbatim. # `blocks` ```elixir @spec blocks(binary()) :: [block()] ``` 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)."}] # `output_block` ```elixir @spec output_block(Tptp.Szs.Ontology.t(), binary() | nil, binary()) :: binary() ``` Wrap a body in `output start` / `output end` markers. A `nil` problem leaves out `for ` on both. 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" iex> Tptp.Szs.output_block(:proof, nil, "fof(a,axiom,p).") "% SZS output start Proof\nfof(a,axiom,p).\n% SZS output end Proof" # `status` ```elixir @spec status(binary()) :: status() | unknown() | :none ``` 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} # `status_line` ```elixir @spec status_line(Tptp.Szs.Ontology.t(), binary() | nil, binary() | nil) :: binary() ``` Write a status line. A `nil` problem leaves out `for `. 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" iex> Tptp.Szs.status_line(:timeout, nil, "wall-clock limit") "% SZS status Timeout : wall-clock limit" # `statuses` ```elixir @spec statuses(binary()) :: [status() | unknown()] ``` 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}] # `success?` ```elixir @spec success?(binary()) :: boolean() ``` 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 # `value` ```elixir @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 --- *Consult [api-reference.md](api-reference.md) for complete listing*