Package org.smtlib.impl

Class SMTExpr.Symbol

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.Pos.AbstractExpr

org.smtlib.impl.SMTExpr.Symbol

All Implemented Interfaces:

IAttributeValue, IExpr, IExpr.IIdentifier, IExpr.IIndex, IExpr.IQualifiedIdentifier, IExpr.ISymbol, INode, IPos.IPosable, IResponse

Enclosing class:

SMTExpr

public static class SMTExpr.Symbol
extends Pos.AbstractExpr
implements IExpr.ISymbol

This class represents an SMT Symbol

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.IError, IResponse.IFactory, IResponse.IPair<T1,T2>, IResponse.IProofResponse, IResponse.IUnsatAssumptionsResponse, IResponse.IUnsatCoreResponse, IResponse.IValueResponse

Field Summary

Fields

Modifier and Type	Field	Description
protected String	originalString
protected String	value

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
Symbol(String v)	The argument is a Symbol string, with or without enclosing bars; a lone or unmatched bar is kept in the value (and reported by the type checker)

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	headSymbol()	The head symbol of the identifier
static boolean	isBarQuoted(String v)	Whether v is enclosed in a pair of bars
boolean	isError()	Returns true if the response is an error response
boolean	isOK()	Returns true if the response is a SUCCESS response
String	toString()	Returns the original String - use for debugging and use a printer to print to concrete syntax.
String	value()	Returns the unique string for this symbol (e.g.

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

setSort, sort

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.IExpr

setSort, sort

Methods inherited from interface org.smtlib.IPos.IPosable

pos, setPos

Field Details

value

protected String value

originalString

protected String originalString

Constructor Details

Symbol

public Symbol(String v)

The argument is a Symbol string, with or without enclosing bars; a lone or unmatched bar is kept in the value (and reported by the type checker)

Method Details

isBarQuoted

public static boolean isBarQuoted(String v)

Whether v is enclosed in a pair of bars

value

public String value()

Returns the unique string for this symbol (e.g. modulo enclosing bars)

Specified by:

value in interface IExpr.ISymbol

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

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

toString

public String toString()

Returns the original String - use for debugging and use a printer to print to concrete syntax.

Specified by:

toString in interface IExpr.ISymbol

Overrides:

toString in class Pos.Printable

isOK

public boolean isOK()

Description copied from interface: IResponse

Returns true if the response is a SUCCESS response

Specified by:

isOK in interface IAttributeValue

Specified by:

isOK in interface IResponse

isError

public boolean isError()

Description copied from interface: IResponse

Returns true if the response is an error response

Specified by:

isError in interface IAttributeValue

Specified by:

isError in interface IExpr

Specified by:

isError in interface IResponse