forge.program
Class QuantifyExpression

java.lang.Object
  forge.program.QuantifyExpression

All Implemented Interfaces:

ForgeExpression, ProgramElement

public final class QuantifyExpression
extends java.lang.Object
implements ForgeExpression

A quantified formula expression.

Author:

Greg Dennis (gdennis@mit.edu)

Nested Class Summary

static class

QuantifyExpression.Op

Nested classes/interfaces inherited from interface forge.program.ForgeExpression

ForgeExpression.Leaf, ForgeExpression.Modifiable

Method Summary

<T> T	accept(ExpressionVisitor<T> visitor) Accept a visitor.
ForgeExpression	and(ForgeExpression expr)
ForgeExpression	apply(UnaryExpression.Op op)
int	arity() Returns type().arity()
ForgeExpression	bitAnd(ForgeExpression expr)
ForgeExpression	bitNot()
ForgeExpression	bitOr(ForgeExpression expr)
ForgeExpression	bitXor(ForgeExpression expr)
ForgeExpression	bool()
ForgeExpression	closure()
ForgeExpression	compose(BinaryExpression.Op op, ForgeExpression expr)
ForgeExpression	comprehension(LocalDecls decls)
LocalDecls	decls()
ForgeExpression	difference(ForgeExpression expr)
ForgeExpression	divide(ForgeExpression expr)
ForgeExpression	domain()
ForgeExpression	eq(ForgeExpression expr)
ForgeExpression	forAll(LocalDecls decls)
ForgeExpression	forSome(LocalDecls decls)
ForgeExpression	gt(ForgeExpression expr)
ForgeExpression	gte(ForgeExpression expr)
ForgeExpression	iden()
ForgeExpression	iff(ForgeExpression expr)
ForgeExpression	implies(ForgeExpression expr)
ForgeExpression	in(ForgeExpression expr)
ForgeExpression	intersection(ForgeExpression expr)
boolean	isUnary() Returns true if the arity is one.
ForgeExpression	join(ForgeExpression expr)
ForgeExpression	lone()
ForgeExpression	lt(ForgeExpression expr)
ForgeExpression	lte(ForgeExpression expr)
ForgeExpression	minus(ForgeExpression expr)
ForgeExpression	modulo(ForgeExpression expr)
ForgeExpression	neg()
ForgeExpression	no()
ForgeExpression	not()
ForgeExpression	one()
QuantifyExpression.Op	op()
ForgeExpression	or(ForgeExpression expr)
ForgeExpression	override(ForgeExpression expr)
ForgeExpression	plus(ForgeExpression expr)
ForgeExpression	product(ForgeExpression expr)
ForgeProgram	program() Returns the program to which this element belongs.
ForgeExpression	projection(int... columns)
ForgeExpression	quantify(QuantifyExpression.Op quant, LocalDecls decls)
ForgeExpression	range()
ForgeExpression	shiftLeft(ForgeExpression expr)
ForgeExpression	shiftRight(ForgeExpression expr)
ForgeExpression	size()
ForgeExpression	some()
ForgeExpression	sub()
ForgeExpression	sum()
ForgeExpression	summation(LocalDecls decls)
ForgeExpression	thenElse(ForgeExpression thenExpr, ForgeExpression elseExpr)
ForgeExpression	times(ForgeExpression expr)
java.lang.String	toString()
ForgeType	type() Returns the type of the expression
ForgeExpression	union(ForgeExpression expr)
ForgeExpression	unsignedShiftRight(ForgeExpression expr)
ForgeExpression	xor(ForgeExpression expr)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface forge.program.ForgeExpression

and, apply, arity, bitAnd, bitNot, bitOr, bitXor, bool, closure, compose, comprehension, difference, divide, domain, eq, forAll, forSome, gt, gte, iden, iff, implies, in, intersection, isUnary, join, lone, lt, lte, minus, modulo, neg, no, not, one, or, override, plus, product, projection, quantify, range, shiftLeft, shiftRight, size, some, sum, summation, thenElse, times, union, unsignedShiftRight, xor

Methods inherited from interface forge.program.ProgramElement

program

Method Detail

type

public ForgeType type()

Returns the type of the expression

Specified by:

type in interface ForgeExpression

op

public QuantifyExpression.Op op()

decls

public LocalDecls decls()

sub

public ForgeExpression sub()

accept

public <T> T accept(ExpressionVisitor<T> visitor)

Description copied from interface: ForgeExpression

Accept a visitor.

Specified by:

accept in interface ForgeExpression

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

program

public final ForgeProgram program()

Description copied from interface: ProgramElement

Returns the program to which this element belongs.

Specified by:

program in interface ProgramElement

arity

public int arity()

Returns type().arity()

Specified by:

arity in interface ForgeExpression

isUnary

public final boolean isUnary()

Description copied from interface: ForgeExpression

Returns true if the arity is one.

Specified by:

isUnary in interface ForgeExpression

domain

public ForgeExpression domain()

Specified by:

domain in interface ForgeExpression

range

public ForgeExpression range()

Specified by:

range in interface ForgeExpression

iden

public final ForgeExpression iden()

Specified by:

iden in interface ForgeExpression

projection

public final ForgeExpression projection(int... columns)

Specified by:

projection in interface ForgeExpression

closure

