AtpClient.Verdict (AtpClient v0.7.2)

Copy Markdown View Source

Reads a system's output into an AtpClient.Result.

Three readings run in order, and the first that finds something decides:

  1. The SZS status line, through Tptp.Szs.status/1: the last status line in the output, with its value looked up in Tptp.Szs.Ontology. A word the ontology does not define is reported as {:error, {:unknown_szs_status, word}}, not converted to an atom. A value from the data ontology on a status line, such as Proof, is {:error, {:not_a_status, value}}.
  2. The SystemOnTPTP summary line, <system> says <Value>, which SystemOnTPTP prints for every system it ran and which carries the same vocabulary.
  3. Prover-specific messages from systems that do not (always) print an SZS line — Alt-Ergo, E, LEO-II, SPASS, Vampire, Waldmeister. The table is patterns/0. Each entry maps to the most faithful SZS value the message alone supports; where a verdict is sound only under flags the reader cannot see, such as SPASS saturating under -SOS, the entry is the conservative :gave_up.

Output none of the three reads is {:error, {:unrecognized_output, output}}.

Isabelle does not print SZS lines; AtpClient.Isabelle.Verdict reads its messages.

Summary

Types

failure()

Why no result could be read from the output.

Functions

interpret(output, backend, fields \\ [])

Reads output from backend into a result.

patterns()

The prover-specific messages read when no SZS line is present, each with the result it stands for.

Types

failure()

@type failure() ::
  {:unknown_szs_status, binary()}
  | {:not_a_status, Tptp.Szs.Ontology.t()}
  | {:unrecognized_output, binary()}
  | :internal_error

Why no result could be read from the output.

  • {:unknown_szs_status, word} — a status line names a value the ontology does not define.
  • {:not_a_status, value} — a status line names a data value.
  • {:unrecognized_output, output} — no status line and no known pattern.
  • :internal_error — a pattern that identifies a crash of the system rather than a verdict.

Functions

interpret(output, backend, fields \\ [])

@spec interpret(binary(), module(), keyword()) ::
  {:ok, AtpClient.Result.t()} | {:error, failure()}

Reads output from backend into a result.

fields are put on the result as given: :system names the system that ran.

iex> {:ok, result} = AtpClient.Verdict.interpret("# SZS status Theorem\n", AtpClient.LocalExec, system: "eprover")
iex> {result.status, result.evidence, result.system}
{:theorem, :szs, "eprover"}

iex> AtpClient.Verdict.interpret("% SZS status Nonsense for x", AtpClient.LocalExec)
{:error, {:unknown_szs_status, "Nonsense"}}

iex> {:ok, result} = AtpClient.Verdict.interpret("SPASS beiseite: Completion found", AtpClient.LocalExec)
iex> {result.status, result.evidence}
{:gave_up, {:pattern, "SPASS beiseite: Completion found"}}

iex> AtpClient.Verdict.interpret("nothing to see", AtpClient.LocalExec)
{:error, {:unrecognized_output, "nothing to see"}}

patterns()

@spec patterns() :: [
  {binary(), {:ok, Tptp.Szs.Ontology.t()} | {:error, :internal_error}}
]

The prover-specific messages read when no SZS line is present, each with the result it stands for.