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

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

Inherited by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.

Collaboration diagram for edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl:
Collaboration graph
[legend]

List of all members.

Classes

class  Atom
class  KodkodIntEval

Public Member Functions

 SquanderKodkodPartImpl ()

Protected Member Functions

void partitionDomains ()
Atom nextAtomForLiteral (Unary partition, ForgeDomain litType, Map< ForgeDomain, Set< ForgeDomain >> deps, Set< Atom > availAtoms)
Universe createUniverse ()
Bounds createBounds ()
IEvaluator getEval (Iterator< Solution > solutions)
Object convAtom (ForgeAtom a)

Protected Attributes

Map< ForgeType.Unary, Map
< Atom, ForgeLiteral > > 		partitions
Map< String, Atom > lit2atom

Private Member Functions

void sort (List< ForgeType.Unary > types)
void processNext (ForgeType.Unary t, Map< ForgeDomain, Set< ForgeDomain >> deps, Set< Atom > allAtoms)
Set< Atom > processFirst (ForgeType.Unary t)
Map< ForgeDomain, Set
< ForgeDomain > > 		createDependencies (List< ForgeType.Unary > types)
String printPartitions ()

Detailed Description

An implementation of the ISquander interface that uses KodkodPart translation to Kodkod in order to minimize the number of atoms in the universe.

Author:
Aleksandar Milicevic

Definition at line 53 of file SquanderKodkodPartImpl.java.

Constructor & Destructor Documentation

edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.SquanderKodkodPartImpl (  ) 

Definition at line 146 of file SquanderKodkodPartImpl.java.

Member Function Documentation

Object edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.convAtom ( ForgeAtom  a  )  [protected]

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

Definition at line 482 of file SquanderKodkodPartImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.lit2atom.

Bounds edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds (  )  [protected]

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

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

Definition at line 410 of file SquanderKodkodPartImpl.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.SquanderKodkodPartImpl.createUniverse(), edu.mit.csail.sdg.squander.engine.SquanderReporter.creatingKodkodBounds(), edu.mit.csail.sdg.squander.engine.SquanderReporter.creatingKodkodUniverse(), edu.mit.csail.sdg.squander.engine.SquanderReporter.end(), 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.SquanderKodkodPartImpl.lit2atom, 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.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.

Map<ForgeDomain, Set<ForgeDomain> > edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createDependencies ( List< ForgeType.Unary >  types  )  [private]

Definition at line 225 of file SquanderKodkodPartImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains().

Universe edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createUniverse (  )  [protected]

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

Definition at line 366 of file SquanderKodkodPartImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.lit2atom, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.printPartitions().

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

IEvaluator edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.getEval ( Iterator< Solution >  solutions  )  [protected]

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

Definition at line 477 of file SquanderKodkodPartImpl.java.

Atom edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.nextAtomForLiteral ( Unary  partition,
ForgeDomain  litType,
Map< ForgeDomain, Set< ForgeDomain >>  deps,
Set< Atom >  availAtoms 
) [protected]

Definition at line 241 of file SquanderKodkodPartImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.ForgeConverter.findLiteralsForType(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.lit2atom.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.processNext().

void edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains (  )  [protected]

Definition at line 159 of file SquanderKodkodPartImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createDependencies(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.ForgeConverter.findLiteralsForType(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.ints, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.lit2atom, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitions, 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.SquanderKodkodImpl.program, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.sort(), and edu.mit.csail.sdg.squander.spec.ForgeScene.usedTypes.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createUniverse().

String edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.printPartitions (  )  [private]

Definition at line 378 of file SquanderKodkodPartImpl.java.

References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitions.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createUniverse().

Set<Atom> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.processFirst ( ForgeType.Unary  t  )  [private]

Definition at line 211 of file SquanderKodkodPartImpl.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.kk.SquanderKodkodPartImpl.lit2atom, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitions.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains().

void edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.processNext ( ForgeType.Unary  t,
Map< ForgeDomain, Set< ForgeDomain >>  deps,
Set< Atom >  allAtoms 
) [private]

Definition at line 180 of file SquanderKodkodPartImpl.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.kk.SquanderKodkodPartImpl.lit2atom, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.nextAtomForLiteral(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitions.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains().

void edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.sort ( List< ForgeType.Unary >  types  )  [private]

Definition at line 148 of file SquanderKodkodPartImpl.java.

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

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains().

Member Data Documentation

Map<String, Atom> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.lit2atom [protected]

Definition at line 144 of file SquanderKodkodPartImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.conv2tuples(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.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.SquanderKodkodPartImpl.createUniverse(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostLower(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.nextAtomForLiteral(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.processFirst(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.processNext().

Map<ForgeType.Unary, Map<Atom, ForgeLiteral> > edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitions [protected]

Definition at line 143 of file SquanderKodkodPartImpl.java.

Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getExtent(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.KodkodIntEval.makeConst(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.printPartitions(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.processFirst(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.processNext().

The documentation for this class was generated from the following file:
Generated by  doxygen 1.6.2-20100208