tptp_parser

Class SimpleTptpParserOutput

java.lang.Object

tptp_parser.SimpleTptpParserOutput

All Implemented Interfaces:

TptpParserOutput

public class SimpleTptpParserOutput
extends Object
implements TptpParserOutput

A simple implementation of the interface TptpParserOutput. This implementation is likely to be sufficient for all simple uses of the parser.

Since:

Feb 02, 2006, Apr 06, 2006, Nov 13, 2007 ("package tptp_parser" added by AR)

Author:

Alexandre Riazanov, Andrei Tchaltsev

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	SimpleTptpParserOutput.AnnotatedClause Represents instances of <cnf annotated> in the BNF grammar.
static class	SimpleTptpParserOutput.AnnotatedFormula Represents instances of <fof annotated> in the BNF grammar.
static class	SimpleTptpParserOutput.AnnotatedThfFormula Represents instances of <thf annotated> in the BNF grammar.
static class	SimpleTptpParserOutput.Annotations
static class	SimpleTptpParserOutput.Clause
static class	SimpleTptpParserOutput.Formula
static class	SimpleTptpParserOutput.GeneralTerm
static class	SimpleTptpParserOutput.IncludeDirective Represents instances of <include> in the BNF grammar.
static class	SimpleTptpParserOutput.InfoItem
static class	SimpleTptpParserOutput.Literal
static class	SimpleTptpParserOutput.ParentInfo
static class	SimpleTptpParserOutput.Source
static class	SimpleTptpParserOutput.Symbol
static class	SimpleTptpParserOutput.Term
static class	SimpleTptpParserOutput.ThfFormula
static class	SimpleTptpParserOutput.TopLevelItem A common base for the classes AnnotatedFormula, AnnotatedClause and IncludeDirective.

Nested classes/interfaces inherited from interface tptp_parser.TptpParserOutput

TptpParserOutput.AtomicFormula, TptpParserOutput.BinaryConnective, TptpParserOutput.CnfFormula, TptpParserOutput.FofFormula, TptpParserOutput.FormulaRole, TptpParserOutput.IntroType, TptpParserOutput.Quantifier, TptpParserOutput.StatusValue, TptpParserOutput.ThfAtomicFormula, TptpParserOutput.TptpInput, TptpParserOutput.UnaryConnective

Constructor Summary

Constructors

Constructor and Description
SimpleTptpParserOutput()

Method Summary

