Package org.smtlib.impl

Class SMTExpr.BinaryLiteral

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

All Implemented Interfaces:

IAttributeValue, IExpr, IExpr.IBinaryLiteral, IExpr.IIndex, IExpr.ILiteral, INode, IPos.IPosable, IResponse

Enclosing class:

SMTExpr

public static class SMTExpr.BinaryLiteral
extends SMTExpr.Literal<String>
implements IExpr.IBinaryLiteral

Represents an SMT-LIB binary literal (e.g. #b1010); the value string contains only 0 and 1 digits.

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 BigInteger	intValue
protected int	length

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
BinaryLiteral(String unquotedValue)	Creates a binary literal from a string of 0 and 1 digits (no #b prefix).

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()
BigInteger	intValue()	The binary value as an unsigned integer
int	length()	Number of binary bits

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

value

Methods inherited from interface org.smtlib.IPos.IPosable

pos, setPos

Field Details

length

protected int length

intValue

protected BigInteger intValue

Constructor Details

BinaryLiteral

public BinaryLiteral(String unquotedValue)

Creates a binary literal from a string of 0 and 1 digits (no #b prefix).

Method Details

intValue

public BigInteger intValue()

Description copied from interface: IExpr.IBinaryLiteral

The binary value as an unsigned integer

Specified by:

intValue in interface IExpr.IBinaryLiteral

length

public int length()

Description copied from interface: IExpr.IBinaryLiteral

Number of binary bits

Specified by:

length in interface IExpr.IBinaryLiteral

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