edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl Class Reference
[Engine]
Inherits edu::mit::csail::sdg::squander::engine::kk::SquanderKodkodPartImpl.
Public Member Functions | |
| SquanderKodkodPart2Impl () | |
Protected Member Functions | |
| Bounds | createBounds () |
| TupleSet | getPostLower (GlobalVariable g, TupleSet initialBound, TupleFactory f) |
| TupleSet | getPostUpper (GlobalVariable var, TupleSet postLower, TupleFactory f) |
| void | boundLocalVar (LocalVariable var, TupleFactory f, Bounds b) |
| TupleSet | conv2tuples (ObjTupleSet fc, TupleFactory f) |
Private Member Functions | |
| TupleSet[] | getPostLowerUpper (GlobalVariable var, TupleSet lowerInitial, TupleFactory f) |
| TupleSet | join (TupleSet ts1, TupleSet ts2, TupleFactory f) |
| TupleSet[] | getBounds (ForgeVariable var, TupleFactory f) |
| TupleSet | getExtent (ForgeVariable var, TupleFactory f) |
| String | getLitNameForObject (Object obj) |
Detailed Description
An implementation of the ISquander interface that uses KodkodPart translation to Kodkod that doesn't use ForgeBounds.
Definition at line 37 of file SquanderKodkodPart2Impl.java.
Constructor & Destructor Documentation
| edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.SquanderKodkodPart2Impl | ( | ) |
Definition at line 39 of file SquanderKodkodPart2Impl.java.
Member Function Documentation
| void edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.boundLocalVar | ( | LocalVariable | var, | |
| TupleFactory | f, | |||
| Bounds | b | |||
| ) | [protected] |
Reimplemented from edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.
Definition at line 162 of file SquanderKodkodPart2Impl.java.
References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.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.SquanderKodkodPart2Impl.createBounds().
| TupleSet edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.conv2tuples | ( | ObjTupleSet | fc, | |
| TupleFactory | f | |||
| ) | [protected] |
Reimplemented from edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.
Definition at line 209 of file SquanderKodkodPart2Impl.java.
References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getLitNameForObject(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.lit2atom, and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getBounds(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostUpper().
| Bounds edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds | ( | ) | [protected] |
Reimplemented from edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.
Definition at line 42 of file SquanderKodkodPart2Impl.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.args, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.boundLocalVar(), 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.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.SquanderKodkodPart2Impl.getBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostLowerUpper(), 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.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.
| TupleSet [] edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getBounds | ( | ForgeVariable | var, | |
| TupleFactory | f | |||
| ) | [private] |
Definition at line 170 of file SquanderKodkodPart2Impl.java.
References edu.mit.csail.sdg.squander.engine.Heap2Bounds.bounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.conv2tuples(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.fconv, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getExtent(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2Lit().
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.boundLocalVar(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds().
| TupleSet edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getExtent | ( | ForgeVariable | var, | |
| TupleFactory | f | |||
| ) | [private] |
Definition at line 187 of file SquanderKodkodPart2Impl.java.
References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitions.
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getBounds(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostUpper().
| String edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getLitNameForObject | ( | Object | obj | ) | [private] |
Definition at line 229 of file SquanderKodkodPart2Impl.java.
References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.forgeScene, and edu.mit.csail.sdg.squander.spec.ForgeScene.instLitForObj().
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.conv2tuples().
| TupleSet edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostLower | ( | GlobalVariable | g, | |
| TupleSet | initialBound, | |||
| TupleFactory | f | |||
| ) | [protected] |
Definition at line 110 of file SquanderKodkodPart2Impl.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.SquanderKodkodImpl.forgeScene, edu.mit.csail.sdg.squander.spec.ForgeScene.instLitForObj(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.join(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.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.SquanderKodkodPart2Impl.getPostLowerUpper().
| TupleSet [] edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostLowerUpper | ( | GlobalVariable | var, | |
| TupleSet | lowerInitial, | |||
| TupleFactory | f | |||
| ) | [private] |
Definition at line 104 of file SquanderKodkodPart2Impl.java.
References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostLower(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostUpper().
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds().
| TupleSet edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostUpper | ( | GlobalVariable | var, | |
| TupleSet | postLower, | |||
| TupleFactory | f | |||
| ) | [protected] |
Definition at line 133 of file SquanderKodkodPart2Impl.java.
References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.conv2tuples(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getExtent(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.join(), 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.SquanderKodkodPart2Impl.getPostLowerUpper().
| TupleSet edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.join | ( | TupleSet | ts1, | |
| TupleSet | ts2, | |||
| TupleFactory | f | |||
| ) | [private] |
Definition at line 147 of file SquanderKodkodPart2Impl.java.
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostLower(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostUpper().
The documentation for this class was generated from the following file:
- src/edu/mit/csail/sdg/squander/engine/kk/SquanderKodkodPart2Impl.java