Modifier and Type	Method and Description
TptpParserOutput.FofFormula	atomAsFormula(TptpParserOutput.AtomicFormula atom) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.ThfFormula	atomAsThfFormula(TptpParserOutput.ThfAtomicFormula atom) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.AtomicFormula	builtInFalse() Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.ThfFormula	builtInThfFalse() Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.ThfFormula	builtInThfTrue() Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.AtomicFormula	builtInTrue() Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.Annotations	createAnnotations(TptpParserOutput.Source source, Iterable<TptpParserOutput.InfoItem> usefulInfo) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.InfoItem	createAssumptionRecordInfoItem(Iterable<String> nameList) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.FofFormula	createBinaryFormula(TptpParserOutput.FofFormula lhs, TptpParserOutput.BinaryConnective connective, TptpParserOutput.FofFormula rhs) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.CnfFormula	createClause(Iterable<TptpParserOutput.Literal> literals) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.TptpInput	createCnfAnnotated(String name, TptpParserOutput.FormulaRole role, TptpParserOutput.CnfFormula clause, TptpParserOutput.Annotations annotations, int lineNumber) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.InfoItem	createDescriptionInfoItem(String singleQuoted) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.AtomicFormula	createEqualityAtom(TptpParserOutput.Term lhs, TptpParserOutput.Term rhs) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.TptpInput	createFofAnnotated(String name, TptpParserOutput.FormulaRole role, TptpParserOutput.FofFormula formula, TptpParserOutput.Annotations annotations, int lineNumber) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.GeneralTerm	createGeneralCnfFormula(TptpParserOutput.CnfFormula formula) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.GeneralTerm	createGeneralColon(TptpParserOutput.GeneralTerm left, TptpParserOutput.GeneralTerm right) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.GeneralTerm	createGeneralDistinctObject(String str) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.GeneralTerm	createGeneralFofFormula(TptpParserOutput.FofFormula formula) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.GeneralTerm	createGeneralFunction(String function, Iterable<TptpParserOutput.GeneralTerm> arguments) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.InfoItem	createGeneralFunctionInfoItem(TptpParserOutput.GeneralTerm generalFunction) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.GeneralTerm	createGeneralList(Iterable<TptpParserOutput.GeneralTerm> list) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.GeneralTerm	createGeneralTerm(TptpParserOutput.Term term) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.GeneralTerm	createGeneralThfFormula(TptpParserOutput.ThfFormula formula) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.GeneralTerm	createGeneralVariable(String var) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.TptpInput	createIncludeDirective(String fileName, Iterable<String> formulaSelection, int lineNumber) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.InfoItem	createInferenceRuleInfoItem(String inferenceRule, String inferenceId, Iterable<TptpParserOutput.GeneralTerm> attributes) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.InfoItem	createInferenceStatusInfoItem(TptpParserOutput.StatusValue statusValue) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.Source	createInternalSource(String introType, Iterable<TptpParserOutput.InfoItem> introInfo) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.InfoItem	createIQuoteInfoItem(String singleQuoted) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.Literal	createLiteral(boolean positive, TptpParserOutput.AtomicFormula atom) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.FofFormula	createNegationOf(TptpParserOutput.FofFormula formula) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.ParentInfo	createParentInfo(TptpParserOutput.Source source, TptpParserOutput.GeneralTerm parentDetails) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.AtomicFormula	createPlainAtom(String predicate, Iterable<TptpParserOutput.Term> arguments) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.Term	createPlainTerm(String function, Iterable<TptpParserOutput.Term> arguments) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.FofFormula	createQuantifiedFormula(TptpParserOutput.Quantifier quantifier, Iterable<String> variableList, TptpParserOutput.FofFormula formula) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.InfoItem	createRefutationInfoItem(TptpParserOutput.Source fileSource) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.Source	createSourceFromCreator(String creatorName, Iterable<TptpParserOutput.InfoItem> usefulInfo) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.Source	createSourceFromFile(String fileName, String fileInfo) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.Source	createSourceFromInferenceRecord(String inferenceRule, Iterable<TptpParserOutput.InfoItem> usefulInfo, Iterable<TptpParserOutput.ParentInfo> parentInfoList) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.Source	createSourceFromListOfSources(Iterable<TptpParserOutput.Source> listOfSources) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.Source	createSourceFromName(String name) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.Source	createSourceFromTheory(String theoryName, Iterable<TptpParserOutput.InfoItem> usefulInfo) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.AtomicFormula	createSystemAtom(String predicate, Iterable<TptpParserOutput.Term> arguments) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.Term	createSystemTerm(String function, Iterable<TptpParserOutput.Term> arguments) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.TptpInput	createThfAnnotated(String name, TptpParserOutput.FormulaRole role, TptpParserOutput.ThfFormula formula, TptpParserOutput.Annotations annotations, int lineNumber) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.ThfFormula	createThfBinaryFormula(TptpParserOutput.ThfFormula lhs, TptpParserOutput.BinaryConnective connective, TptpParserOutput.ThfFormula rhs) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.ThfFormula	createThfPlainAtom(String predicate, Iterable<TptpParserOutput.Term> arguments) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.ThfFormula	createThfQuantifiedFormula(TptpParserOutput.Quantifier quantifier, Iterable<TptpParserOutput.ThfFormula> variableList, TptpParserOutput.ThfFormula formula) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.ThfFormula	createThfSystemAtom(String predicate, Iterable<TptpParserOutput.Term> arguments) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.ThfFormula	createThfUnaryOf(TptpParserOutput.UnaryConnective unary, TptpParserOutput.ThfFormula formula) Implements the corresponding spec in TptpParserOutput.
TptpParserOutput.ThfFormula	createThfVariableAtom(String variable)
TptpParserOutput.Term	createVariableTerm(String variable) Implements the corresponding spec in TptpParserOutput.
void	reset() Reinitialises everything.

