public class TPTPParser extends net.sf.tweety.commons.Parser<FolBeliefSet,FolFormula>
TPTP files consist of any of the following in any order and separated by newlines:
The syntax for first-order logic formulas is 'fof(name,role,formula,source,[useful_info]).':
Supported operators and pre-defined predicates in formulas:
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)
| Constructor and Description |
|---|
TPTPParser() |
| Modifier and Type | Method and Description |
|---|---|
FolSignature |
getSignature()
Returns the signature of this parser.
|
FolBeliefSet |
parseBeliefBase(Reader reader) |
FolFormula |
parseFormula(Reader reader) |
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(String formulaNames)
Set the regular expression that restricts which formulas will be parsed.
|
void |
setFormulaRoles(String formulaRoles)
Set the regular expression that restricts which formulas will be parsed.
|
void |
setIncludePath(String includePath)
Set the location of included files.
|
void |
setSignature(FolSignature signature)
Sets the signature for this parser.
|
public FolBeliefSet parseBeliefBase(Reader reader) throws IOException, net.sf.tweety.commons.ParserException
parseBeliefBase in class net.sf.tweety.commons.Parser<FolBeliefSet,FolFormula>IOExceptionnet.sf.tweety.commons.ParserExceptionpublic FolFormula parseFormula(Reader reader) throws IOException, net.sf.tweety.commons.ParserException
parseFormula in class net.sf.tweety.commons.Parser<FolBeliefSet,FolFormula>IOExceptionnet.sf.tweety.commons.ParserExceptionpublic void setSignature(FolSignature signature)
signature - a fol signature.public FolSignature getSignature()
public void setFormulaNames(String formulaNames)
public void setFormulaRoles(String formulaRoles)
public void resetFormulaRoles()
public void resetFormulaNames()
public void setIncludePath(String includePath)
path - that will be prepended to the paths of all included problem files.Copyright © 2019. All rights reserved.