edu.mit.csail.sdg.squander.absstate.ObjTupleSet Class Reference
[Abstract State]

Collaboration diagram for edu.mit.csail.sdg.squander.absstate.ObjTupleSet:

[legend]

List of all members.

Public Member Functions
	ObjTupleSet (int arity)
	ObjTupleSet (ObjTuple val)
int	arity ()
boolean	isEmpty ()
boolean	isTuple ()
boolean	isUnary ()
boolean	add (ObjTuple e)
boolean	contains (Object o)
boolean	remove (Object o)
int	size ()
Set< ObjTuple >	tuples ()
Iterator< ObjTuple >	iterator ()
String	toString ()
ObjTupleSet	join (ObjTupleSet ots)
ObjTupleSet	product (ObjTupleSet ots)
ObjTupleSet	union (ObjTupleSet ots)
ObjTupleSet	union (ObjTuple val)
ObjTupleSet	diff (ObjTupleSet ots)
boolean	subsetOf (ObjTupleSet rhs)
ObjTupleSet	intersection (ObjTupleSet ots)
int	hashCode ()
boolean	equals (Object obj)
Static Public Member Functions
static ObjTupleSet	singleTuple (Object...tuple)
static ObjTupleSet	filter (ObjTupleSet otset, int i, Object obj)
static ObjTupleSet	join (ObjTupleSet lhs, ObjTupleSet rhs)
static ObjTupleSet	product (ObjTupleSet lhs, ObjTupleSet rhs)
static ObjTupleSet	convertFrom (ForgeConstant val, ForgeConverter fconv)
static ObjTupleSet	union (ObjTupleSet lhs, ObjTupleSet rhs)
static ObjTupleSet	diff (ObjTupleSet lhs, ObjTupleSet rhs)
static ObjTupleSet	intersection (ObjTupleSet lhs, ObjTupleSet rhs)
Static Private Member Functions
static ObjTuple	convertToObjTuple (Tuple t, ForgeConverter fconv)
Private Attributes
final int	arity
final Set< ObjTuple >	tuples = new HashSet<ObjTuple>()

---

Detailed Description

A set of tuples of objects (ObjTuple)

Author:

Aleksandar Milicevic

Definition at line 23 of file ObjTupleSet.java.

---

Constructor & Destructor Documentation

edu.mit.csail.sdg.squander.absstate.ObjTupleSet.ObjTupleSet

(

int

arity

)

Definition at line 28 of file ObjTupleSet.java.

