edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl Class Reference
[Engine]

Inherits edu::mit::csail::sdg::squander::engine::SquanderImpl.

Inherited by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.

Collaboration diagram for edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl:

[legend]

List of all members.

Classes
class	DiscoverHigherOrderQuant
class	KodkodEval
class	Tr2KK
Public Member Functions
	SquanderKodkodImpl ()
Protected Member Functions
Set< GlobalVariable >	getModsForPostState (ForgeConverter fconv, SpecCase sc)
ForgeExpression	getPreSpec (SpecCase cs)
ForgeExpression	getPostSpec (SpecCase cs, ForgeConverter fconv)
IEvaluator	exeSpec (ForgeExpression spec, Set< GlobalVariable > modifies, ForgeConverter fconv)
IEvaluator	getEval (Iterator< Solution > solution)
void	init ()
Formula	convertSpec (ForgeExpression spec)
void	createRelations ()
Bounds	createBounds ()
ForgeConstant	getPostLower (GlobalVariable g, ForgeConstant initialBound)
ForgeConstant	getPostUpper (GlobalVariable var, ForgeConstant postLower)
Universe	createUniverse ()
Formula	node2form (Node node)
IntExpression	node2int (Node node)
Expression	node2expr (Node node)
Expression	form2expr (Formula form)
ForgeConstant	getExtent (GlobalVariable var, ForgeConstant lower)
int	findMaxArrayLength (GlobalVariable var)
ForgeConstant.Unary	nonnegs ()
ForgeConstant.Unary	nonnegs (int upperBound)
void	boundLocalVar (LocalVariable var, TupleFactory f, Bounds b)
void	addRelForVar (ForgeVariable var, String name)
String	relName (ForgeVariable var)
TupleSet	conv2tuples (ForgeConstant fc, TupleFactory f)
Object	convAtom (ForgeAtom a)
TupleSet	conv2tuples (ObjTupleSet fc, TupleFactory f)
Protected Attributes
Set< GlobalVariable >	modifies
ForgeConverter	fconv
ForgeScene	forgeScene
ForgeProgram	program
Map< String, Relation >	lit2rel
Map< ForgeType, Expression >	type2expr
Map< String, Expression >	var2rel
Map< ForgeVariable, ObjTupleSet >	modVal
Map< ForgeVariable, ObjTupleSet >	lowerBounds
Map< ForgeVariable, ObjTupleSet >	upperBounds
Set< Integer >	ints
Relation	trueRelation
Relation	falseRelation
SpecCase	cs
Private Member Functions
String	printBoundsSummary (Bounds bounds)
ForgeAtom	lit2atom (ForgeLiteral lit, ForgeBounds forgeBounds)

---

Detailed Description

An implementation of the ISquander interface that uses Kodkod as the back-end.

Author:

Aleksandar Milicevic

Definition at line 94 of file SquanderKodkodImpl.java.

---

Constructor & Destructor Documentation

edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.SquanderKodkodImpl

(

)

Definition at line 688 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.lowerBounds, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.modVal, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.upperBounds.

---

Member Function Documentation

void edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.addRelForVar	(	ForgeVariable	var,
		String	name
	)			[protected]

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.

Definition at line 1150 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.var2rel.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations().

void edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.boundLocalVar	(	LocalVariable	var,
		TupleFactory	f,
		Bounds	b
	)			[protected]

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.

