Class FolParser
java.lang.Object
org.tweetyproject.commons.Parser<FolBeliefSet,FolFormula>
org.tweetyproject.logics.fol.parser.FolParser
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).
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 Summary
-
Method Summary
Modifier and TypeMethodDescriptionReturns the signature of this parser.returns variablesparseBeliefBase
(Reader reader) Parses the given reader into a belief base of the given type.parseFormula
(Reader reader) Parses the given reader into a formula of the given type.This function parses only the sorts declaration and type declaration parts of a belief base.void
parseSortDeclaration
(String s, FolSignature sig) Parses a sort declaration of the form "SORTNAME "=" "{" (CONSTANTNAME ("," CONSTANTNAME)*)? "}"" and modifies the given signature accordingly.void
parseTypeDeclaration
(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
(Map<String, Variable> variables) sets variablesMethods inherited from class org.tweetyproject.commons.Parser
isNumeric, parseBeliefBase, parseBeliefBaseFromFile, parseFormula, parseFormulaFromFile, parseListOfBeliefBases, parseListOfBeliefBases, parseListOfBeliefBasesFromFile, parseListOfBeliefBasesFromFile
-
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
Description copied from class:Parser
Parses the given reader into a belief base of the given type.- Specified by:
parseBeliefBase
in classParser<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
Parses a sort declaration of the form "SORTNAME "=" "{" (CONSTANTNAME ("," CONSTANTNAME)*)? "}"" and modifies the given signature accordingly.- Parameters:
s
- a stringsig
- a signature- Throws:
ParserException
- if parsing fails
-
parseTypeDeclaration
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 stringsig
- a signature- Throws:
ParserException
- if parsing fails
-
parseFormula
Description copied from class:Parser
Parses the given reader into a formula of the given type.- Specified by:
parseFormula
in classParser<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
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
Sets the signature for this parser.- Parameters:
signature
- a fol signature.
-
getSignature
Returns the signature of this parser.- Returns:
- the signature of this parser.
-
getVariables
returns variables- Returns:
- variables
-
setVariables
sets variables- Parameters:
variables
- variables to be set
-