wyil.lang

Class Bytecode.Quantifier

java.lang.Object

wyil.util.AbstractBytecode

wyil.lang.Bytecode.Quantifier

All Implemented Interfaces:

Bytecode, Bytecode.Expr

Enclosing interface:

Bytecode

public static final class Bytecode.Quantifier
extends AbstractBytecode
implements Bytecode.Expr

A quantifier bytecode has the following layout:

 +--------+-----------+---------+-----+---------+
 | opcode | condition | range[] | ... | range[] |
 +--------+-----------+---------+-----+---------+
 

Here, the condition operand identifies an expression which the quantifier is asserting over the given ranges. The ranges themselves identifier one or more operand groups, each of which holds three entries: the declared variable, the start operand, the end operand.

Nested Class Summary

Nested classes/interfaces inherited from interface wyil.lang.Bytecode

Bytecode.AliasDeclaration, Bytecode.Assert, Bytecode.AssertOrAssume, Bytecode.Assign, Bytecode.Assume, Bytecode.Block, Bytecode.Blocks, Bytecode.Break, Bytecode.Case, Bytecode.Const, Bytecode.Continue, Bytecode.Convert, Bytecode.Debug, Bytecode.DoWhile, Bytecode.Expr, Bytecode.Extras, Bytecode.Fail, Bytecode.FieldLoad, Bytecode.If, Bytecode.Index, Bytecode.IndirectInvoke, Bytecode.Invoke, Bytecode.Lambda, Bytecode.Loop, Bytecode.NamedBlock, Bytecode.OperandGroups, Bytecode.Operands, Bytecode.Operator, Bytecode.OperatorKind, Bytecode.Quantifier, Bytecode.QuantifierKind, Bytecode.Range, Bytecode.Return, Bytecode.Schema, Bytecode.Skip, Bytecode.Stmt, Bytecode.StmtExpr, Bytecode.Switch, Bytecode.Util, Bytecode.VariableAccess, Bytecode.VariableDeclaration, Bytecode.While

Field Summary

Fields inherited from class wyil.util.AbstractBytecode

schemas

Fields inherited from interface wyil.lang.Bytecode

BINARY_ASSIGNABLE, BINARY_OPERATOR, NARY_ASSIGNABLE, OPCODE_add, OPCODE_aliasdecl, OPCODE_all, OPCODE_array, OPCODE_arraygen, OPCODE_arrayindex, OPCODE_arraylength, OPCODE_assert, OPCODE_assign, OPCODE_assume, OPCODE_bitwiseand, OPCODE_bitwiseinvert, OPCODE_bitwiseor, OPCODE_bitwisexor, OPCODE_block, OPCODE_break, OPCODE_const, OPCODE_continue, OPCODE_convert, OPCODE_debug, OPCODE_dereference, OPCODE_div, OPCODE_dowhile, OPCODE_eq, OPCODE_fail, OPCODE_fieldload, OPCODE_ge, OPCODE_gt, OPCODE_if, OPCODE_ifelse, OPCODE_ifis, OPCODE_indirectinvoke, OPCODE_invoke, OPCODE_is, OPCODE_lambda, OPCODE_le, OPCODE_logicaland, OPCODE_logicalnot, OPCODE_logicalor, OPCODE_lt, OPCODE_mul, OPCODE_namedblock, OPCODE_ne, OPCODE_neg, OPCODE_newobject, OPCODE_record, OPCODE_rem, OPCODE_return, OPCODE_shl, OPCODE_shr, OPCODE_skip, OPCODE_some, OPCODE_sub, OPCODE_switch, OPCODE_varcopy, OPCODE_vardecl, OPCODE_vardeclinit, OPCODE_varmove, OPCODE_while, UNARY_ASSIGNABLE, UNARY_OPERATOR

Constructor Summary

Constructors

Constructor and Description
Quantifier(Bytecode.QuantifierKind kind, int operand, Bytecode.Range... ranges)

Method Summary

Modifier and Type	Method and Description
int	body()
int	getOpcode() Return the opcode value of this bytecode.
Bytecode.QuantifierKind	kind()
Bytecode.Range[]	ranges()
String	toString()

Methods inherited from class wyil.util.AbstractBytecode

equals, getBlock, getBlocks, getOperand, getOperandGroup, getOperands, hashCode, numberOfBlocks, numberOfOperandGroups, numberOfOperands

Methods inherited from class java.lang.Object

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

Methods inherited from interface wyil.lang.Bytecode

getOperand, getOperandGroup, getOperands, numberOfOperandGroups, numberOfOperands

Constructor Detail

Quantifier

public Quantifier(Bytecode.QuantifierKind kind,
                  int operand,
                  Bytecode.Range... ranges)

Method Detail

kind

public Bytecode.QuantifierKind kind()

getOpcode

public int getOpcode()

Description copied from class: AbstractBytecode

Return the opcode value of this bytecode.

Specified by:

getOpcode in interface Bytecode

Specified by:

getOpcode in class AbstractBytecode

Returns:

body

public int body()

ranges

public Bytecode.Range[] ranges()

toString

public String toString()

Overrides:

toString in class Object