Referenced by edu.mit.csail.sdg.squander.absstate.ObjTupleSet.convertFrom(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.diff(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.filter(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.intersection(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.join(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.product(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.singleTuple(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.union().

edu.mit.csail.sdg.squander.absstate.ObjTupleSet.ObjTupleSet

(

ObjTuple

val

)

Definition at line 32 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTuple.arity, and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples().

---

Member Function Documentation

boolean edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add

(

ObjTuple

e

)

Definition at line 42 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTuple.arity, edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples().

Referenced by edu.mit.csail.sdg.squander.engine.Heap2Bounds.addBound(), edu.mit.csail.sdg.squander.absstate.FieldValue.addTuple(), edu.mit.csail.sdg.squander.engine.SquanderEval2.boolAtom(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.convertFrom(), edu.mit.csail.sdg.squander.engine.ForgeConverter.extent(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.filter(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getExtent(), edu.mit.csail.sdg.squander.engine.SquanderEval2.intAtom(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.intersection(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.join(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.KodkodIntEval.makeConst(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.KodkodEval.makeConst(), edu.mit.csail.sdg.squander.engine.SquanderEval2.objAtom(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.product(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.singleTuple(), edu.mit.csail.sdg.squander.spec.constant.ConstRel2Bound.visitDec(), and edu.mit.csail.sdg.squander.spec.constant.ConstRel2Bound.visitInc().

int edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity

(

)

Definition at line 37 of file ObjTupleSet.java.

Referenced by edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.equals(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.hashCode(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.isUnary(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.product().

boolean edu.mit.csail.sdg.squander.absstate.ObjTupleSet.contains

(

Object

o

)

Definition at line 47 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples().

static ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.convertFrom	(	ForgeConstant	val,
		ForgeConverter	fconv
	)			[static]

Converts the given Forge constant to a tuple set

Definition at line 158 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.convertToObjTuple(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.ObjTupleSet().

static ObjTuple edu.mit.csail.sdg.squander.absstate.ObjTupleSet.convertToObjTuple	(	Tuple	t,
		ForgeConverter	fconv
	)			[static, private]

Converts the given Forge tuple to ObjTuple

Definition at line 170 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.atom2obj().

Referenced by edu.mit.csail.sdg.squander.absstate.ObjTupleSet.convertFrom().

static ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.diff	(	ObjTupleSet	lhs,
		ObjTupleSet	rhs
	)			[static]

Returns the set difference of the two given tuple sets

Definition at line 193 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity, edu.mit.csail.sdg.squander.absstate.ObjTupleSet.ObjTupleSet(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.

ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.diff

(

ObjTupleSet

ots

)

Performs set difference and returns the result as a new tuple set

Definition at line 64 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.diff().

Referenced by edu.mit.csail.sdg.squander.absstate.ObjTupleSet.diff(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitDiff().

boolean edu.mit.csail.sdg.squander.absstate.ObjTupleSet.equals

(

Object

obj

)

Definition at line 80 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples().

Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visitEquals().

static ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.filter	(	ObjTupleSet	otset,
		int	i,
		Object	obj
	)			[static]

Returns a new tuple set containing the tuples from otset which contain object obj at position i

Definition at line 111 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity, and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.ObjTupleSet().

int edu.mit.csail.sdg.squander.absstate.ObjTupleSet.hashCode

(

)

Definition at line 71 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples().

static ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.intersection	(	ObjTupleSet	lhs,
		ObjTupleSet	rhs
	)			[static]

Returns the set intersection of the two given tuple sets

Definition at line 204 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity, edu.mit.csail.sdg.squander.absstate.ObjTupleSet.ObjTupleSet(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.

ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.intersection

(

ObjTupleSet

ots

)

Performs set intersection and returns the result as a new tuple set

Definition at line 68 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.intersection().

Referenced by edu.mit.csail.sdg.squander.absstate.ObjTupleSet.intersection(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitIntersection().

boolean edu.mit.csail.sdg.squander.absstate.ObjTupleSet.isEmpty

(

)

Definition at line 38 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples().

Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.boolValue(), edu.mit.csail.sdg.squander.engine.SquanderResult.restoreJavaHeap(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().

boolean edu.mit.csail.sdg.squander.absstate.ObjTupleSet.isTuple

(

)

Definition at line 39 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples().

Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().

boolean edu.mit.csail.sdg.squander.absstate.ObjTupleSet.isUnary

(

)

Definition at line 40 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity().

Iterator<ObjTuple> edu.mit.csail.sdg.squander.absstate.ObjTupleSet.iterator

(

)

Definition at line 52 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples().

static ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.join	(	ObjTupleSet	lhs,
		ObjTupleSet	rhs
	)			[static]

Performs relational join of the given two tuple sets and returns the result as a new tuple set.

Definition at line 124 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity, and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.ObjTupleSet().

ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.join

(

ObjTupleSet

ots

)

Performs relational join and returns the result as a new tuple set

Definition at line 56 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.join().

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.SquanderResult.getReturnValue(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.join(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitJoin().

static ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.product	(	ObjTupleSet	lhs,
		ObjTupleSet	rhs
	)			[static]

Performs relational product of the given two tuple sets and returns the result as a new tuple set.

Definition at line 146 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.ObjTupleSet(), edu.mit.csail.sdg.squander.absstate.ObjTuple.product(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.

ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.product

(

ObjTupleSet

ots

)

Performs relational product and returns the result as a new tuple set

Definition at line 58 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.product().

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.extent(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getExtent(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostSpec(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.product(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitProduct().

boolean edu.mit.csail.sdg.squander.absstate.ObjTupleSet.remove

(

Object

o

)

Definition at line 48 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples().

static ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.singleTuple

(

Object...

tuple

)

[static]

Returns a new tuple set containing only the given tuple

Definition at line 101 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.ObjTupleSet().

int edu.mit.csail.sdg.squander.absstate.ObjTupleSet.size

(

)

Definition at line 49 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples().

Referenced by edu.mit.csail.sdg.squander.engine.SquanderResult.convertForgeSetToJavaArray(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitAll(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitExists(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitUnion().

boolean edu.mit.csail.sdg.squander.absstate.ObjTupleSet.subsetOf

(

ObjTupleSet

rhs

)

Returns whether this tuple set is a subset of the given tuple set

Definition at line 66 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visitSubset().

String edu.mit.csail.sdg.squander.absstate.ObjTupleSet.toString

(

)

Definition at line 53 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples().

Set<ObjTuple> edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples

(

)

Definition at line 50 of file ObjTupleSet.java.

Referenced by edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.contains(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.equals(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.hashCode(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.isEmpty(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.isTuple(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.iterator(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.ObjTupleSet(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.remove(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.size(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.subsetOf(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.toString().

static ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.union	(	ObjTupleSet	lhs,
		ObjTupleSet	rhs
	)			[static]

Returns the set union of the two given tuple sets.

Definition at line 182 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.ObjTupleSet(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.

ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.union

(

ObjTuple

val

)

Returns the union of this tuple set and the given tuple

Definition at line 62 of file ObjTupleSet.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.ObjTupleSet().

ObjTupleSet edu.mit.csail.sdg.squander.absstate.ObjTupleSet.union

(

ObjTupleSet

ots

)

Returns the union of this tuple set and the given tuple set

Definition at line 60 of file ObjTupleSet.java.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visitClosure(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitRelUnion(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitUnion().

---

Member Data Documentation

final int edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity [private]

Definition at line 25 of file ObjTupleSet.java.

Referenced by edu.mit.csail.sdg.squander.engine.Heap2Bounds.addBound(), edu.mit.csail.sdg.squander.engine.SquanderEval2.boolValue(), edu.mit.csail.sdg.squander.serializer.special.DefaultObjSer.concrFunc(), edu.mit.csail.sdg.squander.engine.ForgeConverter.conv2fc(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.conv2tuples(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.conv2tuples(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.diff(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.equals(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.filter(), edu.mit.csail.sdg.squander.engine.SquanderResult.getSpecField(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.intersection(), edu.mit.csail.sdg.squander.engine.SquanderEval2.intValue(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.join(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.product(), edu.mit.csail.sdg.squander.serializer.special.SetSer.restoreElems(), edu.mit.csail.sdg.squander.serializer.special.MapSer.restoreElems(), edu.mit.csail.sdg.squander.serializer.special.ListSer.restoreElems(), edu.mit.csail.sdg.squander.serializer.special.ArraySer.restoreElems(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitClosure(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitUnion().

final Set<ObjTuple> edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples = new HashSet<ObjTuple>() [private]

Definition at line 26 of file ObjTupleSet.java.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.boolValue(), edu.mit.csail.sdg.squander.serializer.special.DefaultObjSer.concrFunc(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.conv2tuples(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.conv2tuples(), edu.mit.csail.sdg.squander.engine.SquanderResult.convertForgeSetToJavaArray(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.diff(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.equals(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getModLits(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostLower(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostLower(), edu.mit.csail.sdg.squander.engine.SquanderResult.getReturnValue(), edu.mit.csail.sdg.squander.engine.SquanderResult.getSpecField(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.intersection(), edu.mit.csail.sdg.squander.engine.SquanderEval2.intValue(), edu.mit.csail.sdg.squander.engine.ForgeConverter.printObjSet(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.product(), edu.mit.csail.sdg.squander.serializer.special.ListSer.restoreElems(), edu.mit.csail.sdg.squander.serializer.special.ArraySer.restoreElems(), edu.mit.csail.sdg.squander.engine.SquanderResult.restoreJavaHeap(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.subsetOf(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.union(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitAll(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitClosure(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitExists(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitUnion().

---

The documentation for this class was generated from the following file:

• src/edu/mit/csail/sdg/squander/absstate/ObjTupleSet.java