forge.util
Class ExpressionUtil

java.lang.Object
  extended by forge.util.ExpressionUtil

public final class ExpressionUtil
extends java.lang.Object

Utilities with expressions.

Author:
Kuat Yessenov (kuat@mit.edu), Greg Dennis (gdennis@mit.edu)

Method Summary
static ForgeExpression bringToPostState(ForgeExpression expr)
          Replace old expressions with variables under it.
static ForgeExpression bringToPreState(ForgeExpression expr)
          Replace all global variables with old expressions on these global variables.
static java.util.Set<ForgeExpression.Modifiable> findModifiables(ForgeExpression expr)
          Returns the set of variables found in the given expression, provided the expression does not contain any old expressions.
static java.util.Set<ForgeExpression> flatten(ForgeExpression expr)
          Flattens conjunctions into a set of top-level constraints.
static java.lang.String prettyPrint(ForgeExpression expr)
          Pretty-prints the given expression to the given PrintStream.
static ForgeExpression replaceVariable(ForgeExpression expr, ForgeVariable from, ForgeVariable to)
          Replace all occurrences of variable from to variable to.
static ForgeExpression replaceVariables(ForgeExpression expr, java.util.Map<ForgeVariable,ForgeVariable> map)
          Replaces variables according to the map (map is from variables to be replaced to their desired replacements.)
static java.util.Set<kodkod.ast.Formula> roots(kodkod.ast.Formula formula)
          Returns the non-trivial roots the formula.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Method Detail

bringToPostState

public static ForgeExpression bringToPostState(ForgeExpression expr)
Replace old expressions with variables under it.


bringToPreState

public static ForgeExpression bringToPreState(ForgeExpression expr)
Replace all global variables with old expressions on these global variables.


replaceVariable

public static ForgeExpression replaceVariable(ForgeExpression expr,
                                              ForgeVariable from,
                                              ForgeVariable to)
Replace all occurrences of variable from to variable to.


replaceVariables

public static ForgeExpression replaceVariables(ForgeExpression expr,
                                               java.util.Map<ForgeVariable,ForgeVariable> map)
Replaces variables according to the map (map is from variables to be replaced to their desired replacements.)


prettyPrint

public static java.lang.String prettyPrint(ForgeExpression expr)
Pretty-prints the given expression to the given PrintStream. (Note: System.out is a PrintStream).


flatten

public static java.util.Set<ForgeExpression> flatten(ForgeExpression expr)
Flattens conjunctions into a set of top-level constraints.


findModifiables

public static java.util.Set<ForgeExpression.Modifiable> findModifiables(ForgeExpression expr)
Returns the set of variables found in the given expression, provided the expression does not contain any old expressions.


roots

public static java.util.Set<kodkod.ast.Formula> roots(kodkod.ast.Formula formula)
Returns the non-trivial roots the formula.