Methods inherited from class java.lang.Object

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

Constructor Detail

SimpleTptpParserOutput

public SimpleTptpParserOutput()

Method Detail

createThfAnnotated

public TptpParserOutput.TptpInput createThfAnnotated(String name,
                                                     TptpParserOutput.FormulaRole role,
                                                     TptpParserOutput.ThfFormula formula,
                                                     TptpParserOutput.Annotations annotations,
                                                     int lineNumber)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createThfAnnotated in interface TptpParserOutput

Parameters:

name - != null

role - != null

formula - != null

annotations - can be null

lineNumber - location in the input

createFofAnnotated

public TptpParserOutput.TptpInput createFofAnnotated(String name,
                                                     TptpParserOutput.FormulaRole role,
                                                     TptpParserOutput.FofFormula formula,
                                                     TptpParserOutput.Annotations annotations,
                                                     int lineNumber)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createFofAnnotated in interface TptpParserOutput

Parameters:

name - != null

role - != null

formula - != null

annotations - can be null

lineNumber - location in the input

createCnfAnnotated

public TptpParserOutput.TptpInput createCnfAnnotated(String name,
                                                     TptpParserOutput.FormulaRole role,
                                                     TptpParserOutput.CnfFormula clause,
                                                     TptpParserOutput.Annotations annotations,
                                                     int lineNumber)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createCnfAnnotated in interface TptpParserOutput

Parameters:

name - != null

role - != null

clause - != null

annotations - can be null

lineNumber - location in the input

createIncludeDirective

public TptpParserOutput.TptpInput createIncludeDirective(String fileName,
                                                         Iterable<String> formulaSelection,
                                                         int lineNumber)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createIncludeDirective in interface TptpParserOutput

Parameters:

fileName - != null

formulaSelection - satisfies (formulaSelection == null || formulaSelection.iterator().hasNext())

lineNumber - location in the input

createThfBinaryFormula

public TptpParserOutput.ThfFormula createThfBinaryFormula(TptpParserOutput.ThfFormula lhs,
                                                          TptpParserOutput.BinaryConnective connective,
                                                          TptpParserOutput.ThfFormula rhs)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createThfBinaryFormula in interface TptpParserOutput

Parameters:

lhs - != null

connective - != null

rhs - != null

createThfUnaryOf

public TptpParserOutput.ThfFormula createThfUnaryOf(TptpParserOutput.UnaryConnective unary,
                                                    TptpParserOutput.ThfFormula formula)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createThfUnaryOf in interface TptpParserOutput

formula - != null

createThfQuantifiedFormula

public TptpParserOutput.ThfFormula createThfQuantifiedFormula(TptpParserOutput.Quantifier quantifier,
                                                              Iterable<TptpParserOutput.ThfFormula> variableList,
                                                              TptpParserOutput.ThfFormula formula)

Implements the corresponding spec in TptpParserOutput. For this implementation the list of variables is expected to be reversed

Specified by:

createThfQuantifiedFormula in interface TptpParserOutput

Parameters:

quantifier - != null

variableList - != null && variableList.iterator().hasNext()

formula - != null

atomAsThfFormula

public TptpParserOutput.ThfFormula atomAsThfFormula(TptpParserOutput.ThfAtomicFormula atom)

Implements the corresponding spec in TptpParserOutput.

Specified by:

atomAsThfFormula in interface TptpParserOutput

Parameters:

atom - != null

createThfPlainAtom

public TptpParserOutput.ThfFormula createThfPlainAtom(String predicate,
                                                      Iterable<TptpParserOutput.Term> arguments)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createThfPlainAtom in interface TptpParserOutput

