public class MergeByIfThenElse extends MergeProcedure implements UnparametricMergeProcedure
MergeIfThenElseAntecedent
.MergeIfThenElseAntecedent
,
MergeRule
MergeProcedure.ValuesMergeResult
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
DISPLAY_NAME |
private static MergeByIfThenElse |
INSTANCE |
(package private) static int |
MAX_UPDATE_TERM_DEPTH_FOR_CHECKING |
private static int |
SIMPLIFICATION_TIMEOUT_MS
Time in milliseconds after which a simplification attempt of a
distinguishing formula times out.
|
Constructor and Description |
---|
MergeByIfThenElse() |
Modifier and Type | Method and Description |
---|---|
boolean |
complete()
Similar to
AbstractBuiltInRuleApp.complete() . |
(package private) static Quadruple<Term,Term,Term,java.lang.Boolean> |
createDistFormAndRightSidesForITEUpd(LocationVariable v,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Services services)
Creates the input for an if-then-else update for the variable v.
|
(package private) static Quadruple<Term,Term,Term,java.lang.Boolean> |
createDistFormAndRightSidesForITEUpd(SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term ifTerm,
Term elseTerm,
Services services)
Creates the input for an if-then-else update.
|
static Term |
createIfThenElseTerm(SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term ifTerm,
Term elseTerm,
Term distinguishingFormula,
Services services)
Creates an if-then-else term for the variable v.
|
static MergeByIfThenElse |
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 MergeByIfThenElse INSTANCE
private static final int SIMPLIFICATION_TIMEOUT_MS
private static final java.lang.String DISPLAY_NAME
static final int MAX_UPDATE_TERM_DEPTH_FOR_CHECKING
public static MergeByIfThenElse 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
public static Term createIfThenElseTerm(SymbolicExecutionState state1, SymbolicExecutionState state2, Term ifTerm, Term elseTerm, Term distinguishingFormula, Services services)
\if (c1) \then (t1) \else (t2)
, where c1 is
the path condition of state1. However, the method also tries an
optimization: The path condition c2 of state2 could be used if it is
shorter than c1. Moreover, equal parts of c1 and c2 could be omitted,
since the condition shall only distinguish between the states.state1
- First state to evaluate.state2
- Second state to evaluate.ifTerm
- The term t1 (in the context of state1).elseTerm
- The term t2 (in the context of state2).distinguishingFormula
- The user-specified distinguishing formula. May be null (for
automatic generation).services
- The services object.\if (c1) \then (t1) \else (t2)
, where the cI are the
path conditions of stateI.static Quadruple<Term,Term,Term,java.lang.Boolean> createDistFormAndRightSidesForITEUpd(LocationVariable v, SymbolicExecutionState state1, SymbolicExecutionState state2, Services services)
{ v := \if (c1) \then (t1) \else (t2) }
, where c1 is the
path condition of state1. However, the method also tries an optimization:
The path condition c2 of state2 could be used if it is shorter than c1.
Moreover, equal parts of c1 and c2 could be omitted, since the condition
shall only distinguish between the states. The first element of the
triple is the discriminating condition, the second and third elements are
the respective parts for the if and else branch.v
- Variable to return the update for.state1
- First state to evaluate.state2
- Second state to evaluate.services
- The services object.{ v := \if (first) \then (second) \else (third) }
,
where first, second and third are the respective components of
the returned triple. The fourth component indicates whether the
path condition of the first (fourth component = false) or the
second (fourth component = true) state was used as a basis for
the condition (first component).static Quadruple<Term,Term,Term,java.lang.Boolean> createDistFormAndRightSidesForITEUpd(SymbolicExecutionState state1, SymbolicExecutionState state2, Term ifTerm, Term elseTerm, Services services)
{ v := \if (c1) \then (ifTerm) \else (elseTerm) }
, where c1
is the path condition of state1. However, the method also tries an
optimization: The path condition c2 of state2 could be used if it is
shorter than c1. Moreover, equal parts of c1 and c2 could be omitted,
since the condition shall only distinguish between the states. The first
element of the triple is the discriminating condition, the second and
third elements are the respective parts for the if and else branch.state1
- First state to evaluate.state2
- Second state to evaluate.ifTerm
- The if term.elseTerm
- The else term.services
- The services object.{ v := \if (first) \then (second) \else (third) }
,
where first, second and third are the respective components of
the returned triple. The fourth component indicates whether the
path condition of the first (fourth component = false) or the
second (fourth component = true) state was used as a basis for
the condition (first component).public java.lang.String toString()
toString
in class java.lang.Object