Package com.articulate.sigma.tp

Class Vampire

java.lang.Object
com.articulate.sigma.tp.Vampire
public class Vampire extends Object
Class for invoking the latest research version of Vampire from Java A previous version invoked the KIF version of Vampire from Java but that's 15 years old now. The current Vampire does TPTP3 output instead of XML.
Since:
14/08/2003, Acapulco
Author:
Andrei Voronkov, apease

  • Field Details

    • qlist

      public StringBuilder qlist

    • output

      public List<String> output

    • axiomIndex

      public static int axiomIndex

    • logic

      public Vampire.Logic logic

    • mode

      public static Vampire.ModeType mode

    • debug

      public static boolean debug

    • askQuestion

      public static boolean askQuestion

  • Constructor Details

    • Vampire

      public Vampire()

  • Method Details

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • getResult

      public ATPResult getResult()
      Get the full ATPResult for this run. This provides detailed execution metadata, SZS status, and error info.
      Returns:
      The ATPResult, or null if run() hasn't been called

    • hasError

      public boolean hasError()
      Check if there was an error during execution.
      Returns:
      true if the result indicates an error

    • getSzsStatus

      public SZSStatus getSzsStatus()
      Get the SZS status from the last run.
      Returns:
      The SZSStatus, or SZSStatus.NOT_RUN if not run

    • assertFormula

      public static boolean assertFormula(String userAssertionTPTP, KB kb, List<Formula> parsedFormulas, boolean tptp)
      Add an assertion for inference.
      Parameters:
      userAssertionTPTP - asserted formula in the TPTP/TFF syntax
      kb - Knowledge base
      parsedFormulas - a lit of parsed formulas in KIF syntax
      tptp - convert formula to TPTP if tptp = true
      Returns:
      true if all assertions are added for inference TODO: This function might not be necessary if we find a way to directly add assertion into opened inference engine (e_ltb_runner)

    • run

      public void run(File kbFile, int timeout) throws Exception
      Creates a running instance of Vampire and collects its output
      Parameters:
      kbFile - A File object denoting the initial knowledge base to be loaded by the Vampire executable.
      timeout - the time given for Vampire to finish execution
      Throws:
      ExecutableNotFoundException - if the Vampire executable is not found
      ProverCrashedException - if Vampire crashes with a non-zero exit code
      ProverTimeoutException - if Vampire times out
      Exception - for other errors

    • runCustom

      public void runCustom(File kbFile, int timeout, Collection<String> commands) throws Exception
      Creates a running instance of Vampire with custom command line options.
      Parameters:
      kbFile - A File object denoting the initial knowledge base to be loaded by the Vampire executable.
      Throws:
      ExecutableNotFoundException - if the Vampire executable is not found
      ProverCrashedException - if Vampire crashes with a non-zero exit code
      ProverTimeoutException - if Vampire times out
      Exception - for other errors

    • writeStatements

      public void writeStatements(Set<String> stmts, String type)
      Write all the strings in @param stmts to temp-stmt.[tptp|tff|thf]

    • concatFiles

      public void concatFiles(String f1, String f2, String fout) throws IOException
      Read in two files and write their contents to a new file
      Throws:
      IOException

    • getUserAssertions

      public List<String> getUserAssertions(KB kb)

    • run

      public void run(KB kb, File kbFile, int timeout, Set<String> stmts) throws Exception
      Creates a running instance of Vampire adding a set of statements in TFF or TPTP language to a file and then calling Vampire. Note that any query must be given as a "conjecture"
      Parameters:
      kb - the current knowledge base
      kbFile - the current knowledge base TPTP file
      timeout - the timeout given to Vampire to find a proof
      stmts - a Set of user assertions
      Throws:
      Exception - of something goes south

    • printHelp

      public static void printHelp()

    • main

      public static void main(String[] args) throws Exception
      Throws:
      Exception