Class FolParser

java.lang.Object
org.tweetyproject.commons.Parser<FolBeliefSet,FolFormula>
org.tweetyproject.logics.fol.parser.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 |
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 the containsEquality attribute enabled (which is not the case by default).
Author:
Matthias Thimm, Anna Gessler
  • Constructor Details

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

    • parseBeliefBase

      public FolBeliefSet parseBeliefBase(Reader reader) throws 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:
      IOException - if some IO issue occurred.
      ParserException - some parsing exceptions may be added here.
    • parseSortDeclaration

      public void parseSortDeclaration(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(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(Reader reader) throws 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:
      IOException - if some IO issue occurred.
      ParserException - some parsing exceptions may be added here.
    • parseSignature

      public FolSignature parseSignature(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 Map<String,Variable> getVariables()
      returns variables
      Returns:
      variables
    • setVariables

      public void setVariables(Map<String,Variable> variables)
      sets variables
      Parameters:
      variables - variables to be set