Package org.smtlib.impl

Class SMTExpr.ParameterizedIdentifier

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.Pos.AbstractExpr

org.smtlib.impl.SMTExpr.ParameterizedIdentifier

All Implemented Interfaces:

IAttributeValue, IExpr, IExpr.IIdentifier, IExpr.IParameterizedIdentifier, IExpr.IQualifiedIdentifier, INode, IPos.IPosable, IResponse

Enclosing class:

SMTExpr

public static class SMTExpr.ParameterizedIdentifier
extends Pos.AbstractExpr
implements IExpr.IParameterizedIdentifier

This class represents an SMT parameterized-identifier AST (e.g. (_ BitVec 32)).

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 IExpr.ISymbol	head
protected List<IExpr.IIndex>	indices

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
ParameterizedIdentifier(IExpr.ISymbol symbol, List<IExpr.IIndex> indices)	Creates a parameterized identifier from the given head symbol and index 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); }
boolean	equals(Object o)
int	hashCode()
IExpr.ISymbol	head()	The head symbol of the identifier
IExpr.ISymbol	headSymbol()	The head symbol of the identifier
List<IExpr.IIndex>	indices()	All indices of the identifier: INumeral or ISymbol, or the literals IIndex describes.

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

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

head

protected IExpr.ISymbol head

indices

protected List<IExpr.IIndex> indices

Constructor Details

ParameterizedIdentifier

public ParameterizedIdentifier(IExpr.ISymbol symbol,
 List<IExpr.IIndex> indices)

Creates a parameterized identifier from the given head symbol and index list.

Method Details

head

public IExpr.ISymbol head()

Description copied from interface: IExpr.IParameterizedIdentifier

The head symbol of the identifier

Specified by:

head in interface IExpr.IParameterizedIdentifier

headSymbol

public IExpr.ISymbol headSymbol()

Description copied from interface: IExpr.IIdentifier

The head symbol of the identifier

Specified by:

headSymbol in interface IExpr.IIdentifier

Specified by:

headSymbol in interface IExpr.IQualifiedIdentifier

indices

public List<IExpr.IIndex> indices()

Description copied from interface: IExpr.IParameterizedIdentifier

All indices of the identifier: INumeral or ISymbol, or the literals IIndex describes. Symbol indices are allowed only in SMT-LIB V2.5 and later.

Specified by:

indices in interface IExpr.IParameterizedIdentifier

equals

public boolean equals(Object o)

Overrides:

equals in class Pos.Posable

hashCode

public int hashCode()

Overrides:

hashCode in class Pos.Posable

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