createThfSystemAtom

public TptpParserOutput.ThfFormula createThfSystemAtom(String predicate,
                                                       Iterable<TptpParserOutput.Term> arguments)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createThfSystemAtom in interface TptpParserOutput

builtInThfTrue

public TptpParserOutput.ThfFormula builtInThfTrue()

Implements the corresponding spec in TptpParserOutput.

Specified by:

builtInThfTrue in interface TptpParserOutput

builtInThfFalse

public TptpParserOutput.ThfFormula builtInThfFalse()

Implements the corresponding spec in TptpParserOutput.

Specified by:

builtInThfFalse in interface TptpParserOutput

createThfVariableAtom

public TptpParserOutput.ThfFormula createThfVariableAtom(String variable)

Specified by:

createThfVariableAtom in interface TptpParserOutput

createBinaryFormula

public TptpParserOutput.FofFormula createBinaryFormula(TptpParserOutput.FofFormula lhs,
                                                       TptpParserOutput.BinaryConnective connective,
                                                       TptpParserOutput.FofFormula rhs)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createBinaryFormula in interface TptpParserOutput

Parameters:

lhs - != null

connective - != null

rhs - != null

createNegationOf

public TptpParserOutput.FofFormula createNegationOf(TptpParserOutput.FofFormula formula)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createNegationOf in interface TptpParserOutput

Parameters:

formula - != null

createQuantifiedFormula

public TptpParserOutput.FofFormula createQuantifiedFormula(TptpParserOutput.Quantifier quantifier,
                                                           Iterable<String> variableList,
                                                           TptpParserOutput.FofFormula formula)

Implements the corresponding spec in TptpParserOutput. For this implementation the list of variables is expected to be reversed

Specified by:

createQuantifiedFormula in interface TptpParserOutput

Parameters:

quantifier - != null

variableList - != null && variableList.iterator().hasNext()

formula - != null

createClause

public TptpParserOutput.CnfFormula createClause(Iterable<TptpParserOutput.Literal> literals)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createClause in interface TptpParserOutput

Parameters:

literals - satisfies (literals == null || literals.iterator().hasNext())

atomAsFormula

public TptpParserOutput.FofFormula atomAsFormula(TptpParserOutput.AtomicFormula atom)

Implements the corresponding spec in TptpParserOutput.

Specified by:

atomAsFormula in interface TptpParserOutput

Parameters:

atom - != null

createLiteral

public TptpParserOutput.Literal createLiteral(boolean positive,
                                              TptpParserOutput.AtomicFormula atom)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createLiteral in interface TptpParserOutput

Parameters:

positive - == true iff the literal has to be positive

atom - != null

createPlainAtom

public TptpParserOutput.AtomicFormula createPlainAtom(String predicate,
                                                      Iterable<TptpParserOutput.Term> arguments)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createPlainAtom in interface TptpParserOutput

Parameters:

predicate - != null

arguments - satisfies (arguments == null || arguments.iterator().hasNext())

createSystemAtom

public TptpParserOutput.AtomicFormula createSystemAtom(String predicate,
                                                       Iterable<TptpParserOutput.Term> arguments)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createSystemAtom in interface TptpParserOutput

Parameters:

predicate - != null

arguments - satisfies (arguments == null || arguments.iterator().hasNext())

createEqualityAtom

public TptpParserOutput.AtomicFormula createEqualityAtom(TptpParserOutput.Term lhs,
                                                         TptpParserOutput.Term rhs)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createEqualityAtom in interface TptpParserOutput

builtInTrue

public TptpParserOutput.AtomicFormula builtInTrue()

Implements the corresponding spec in TptpParserOutput.

Specified by:

builtInTrue in interface TptpParserOutput

builtInFalse

public TptpParserOutput.AtomicFormula builtInFalse()

Implements the corresponding spec in TptpParserOutput.

Specified by:

builtInFalse in interface TptpParserOutput

