edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK Class Reference
Inherits forge::program::ExpressionVisitor< Node >.
Classes | |
| class | StackElem |
Protected Member Functions | |
| Expression | visit (ForgeType ftype) |
| Node | visit (ForgeLiteral lit) |
| Expression | visit (ForgeVariable var) |
| Node | visit (UnaryExpression expr) |
| Node | visit (BinaryExpression expr) |
| Node | visit (ConditionalExpression expr) |
| Node | visit (ProjectionExpression expr) |
| Node | visit (QuantifyExpression expr) |
| Node | visit2 (QuantifyExpression expr) |
| Expression | visit (OldExpression expr) |
Private Member Functions | |
| Expression | visitForgeType (ForgeType ftype) |
| Node | fix (Formula quantFormula) |
| Expression | getRelForVarAndCheck (ForgeVariable var) |
| StackElem | searchStack (String varName) |
Private Attributes | |
| final Stack< StackElem > | quantStack = new Stack<StackElem>() |
Detailed Description
Translates Forge expressions to Kodkod expressions/formulas
Definition at line 239 of file SquanderKodkodImpl.java.
Member Function Documentation
| Node edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.fix | ( | Formula | quantFormula | ) | [private] |
Definition at line 615 of file SquanderKodkodImpl.java.
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit2().
| Expression edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.getRelForVarAndCheck | ( | ForgeVariable | var | ) | [private] |
Definition at line 652 of file SquanderKodkodImpl.java.
References 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.SquanderKodkodImpl.Tr2KK.visit().
| StackElem edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.searchStack | ( | String | varName | ) | [private] |
Definition at line 658 of file SquanderKodkodImpl.java.
References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.StackElem.name, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.quantStack.
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit().
| Expression edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit | ( | OldExpression | expr | ) | [protected] |
| Node edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit | ( | QuantifyExpression | expr | ) | [protected] |
Definition at line 482 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.kk.SquanderKodkodImpl.node2expr(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.node2form(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.quantStack, edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.trueRelation, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit2().
| Node edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit | ( | ProjectionExpression | expr | ) | [protected] |
Definition at line 471 of file SquanderKodkodImpl.java.
References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.node2expr().
| Node edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit | ( | ConditionalExpression | expr | ) | [protected] |
Definition at line 463 of file SquanderKodkodImpl.java.
References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.node2expr(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.node2form().
| Node edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit | ( | BinaryExpression | expr | ) | [protected] |
| Node edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit | ( | UnaryExpression | expr | ) | [protected] |
| Expression edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit | ( | ForgeVariable | var | ) | [protected] |
Definition at line 294 of file SquanderKodkodImpl.java.
References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.getRelForVarAndCheck(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.searchStack(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.StackElem.var.
| Node edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit | ( | ForgeLiteral | lit | ) | [protected] |
Definition at line 285 of file SquanderKodkodImpl.java.
References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.lit2rel.
| Expression edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit | ( | ForgeType | ftype | ) | [protected] |
Definition at line 254 of file SquanderKodkodImpl.java.
References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.type2expr, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visitForgeType().
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit2().
| Node edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit2 | ( | QuantifyExpression | expr | ) | [protected] |
Definition at line 556 of file SquanderKodkodImpl.java.
References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.fix(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.node2form(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.node2int(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.quantStack, and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit().
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit().
| Expression edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visitForgeType | ( | ForgeType | ftype | ) | [private] |
Definition at line 263 of file SquanderKodkodImpl.java.
References edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.type2expr.
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.visit().
Member Data Documentation
final Stack<StackElem> edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.Tr2KK.quantStack = new Stack<StackElem>() [private] |
The documentation for this class was generated from the following file:
- src/edu/mit/csail/sdg/squander/engine/kk/SquanderKodkodImpl.java
