Package com.articulate.sigma

Class InferenceTestSuite

java.lang.Object
com.articulate.sigma.InferenceTestSuite
public class InferenceTestSuite extends Object
A framework for doing a series of assertions and queries, and for comparing the actual result of queries against an expected result. Also will keep track of the time needed for each query. Tests are expected in files with a .tq extension contained in a directory specified by the "inferenceTestDir" parameter, and results are provided in the same directory with a .res extension. The test files contain legal KIF expressions including several kinds of meta-information. Meta-predicates include (note ), (query ), and (answer ..). There may be only one note and query statements, but there may be several answer statements, if multiple binding sets are expected. Comments are allowed in test files, and are signified by a ';', after which all content on the line is ignored. Note that since answers are provided in an ordered list, without reference to their respective variable names, that the inference engine is assumed to return bindings in the same order. All test file statements must be valid SUO-KIF. Allowable meta-predicates are: note, time, query, answer. All other predicates are assumed to be SUO-KIF expressions. 'answer' may take multiple SUO-KIF statements where there could be more than one valid answer.

  • Field Details

    • totalTime

      public static long totalTime
      Total time

    • _DEFAULT_TIMEOUT

      public static int _DEFAULT_TIMEOUT
      Default timeout for queries with unspecified timeouts or override when selected

    • overrideTimeout

      public static boolean overrideTimeout

    • kb

      public KB kb

    • debug

      public static boolean debug

    • saveTPTP

      public static boolean saveTPTP

    • metaPred

      public static Set<String> metaPred

  • Constructor Details

    • InferenceTestSuite

      public InferenceTestSuite()

  • Method Details

    • runOne

      public InferenceTestSuite.OneResult runOne(KB kb, String engine, int timeoutSec, String tqPath, boolean modusPonens)
      Thin wrapper for the JSP buttons: returns PASS/FAIL + time + a tiny HTML summary.

    • test

      public String test(KB kb) throws IOException
      Convenience method that sets default parameters
      Throws:
      IOException

    • test

      public String test(KB kb, String systemChosen, int timeout) throws IOException
      Convenience method that sets some default parameters
      Parameters:
      timeout - is a default timeout that is likely to be overwritten by a specification in the test data
      Throws:
      IOException

    • compareFiles

      public boolean compareFiles(InferenceTestSuite.InfTestData itd)
      Check if the required SUO-KIF file set is loaded and return false and print an error if not. Also issue a warning if extra non-required files are present.

    • normalizeSkolem

      public static String normalizeSkolem(String s)
      skolem terms in a string are converted to 'sK1'

    • parseAnswers

      public static void parseAnswers(String s, InferenceTestSuite.InfTestData itd)
      parse answers

    • readTestFile

      public InferenceTestSuite.InfTestData readTestFile(File f)
      Read in a .tq inference test files and return an InfTestData object or null if error Note that if the expected answer is a skolem term, the function is converted to 'sK1'

    • readTestFiles

      public List<InferenceTestSuite.InfTestData> readTestFiles(List<File> files)
      Read in all the .tq inference test files from the given list

    • saveTPTP

      public void saveTPTP(InferenceTestSuite.InfTestData itd)

    • printResults

      public void printResults(Collection<InferenceTestSuite.InfTestData> tests)

    • test

      public String test(KB inputKB, int defaultTimeout, String TPTPlocation) throws IOException
      The main method that controls running a set of tests and returning the result as an HTML page showing test results and links to proofs. Note that this procedure deletes any prior user assertions. If a test file has a set of KIF files different from what is already loaded, create a new KB for it.
      Throws:
      IOException

    • inferenceUnitTest

      public InferenceTestSuite.InfTestData inferenceUnitTest(String testpath, KB kb)
      The method will be called in InferenceTest in unit test; It takes a TQG file path, reading the kif statements and queries and expected answers; It parses the theorem prover's inference output for actual answers; Note that this procedure DOES NOT delete any prior user assertions.

    • runPassing

      public void runPassing()
      Test method

    • cmdLineTest

      public boolean cmdLineTest(String filename)
      Test method

    • resetAllForInference

      public static void resetAllForInference(KB kb) throws IOException
      Undo all parts of the state that have anything to do with user assertions made during inference.
      Throws:
      IOException

    • showHelp

      public static void showHelp()

    • main

      public static void main(String[] args)
      Test method