Package net.sf.tweety.logics.ml.parser
Class MlParser
- java.lang.Object
-
- net.sf.tweety.commons.Parser<MlBeliefSet,RelationalFormula>
-
- net.sf.tweety.logics.ml.parser.MlParser
-
public class MlParser extends Parser<MlBeliefSet,RelationalFormula>
This class implements a parser for modal logic. The BNF for a modal 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 equality (which is not the case by default).- Author:
- Matthias Thimm, Anna Gessler
-
-
Constructor Summary
Constructors Constructor Description MlParser()
-
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 modal formula from the stream.FolSignature
getSignature()
Returns the signature of this parser.private RelationalFormula
parseAtomic(java.util.List<java.lang.Object> l)
Parses a simple formula as a list of String tokens or formulas into a fol formula.MlBeliefSet
parseBeliefBase(java.io.Reader reader)
Parses the given reader into a belief base of the given type.private RelationalFormula
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 RelationalFormula
parseDisjunction(java.util.List<java.lang.Object> l)
Parses a disjunction as a list of String tokens or formulas into a fol formula.private RelationalFormula
parseEquivalence(java.util.List<java.lang.Object> l)
Parses an equivalence as a list of String tokens or formulas into a fol formula.RelationalFormula
parseFormula(java.io.Reader reader)
Parses the given reader into a formula of the given type.private RelationalFormula
parseImplication(java.util.List<java.lang.Object> l)
Parses an implication as a list of String tokens or formulas into a fol formula.private RelationalFormula
parseModalization(java.util.List<java.lang.Object> l)
Parses a formula containing at least one modal operator as a list of String tokens or formulas.private RelationalFormula
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 RelationalFormula
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.void
setSignature(FolSignature signature)
Sets the signature for this parser.-
Methods inherited from class net.sf.tweety.commons.Parser
isNumeric, parseBeliefBase, parseBeliefBaseFromFile, parseFormula, parseFormulaFromFile
-
-
-
-
Field Detail
-
folparser
FolParser folparser
First-order logic parser used for parsing sorts and type declaration.
-
-
Method Detail
-
parseBeliefBase
public MlBeliefSet 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<MlBeliefSet,RelationalFormula>
- 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.
-
parseFormula
public RelationalFormula 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<MlBeliefSet,RelationalFormula>
- 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 modal 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 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 RelationalFormula 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.
-
parseModalization
private RelationalFormula parseModalization(java.util.List<java.lang.Object> l) throws ParserException
Parses a formula containing at least one modal operator 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 RelationalFormula 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 RelationalFormula 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 RelationalFormula 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 RelationalFormula 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 RelationalFormula 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 RelationalFormula 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
-
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.
-
-