Packages

  • package root

    This is the documentation for the Scala TPTP parser used, e.g., by the Leo-III prover.

    This is the documentation for the Scala TPTP parser used, e.g., by the Leo-III prover.

    Package structure

    The leo package contains two sub-packages as follows:

    Usage (in short)

    The leo.modules.input.TPTPParser offers several parsing methods:

    Exemplary use case 

    import leo.modules.input.{TPTPParser => Parser}
import TPTPParser.TPTPParseException
import leo.datastructures.TPTP.THF

try {
 val result = Parser.problem(io.Source.fromFile("/path/to/file"))
 println(s"Parsed ${result.formulas.size} formulae and ${result.includes.size} include statements.")
 // ...
 val annotatedFormula = Parser.annotatedTHF("thf(f, axiom, ![X:$i]: (p @ X)).")
 println(s"${annotatedFormula.name} is an ${annotatedFormula.role}.")
 // ...
 val formula = Parser.thf("![X:$i]: (p @ X)")
 formula match {
   case THF.FunctionTerm(f, args) => // ...
   case THF.QuantifiedFormula(quantifier, variableList, body) => // ...
   case THF.Variable(name) => // ...
   case THF.UnaryFormula(connective, body) => // ...
   case THF.BinaryFormula(connective, left, right) => // ...
   case THF.Tuple(elements) => // ...
   case THF.ConditionalTerm(condition, thn, els) => // ...
   case THF.LetTerm(typing, binding, body) => // ...
   case THF.DefinedTH1ConstantTerm(constant) => // ...
   case THF.ConnectiveTerm(conn) => // ...
   case THF.DistinctObject(name) => // ...
   case THF.NumberTerm(value) => // ...
 }
 // ...
} catch {
 case e: TPTPParseException => println(s"Parse error at line ${e.line}:${e.offset}: ${e.getMessage}")
}
    Definition Classes
    root
  • package leo
    Definition Classes
    root
  • package modules
    Definition Classes
    leo
  • package input
    Definition Classes
    modules
  • TPTPParser
o

leo.modules.input

TPTPParser

object TPTPParser

Parser for TPTP-based input languages for automated theorem proving, including ...

  • THF (TH0/TH1): Monomorphic and polymorphic higher-order logic,
  • TFF (TF0/TF1): Monomorphic and polymorphic typed first-order logic, including extended TFF (TFX),
  • FOF: Untyped first-order logic,
  • TCF: Typed clause-normal form,
  • CNF: (Untyped) clause-normal form, and
  • TPI: TPTP Process Instruction language.

Both annotated as well as "plain" (meant here: not annotated) formulas can be read. An annotated formula (here, as an example: annotated THF formula) is of form thf(name, role, formula, annotations) whereas the plain formula is the formula part of this instance.

The parser translated plain formulas into an abstract syntax tree defined at datastructures.TPTP, resp. its corresponding specializations for the respective language dialect:

Annotated formulas are additionally wrapped in an datastructures.TPTP.AnnotatedFormula object as follows:

Whole TPTP files are represented by datastructures.TPTP.Problem objects. Note that include directives etc. are parsed as-is and are represented by an datastructures.TPTP.Include entry in the datastructures.TPTP.Problem representation. In particular, they are not parsed recursively. This has to be implemented externally (e.g., by recursive calls to the parser).

Parsing errors will cause TPTPParser.TPTPParseExceptions.

Since

January 2021

Note

For the original implementation of this parser v7.4.0.3 of the TPTP syntax was used, but it's being updated constantly to keep track with TPTP language updates.

See also

