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

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

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

[legend]

List of all members.

Classes
class	FldRelElem
Public Member Functions
	SquanderKodkod2Impl ()
Protected Member Functions
Set< GlobalVariable >	getModsForPostState (ForgeConverter fconv, SpecCase sc)
ForgeExpression	getPreSpec (SpecCase cs)
ForgeExpression	getPostSpec (SpecCase cs, ForgeConverter fconv)
Formula	convertSpec (ForgeExpression spec)
IEvaluator	getEval (Iterator< Solution > solutions)
void	init ()
void	createRelations ()
void	addRelForVar (ForgeVariable var, String name)
Bounds	createBounds ()
void	boundLocalVar (LocalVariable var, TupleFactory f, Bounds b)
Private Member Functions
Formula	wellformed ()
Formula	one (Expression rel)
Formula	arrLenConstr (FldRelElem fre)
Formula	arrElemsConstr (FldRelElem fre)
Expression	intsExpr ()
List< InstanceLiteral >	getModLits (GlobalVariable g, ForgeExpression expr)
void	addRelForVar (String name, Expression expr)
void	addFldRel (InstanceLiteral l, GlobalVariable g, List< InstanceLiteral > modLits)
List< FldRelElem >	findFldRelsForVar (GlobalVariable var)
ObjTupleSet[]	getBounds (ForgeVariable var)
ObjTupleSet	getExtent (ForgeVariable var)
Private Attributes
HashMap< String, FldRelElem >	fldRels

---

Detailed Description

An alternative implementation of the ISquander interface that uses a different translation to Kodkod.

Author:

Aleksandar Milicevic

Definition at line 49 of file SquanderKodkod2Impl.java.

---

Constructor & Destructor Documentation

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

(

)

Definition at line 74 of file SquanderKodkod2Impl.java.

---

Member Function Documentation

void edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.addFldRel	(	InstanceLiteral	l,
		GlobalVariable	g,
		List< InstanceLiteral >	modLits
	)			[private]

Definition at line 254 of file SquanderKodkod2Impl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.addRelForVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.fldRels, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.lit2rel, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.modifies, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.relName().

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

void edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.addRelForVar	(	String	name,
		Expression	expr
	)			[private]

Definition at line 245 of file SquanderKodkod2Impl.java.

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

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

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

Definition at line 241 of file SquanderKodkod2Impl.java.

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

Formula edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.arrElemsConstr

(

FldRelElem

fre

)

[private]

Definition at line 143 of file SquanderKodkod2Impl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.fldRels, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.intsExpr(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.one().

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

Formula edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.arrLenConstr

(

FldRelElem

fre

)

[private]

Definition at line 138 of file SquanderKodkod2Impl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.one().

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

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

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

Definition at line 325 of file SquanderKodkod2Impl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.conv2tuples(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getBounds(), 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.SquanderKodkod2Impl.createBounds().

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

(

ForgeExpression

spec

)

[protected]

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

Definition at line 96 of file SquanderKodkod2Impl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.wellformed().

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

(

)

[protected]

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

Definition at line 278 of file SquanderKodkod2Impl.java.

References edu.mit.csail.sdg.squander.spec.ForgeScene.args, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.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.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.findFldRelsForVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getExtent(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.ints, edu.mit.csail.sdg.squander.spec.ForgeScene.isConst(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.join(), edu.mit.csail.sdg.squander.engine.ForgeConverter.lit2obj(), 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.relName(), edu.mit.csail.sdg.squander.spec.ForgeScene.returnVar, edu.mit.csail.sdg.squander.spec.ForgeScene.thisVar, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.var2rel.

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

(

)

[protected]

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

Definition at line 161 of file SquanderKodkod2Impl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.addFldRel(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.addRelForVar(), edu.mit.csail.sdg.squander.spec.ForgeScene.args, edu.mit.csail.sdg.squander.spec.ForgeScene.consts, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.cs, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.falseRelation, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.ForgeConverter.findInstLiteralsForType(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, edu.mit.csail.sdg.squander.spec.Spec.SpecCase.frame, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getModLits(), edu.mit.csail.sdg.squander.spec.ForgeScene.isConst(), 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.

List<FldRelElem> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.findFldRelsForVar

(

GlobalVariable

var

)

[private]

Definition at line 268 of file SquanderKodkod2Impl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.fldRels.

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

ObjTupleSet [] edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getBounds

(

ForgeVariable

var

)

[private]

Definition at line 335 of file SquanderKodkod2Impl.java.

References edu.mit.csail.sdg.squander.engine.Heap2Bounds.bounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getExtent(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2Lit().

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

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

(

Iterator< Solution >

solutions

)

[protected]

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

Definition at line 103 of file SquanderKodkod2Impl.java.

ObjTupleSet edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getExtent

(

ForgeVariable

var

)

[private]

Definition at line 352 of file SquanderKodkod2Impl.java.

References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.ForgeConverter.findLiteralsForType(), edu.mit.csail.sdg.squander.engine.ForgeConverter.lit2obj(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.product().

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

List<InstanceLiteral> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getModLits	(	GlobalVariable	g,
		ForgeExpression	expr
	)			[private]

Definition at line 218 of file SquanderKodkod2Impl.java.

References edu.mit.csail.sdg.squander.engine.SquanderEval2.eval(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.ForgeConverter.findInstLiteralsForType(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, edu.mit.csail.sdg.squander.spec.ForgeScene.instLitForObj(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.

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

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

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

Definition at line 77 of file SquanderKodkod2Impl.java.

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

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

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

Definition at line 88 of file SquanderKodkod2Impl.java.

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

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

(

SpecCase

cs

)

[protected]

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

Definition at line 82 of file SquanderKodkod2Impl.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.SquanderKodkod2Impl.init

(

)

[protected]

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

Definition at line 108 of file SquanderKodkod2Impl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.fldRels.

Expression edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.intsExpr

(

)

[private]

Definition at line 156 of file SquanderKodkod2Impl.java.

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

Formula edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.one

(

Expression

rel

)

[private]

Definition at line 134 of file SquanderKodkod2Impl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.arrElemsConstr(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.arrLenConstr(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.wellformed().

Formula edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.wellformed

(

)

[private]

Definition at line 113 of file SquanderKodkod2Impl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.arrElemsConstr(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.arrLenConstr(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.fldRels, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, edu.mit.csail.sdg.squander.spec.ForgeScene.isSpecField(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.modifies, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.one(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.relName(), edu.mit.csail.sdg.squander.spec.ForgeScene.returnVar, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.var2rel.

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

---

Member Data Documentation

HashMap<String, FldRelElem> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.fldRels [private]

Definition at line 72 of file SquanderKodkod2Impl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.addFldRel(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.arrElemsConstr(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.findFldRelsForVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.init(), 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/SquanderKodkod2Impl.java