Package org.smtlib.impl

Class SMTExpr.FcnExpr

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.Pos.AbstractExpr

org.smtlib.impl.SMTExpr.FcnExpr

All Implemented Interfaces:

IAttributeValue, IExpr, IExpr.IFcnExpr, INode, IPos.IPosable, IResponse

Enclosing class:

SMTExpr

public static class SMTExpr.FcnExpr
extends Pos.AbstractExpr
implements IExpr.IFcnExpr

Represents a function-application expression: a qualified identifier applied to a list of argument expressions.

Nested Class Summary

Nested classes/interfaces inherited from interface org.smtlib.IExpr

IExpr.IAsIdentifier, IExpr.IAttribute<TT extends IAttributeValue>, IExpr.IAttributedExpr, IExpr.IBinaryLiteral, IExpr.IBinding, IExpr.IConstructor, IExpr.IDecimal, IExpr.IDeclaration, IExpr.IError, IExpr.IExists, IExpr.IFactory, IExpr.IFcnExpr, IExpr.IForall, IExpr.IFunctionDeclaration, IExpr.IHexLiteral, IExpr.IIdentifier, IExpr.IIndex, IExpr.IKeyword, IExpr.ILambda, IExpr.ILet, IExpr.ILiteral, IExpr.IMatch, IExpr.IMatchCase, IExpr.INumeral, IExpr.IParameterizedIdentifier, IExpr.IPattern, IExpr.IPatternTerms, IExpr.IQualifiedIdentifier, IExpr.ISelector, IExpr.ISortDeclaration, IExpr.IStringLiteral, IExpr.ISymbol

Nested classes/interfaces inherited from interface org.smtlib.IResponse

IResponse.IAssertionsResponse, IResponse.IAssignmentResponse, IResponse.IAttributeList, IResponse.IPair<T1,T2>, IResponse.IProofResponse, IResponse.IUnsatAssumptionsResponse, IResponse.IUnsatCoreResponse, IResponse.IValueResponse

Field Summary

Fields

Modifier and Type	Field	Description
protected List<IExpr>	args
protected IExpr.IQualifiedIdentifier	id

Fields inherited from class org.smtlib.impl.Pos.AbstractExpr

sort

Fields inherited from class org.smtlib.impl.Pos.Posable

pos

Constructor Summary

Constructors

Constructor	Description
FcnExpr(IExpr.IQualifiedIdentifier id, List<IExpr> args)	Creates a function application from the given identifier and argument list.

Method Summary

Modifier and Type	Method	Description
<T> T	accept(IVisitor<T> v)	The accept method corresponding to IVisitor, to be implemented in each subclass as { return v.visit(this); }
List<IExpr>	args()	The arguments of the function
IExpr.IQualifiedIdentifier	head()	The function identifier

Methods inherited from class org.smtlib.impl.Pos.AbstractExpr

setSort, sort

Methods inherited from class org.smtlib.impl.Pos.Printable

toString

Methods inherited from class org.smtlib.impl.Pos.Posable

equals, hashCode, pos, setPos

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface org.smtlib.IAttributeValue

isOK

Methods inherited from interface org.smtlib.IExpr

isError, setSort, sort

Methods inherited from interface org.smtlib.IPos.IPosable

pos, setPos

Field Details

id

protected IExpr.IQualifiedIdentifier id

args

protected List<IExpr> args

Constructor Details

FcnExpr

public FcnExpr(IExpr.IQualifiedIdentifier id,
 List<IExpr> args)

Creates a function application from the given identifier and argument list.

Method Details

head

public IExpr.IQualifiedIdentifier head()

Description copied from interface: IExpr.IFcnExpr

The function identifier

Specified by:

head in interface IExpr.IFcnExpr

args

public List<IExpr> args()

Description copied from interface: IExpr.IFcnExpr

The arguments of the function

Specified by:

args in interface IExpr.IFcnExpr

accept

public <T> T accept(IVisitor<T> v)
             throws IVisitor.VisitorException

Description copied from interface: INode

The accept method corresponding to IVisitor, to be implemented in each subclass as { return v.visit(this); }

Specified by:

accept in interface INode

Type Parameters:

T - the return type desired from the visit methods

Parameters:

v - the visitor class

Returns:

the value returned by the visit method

Throws:

IVisitor.VisitorException