| java.lang.Object
 de.uka.ilkd.key.rule.UpdateSimplifier
| UpdateSimplifier | | public class UpdateSimplifier (Code) | | The update simplifier applies updates on tems/formulas. Therefore
it can be initialiazed with a set of simplification rules that
shall be used.
Calling the simplifier from outside must only be done by using
the apply methods. The simplify methods are only for recursive
calls made by the update simplification rules.
|
| UpdateSimplifier | | public UpdateSimplifier()(Code) | | |
| UpdateSimplifier | | public UpdateSimplifier(boolean deletionEnabled, boolean eager)(Code) | | creates an instance of the update simplifier
Parameters:
deletionEnable - a boolean flag indicating if unused or effectless assignment pairs should be removed |
| formulaConstraint | | public Constraint formulaConstraint()(Code) | | returns the formula constraint of the formula to be simpliefied
the formula constraint |
| matchingCondition | | public Term matchingCondition(Update update, Term target, Services services)(Code) | | Derive a formula that describes in which cases the top-level operator
(location) described by target is updated by the given
update.
Parameters:
update - the modification of function interpretations that isconsidered
Parameters:
target - description of the location we are interested in;precondition: target.op() instanceof Location
Parameters:
services - services object formula that evaluates to true iff updateevaluates to a semantic update that affects the locationdescribed by target |
| setSimplificationRules | | public void setSimplificationRules(ListOfIUpdateRule rules)(Code) | | Uses the given rules for update simplification. The order is
important as the first applicable rule is taken.
Parameters:
rules - a ListOfUpdateRule to use for updatesimplification |
|
|