| java.lang.Object
 de.uka.ilkd.key.rule.updatesimplifier.UpdateSimplifierTermFactory
| UpdateSimplifierTermFactory | | public class UpdateSimplifierTermFactory (Code) | | |
| Inner Class :public static interface IfExCascade | |
| Method Summary | |
| public Term | createIfExCascade(IfExCascade cascade, Term defaultTerm)
| | public Term | createUpdateTerm(ArrayOfAssignmentPair assignmentPairs, Term target)
creates an update term out of the given internal representation
used by the update simplifier, i.e. | | public Term | createUpdateTerm(AssignmentPair[] update, Term target)
creates an update term out of the given internal representation
used by the update simplifier, i.e. | | public TermFactory | getBasicTermFactory()
| | public Term | getUnsatisfiableGuard()
| | public Term | getValidGuard()
| | public Term | matchingCondition(IfExCascade cascade)
Compose the formula expressing that at least one of the conditions of an
ifEx-cascade evaluates to true, i.e. | | public AssignmentPair | resolveCollisions(AssignmentPair pair, SetOfQuantifiableVariable criticalVars)
Ensure that none of the variables criticalVars is bound by
pair (turns up in pair.boundVars()). | | public Update | resolveCollisions(Update update, SetOfQuantifiableVariable criticalVars)
Ensure that none of the variables criticalVars is bound by
update. | | public AssignmentPair | substitute(AssignmentPair pair, QuantifiableVariable var, Term substTerm)
Substitute substTerm for the variable var in
the given assignment pair. | | public Update | substitute(Update update, QuantifiableVariable var, Term substTerm)
Substitute substTerm for the variable var in
the given update. |
| createIfExCascade | | public Term createIfExCascade(IfExCascade cascade, Term defaultTerm)(Code) | | |
| createUpdateTerm | | public Term createUpdateTerm(ArrayOfAssignmentPair assignmentPairs, Term target)(Code) | | creates an update term out of the given internal representation
used by the update simplifier, i.e. the assignmentpairs are made
explicit
Parameters:
target - the term evaluated under the update the update term {l1:=r1,...,ln:=rn}target |
| createUpdateTerm | | public Term createUpdateTerm(AssignmentPair[] update, Term target)(Code) | | creates an update term out of the given internal representation
used by the update simplifier, i.e. the assignmentpairs are made
explicit
Parameters:
update - an array of AssignmentPairs l:=r of thesimulataneous update to be created
Parameters:
target - the term evaluated under the update the update term {l1:=r1,...,ln:=rn}target |
| getBasicTermFactory | | public TermFactory getBasicTermFactory()(Code) | | the default termfactory for JavaCardDL terms |
| getUnsatisfiableGuard | | public Term getUnsatisfiableGuard()(Code) | | |
| matchingCondition | | public Term matchingCondition(IfExCascade cascade)(Code) | | Compose the formula expressing that at least one of the conditions of an
ifEx-cascade evaluates to true, i.e. that the result of the
cascade is one of the then-branches (and not the default branch)
|
| resolveCollisions | | public AssignmentPair resolveCollisions(AssignmentPair pair, SetOfQuantifiableVariable criticalVars)(Code) | | Ensure that none of the variables criticalVars is bound by
pair (turns up in pair.boundVars()). When
necessary, variables are renamed to this end
|
| resolveCollisions | | public Update resolveCollisions(Update update, SetOfQuantifiableVariable criticalVars)(Code) | | Ensure that none of the variables criticalVars is bound by
update. When necessary, variables are renamed to this end
|
|
|