Original TPTP syntax definition at http://tptp.org/TPTP/SyntaxBNF.html.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TPTPParser
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. final class TPTPLexer extends BufferedIterator[TPTPLexerToken]

    A token stream of leo.modules.input.TPTPParser.TPTPLexer.TPTPLexerTokens that represents a TPTP input.

  2. class TPTPParseException extends RuntimeException

    Main exception thrown by the leo.modules.input.TPTPParser if some parsing error occurs.

  3. final class TPTPParser extends AnyRef

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. final def annotated(annotatedFormula: String): AnnotatedFormula

    Parses an TPTP annotated formula given as String.

    Parses an TPTP annotated formula given as String. Any kind of annotated formula can be passed to the function (THF/TFF/FOF/CNF/TPI), the parser will produce the respective specialization of AnnotatedFormula, e.g., THFAnnotated for annotated THF formulas.

    annotatedFormula

    The annotated formula as string.

    returns

    The parsing result as an AnnotatedFormula object.

    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  5. final def annotatedCNF(annotatedFormula: String): CNFAnnotated

    Parses an TPTP CNF annotated formula given as String.

    Parses an TPTP CNF annotated formula given as String.

    annotatedFormula

    The annotated formula as string.

    returns

    The parsing result as CNFAnnotated object

    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  6. final def annotatedFOF(annotatedFormula: String): FOFAnnotated

    Parses an TPTP FOF annotated formula given as String.

    Parses an TPTP FOF annotated formula given as String.

    annotatedFormula

    The annotated formula as string.

    returns

    The parsing result as FOFAnnotated object

    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  7. final def annotatedTCF(annotatedFormula: String): TCFAnnotated

    Parses an TPTP TCF annotated formula given as String.

    Parses an TPTP TCF annotated formula given as String.

    annotatedFormula

    The annotated formula as string.

    returns

    The parsing result as leo.datastructures.TPTP.TCFAnnotated object

    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  8. final def annotatedTFF(annotatedFormula: String, tfx: Boolean = true): TFFAnnotated

    Parses an TPTP TFF annotated formula given as String.

    Parses an TPTP TFF annotated formula given as String.

    annotatedFormula

    The annotated formula as string.

    tfx

    If set to true, accept TFX formulas as well (default); otherwise exclude TFX inputs.

    returns

    The parsing result as TFFAnnotated object

    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  9. final def annotatedTHF(annotatedFormula: String): THFAnnotated

    Parses an TPTP THF annotated formula given as String.

    Parses an TPTP THF annotated formula given as String.

    annotatedFormula

    The annotated formula as string.

    returns

    The parsing result as THFAnnotated object

    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  10. final def annotatedTPI(annotatedFormula: String): TPIAnnotated

    Parses an TPTP TPI annotated formula given as String.

    Parses an TPTP TPI annotated formula given as String.

    annotatedFormula

    The annotated formula as string.

    returns

    The parsing result as TPIAnnotated object

    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  11. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  12. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @IntrinsicCandidate()
  13. final def cnf(formula: String): Formula

    Parses a plain CNF formula (i.e., without annotations) given as String.

    Parses a plain CNF formula (i.e., without annotations) given as String.

    formula

    The annotated formula as string.

    returns

    The parsing resultas CNFFormula object

    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  14. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  15. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  16. final def fof(formula: String): Formula

    Parses a plain FOF formula (i.e., without annotations) given as String.

    Parses a plain FOF formula (i.e., without annotations) given as String.

    formula

    The annotated formula as string.

    returns

    The parsing resultas FOFFormula object

    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  17. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  18. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  19. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  20. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  21. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  22. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  23. final def problem(input: String): Problem

    Parses a whole TPTP file given as String.

    Parses a whole TPTP file given as String.

    input

    The TPTP problem file contents as string.

    returns

    The parsing result as a leo.datastructures.TPTP.Problem object.

    Annotations
    @inline()
    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  24. final def problem(input: Source): Problem

    Parses a whole TPTP file given as scala.io.Source.

    Parses a whole TPTP file given as scala.io.Source.

    input

    The TPTP problem file.

    returns

    The parsing result as a leo.datastructures.TPTP.Problem object.

    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  25. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  26. final def tcf(formula: String): Formula

    Parses a plain TCF formula (i.e., without annotations) given as String.

    Parses a plain TCF formula (i.e., without annotations) given as String.

    formula

    The annotated formula as string.

    returns

    The parsing resultas TCFFormula object

    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  27. final def tff(formula: String, tfx: Boolean = true): Formula

    Parses a plain TFF formula (i.e., without annotations) given as String.

    Parses a plain TFF formula (i.e., without annotations) given as String.

    formula

    The annotated formula as string.

    tfx

    If set to true, accept TFX formulas as well (default); otherwise exclude TFX inputs.

    returns

    The parsing resultas TFFFormula object

    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  28. final def thf(formula: String): Formula

    Parses a plain THF formula (i.e., without annotations) given as String.

    Parses a plain THF formula (i.e., without annotations) given as String.

    formula

    The annotated formula as string.

    returns

    The parsing result as THFFormula object

    Exceptions thrown

    TPTPParseException If an parsing error occurred.

  29. def toString(): String
    Definition Classes
    AnyRef → Any
  30. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  31. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  32. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  33. object TPTPLexer

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

Inherited from AnyRef

Inherited from Any

Ungrouped