Package com.articulate.sigma.tp

Class SZSExtractor

java.lang.Object
com.articulate.sigma.tp.SZSExtractor
public class SZSExtractor extends Object
Utility class for extracting SZS (TPTP Standard for System status values) information from prover output. Handles output formats from: - Vampire: "% SZS status Theorem for SUMO" - EProver: "# SZS status Theorem" - LEO-III: "% SZS status Theorem for problem"

  • Method Details

    • extractStatus

      public static SZSStatus extractStatus(List<String> output)
      Extract the SZS status from prover output.
      Parameters:
      output - List of output lines from the prover
      Returns:
      The extracted SZSStatus, or null if none found

    • extractStatusLine

      public static String extractStatusLine(List<String> output)
      Extract the raw SZS status line from prover output.
      Parameters:
      output - List of output lines from the prover
      Returns:
      The full status line, or null if none found

    • extractStatusRaw

      public static String extractStatusRaw(List<String> output)
      Extract the raw status string (just the status word) from output.
      Parameters:
      output - List of output lines
      Returns:
      The status word (e.g., "Theorem", "Timeout"), or null

    • extractDiagnostics

      public static String extractDiagnostics(List<String> output)
      Extract diagnostics from SZS status line (text after colon). Example: "% SZS status TypeError : line 42, bad type" Returns: "line 42, bad type"
      Parameters:
      output - List of output lines
      Returns:
      Diagnostics string, or null if none

    • extractOutputType

      public static String extractOutputType(List<String> output)
      Extract the SZS output type (Proof, Refutation, Model, etc.)
      Parameters:
      output - List of output lines
      Returns:
      Output type string, or null if none found

    • extractErrorLines

      public static List<String> extractErrorLines(List<String> output)
      Extract lines that appear to contain error messages from stdout.
      Parameters:
      output - List of stdout lines
      Returns:
      List of lines containing error indicators

    • extractErrorLines

      public static List<String> extractErrorLines(List<String> stdout, List<String> stderr)
      Extract error lines from both stdout and stderr.
      Parameters:
      stdout - List of stdout lines
      stderr - List of stderr lines
      Returns:
      Combined list of error lines (stderr takes precedence)

    • extractWarnings

      public static List<String> extractWarnings(List<String> output)
      Extract warning lines from output.
      Parameters:
      output - List of output lines
      Returns:
      List of warning lines

    • indicatesTimeout

      public static boolean indicatesTimeout(List<String> output)
      Check if output indicates the prover timed out. Looks for both SZS status and common timeout patterns.
      Parameters:
      output - List of output lines
      Returns:
      true if timeout is indicated

    • indicatesResourceOut

      public static boolean indicatesResourceOut(List<String> output)
      Check if output indicates resource exhaustion.
      Parameters:
      output - List of output lines
      Returns:
      true if resource exhaustion is indicated

    • getPrimaryError

      public static String getPrimaryError(List<String> stdout, List<String> stderr)
      Get the primary error message from the output. Tries to find the most informative single error line.
      Parameters:
      stdout - Stdout lines
      stderr - Stderr lines
      Returns:
      Primary error message, or null if none found

    • indicatesSuccess

      public static boolean indicatesSuccess(List<String> output)
      Determine if output suggests success (proof found, etc.)
      Parameters:
      output - List of output lines
      Returns:
      true if output indicates success

    • containsProof

      public static boolean containsProof(List<String> output)
      Determine if output contains a proof.
      Parameters:
      output - List of output lines
      Returns:
      true if a proof section is present