Package net.sf.tweety.logics.fol.parser

Class TPTPParser

  • public class TPTPParser
extends Parser<FolBeliefSet,​FolFormula>
    This class implements a parser for the TPTP syntax that parses single fol formulas and knowledge bases (TPTP problem files or axiom files). TPTP files consist of any of the following in any order and separated by newlines:
    • formulas
    • comments, i.e. lines starting with "%"
    • includes of other TPTP files, i.e. lines like "include('path/to/file',[optional,formula,names])"
    The syntax for first-order logic formulas is 'fof(name,role,formula,source,[useful_info]).':
    • name is the name of the formula
    • role is anything out of {axiom, hypothesis, definition, assumption, lemma, theorem, corollary conjecture, negated_conjecture}
    • formula is the actual formula
    • The other arguments are optional and ignored by this parser.
    Supported operators and pre-defined predicates in formulas:
    Negation: ~ formula
    Conjunction: formula & formula
    Disjunction: formula | formula
    Implication: formula => formula
    formula <= formula
    Equivalence: formula <=> formula
    Universal quantifier: ! [Variable1,Variable2,...] : (formula)
    Existential quantifier: ? [Variable1,Variable2,...] : (formula)
    Tautology: $true
    Contradiction: $false
    Equality: = (TODO soon to be added)
    Inequality: != (TODO soon to be added)
    Author:
    Anna Gessler

    • Field Summary

      Fields 
      Modifier and Type Field Description
      private java.lang.String formulaNames
      Regular expression that restricts which formulas will be parsed.
      private java.lang.String formulaRoles
      Regular expression that restricts which formulas will be parsed.
      private java.lang.String includePath
      Location of included files (optional).
      private FolSignature signature
      Keeps track of the signature.
      private java.util.Map<java.lang.String,​Variable> variables
      Keeps track of variables defined.

    • Constructor Summary

      Constructors 
      Constructor Description
      TPTPParser()  

    • Method Summary

      Modifier and Type Method Description
      private void consumeToken​(java.util.Stack<java.lang.Object> stack, int c)
      This method reads one token from the given reader and appropriately constructs a fol formula from the stream.
      FolSignature getSignature()
      Returns the signature of this parser.
      private FolFormula parseAtomic​(java.util.List<java.lang.Object> l)  
      FolBeliefSet parseBeliefBase​(java.io.Reader reader)
      Parses the given reader into a belief base of the given type.
      private FolFormula parseConjunction​(java.util.List<java.lang.Object> l)
      Parses a conjunction as a list of String tokens or formulas into a fol formula.
      private FolFormula parseDisjunction​(java.util.List<java.lang.Object> l)
      Parses a disjunction as a list of String tokens or formulas into a fol formula.
      private FolFormula parseEquivalence​(java.util.List<java.lang.Object> l)
      Parses an equivalence as a list of String tokens or formulas into a fol formula.
      FolFormula parseFormula​(java.io.Reader reader)
      Parses the given reader into a formula of the given type.
      private FolFormula parseImplication​(java.util.List<java.lang.Object> l)
      Parses an implication as a list of String tokens or formulas into a fol formula.
      private FolBeliefSet parseIncludedFiles​(java.lang.String s)
      Parses formulas of an included TPTP problem file.
      private FolFormula parseNegation​(java.util.List<java.lang.Object> l)  
      private FolFormula parseQuantification​(java.util.List<java.lang.Object> l)
      Parses a quantified formula as a list of String tokens or formulas.
      private java.util.List<Term<?>> parseTermlist​(java.util.List<java.lang.Object> l)
      Parses a term list as a list of String tokens or terms into a list of terms.
      private void parseTypes​(java.lang.String formula)
      Parse signature of a problem file.
      void resetFormulaNames()
      Reset the regular expression that restricts which formulas will be parsed to the default value, meaning formulas of all names will be parsed.
      void resetFormulaRoles()
      Reset the regular expression that restricts which formulas will be parsed to the default value, meaning formulas of any TPTP roles will be parsed.
      void setFormulaNames​(java.lang.String formulaNames)
      Set the regular expression that restricts which formulas will be parsed.
      void setFormulaRoles​(java.lang.String formulaRoles)
      Set the regular expression that restricts which formulas will be parsed.
      void setIncludePath​(java.lang.String includePath)
      Set the location of included files.
      void setSignature​(FolSignature signature)
      Sets the signature for this parser.

      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

    • Field Detail

      • signature

        private FolSignature signature
        Keeps track of the signature.

      • variables

        private java.util.Map<java.lang.String,​Variable> variables
        Keeps track of variables defined.

      • includePath

        private java.lang.String includePath
        Location of included files (optional). This path will be prepended to the path given in the include('included_file') paths.

      • formulaNames

        private java.lang.String formulaNames
        Regular expression that restricts which formulas will be parsed. Formulas with names that do not match the expression will not be parsed. By default, all formulas are parsed.

      • formulaRoles

        private java.lang.String formulaRoles
        Regular expression that restricts which formulas will be parsed. Formulas with roles that do not match the expression will not be parsed. By default, all formulas are parsed.

    • Constructor Detail

      • TPTPParser

        public TPTPParser()

    • Method Detail

      • parseBeliefBase

        public FolBeliefSet parseBeliefBase​(java.io.Reader reader)
                             throws java.io.IOException,
                                    ParserException
        Description copied from class: Parser
        Parses the given reader into a belief base of the given type.
        Specified by:
        parseBeliefBase in class Parser<FolBeliefSet,​FolFormula>
        Parameters:
        reader - a reader
        Returns:
        a belief base
        Throws:
        java.io.IOException - if some IO issue occurred.
        ParserException - some parsing exceptions may be added here.

      • parseIncludedFiles

        private FolBeliefSet parseIncludedFiles​(java.lang.String s)
                                 throws java.io.FileNotFoundException,
                                        ParserException,
                                        java.io.IOException
        Parses formulas of an included TPTP problem file. If the given string contains a list of formula names in addition to the include path, only formulas of the given names will be parsed.
        Parameters:
        s - String of format "include('path/to/file')." or "include('path/to/file',[formula,names,separated,by,commata])."
        Returns:
        a belief set containing the parsed included formulas
        Throws:
        java.io.FileNotFoundException - if a file could not be found
        ParserException - if parsing fails
        java.io.IOException - if there is an IO issue

      • parseFormula

        public FolFormula parseFormula​(java.io.Reader reader)
                        throws java.io.IOException,
                               ParserException
        Description copied from class: Parser
        Parses the given reader into a formula of the given type.
        Specified by:
        parseFormula in class Parser<FolBeliefSet,​FolFormula>
        Parameters:
        reader - a reader
        Returns:
        a formula
        Throws:
        java.io.IOException - if some IO issue occurred.
        ParserException - some parsing exceptions may be added here.

      • parseTypes

        private void parseTypes​(java.lang.String formula)
        Parse signature of a problem file. If some or all of the symbols are already part of the signature, they will not be overwritten.
        Parameters:
        formula - a String of a formula

      • consumeToken

        private void consumeToken​(java.util.Stack<java.lang.Object> stack,
                          int c)
        This method reads one token from the given reader and appropriately constructs a fol formula from the stream.
        Parameters:
        stack - a stack used for monitoring the read items.
        c - a token from a stream.
        Throws:
        ParserException - in case of parser errors.

      • parseTermlist

        private java.util.List<Term<?>> parseTermlist​(java.util.List<java.lang.Object> l)
        Parses a term list as a list of String tokens or terms into a list of terms.
        Parameters:
        l - a list of objects, either String tokens or objects of type List.
        Returns:
        a list of terms.
        Throws:
        ParserException - if the list could not be parsed.

      • parseQuantification

        private FolFormula parseQuantification​(java.util.List<java.lang.Object> l)
        Parses a quantified formula as a list of String tokens or formulas.
        Parameters:
        l - a list objects, either String tokens or objects of type FolFormula.
        Returns:
        a FolFormula.
        Throws:
        ParserException - if the list could not be parsed.

      • parseEquivalence

        private FolFormula parseEquivalence​(java.util.List<java.lang.Object> l)
        Parses an equivalence as a list of String tokens or formulas into a fol formula.
        Parameters:
        l - a list objects, either String tokens or objects of type FolFormula.
        Returns:
        a FolFormula.
        Throws:
        ParserException - if the list could not be parsed.

      • parseImplication

        private FolFormula parseImplication​(java.util.List<java.lang.Object> l)
        Parses an implication as a list of String tokens or formulas into a fol formula. Reverse implications like 'A <= B' will be parsed as 'B => A'.
        Parameters:
        l - a list objects, either String tokens or objects of type FolFormula.
        Returns:
        a FolFormula.
        Throws:
        ParserException - if the list could not be parsed.

      • parseDisjunction

        private FolFormula parseDisjunction​(java.util.List<java.lang.Object> l)
        Parses a disjunction as a list of String tokens or formulas into a fol formula.
        Parameters:
        l - a list objects, either String tokens or objects of type FolFormula.
        Returns:
        a FolFormula.
        Throws:
        ParserException - if the list could not be parsed.

      • parseConjunction

        private FolFormula parseConjunction​(java.util.List<java.lang.Object> l)
        Parses a conjunction as a list of String tokens or formulas into a fol formula.
        Parameters:
        l - a list objects, either String tokens or objects of type FolFormula.
        Returns:
        a FolFormula.
        Throws:
        ParserException - if the list could not be parsed.

      • parseNegation

        private FolFormula parseNegation​(java.util.List<java.lang.Object> l)

      • parseAtomic

        private FolFormula parseAtomic​(java.util.List<java.lang.Object> l)

      • setSignature

        public void setSignature​(FolSignature signature)
        Sets the signature for this parser.
        Parameters:
        signature - a fol signature.

      • getSignature

        public FolSignature getSignature()
        Returns the signature of this parser.
        Returns:
        the signature of this parser.

      • setFormulaNames

        public void setFormulaNames​(java.lang.String formulaNames)
        Set the regular expression that restricts which formulas will be parsed. Formulas with names that do not match the expression will not be parsed.
        Parameters:
        formulaNames - the regex for formula names

      • setFormulaRoles

        public void setFormulaRoles​(java.lang.String formulaRoles)
        Set the regular expression that restricts which formulas will be parsed. Formulas with roles that do not match the expression will not be parsed.
        Parameters:
        formulaRoles - the regex for formula roles

      • resetFormulaRoles

        public void resetFormulaRoles()
        Reset the regular expression that restricts which formulas will be parsed to the default value, meaning formulas of any TPTP roles will be parsed. Possible TPTP roles are axiom, hypothesis, definition, assumption, lemma, theorem, corollary, conjecture and negated_conjecture.

      • resetFormulaNames

        public void resetFormulaNames()
        Reset the regular expression that restricts which formulas will be parsed to the default value, meaning formulas of all names will be parsed.

      • setIncludePath

        public void setIncludePath​(java.lang.String includePath)
        Set the location of included files.
        Parameters:
        includePath - path that will be prepended to the paths of all included problem files.