public class ExprUtil
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
ExprUtil.SatResult |
Constructor and Description |
---|
ExprUtil() |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
AstToString(za.ac.sun.cs.green.expr.Expression expression)
Pretty print method to print Green expression.
|
static Stmt |
compose(Stmt s1,
Stmt s2,
boolean allowBothNull) |
static za.ac.sun.cs.green.expr.Expression |
createGreenVar(java.lang.String type,
java.lang.String varId)
Creates a Green variable depending on its type.
|
static ExprUtil.SatResult |
foldBooleanOp(za.ac.sun.cs.green.expr.Operation operation) |
static java.lang.String |
getConstantType(za.ac.sun.cs.green.expr.Expression expr) |
static java.lang.String |
getGreenVariableType(za.ac.sun.cs.green.expr.Expression expr) |
static gov.nasa.jpf.symbc.numeric.Expression |
greenToSPFExpression(za.ac.sun.cs.green.expr.Expression greenExpression)
Translates Green Expession to SPF.
|
static boolean |
isConstant(za.ac.sun.cs.green.expr.Expression expr) |
static boolean |
isPCSat(gov.nasa.jpf.symbc.numeric.PathCondition pc) |
static ExprUtil.SatResult |
isSatGreenExpression(za.ac.sun.cs.green.expr.Expression expression) |
static boolean |
isSatisfiable(gov.nasa.jpf.symbc.numeric.PathCondition pc) |
static boolean |
isVariable(za.ac.sun.cs.green.expr.Expression expr) |
static za.ac.sun.cs.green.expr.Expression |
SPFToGreenExpr(gov.nasa.jpf.symbc.numeric.Expression spfExp)
Translates an SPF expression to a Green Expression.
|
static za.ac.sun.cs.green.expr.Expression |
translateNotExpr(za.ac.sun.cs.green.expr.Operation op) |
public static za.ac.sun.cs.green.expr.Expression SPFToGreenExpr(gov.nasa.jpf.symbc.numeric.Expression spfExp)
spfExp
- SPF Expressionpublic static java.lang.String AstToString(za.ac.sun.cs.green.expr.Expression expression)
expression
- Green expression.public static gov.nasa.jpf.symbc.numeric.Expression greenToSPFExpression(za.ac.sun.cs.green.expr.Expression greenExpression)
greenExpression
- A Green expression to be translated to SPF.public static za.ac.sun.cs.green.expr.Expression createGreenVar(java.lang.String type, java.lang.String varId)
type
- Type of the variable.varId
- Name of the variable.public static boolean isConstant(za.ac.sun.cs.green.expr.Expression expr)
public static boolean isVariable(za.ac.sun.cs.green.expr.Expression expr)
public static java.lang.String getConstantType(za.ac.sun.cs.green.expr.Expression expr)
public static java.lang.String getGreenVariableType(za.ac.sun.cs.green.expr.Expression expr)
public static boolean isPCSat(gov.nasa.jpf.symbc.numeric.PathCondition pc) throws StaticRegionException
StaticRegionException
public static boolean isSatisfiable(gov.nasa.jpf.symbc.numeric.PathCondition pc) throws StaticRegionException
StaticRegionException
public static ExprUtil.SatResult isSatGreenExpression(za.ac.sun.cs.green.expr.Expression expression)
public static ExprUtil.SatResult foldBooleanOp(za.ac.sun.cs.green.expr.Operation operation)
public static za.ac.sun.cs.green.expr.Expression translateNotExpr(za.ac.sun.cs.green.expr.Operation op)