public class MergeIfThenElseAntecedent extends MergeProcedure implements UnparametricMergeProcedure
MergeByIfThenElse
rule, the distinction is
not realized in the update / symbolic state, but in the antecedent / path
condition. This can be much more efficient.MergeByIfThenElse
,
MergeRule
MergeProcedure.ValuesMergeResult
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
DISPLAY_NAME |
private static MergeIfThenElseAntecedent |
INSTANCE |
Constructor and Description |
---|
MergeIfThenElseAntecedent() |
Modifier and Type | Method and Description |
---|---|
boolean |
complete()
Similar to
AbstractBuiltInRuleApp.complete() . |
private static ImmutableSet<Term> |
getIfThenElseConstraints(Term constrained,
Term ifTerm,
Term elseTerm,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term distinguishingFormula,
Services services)
Returns a list of if-then-else constraints for the given constrained
term, states and if/else terms.
|
static MergeIfThenElseAntecedent |
instance() |
MergeProcedure.ValuesMergeResult |
mergeValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services)
Merges two values valueInState1 and valueInState2 of corresponding SE
states state1 and state2 to a new value of a merge state.
|
boolean |
requiresDistinguishablePathConditions() |
java.lang.String |
toString() |
getMergeProcedures, getProcedureByName
private static MergeIfThenElseAntecedent INSTANCE
private static final java.lang.String DISPLAY_NAME
public static MergeIfThenElseAntecedent instance()
public boolean complete()
MergeProcedure
AbstractBuiltInRuleApp.complete()
. Method was
introduced for predicate abstraction (which is not complete if the
abstraction predicates are not set).complete
in class MergeProcedure
public MergeProcedure.ValuesMergeResult mergeValuesInStates(Term v, SymbolicExecutionState state1, Term valueInState1, SymbolicExecutionState state2, Term valueInState2, Term distinguishingFormula, Services services)
MergeProcedure
mergeValuesInStates
in class MergeProcedure
v
- The variable for which the values should be mergedstate1
- First SE state.valueInState1
- Value in state1.state2
- Second SE state.valueInState2
- Value in state2.distinguishingFormula
- The user-specified distinguishing formula. May be null (for
automatic generation).services
- The services object.public boolean requiresDistinguishablePathConditions()
requiresDistinguishablePathConditions
in class MergeProcedure
private static ImmutableSet<Term> getIfThenElseConstraints(Term constrained, Term ifTerm, Term elseTerm, SymbolicExecutionState state1, SymbolicExecutionState state2, Term distinguishingFormula, Services services)
constrained
- The constrained term.ifTerm
- The value for the if case.elseTerm
- The value for the else case.state1
- First SE state ("if").state2
- Second SE state ("else").distinguishingFormula
- The user-specified distinguishing formula. May be null (for
automatic generation).services
- The services object.public java.lang.String toString()
toString
in class java.lang.Object