Package net.sf.tweety.logics.fol.parser
Class TPTPParser
- java.lang.Object
-
- net.sf.tweety.commons.Parser<FolBeliefSet,FolFormula>
-
- net.sf.tweety.logics.fol.parser.TPTPParser
-
public class TPTPParser extends Parser<FolBeliefSet,FolFormula>
This class implements a parser for the TPTP syntax that parses single fol formulas and knowledge bases (TPTP problem files or axiom files). TPTP files consist of any of the following in any order and separated by newlines:- formulas
- comments, i.e. lines starting with "%"
- includes of other TPTP files, i.e. lines like "include('path/to/file',[optional,formula,names])"
- name is the name of the formula
- role is anything out of {axiom, hypothesis, definition, assumption, lemma, theorem, corollary conjecture, negated_conjecture}
- formula is the actual formula
- The other arguments are optional and ignored by this parser.
Negation: ~ formula
Conjunction: formula & formula
Disjunction: formula | formula
Implication: formula => formula
formula <= formula
Equivalence: formula <=> formula
Universal quantifier: ! [Variable1,Variable2,...] : (formula)
Existential quantifier: ? [Variable1,Variable2,...] : (formula)
Tautology: $true
Contradiction: $false
Equality: = (TODO soon to be added)
Inequality: != (TODO soon to be added)- Author:
- Anna Gessler
-
-
Field Summary
Fields Modifier and Type Field Description private java.lang.String
formulaNames
Regular expression that restricts which formulas will be parsed.private java.lang.String
formulaRoles
Regular expression that restricts which formulas will be parsed.private java.lang.String
includePath
Location of included files (optional).private FolSignature
signature
Keeps track of the signature.private java.util.Map<java.lang.String,Variable>
variables
Keeps track of variables defined.
-
Constructor Summary
Constructors Constructor Description TPTPParser()
-
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.private FolFormula
parseAtomic(java.util.List<java.lang.Object> l)
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 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 FolBeliefSet
parseIncludedFiles(java.lang.String s)
Parses formulas of an included TPTP problem file.private FolFormula
parseNegation(java.util.List<java.lang.Object> l)
private FolFormula
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.private void
parseTypes(java.lang.String formula)
Parse signature of a problem file.void
resetFormulaNames()
Reset the regular expression that restricts which formulas will be parsed to the default value, meaning formulas of all names will be parsed.void
resetFormulaRoles()
Reset the regular expression that restricts which formulas will be parsed to the default value, meaning formulas of any TPTP roles will be parsed.void
setFormulaNames(java.lang.String formulaNames)
Set the regular expression that restricts which formulas will be parsed.void
setFormulaRoles(java.lang.String formulaRoles)
Set the regular expression that restricts which formulas will be parsed.void
setIncludePath(java.lang.String includePath)
Set the location of included files.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
-
signature
private FolSignature signature
Keeps track of the signature.
-
variables
private java.util.Map<java.lang.String,Variable> variables
Keeps track of variables defined.
-
includePath
private java.lang.String includePath
Location of included files (optional). This path will be prepended to the path given in the include('included_file') paths.
-
formulaNames
private java.lang.String formulaNames
Regular expression that restricts which formulas will be parsed. Formulas with names that do not match the expression will not be parsed. By default, all formulas are parsed.
-
formulaRoles
private java.lang.String formulaRoles
Regular expression that restricts which formulas will be parsed. Formulas with roles that do not match the expression will not be parsed. By default, all formulas are parsed.
-
-
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.
-
parseIncludedFiles
private FolBeliefSet parseIncludedFiles(java.lang.String s) throws java.io.FileNotFoundException, ParserException, java.io.IOException
Parses formulas of an included TPTP problem file. If the given string contains a list of formula names in addition to the include path, only formulas of the given names will be parsed.- Parameters:
s
- String of format "include('path/to/file')." or "include('path/to/file',[formula,names,separated,by,commata])."- Returns:
- a belief set containing the parsed included formulas
- Throws:
java.io.FileNotFoundException
- if a file could not be foundParserException
- if parsing failsjava.io.IOException
- if there is an IO issue
-
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.
-
parseTypes
private void parseTypes(java.lang.String formula)
Parse signature of a problem file. If some or all of the symbols are already part of the signature, they will not be overwritten.- Parameters:
formula
- a String of a formula
-
consumeToken
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.- 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 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)
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. Reverse implications like 'A <= B' will be parsed as 'B => A'.- 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.- 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)
Parses a 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)
-
parseAtomic
private FolFormula parseAtomic(java.util.List<java.lang.Object> l)
-
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.
-
setFormulaNames
public void setFormulaNames(java.lang.String formulaNames)
Set the regular expression that restricts which formulas will be parsed. Formulas with names that do not match the expression will not be parsed.- Parameters:
formulaNames
- the regex for formula names
-
setFormulaRoles
public void setFormulaRoles(java.lang.String formulaRoles)
Set the regular expression that restricts which formulas will be parsed. Formulas with roles that do not match the expression will not be parsed.- Parameters:
formulaRoles
- the regex for formula roles
-
resetFormulaRoles
public void resetFormulaRoles()
Reset the regular expression that restricts which formulas will be parsed to the default value, meaning formulas of any TPTP roles will be parsed. Possible TPTP roles are axiom, hypothesis, definition, assumption, lemma, theorem, corollary, conjecture and negated_conjecture.
-
resetFormulaNames
public void resetFormulaNames()
Reset the regular expression that restricts which formulas will be parsed to the default value, meaning formulas of all names will be parsed.
-
setIncludePath
public void setIncludePath(java.lang.String includePath)
Set the location of included files.- Parameters:
includePath
- path that will be prepended to the paths of all included problem files.
-
-