Package net.sf.tweety.logics.fol.parser
Class FolParser
- java.lang.Object
-
- net.sf.tweety.commons.Parser<FolBeliefSet,FolFormula>
-
- net.sf.tweety.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 |
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 THINGprivate FolSignature
signature
Keeps track of the signature.private java.util.Map<java.lang.String,Variable>
variables
Keeps track of variables defined.
-
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 net.sf.tweety.commons.Parser
isNumeric, parseBeliefBase, parseBeliefBaseFromFile, parseFormula, parseFormulaFromFile
-
-
-
-
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
-
-
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 classParser<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 stringsig
- 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 stringsig
- 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 classParser<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)
-
-