@spec extract_isabelle_text(map()) :: String.t()

Concatenates all "message" strings from a use_theories payload (the result field of a finished %IsabelleClient.Task{}) into a single newline-separated string.

Walks all nodes in the payload, not just the first — useful when a theory transitively imports others and the server reports messages against multiple nodes.

@spec interpret_isabelle_result(map()) :: atp_result()

Interprets the result payload of a finished use_theories task — the map returned in %IsabelleClient.Task{status: :finished, result: ...}, with top-level keys "ok", "errors", "nodes", etc.

Classification is driven by the messages Isabelle emits, not by whether the task finished without errors. Isabelle is goal-directed (it proves stated conjectures), so successful proofs map to :theorem rather than :unsatisfiable, and a refuted goal maps to :counter_satisfiable:

• a "Nitpick / Quickcheck found a counterexample" message yields {:ok, :counter_satisfiable};
• a "Nitpick / Quickcheck found a model" message yields {:ok, :satisfiable};
• a Sledgehammer "found a proof" message yields {:ok, :theorem};
• any message starting with "theorem " (Isabelle's proof-completion notification, emitted for every discharged goal regardless of the tactic used) yields {:ok, :theorem};
• a "timed out" / "TIMEOUT" message yields {:ok, :timeout};
• a "Out of memory" message yields {:ok, :memory_out};
• remaining cases yield {:ok, :gave_up}.

Failed tasks should be surfaced through AtpClient.Isabelle.prove_theory/4's {:error, {:isabelle_failed, _, _}} channel and never reach this function.

@spec interpret_result(String.t()) :: atp_result()

Interprets the output of provers that follow the SZS ontology (including those available on SystemOnTPTP) into the standardized representation.

Three layers run in order:

1. Prover-specific patterns for solvers that do not (always) emit an SZS status line — Alt-Ergo, E, iProver, LEO-II, SPASS, Vampire, Waldmeister. Mirrors the sledgehammer source (https://github.com/seL4/isabelle/blob/master/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML) but maps to the honest SZS atom rather than sledgehammer's negated-conjecture interpretation: e.g. SPASS "Completion found" becomes {:ok, :satisfiable}, not {:ok, :gave_up}.
2. The explicit SZS table (@known_szs_results) recognises every status in szs_success/0 and szs_no_success/0 from a "SZS status <Name>" or " says <Name>" substring.
3. A permissive fallback converts any remaining "SZS status <CamelCase>" (or " says <CamelCase>") line to its snake-case atom, so SZS additions like EquivalentTheorem become {:ok, :equivalent_theorem} without a code change.

Output that none of the three layers matches comes back as {:error, {:unrecognized_output, res_str}}.

@spec per_lemma_results(map(), [lemma_spec()], keyword()) :: [lemma_result()]

Classifies a finished use_theories payload into one entry per lemma, in the order given by lemma_specs.

Messages from each lemma's body-line range are bucketed and scanned one-at-a-time — never across the concatenated text of a bucket. The cross-message scan that earlier versions of this function used produced false :counter_satisfiable verdicts when one message read Nitpick found a model and another read Nitpick found no counterexample (the "Nitpick found a" + "counterexample" substring test fires across the two), and false :theorem verdicts when by auto failed on a False goal (Isabelle still echoes theorem name: <goal> at the by position next to the Failed to finish proof error).

Options

• :file — keep only messages whose pos.file ends with the given suffix (typically "/<theory_name>.thy"). Messages from the bundled TPTP.thy and from transitively imported theories are dropped. Defaults to no filter.
• :line_offset — number to subtract from each Isabelle-reported pos.line before comparing against lemma_spec.range. Auto-wrap adds one line (theory <name> imports … begin) to the on-disk file, so callers that pass a body without the header set this to 1. Defaults to 0.

Verdict precedence

Within a lemma bucket, signals collected per-message are reconciled in this order (each step short-circuits):

1. :counter_satisfiable (Nitpick / Quickcheck counter-example) — disproves the goal; dominates any concurrent proof attempt.
2. :theorem from a sledgehammer / metis "found a proof" line.
3. :satisfiable (Nitpick / Quickcheck model).
4. Proof-method failure veto — an error-kind message containing "Failed to finish proof" cancels a theorem name: verdict from the same bucket.
5. :theorem from a theorem name: completion notification.
6. :timeout, :memory_out, then :gave_up.

Lemmas whose bucket is empty come back as {:ok, :gave_up}.