Definition at line 1139 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.conv2tuples(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.relName(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.var2rel.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds().

TupleSet edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.conv2tuples	(	ObjTupleSet	fc,
		TupleFactory	f
	)			[protected]

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.

Definition at line 1192 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity, edu.mit.csail.sdg.squander.spec.ForgeScene.forgeLitForObj(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.

TupleSet edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.conv2tuples	(	ForgeConstant	fc,
		TupleFactory	f
	)			[protected]

Definition at line 1162 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.convAtom().

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.boundLocalVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.boundLocalVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds().

Object edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.convAtom

(

ForgeAtom

a

)

[protected]

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.

Definition at line 1182 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.ints.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.conv2tuples().

Formula edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.convertSpec

(

ForgeExpression

spec

)

[protected]

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.

Definition at line 839 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.node2form().

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec().

Bounds edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds

(

)

[protected]

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.

Definition at line 885 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.spec.ForgeScene.args, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.boundLocalVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.conv2tuples(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createUniverse(), edu.mit.csail.sdg.squander.engine.SquanderReporter.creatingKodkodBounds(), edu.mit.csail.sdg.squander.engine.SquanderReporter.creatingKodkodUniverse(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.ForgeConverter.findLiteralsForType(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostLower(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostUpper(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.ints, edu.mit.csail.sdg.squander.spec.ForgeScene.isSpecField(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.lit2rel, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.modifies, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.program, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.relName(), edu.mit.csail.sdg.squander.engine.SquanderImpl.reporter, edu.mit.csail.sdg.squander.spec.ForgeScene.returnVar, edu.mit.csail.sdg.squander.spec.ForgeScene.thisVar, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.type2expr, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.var2rel.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec().

void edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations

(

)

[protected]

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.

Definition at line 844 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.addRelForVar(), edu.mit.csail.sdg.squander.spec.ForgeScene.args, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.falseRelation, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.lit2rel, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.modifies, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.program, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.relName(), edu.mit.csail.sdg.squander.spec.ForgeScene.returnVar, edu.mit.csail.sdg.squander.spec.ForgeScene.thisVar, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.trueRelation, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.type2expr.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec().

Universe edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createUniverse

(

)

[protected]

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.

Definition at line 995 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, edu.mit.csail.sdg.squander.spec.ForgeScene.ints, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.ints, edu.mit.csail.sdg.squander.spec.ForgeScene.isEnsureAllInts(), edu.mit.csail.sdg.squander.engine.ForgeConverter.maxInt(), edu.mit.csail.sdg.squander.engine.ForgeConverter.minInt(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.program.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds().

IEvaluator edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec	(	ForgeExpression	spec,
		Set< GlobalVariable >	modifies,
		ForgeConverter	fconv
	)			[protected]

Executes the given forge expression.

Reimplemented from edu.mit.csail.sdg.squander.engine.SquanderImpl.

Definition at line 757 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.convertSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getEval(), edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2Lit(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.init(), edu.mit.csail.sdg.squander.engine.ForgeConverter.javaScene, edu.mit.csail.sdg.squander.spec.JavaScene.methodSpec(), edu.mit.csail.sdg.squander.engine.Heap2Bounds.minBW(), edu.mit.csail.sdg.squander.spec.MethodSpec.options, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.printBoundsSummary(), edu.mit.csail.sdg.squander.spec.ForgeScene.program, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.program, and edu.mit.csail.sdg.squander.annotations.Options.solveAll().

int edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.findMaxArrayLength

(

GlobalVariable

var

)

[protected]

Definition at line 1108 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, edu.mit.csail.sdg.squander.spec.ForgeScene.global(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.modifies.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getExtent().

Expression edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.form2expr

(

Formula

form

)

[protected]

converts a Kodkod formula to a Kodkod expressoin

Definition at line 1069 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.falseRelation, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.trueRelation.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.node2expr().

IEvaluator edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getEval

(

Iterator< Solution >

solution

)

[protected]

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.

Definition at line 826 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec().

ForgeConstant edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getExtent	(	GlobalVariable	var,
		ForgeConstant	lower
	)			[protected]

Definition at line 1075 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.findMaxArrayLength(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, edu.mit.csail.sdg.squander.spec.ForgeScene.isOneField(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.nonnegs().

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostUpper().

Set<GlobalVariable> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getModsForPostState	(	ForgeConverter	fconv,
		SpecCase	sc
	)			[protected]

Reimplemented from edu.mit.csail.sdg.squander.engine.SquanderImpl.

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.

Definition at line 695 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.spec.Spec.SpecCase.frame.

ForgeConstant edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostLower	(	GlobalVariable	g,
		ForgeConstant	initialBound
	)			[protected]

Definition at line 949 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.ForgeConverter.findLiteralsForType(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, edu.mit.csail.sdg.squander.spec.ForgeScene.instLitForObj(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.lit2atom(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.modVal, and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds().

ForgeExpression edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostSpec	(	SpecCase	cs,
		ForgeConverter	fconv
	)			[protected]

Reimplemented from edu.mit.csail.sdg.squander.engine.SquanderImpl.

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.

Definition at line 707 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.spec.Spec.abstractConstraint(), edu.mit.csail.sdg.squander.engine.SquanderEval2.eval(), edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeScene, edu.mit.csail.sdg.squander.spec.Spec.SpecCase.frame, edu.mit.csail.sdg.squander.spec.Spec.funcConstraint(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.lowerBounds, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.modVal, edu.mit.csail.sdg.squander.spec.Spec.SpecCase.post, edu.mit.csail.sdg.squander.absstate.ObjTupleSet.product(), edu.mit.csail.sdg.squander.spec.ForgeScene.program, edu.mit.csail.sdg.squander.spec.Spec.SpecCase.spec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.upperBounds, and edu.mit.csail.sdg.squander.spec.Spec.wellformedPost().

ForgeConstant edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostUpper	(	GlobalVariable	var,
		ForgeConstant	postLower
	)			[protected]

Definition at line 983 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.ForgeConverter.conv2fc(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getExtent(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.modVal, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.upperBounds.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds().

ForgeExpression edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPreSpec

(

SpecCase

cs

)

[protected]

Reimplemented from edu.mit.csail.sdg.squander.engine.SquanderImpl.

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.

Definition at line 700 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.spec.Spec.abstractConstraint(), edu.mit.csail.sdg.squander.spec.Spec.SpecCase.pre, and edu.mit.csail.sdg.squander.spec.Spec.SpecCase.spec().

void edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.init

(

)

[protected]

Reimplemented in edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.

Definition at line 831 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.ints, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.lit2rel, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.program, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.type2expr, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.var2rel.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec().

ForgeAtom edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.lit2atom	(	ForgeLiteral	lit,
		ForgeBounds	forgeBounds
	)			[private]

Definition at line 972 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostLower().

Expression edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.node2expr

(

Node

node

)

[protected]

converts a Kodkod node to a Kodkod expression.

Definition at line 1056 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.form2expr().

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit().

Formula edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.node2form

(

Node

node

)

[protected]

converts a Kodkod node to a Kodkod formula.

Definition at line 1027 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.falseRelation, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.trueRelation.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.convertSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit2().

IntExpression edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.node2int

(

Node

node

)

[protected]

converts a Kodkod expression to a Kodkod integer.

Definition at line 1045 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit2().

ForgeConstant.Unary edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.nonnegs

(

int

upperBound

)

[protected]

Definition at line 1128 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.nonnegs().

ForgeConstant.Unary edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.nonnegs

(

)

[protected]

Definition at line 1124 of file SquanderKodkodImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, and edu.mit.csail.sdg.squander.engine.ForgeConverter.forgeBounds.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getExtent(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.nonnegs().

String edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.printBoundsSummary

(

Bounds

bounds

)

[private]

Definition at line 806 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec().

String edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.relName

(

ForgeVariable

var

)

[protected]

Definition at line 1155 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.addFldRel(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.boundLocalVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.boundLocalVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.boundLocalVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.getRelForVarAndCheck(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.wellformed().

---

Member Data Documentation

SpecCase edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.cs [protected]

Definition at line 686 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations().

Relation edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.falseRelation [protected]

Definition at line 685 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.form2expr(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.node2form().

ForgeConverter edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv [protected]

Definition at line 672 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.boundLocalVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createUniverse(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.findMaxArrayLength(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getExtent(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getExtent(), 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.kk.SquanderKodkodImpl.getPostUpper(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.KodkodIntEval.makeConst(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.nextAtomForLiteral(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.nonnegs(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.processFirst(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.processNext(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.sort(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit().

ForgeScene edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene [protected]

Definition at line 673 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.conv2tuples(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createUniverse(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.findMaxArrayLength(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getExtent(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getLitNameForObject(), 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.kk.SquanderKodkodImpl.KodkodEval.makeConst(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.wellformed().

Set<Integer> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.ints [protected]

Definition at line 683 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.convAtom(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createUniverse(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.init(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains().

Map<String, Relation> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.lit2rel [protected]

Definition at line 676 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.addFldRel(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.init(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit().

Map<ForgeVariable, ObjTupleSet> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.lowerBounds [protected]

Definition at line 680 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostSpec(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.SquanderKodkodImpl().

Set<GlobalVariable> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.modifies [protected]

Definition at line 671 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.addFldRel(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.findMaxArrayLength(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.wellformed().

Map<ForgeVariable, ObjTupleSet> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.modVal [protected]

Definition at line 679 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostLower(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostLower(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostUpper(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostUpper(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.SquanderKodkodImpl().

ForgeProgram edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.program [protected]

Definition at line 674 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createUniverse(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.init(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains().

Relation edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.trueRelation [protected]

Definition at line 684 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.form2expr(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.node2form(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit().

Map<ForgeType, Expression> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.type2expr [protected]

Definition at line 677 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.init(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visitForgeType().

Map<ForgeVariable, ObjTupleSet> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.upperBounds [protected]

Definition at line 681 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostUpper(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostUpper(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.SquanderKodkodImpl().

Map<String, Expression> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.var2rel [protected]

Definition at line 678 of file SquanderKodkodImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.addRelForVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.addRelForVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.boundLocalVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.boundLocalVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.boundLocalVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.getRelForVarAndCheck(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.init(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.wellformed().

---

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

• src/edu/mit/csail/sdg/squander/engine/kk/SquanderKodkodImpl.java