edu.mit.csail.sdg.squander.engine.SquanderEval2 Class Reference
[Engine]
Inherits forge::program::ExpressionVisitor< ObjTupleSet >.
Classes | |
| interface | BinFunc< R, T > |
| class | StackElem |
Public Member Functions | |
| Map< ForgeVariable, ObjTupleSet > | getAssignments () |
| ISquanderResult.IEvaluator | getEvaluator () |
| ObjTupleSet | eval (ForgeExpression expr, ForgeConverter fconv) |
Protected Member Functions | |
| ObjTupleSet | visit (BinaryExpression expr) |
| ObjTupleSet | visit (ConditionalExpression expr) |
| ObjTupleSet | visit (ForgeLiteral expr) |
| ObjTupleSet | visit (ForgeType expr) |
| ObjTupleSet | visit (ForgeVariable expr) |
| ObjTupleSet | visit (OldExpression expr) |
| ObjTupleSet | visit (ProjectionExpression expr) |
| ObjTupleSet | visit (QuantifyExpression expr) |
| ObjTupleSet | visit (UnaryExpression expr) |
Package Functions | |
| private< R > ObjTupleSet | visitIntBinExpr (BinaryExpression expr, BinFunc< R, Integer > f) |
Private Member Functions | |
| ObjTupleSet | visitVariable (ForgeVariable var) |
| ObjTupleSet | visitLocalVariable (LocalVariable var) |
| StackElem | searchStack (LocalVariable var) |
| ObjTupleSet | visitAssignment (BinaryExpression expr) |
| ObjTupleSet | visitEquals (BinaryExpression expr) |
| ObjTupleSet | visitJoin (BinaryExpression expr) |
| ObjTupleSet | visitProduct (BinaryExpression expr) |
| ObjTupleSet | visitRelUnion (BinaryExpression expr) |
| ObjTupleSet | visitDiff (BinaryExpression expr) |
| ObjTupleSet | visitSubset (BinaryExpression expr) |
| ObjTupleSet | visitIntersection (BinaryExpression expr) |
| ObjTupleSet | visitClosure (ObjTupleSet res) |
| ObjTupleSet | visitBoolBinExpr (BinaryExpression expr, BinFunc< Boolean, Boolean > f) |
| ObjTupleSet | visitUnion (QuantifyExpression expr) |
| ObjTupleSet | visitAll (QuantifyExpression expr) |
| ObjTupleSet | visitExists (QuantifyExpression expr) |
Static Private Member Functions | |
| static ObjTupleSet | boolAtom (boolean val) |
| static ObjTupleSet | intAtom (int val) |
| static ObjTupleSet | objAtom (Object obj) |
| static boolean | boolValue (ObjTupleSet condEval) |
| static int | intValue (ObjTupleSet condEval) |
Private Attributes | |
| ForgeConverter | fconv |
| Heap2Bounds | heap2lit |
| boolean | hasSolution = false |
| Stack< StackElem > | quantStack = new Stack<StackElem>() |
| Map< ForgeVariable, ObjTupleSet > | assignments = new HashMap<ForgeVariable, ObjTupleSet>() |
Detailed Description
Used to evaluate relational Forge expressions against the heap. It uses ObjTupleSet instead of ForgeBounds.
Definition at line 35 of file SquanderEval2.java.
Member Function Documentation
| static ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.boolAtom | ( | boolean | val | ) | [static, private] |
Definition at line 431 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitAll(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitAssignment(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitBoolBinExpr(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitEquals(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitExists(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitIntBinExpr(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitSubset().
| static boolean edu.mit.csail.sdg.squander.engine.SquanderEval2.boolValue | ( | ObjTupleSet | condEval | ) | [static, private] |
Definition at line 449 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity, edu.mit.csail.sdg.squander.absstate.ObjTupleSet.isEmpty(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitAll(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitBoolBinExpr(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitExists(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitUnion().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.eval | ( | ForgeExpression | expr, | |
| ForgeConverter | fconv | |||
| ) |
Evaluates the given Forge expression against the given bounds (which represent the heap) and returns an ObjTupleSet as the result of the evaluation.
Definition at line 108 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.hasSolution, edu.mit.csail.sdg.squander.engine.ForgeConverter.heap2Lit(), edu.mit.csail.sdg.squander.engine.SquanderEval2.heap2lit, and edu.mit.csail.sdg.squander.engine.SquanderEval2.quantStack.
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getModLits(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostSpec().
| Map<ForgeVariable, ObjTupleSet> edu.mit.csail.sdg.squander.engine.SquanderEval2.getAssignments | ( | ) |
Definition at line 65 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.assignments.
| ISquanderResult.IEvaluator edu.mit.csail.sdg.squander.engine.SquanderEval2.getEvaluator | ( | ) |
Definition at line 69 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.assignments, and edu.mit.csail.sdg.squander.engine.SquanderEval2.hasSolution.
| static ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.intAtom | ( | int | val | ) | [static, private] |
Definition at line 437 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visitIntBinExpr().
| static int edu.mit.csail.sdg.squander.engine.SquanderEval2.intValue | ( | ObjTupleSet | condEval | ) | [static, private] |
Definition at line 457 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity, and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visitIntBinExpr().
| static ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.objAtom | ( | Object | obj | ) | [static, private] |
Definition at line 443 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.add().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| StackElem edu.mit.csail.sdg.squander.engine.SquanderEval2.searchStack | ( | LocalVariable | var | ) | [private] |
Definition at line 271 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.quantStack.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visitLocalVariable().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visit | ( | UnaryExpression | expr | ) | [protected] |
Definition at line 221 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.boolAtom(), edu.mit.csail.sdg.squander.engine.SquanderEval2.boolValue(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.isEmpty(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.isTuple(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitClosure().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visit | ( | QuantifyExpression | expr | ) | [protected] |
Definition at line 207 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.visitAll(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitExists(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitUnion().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visit | ( | ProjectionExpression | expr | ) | [protected] |
Definition at line 201 of file SquanderEval2.java.
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visit | ( | OldExpression | expr | ) | [protected] |
Definition at line 196 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visit | ( | ForgeVariable | expr | ) | [protected] |
Definition at line 188 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.visitLocalVariable(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitVariable().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visit | ( | ForgeType | expr | ) | [protected] |
Definition at line 183 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.ForgeConverter.extent(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.fconv.
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visit | ( | ForgeLiteral | expr | ) | [protected] |
Definition at line 178 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.fconv, edu.mit.csail.sdg.squander.engine.ForgeConverter.lit2obj(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.objAtom().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visit | ( | ConditionalExpression | expr | ) | [protected] |
Definition at line 168 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.boolValue().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visit | ( | BinaryExpression | expr | ) | [protected] |
Definition at line 118 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.visitBoolBinExpr(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitDiff(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitEquals(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitIntBinExpr(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitIntersection(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitJoin(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitProduct(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitRelUnion(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitSubset().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitAll | ( | QuantifyExpression | expr | ) | [private] |
Definition at line 401 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.boolAtom(), edu.mit.csail.sdg.squander.engine.SquanderEval2.boolValue(), edu.mit.csail.sdg.squander.engine.ForgeConverter.extent(), edu.mit.csail.sdg.squander.engine.SquanderEval2.fconv, edu.mit.csail.sdg.squander.engine.SquanderEval2.quantStack, edu.mit.csail.sdg.squander.absstate.ObjTupleSet.size(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitAssignment | ( | BinaryExpression | expr | ) | [private] |
Definition at line 281 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.assignments, and edu.mit.csail.sdg.squander.engine.SquanderEval2.boolAtom().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitBoolBinExpr | ( | BinaryExpression | expr, | |
| BinFunc< Boolean, Boolean > | f | |||
| ) | [private] |
Definition at line 347 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.boolAtom(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.boolValue().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitClosure | ( | ObjTupleSet | res | ) | [private] |
Definition at line 333 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity, edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples, and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.union().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitDiff | ( | BinaryExpression | expr | ) | [private] |
Definition at line 314 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.diff().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitEquals | ( | BinaryExpression | expr | ) | [private] |
Definition at line 289 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.boolAtom(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.equals().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitExists | ( | QuantifyExpression | expr | ) | [private] |
Definition at line 416 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.boolAtom(), edu.mit.csail.sdg.squander.engine.SquanderEval2.boolValue(), edu.mit.csail.sdg.squander.engine.ForgeConverter.extent(), edu.mit.csail.sdg.squander.engine.SquanderEval2.fconv, edu.mit.csail.sdg.squander.engine.SquanderEval2.quantStack, edu.mit.csail.sdg.squander.absstate.ObjTupleSet.size(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| private<R> ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitIntBinExpr | ( | BinaryExpression | expr, | |
| BinFunc< R, Integer > | f | |||
| ) | [package] |
Definition at line 358 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.boolAtom(), edu.mit.csail.sdg.squander.engine.SquanderEval2.intAtom(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.intValue().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitIntersection | ( | BinaryExpression | expr | ) | [private] |
Definition at line 327 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.intersection().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitJoin | ( | BinaryExpression | expr | ) | [private] |
Definition at line 296 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.join().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitLocalVariable | ( | LocalVariable | var | ) | [private] |
Definition at line 263 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.searchStack(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitVariable().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitProduct | ( | BinaryExpression | expr | ) | [private] |
Definition at line 302 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.product().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitRelUnion | ( | BinaryExpression | expr | ) | [private] |
Definition at line 308 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.union().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitSubset | ( | BinaryExpression | expr | ) | [private] |
Definition at line 321 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval2.boolAtom(), and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.subsetOf().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitUnion | ( | QuantifyExpression | expr | ) | [private] |
Definition at line 384 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.absstate.ObjTupleSet.arity, edu.mit.csail.sdg.squander.engine.SquanderEval2.boolValue(), edu.mit.csail.sdg.squander.engine.ForgeConverter.extent(), edu.mit.csail.sdg.squander.engine.SquanderEval2.fconv, edu.mit.csail.sdg.squander.engine.SquanderEval2.quantStack, edu.mit.csail.sdg.squander.absstate.ObjTupleSet.size(), edu.mit.csail.sdg.squander.absstate.ObjTupleSet.tuples, and edu.mit.csail.sdg.squander.absstate.ObjTupleSet.union().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit().
| ObjTupleSet edu.mit.csail.sdg.squander.engine.SquanderEval2.visitVariable | ( | ForgeVariable | var | ) | [private] |
Definition at line 257 of file SquanderEval2.java.
References edu.mit.csail.sdg.squander.engine.Heap2Bounds.getBound(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.heap2lit.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitLocalVariable().
Member Data Documentation
Map<ForgeVariable, ObjTupleSet> edu.mit.csail.sdg.squander.engine.SquanderEval2.assignments = new HashMap<ForgeVariable, ObjTupleSet>() [private] |
Definition at line 63 of file SquanderEval2.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.getAssignments(), edu.mit.csail.sdg.squander.engine.SquanderEval2.getEvaluator(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitAssignment().
Definition at line 58 of file SquanderEval2.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.visit(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitAll(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitExists(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitUnion().
boolean edu.mit.csail.sdg.squander.engine.SquanderEval2.hasSolution = false [private] |
Definition at line 61 of file SquanderEval2.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.eval(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.getEvaluator().
Definition at line 59 of file SquanderEval2.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.eval(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitVariable().
Stack<StackElem> edu.mit.csail.sdg.squander.engine.SquanderEval2.quantStack = new Stack<StackElem>() [private] |
Definition at line 62 of file SquanderEval2.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval2.eval(), edu.mit.csail.sdg.squander.engine.SquanderEval2.searchStack(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitAll(), edu.mit.csail.sdg.squander.engine.SquanderEval2.visitExists(), and edu.mit.csail.sdg.squander.engine.SquanderEval2.visitUnion().
The documentation for this class was generated from the following file:
- src/edu/mit/csail/sdg/squander/engine/SquanderEval2.java