public final ForgeExpression closure()

Specified by:

closure in interface ForgeExpression

no

public final ForgeExpression no()

Specified by:

no in interface ForgeExpression

lone

public final ForgeExpression lone()

Specified by:

lone in interface ForgeExpression

one

public final ForgeExpression one()

Specified by:

one in interface ForgeExpression

some

public final ForgeExpression some()

Specified by:

some in interface ForgeExpression

size

public final ForgeExpression size()

Specified by:

size in interface ForgeExpression

bool

public final ForgeExpression bool()

Specified by:

bool in interface ForgeExpression

not

public final ForgeExpression not()

Specified by:

not in interface ForgeExpression

sum

public final ForgeExpression sum()

Specified by:

sum in interface ForgeExpression

neg

public final ForgeExpression neg()

Specified by:

neg in interface ForgeExpression

bitNot

public final ForgeExpression bitNot()

Specified by:

bitNot in interface ForgeExpression

apply

public ForgeExpression apply(UnaryExpression.Op op)

Specified by:

apply in interface ForgeExpression

union

public final ForgeExpression union(ForgeExpression expr)

Specified by:

union in interface ForgeExpression

difference

public final ForgeExpression difference(ForgeExpression expr)

Specified by:

difference in interface ForgeExpression

intersection

public final ForgeExpression intersection(ForgeExpression expr)

Specified by:

intersection in interface ForgeExpression

join

public final ForgeExpression join(ForgeExpression expr)

Specified by:

join in interface ForgeExpression

product

public final ForgeExpression product(ForgeExpression expr)

Specified by:

product in interface ForgeExpression

override

public final ForgeExpression override(ForgeExpression expr)

Specified by:

override in interface ForgeExpression

and

public final ForgeExpression and(ForgeExpression expr)

Specified by:

and in interface ForgeExpression

or

public final ForgeExpression or(ForgeExpression expr)

Specified by:

or in interface ForgeExpression

xor

public final ForgeExpression xor(ForgeExpression expr)

Specified by:

xor in interface ForgeExpression

implies

public final ForgeExpression implies(ForgeExpression expr)

Specified by:

implies in interface ForgeExpression

iff

public final ForgeExpression iff(ForgeExpression expr)

Specified by:

iff in interface ForgeExpression

eq

public final ForgeExpression eq(ForgeExpression expr)

Specified by:

eq in interface ForgeExpression

in

public final ForgeExpression in(ForgeExpression expr)

Specified by:

in in interface ForgeExpression

lt

public final ForgeExpression lt(ForgeExpression expr)

Specified by:

lt in interface ForgeExpression

gt

public final ForgeExpression gt(ForgeExpression expr)

Specified by:

gt in interface ForgeExpression

lte

public final ForgeExpression lte(ForgeExpression expr)

Specified by:

lte in interface ForgeExpression

gte

public final ForgeExpression gte(ForgeExpression expr)

Specified by:

gte in interface ForgeExpression

plus

public final ForgeExpression plus(ForgeExpression expr)

Specified by:

plus in interface ForgeExpression

minus

public final ForgeExpression minus(ForgeExpression expr)

Specified by:

minus in interface ForgeExpression

times

public final ForgeExpression times(ForgeExpression expr)

Specified by:

times in interface ForgeExpression

divide

public final ForgeExpression divide(ForgeExpression expr)

Specified by:

divide in interface ForgeExpression

modulo

public final ForgeExpression modulo(ForgeExpression expr)

Specified by:

modulo in interface ForgeExpression

bitAnd

public final ForgeExpression bitAnd(ForgeExpression expr)

Specified by:

bitAnd in interface ForgeExpression

bitOr

public final ForgeExpression bitOr(ForgeExpression expr)

Specified by:

bitOr in interface ForgeExpression

bitXor

public final ForgeExpression bitXor(ForgeExpression expr)

Specified by:

bitXor in interface ForgeExpression

shiftLeft

public final ForgeExpression shiftLeft(ForgeExpression expr)

Specified by:

shiftLeft in interface ForgeExpression

shiftRight

public final ForgeExpression shiftRight(ForgeExpression expr)

Specified by:

shiftRight in interface ForgeExpression

unsignedShiftRight

public final ForgeExpression unsignedShiftRight(ForgeExpression expr)

Specified by:

unsignedShiftRight in interface ForgeExpression

compose

public final ForgeExpression compose(BinaryExpression.Op op,
                                     ForgeExpression expr)

Specified by:

compose in interface ForgeExpression

thenElse

public final ForgeExpression thenElse(ForgeExpression thenExpr,
                                      ForgeExpression elseExpr)

Specified by:

thenElse in interface ForgeExpression

forAll

public final ForgeExpression forAll(LocalDecls decls)

Specified by:

forAll in interface ForgeExpression

forSome

public final ForgeExpression forSome(LocalDecls decls)

Specified by:

forSome in interface ForgeExpression

comprehension

public final ForgeExpression comprehension(LocalDecls decls)

Specified by:

comprehension in interface ForgeExpression

summation

public final ForgeExpression summation(LocalDecls decls)

Specified by:

summation in interface ForgeExpression

quantify

public final ForgeExpression quantify(QuantifyExpression.Op quant,
                                      LocalDecls decls)

Specified by:

quantify in interface ForgeExpression