edu.mit.csail.sdg.squander.engine.SquanderEval Class Reference
[Engine]
Inherits forge::program::ExpressionVisitor< ForgeConstant >.
Classes | |
| interface | BinFunc< R, T > |
| class | StackElem |
Public Member Functions | |
| Map< ForgeVariable, ForgeConstant > | getAssignments () |
| ISquanderResult.IEvaluator | getEvaluator () |
| ForgeConstant | eval (ForgeExpression expr, ForgeBounds bounds, ForgeConverter fconv) |
Protected Member Functions | |
| ForgeConstant | visit (BinaryExpression expr) |
| ForgeConstant | visit (ConditionalExpression expr) |
| ForgeConstant | visit (ForgeLiteral expr) |
| ForgeConstant | visit (ForgeType expr) |
| ForgeConstant | visit (ForgeVariable expr) |
| ForgeConstant | visit (OldExpression expr) |
| ForgeConstant | visit (ProjectionExpression expr) |
| ForgeConstant | visit (QuantifyExpression expr) |
| ForgeConstant | visit (UnaryExpression expr) |
Package Functions | |
| private< R > ForgeConstant | visitIntBinExpr (BinaryExpression expr, BinFunc< R, Integer > f) |
Private Member Functions | |
| ForgeConstant | visitVariable (ForgeVariable var) |
| ForgeConstant | visitLocalVariable (LocalVariable var) |
| StackElem | searchStack (LocalVariable var) |
| ForgeConstant | visitAssignment (BinaryExpression expr) |
| ForgeConstant | visitEquals (BinaryExpression expr) |
| ForgeConstant | visitJoin (BinaryExpression expr) |
| ForgeConstant | visitProduct (BinaryExpression expr) |
| ForgeConstant | visitRelUnion (BinaryExpression expr) |
| ForgeConstant | visitDiff (BinaryExpression expr) |
| ForgeConstant | visitSubset (BinaryExpression expr) |
| ForgeConstant | visitIntersection (BinaryExpression expr) |
| ForgeConstant | visitClosure (ForgeConstant res) |
| ForgeConstant | visitBoolBinExpr (BinaryExpression expr, BinFunc< Boolean, Boolean > f) |
| ForgeConstant | visitUnion (QuantifyExpression expr) |
| ForgeConstant | visitAll (QuantifyExpression expr) |
| ForgeConstant | visitExists (QuantifyExpression expr) |
Private Attributes | |
| ForgeBounds | bounds |
| ForgeConverter | fconv |
| boolean | hasSolution = false |
| Stack< StackElem > | quantStack = new Stack<StackElem>() |
| Map< ForgeVariable, ForgeConstant > | assignments = new HashMap<ForgeVariable, ForgeConstant>() |
Detailed Description
Used to evaluate relational Forge expressions against the heap.
Definition at line 42 of file SquanderEval.java.
Member Function Documentation
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.eval | ( | ForgeExpression | expr, | |
| ForgeBounds | bounds, | |||
| ForgeConverter | fconv | |||
| ) |
Evaluates the given Forge expression against the given bounds (which represent the heap) and returns a Forge constant as the result of the evaluation.
Definition at line 115 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.hasSolution, and edu.mit.csail.sdg.squander.engine.SquanderEval.quantStack.
| Map<ForgeVariable, ForgeConstant> edu.mit.csail.sdg.squander.engine.SquanderEval.getAssignments | ( | ) |
Definition at line 71 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.assignments.
| ISquanderResult.IEvaluator edu.mit.csail.sdg.squander.engine.SquanderEval.getEvaluator | ( | ) |
Definition at line 75 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.assignments, edu.mit.csail.sdg.squander.engine.SquanderEval.fconv, and edu.mit.csail.sdg.squander.engine.SquanderEval.hasSolution.
| StackElem edu.mit.csail.sdg.squander.engine.SquanderEval.searchStack | ( | LocalVariable | var | ) | [private] |
Definition at line 283 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.quantStack.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visitLocalVariable().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visit | ( | UnaryExpression | expr | ) | [protected] |
Definition at line 232 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.bounds, and edu.mit.csail.sdg.squander.engine.SquanderEval.visitClosure().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visit | ( | QuantifyExpression | expr | ) | [protected] |
Definition at line 218 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.visitAll(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitExists(), and edu.mit.csail.sdg.squander.engine.SquanderEval.visitUnion().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visit | ( | ProjectionExpression | expr | ) | [protected] |
Definition at line 212 of file SquanderEval.java.
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visit | ( | OldExpression | expr | ) | [protected] |
Definition at line 207 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visit | ( | ForgeVariable | expr | ) | [protected] |
Definition at line 199 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.visitLocalVariable(), and edu.mit.csail.sdg.squander.engine.SquanderEval.visitVariable().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visit | ( | ForgeType | expr | ) | [protected] |
Definition at line 194 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.bounds.
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visit | ( | ForgeLiteral | expr | ) | [protected] |
Definition at line 185 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.bounds.
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visit | ( | ConditionalExpression | expr | ) | [protected] |
Definition at line 175 of file SquanderEval.java.
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visit | ( | BinaryExpression | expr | ) | [protected] |
Definition at line 125 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.visitBoolBinExpr(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitDiff(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitEquals(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitIntBinExpr(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitIntersection(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitJoin(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitProduct(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitRelUnion(), and edu.mit.csail.sdg.squander.engine.SquanderEval.visitSubset().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitAll | ( | QuantifyExpression | expr | ) | [private] |
Definition at line 413 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.bounds, and edu.mit.csail.sdg.squander.engine.SquanderEval.quantStack.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitAssignment | ( | BinaryExpression | expr | ) | [private] |
Definition at line 293 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.assignments, and edu.mit.csail.sdg.squander.engine.SquanderEval.bounds.
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitBoolBinExpr | ( | BinaryExpression | expr, | |
| BinFunc< Boolean, Boolean > | f | |||
| ) | [private] |
Definition at line 359 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.bounds.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitClosure | ( | ForgeConstant | res | ) | [private] |
Definition at line 345 of file SquanderEval.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitDiff | ( | BinaryExpression | expr | ) | [private] |
Definition at line 326 of file SquanderEval.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitEquals | ( | BinaryExpression | expr | ) | [private] |
Definition at line 301 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.bounds.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitExists | ( | QuantifyExpression | expr | ) | [private] |
Definition at line 428 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.bounds, and edu.mit.csail.sdg.squander.engine.SquanderEval.quantStack.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| private<R> ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitIntBinExpr | ( | BinaryExpression | expr, | |
| BinFunc< R, Integer > | f | |||
| ) | [package] |
Definition at line 370 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.bounds.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitIntersection | ( | BinaryExpression | expr | ) | [private] |
Definition at line 339 of file SquanderEval.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitJoin | ( | BinaryExpression | expr | ) | [private] |
Definition at line 308 of file SquanderEval.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitLocalVariable | ( | LocalVariable | var | ) | [private] |
Definition at line 275 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.searchStack(), and edu.mit.csail.sdg.squander.engine.SquanderEval.visitVariable().
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitProduct | ( | BinaryExpression | expr | ) | [private] |
Definition at line 314 of file SquanderEval.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitRelUnion | ( | BinaryExpression | expr | ) | [private] |
Definition at line 320 of file SquanderEval.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitSubset | ( | BinaryExpression | expr | ) | [private] |
Definition at line 333 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.bounds.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitUnion | ( | QuantifyExpression | expr | ) | [private] |
Definition at line 396 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.bounds, and edu.mit.csail.sdg.squander.engine.SquanderEval.quantStack.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit().
| ForgeConstant edu.mit.csail.sdg.squander.engine.SquanderEval.visitVariable | ( | ForgeVariable | var | ) | [private] |
Definition at line 268 of file SquanderEval.java.
References edu.mit.csail.sdg.squander.engine.SquanderEval.bounds.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit(), and edu.mit.csail.sdg.squander.engine.SquanderEval.visitLocalVariable().
Member Data Documentation
Map<ForgeVariable, ForgeConstant> edu.mit.csail.sdg.squander.engine.SquanderEval.assignments = new HashMap<ForgeVariable, ForgeConstant>() [private] |
Definition at line 69 of file SquanderEval.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.getAssignments(), edu.mit.csail.sdg.squander.engine.SquanderEval.getEvaluator(), and edu.mit.csail.sdg.squander.engine.SquanderEval.visitAssignment().
ForgeBounds edu.mit.csail.sdg.squander.engine.SquanderEval.bounds [private] |
Definition at line 65 of file SquanderEval.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.visit(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitAll(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitAssignment(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitBoolBinExpr(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitEquals(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitExists(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitIntBinExpr(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitSubset(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitUnion(), and edu.mit.csail.sdg.squander.engine.SquanderEval.visitVariable().
Definition at line 66 of file SquanderEval.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.getEvaluator().
boolean edu.mit.csail.sdg.squander.engine.SquanderEval.hasSolution = false [private] |
Definition at line 67 of file SquanderEval.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.eval(), and edu.mit.csail.sdg.squander.engine.SquanderEval.getEvaluator().
Stack<StackElem> edu.mit.csail.sdg.squander.engine.SquanderEval.quantStack = new Stack<StackElem>() [private] |
Definition at line 68 of file SquanderEval.java.
Referenced by edu.mit.csail.sdg.squander.engine.SquanderEval.eval(), edu.mit.csail.sdg.squander.engine.SquanderEval.searchStack(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitAll(), edu.mit.csail.sdg.squander.engine.SquanderEval.visitExists(), and edu.mit.csail.sdg.squander.engine.SquanderEval.visitUnion().
The documentation for this class was generated from the following file:
- src/edu/mit/csail/sdg/squander/engine/SquanderEval.java