createVariableTerm

public TptpParserOutput.Term createVariableTerm(String variable)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createVariableTerm in interface TptpParserOutput

Parameters:

variable - != null

createPlainTerm

public TptpParserOutput.Term createPlainTerm(String function,
                                             Iterable<TptpParserOutput.Term> arguments)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createPlainTerm in interface TptpParserOutput

Parameters:

function - != null

arguments - satisfies (arguments == null || arguments.iterator().hasNext())

createSystemTerm

public TptpParserOutput.Term createSystemTerm(String function,
                                              Iterable<TptpParserOutput.Term> arguments)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createSystemTerm in interface TptpParserOutput

Parameters:

function - != null

arguments - satisfies (arguments == null || arguments.iterator().hasNext())

createAnnotations

public TptpParserOutput.Annotations createAnnotations(TptpParserOutput.Source source,
                                                      Iterable<TptpParserOutput.InfoItem> usefulInfo)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createAnnotations in interface TptpParserOutput

Parameters:

source - != null

usefulInfo - satisfies (usefulInfo == null || usefulInfo.iterator().hasNext())

createSourceFromName

public TptpParserOutput.Source createSourceFromName(String name)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createSourceFromName in interface TptpParserOutput

Parameters:

name - != null

createSourceFromListOfSources

public TptpParserOutput.Source createSourceFromListOfSources(Iterable<TptpParserOutput.Source> listOfSources)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createSourceFromListOfSources in interface TptpParserOutput

Parameters:

listOfSources - nonempty

createSourceFromInferenceRecord

public TptpParserOutput.Source createSourceFromInferenceRecord(String inferenceRule,
                                                               Iterable<TptpParserOutput.InfoItem> usefulInfo,
                                                               Iterable<TptpParserOutput.ParentInfo> parentInfoList)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createSourceFromInferenceRecord in interface TptpParserOutput

Parameters:

inferenceRule - != null

usefulInfo - satisfies (usefulInfo == null || usefulInfo.iterator().hasNext())

parentInfoList - nonempty

createInternalSource

public TptpParserOutput.Source createInternalSource(String introType,
                                                    Iterable<TptpParserOutput.InfoItem> introInfo)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createInternalSource in interface TptpParserOutput

Parameters:

introType - != null

introInfo - satisfies (usefulInfo == null || usefulInfo.iterator().hasNext())

createSourceFromFile

public TptpParserOutput.Source createSourceFromFile(String fileName,
                                                    String fileInfo)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createSourceFromFile in interface TptpParserOutput

Parameters:

fileName - != null

fileInfo - (may be null)

createSourceFromCreator

public TptpParserOutput.Source createSourceFromCreator(String creatorName,
                                                       Iterable<TptpParserOutput.InfoItem> usefulInfo)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createSourceFromCreator in interface TptpParserOutput

Parameters:

creatorName - != null

usefulInfo - satisfies (usefulInfo == null || usefulInfo.iterator().hasNext())

createSourceFromTheory

public TptpParserOutput.Source createSourceFromTheory(String theoryName,
                                                      Iterable<TptpParserOutput.InfoItem> usefulInfo)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createSourceFromTheory in interface TptpParserOutput

Parameters:

theoryName - != null

usefulInfo - satisfies (usefulInfo == null || usefulInfo.iterator().hasNext())

createDescriptionInfoItem

public TptpParserOutput.InfoItem createDescriptionInfoItem(String singleQuoted)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createDescriptionInfoItem in interface TptpParserOutput

Parameters:

singleQuoted - != null

createIQuoteInfoItem

public TptpParserOutput.InfoItem createIQuoteInfoItem(String singleQuoted)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createIQuoteInfoItem in interface TptpParserOutput

Parameters:

singleQuoted - != null

createInferenceStatusInfoItem

public TptpParserOutput.InfoItem createInferenceStatusInfoItem(TptpParserOutput.StatusValue statusValue)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createInferenceStatusInfoItem in interface TptpParserOutput

