Package com.articulate.sigma.tp

Class ATPResult

java.lang.Object
com.articulate.sigma.tp.ATPResult
public class ATPResult extends Object
Generic result structure for ATP (Automated Theorem Prover) runs. Captures execution metadata, SZS status, output, and proof data. This class provides a unified interface for results from different provers: - Vampire - EProver - LEO-III

  • Constructor Details

    • ATPResult

      public ATPResult()
      Default constructor

  • Method Details

    • notRun

      public static ATPResult notRun(String engineName, String reason)
      Create an ATPResult indicating the prover was not run

    • crashed

      public static ATPResult crashed(String engineName, int exitCode, List<String> stdout, List<String> stderr)
      Create an ATPResult for a crashed prover

    • timeout

      public static ATPResult timeout(String engineName, long timeoutMs, long elapsedMs, List<String> stdout, List<String> stderr)
      Create an ATPResult for a timeout

    • getEngineName

      public String getEngineName()

    • setEngineName

      public void setEngineName(String engineName)

    • getEngineMode

      public String getEngineMode()

    • setEngineMode

      public void setEngineMode(String engineMode)

    • getInputLanguage

      public String getInputLanguage()

    • setInputLanguage

      public void setInputLanguage(String inputLanguage)

    • getInputSource

      public String getInputSource()

    • setInputSource

      public void setInputSource(String inputSource)

    • getTimeoutMs

      public long getTimeoutMs()

    • setTimeoutMs

      public void setTimeoutMs(long timeoutMs)

    • getCommandLine

      public List<String> getCommandLine()

    • setCommandLine

      public void setCommandLine(List<String> commandLine)

    • setCommandLine

      public void setCommandLine(String[] commandLine)

    • getCommandLineString

      public String getCommandLineString()

    • getExitCode

      public int getExitCode()

    • setExitCode

      public void setExitCode(int exitCode)

    • getElapsedTimeMs

      public long getElapsedTimeMs()

    • setElapsedTimeMs

      public void setElapsedTimeMs(long elapsedTimeMs)

    • isTimedOut

      public boolean isTimedOut()

    • setTimedOut

      public void setTimedOut(boolean timedOut)

    • getTerminationSignal

      public String getTerminationSignal()

    • setTerminationSignal

      public void setTerminationSignal(String terminationSignal)

    • getStdout

      public List<String> getStdout()

    • setStdout

      public void setStdout(List<String> stdout)

    • getStderr

      public List<String> getStderr()

    • setStderr

      public void setStderr(List<String> stderr)

    • getSzsStatus

      public SZSStatus getSzsStatus()

    • setSzsStatus

      public void setSzsStatus(SZSStatus szsStatus)

    • getSzsStatusRaw

      public String getSzsStatusRaw()

    • setSzsStatusRaw

      public void setSzsStatusRaw(String szsStatusRaw)

    • getSzsDiagnostics

      public String getSzsDiagnostics()

    • setSzsDiagnostics

      public void setSzsDiagnostics(String szsDiagnostics)

    • getSzsOutputType

      public String getSzsOutputType()

    • setSzsOutputType

      public void setSzsOutputType(String szsOutputType)

    • getProofSteps

      public List<tptp_parser.TPTPFormula> getProofSteps()

    • setProofSteps

      public void setProofSteps(List<tptp_parser.TPTPFormula> proofSteps)

    • getAnswerBindings

      public Map<String,String> getAnswerBindings()

    • setAnswerBindings

      public void setAnswerBindings(Map<String,String> answerBindings)

    • isInconsistencyDetected

      public boolean isInconsistencyDetected()

    • setInconsistencyDetected

      public void setInconsistencyDetected(boolean inconsistencyDetected)

    • getParsingWarnings

      public List<String> getParsingWarnings()

    • setParsingWarnings

      public void setParsingWarnings(List<String> parsingWarnings)

    • getErrorLines

      public List<String> getErrorLines()

    • setErrorLines

      public void setErrorLines(List<String> errorLines)

    • getPrimaryError

      public String getPrimaryError()

    • setPrimaryError

      public void setPrimaryError(String primaryError)

    • getWarnings

      public List<String> getWarnings()

    • setWarnings

      public void setWarnings(List<String> warnings)

    • isSuccess

      public boolean isSuccess()
      Returns:
      true if the prover found a proof or determined the status successfully

    • hasProof

      public boolean hasProof()
      Returns:
      true if proof steps are available

    • hasAnswers

      public boolean hasAnswers()
      Returns:
      true if answer bindings are available

    • hasErrors

      public boolean hasErrors()
      Returns:
      true if there were errors (exit code != 0, error status, or error lines)

    • hasWarnings

      public boolean hasWarnings()
      Returns:
      true if there are warnings

    • hasStderr

      public boolean hasStderr()
      Returns:
      true if stderr has content

    • hasStdout

      public boolean hasStdout()
      Returns:
      true if stdout has content

    • getSummary

      public String getSummary()
      Get a human-readable summary of the result

    • getCssClass

      public String getCssClass()
      Get CSS class for UI styling based on status

    • getStatusBadgeClass

      public String getStatusBadgeClass()
      Get CSS class for the status badge

    • extractSzsFromOutput

      public void extractSzsFromOutput()
      Extract and populate SZS information from stdout

    • finalize

      public void finalize(int exitCode, long elapsedMs, boolean timedOut)
      Finalize the result after prover execution. Extracts SZS info and sets defaults based on execution outcome.

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • builder

      public static ATPResult.Builder builder()