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

Class FolParser

  • public class FolParser
extends Parser<FolBeliefSet,​FolFormula>
    This class implements a parser for first-order logic. The BNF for a first-order knowledge base is given by (starting symbol is KB)

    KB ::== SORTSDEC DECLAR FORMULAS
    DECLAR ::== (FUNCTORDEC | PREDDEC)*
    SORTSDEC ::== ( SORTNAME "=" "{" (CONSTANTNAME ("," CONSTANTNAME)*)? "}" "\n" )*
    PREDDEC ::== "type" "(" PREDICATENAME ("(" SORTNAME ("," SORTNAME)* ")")? ")" "\n"
    FUNCTORDEC ::== "type" "(" SORTNAME "=" FUNCTORNAME "(" (SORTNAME ("," SORTNAME)*)? ")" ")" "\n"
    FORMULAS ::== ( "\n" FORMULA)*
    FORMULA ::== ATOM | "forall" VARIABLENAME ":" "(" FORMULA ")" | "exists" VARIABLENAME ":" "(" FORMULA ")" |
    "(" FORMULA ")" | FORMULA "&&" FORMULA | FORMULA "||" FORMULA | "!" FORMULA | "+" | "-" |
    FORMULA "=>" FORMULA | FORMULA "<=>" FORMULA | FORMULA "==" FORMULA | FORMULA "/==" FORMULA |
    ATOM ::== PREDICATENAME ("(" TERM ("," TERM)* ")")?
    TERM ::== VARIABLENAME | CONSTANTNAME | FUNCTORNAME "(" (TERM ("," TERM)*)? ")"

    where SORTNAME, PREDICATENAME, CONSTANTNAME and FUNCTORNAME are sequences of
    symbols from {a,...,z,A,...,Z,0,...,9} with a letter at the beginning and VARIABLENAME
    is a sequence of symbols from {a,...,z,A,...,Z,0,...,9} with an uppercase letter at the beginning.

    Note: Equality/Inequality predicates (== and /==) can only be parsed if the parser is given a FolSignature
    with equality (which is not the case by default).
    Author:
    Matthias Thimm, Anna Gessler

    • Field Summary

      Fields 
      Modifier and Type Field Description
      private boolean ignoreUndeclaredConstants
      Do not raise exceptions when encountering new constants, all new constants are treated as THING
      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
      FolParser()
      Creates a new FolParser
      FolParser​(boolean ignoreUndeclaredConstants)
      Creates a new FolParser

    • 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.
      java.util.Map<java.lang.String,​Variable> getVariables()  
      private FolFormula parseAtomic​(java.util.List<java.lang.Object> l)
      Parses a simple formula as a list of String tokens or formulas into a fol formula.
      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 simple 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 FolFormula parseNegation​(java.util.List<java.lang.Object> l)
      Parses a simple formula as a list of String tokens or formulas into a fol formula.
      private FolFormula parseQuantification​(java.util.List<java.lang.Object> l)
      Parses a quantified formula as a list of String tokens or formulas.
      FolSignature parseSignature​(java.lang.String s)
      This function parses only the sorts declaration and type declaration parts of a belief base.
      void parseSortDeclaration​(java.lang.String s, FolSignature sig)
      Parses a sort declaration of the form "SORTNAME "=" "{" (CONSTANTNAME ("," CONSTANTNAME)*)? "}"" and modifies the given signature accordingly.
      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.
      void parseTypeDeclaration​(java.lang.String s, FolSignature sig)
      Parses a predicate declaration of the form "type" "(" PREDICATENAME "(" (SORTNAME ("," SORTNAME)*)? ")" ")" or a functor declaration of the form "type" "(" SORTNAME "=" FUNCTORNAME "(" (SORTNAME ("," SORTNAME)*)? ")" ")" and modifies the given signature accordingly.
      void setSignature​(FolSignature signature)
      Sets the signature for this parser.
      void setVariables​(java.util.Map<java.lang.String,​Variable> variables)  

      • 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.

      • ignoreUndeclaredConstants

        private boolean ignoreUndeclaredConstants
        Do not raise exceptions when encountering new constants, all new constants are treated as THING

    • Constructor Detail

      • FolParser

        public FolParser()
        Creates a new FolParser

      • FolParser

        public FolParser​(boolean ignoreUndeclaredConstants)
        Creates a new FolParser
        Parameters:
        ignoreUndeclaredConstants - Do not raise exceptions when encountering new constants, all new constants are treated as THING

    • 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.

      • parseSortDeclaration

        public void parseSortDeclaration​(java.lang.String s,
                                 FolSignature sig)
                          throws ParserException
        Parses a sort declaration of the form "SORTNAME "=" "{" (CONSTANTNAME ("," CONSTANTNAME)*)? "}"" and modifies the given signature accordingly.
        Parameters:
        s - a string
        sig - a signature
        Throws:
        ParserException - if parsing fails

      • parseTypeDeclaration

        public void parseTypeDeclaration​(java.lang.String s,
                                 FolSignature sig)
                          throws ParserException
        Parses a predicate declaration of the form "type" "(" PREDICATENAME "(" (SORTNAME ("," SORTNAME)*)? ")" ")" or a functor declaration of the form "type" "(" SORTNAME "=" FUNCTORNAME "(" (SORTNAME ("," SORTNAME)*)? ")" ")" and modifies the given signature accordingly.
        Parameters:
        s - a string
        sig - a signature
        Throws:
        ParserException - if parsing fails

      • 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.

      • consumeToken

        private void consumeToken​(java.util.Stack<java.lang.Object> stack,
                          int c)
                   throws ParserException
        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)
                                       throws ParserException
        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)
                                throws ParserException
        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.
        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. This method expects no parentheses in the list and as such treats the formula as a disjunction.
        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)
                             throws ParserException
        Parses a simple 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)
                          throws ParserException
        Parses a simple formula as a list of String tokens or formulas into a fol formula. This method expects no parentheses, no disjunctions, and no conjunctions in the list and as such treats the formula as a negation.
        Parameters:
        l - a list objects, either String tokens or objects of type FolFormula.
        Returns:
        a fol formula.
        Throws:
        ParserException - if the list could not be parsed.

      • parseAtomic

        private FolFormula parseAtomic​(java.util.List<java.lang.Object> l)
                        throws ParserException
        Parses a simple formula as a list of String tokens or formulas into a fol formula. This method expects no parentheses, no disjunctions, no conjunctions, and no negation in the list and as such treats the formula as an atomic construct, either a contradiction, a tautology, or an atom (a predicate with a list of terms).
        Parameters:
        l - a list objects, either String tokens or objects of type folFormula.
        Returns:
        a fol formula.
        Throws:
        ParserException - if parsing fails

      • parseSignature

        public FolSignature parseSignature​(java.lang.String s)
        This function parses only the sorts declaration and type declaration parts of a belief base.
        Parameters:
        s - the signature as a string
        Returns:
        the parsed fol signature

      • 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.

      • getVariables

        public java.util.Map<java.lang.String,​Variable> getVariables()

      • setVariables

        public void setVariables​(java.util.Map<java.lang.String,​Variable> variables)