Package org.smtlib.impl

Class SMTExpr.StringLiteral

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.Pos.AbstractExpr

org.smtlib.impl.SMTExpr.Literal<String>

org.smtlib.impl.SMTExpr.StringLiteral

All Implemented Interfaces:

IAttributeValue, IExpr, IExpr.ILiteral, IExpr.IStringLiteral, INode, IPos.IPosable, IResponse

Enclosing class:

SMTExpr

public static class SMTExpr.StringLiteral
extends SMTExpr.Literal<String>
implements IExpr.IStringLiteral

This class represents an SMT String literal expression or syntax token

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 inherited from class org.smtlib.impl.SMTExpr.Literal

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
StringLiteral(SMT.Configuration smtConfig, String value, boolean quoted)	Creates a string literal.

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)	Equal to any IStringLiteral with the same string value
int	hashCode()

Methods inherited from class org.smtlib.impl.SMTExpr.Literal

isError, value

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

toString, value

Methods inherited from interface org.smtlib.IPos.IPosable

pos, setPos

Constructor Details

StringLiteral

public StringLiteral(SMT.Configuration smtConfig,
 String value,
 boolean quoted)

Creates a string literal. If quoted is true the argument is the raw SMT-LIB text (with enclosing quotes and escape sequences), unescaped per the given Configuration's rules (escaping is version-dependent -- see Utils.unescape); if false it is already the unescaped Java string and smtConfig is unused. Issue #22: this used to read a single static SMTExpr.smtConfig field shared process-wide, so which Configuration's rules applied depended on whichever Configuration was most recently constructed anywhere in the process, not the one actually driving this literal's construction.

Method Details

equals

public boolean equals(Object o)

Equal to any IStringLiteral with the same string value

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