Parameters:

statusValue - != null

createInferenceRuleInfoItem

public TptpParserOutput.InfoItem createInferenceRuleInfoItem(String inferenceRule,
                                                             String inferenceId,
                                                             Iterable<TptpParserOutput.GeneralTerm> attributes)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createInferenceRuleInfoItem in interface TptpParserOutput

Parameters:

inferenceRule - != null

inferenceId - != null

attributes - satisfies (attributes == null || attributes.iterator().hasNext())

createAssumptionRecordInfoItem

public TptpParserOutput.InfoItem createAssumptionRecordInfoItem(Iterable<String> nameList)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createAssumptionRecordInfoItem in interface TptpParserOutput

Parameters:

nameList - != null

createRefutationInfoItem

public TptpParserOutput.InfoItem createRefutationInfoItem(TptpParserOutput.Source fileSource)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createRefutationInfoItem in interface TptpParserOutput

Parameters:

fileSource - returned by a call to createSourceFromFile(..)

createGeneralFunctionInfoItem

public TptpParserOutput.InfoItem createGeneralFunctionInfoItem(TptpParserOutput.GeneralTerm generalFunction)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createGeneralFunctionInfoItem in interface TptpParserOutput

Parameters:

generalFunction - returned by a call to createGeneralFunction(..)

createGeneralFunction

public TptpParserOutput.GeneralTerm createGeneralFunction(String function,
                                                          Iterable<TptpParserOutput.GeneralTerm> arguments)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createGeneralFunction in interface TptpParserOutput

Parameters:

function - != null

arguments - satisfies (arguments == null || arguments.iterator().hasNext())

createGeneralList

public TptpParserOutput.GeneralTerm createGeneralList(Iterable<TptpParserOutput.GeneralTerm> list)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createGeneralList in interface TptpParserOutput

Parameters:

list - satisfies (list == null || list.iterator().hasNext())

createGeneralColon

public TptpParserOutput.GeneralTerm createGeneralColon(TptpParserOutput.GeneralTerm left,
                                                       TptpParserOutput.GeneralTerm right)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createGeneralColon in interface TptpParserOutput

Parameters:

left - should not be a general term presenting a list

createGeneralDistinctObject

public TptpParserOutput.GeneralTerm createGeneralDistinctObject(String str)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createGeneralDistinctObject in interface TptpParserOutput

createGeneralVariable

public TptpParserOutput.GeneralTerm createGeneralVariable(String var)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createGeneralVariable in interface TptpParserOutput

createGeneralThfFormula

public TptpParserOutput.GeneralTerm createGeneralThfFormula(TptpParserOutput.ThfFormula formula)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createGeneralThfFormula in interface TptpParserOutput

createGeneralFofFormula

public TptpParserOutput.GeneralTerm createGeneralFofFormula(TptpParserOutput.FofFormula formula)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createGeneralFofFormula in interface TptpParserOutput

createGeneralCnfFormula

public TptpParserOutput.GeneralTerm createGeneralCnfFormula(TptpParserOutput.CnfFormula formula)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createGeneralCnfFormula in interface TptpParserOutput

createGeneralTerm

public TptpParserOutput.GeneralTerm createGeneralTerm(TptpParserOutput.Term term)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createGeneralTerm in interface TptpParserOutput

createParentInfo

public TptpParserOutput.ParentInfo createParentInfo(TptpParserOutput.Source source,
                                                    TptpParserOutput.GeneralTerm parentDetails)

Implements the corresponding spec in TptpParserOutput.

Specified by:

createParentInfo in interface TptpParserOutput

Parameters:

source - != null

parentDetails - if nonnull, corresponds to <single quoted> in the -<single quoted> option in the BNF rule for <parent details> when parentDetails = null, it corresponds to the <null> option in that rule

reset

public void reset()

Reinitialises everything. Note that after a call to reset() objects created by various method calls prior to that call to reset(), are considered invalid and should not be used in any way.