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 net.sf.tweety.commons.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

Constructor Summary

Constructors

Constructor and Description
FolParser() Creates a new FolParser
FolParser(boolean ignoreUndeclaredConstants) Creates a new FolParser

Method Summary

Modifier and Type	Method and Description
FolSignature	getSignature() Returns the signature of this parser.
Map<String,net.sf.tweety.logics.commons.syntax.Variable>	getVariables()
FolBeliefSet	parseBeliefBase(Reader reader)
FolFormula	parseFormula(Reader reader)
FolSignature	parseSignature(String s) 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,net.sf.tweety.logics.commons.syntax.Variable> variables)

Methods inherited from class net.sf.tweety.commons.Parser

isNumeric, parseBeliefBase, parseBeliefBaseFromFile, parseFormula, parseFormulaFromFile

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

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(Reader reader)
                             throws IOException,
                                    net.sf.tweety.commons.ParserException

Specified by:

parseBeliefBase in class net.sf.tweety.commons.Parser<FolBeliefSet,FolFormula>

Throws:

IOException

net.sf.tweety.commons.ParserException

parseSortDeclaration

public void parseSortDeclaration(String s,
                                 FolSignature sig)
                          throws net.sf.tweety.commons.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:

net.sf.tweety.commons.ParserException

parseTypeDeclaration

public void parseTypeDeclaration(String s,
                                 FolSignature sig)
                          throws net.sf.tweety.commons.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:

net.sf.tweety.commons.ParserException

parseFormula

public FolFormula parseFormula(Reader reader)
                        throws IOException,
                               net.sf.tweety.commons.ParserException

Specified by:

parseFormula in class net.sf.tweety.commons.Parser<FolBeliefSet,FolFormula>

Throws:

IOException

net.sf.tweety.commons.ParserException

parseSignature

public FolSignature parseSignature(String s)

This function parses only the sorts declaration and type declaration parts of a belief base.

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,net.sf.tweety.logics.commons.syntax.Variable> getVariables()

setVariables

public void setVariables(Map<String,net.sf.tweety.logics.commons.syntax.Variable> variables)