public class JoinIfThenElseAntecedent extends JoinProcedure
JoinIfThenElse
rule, the distinction is not realized in the update /
symbolic state, but in the antecedent / path condition.
This can be much more efficient.JoinIfThenElse
,
JoinRule
Modifier and Type | Field and Description |
---|---|
private static String |
DISPLAY_NAME |
private static JoinIfThenElseAntecedent |
INSTANCE |
Constructor and Description |
---|
JoinIfThenElseAntecedent() |
Modifier and Type | Method and Description |
---|---|
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 JoinIfThenElseAntecedent |
instance() |
Triple<ImmutableSet<Term>,Term,ImmutableSet<Name>> |
joinValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services)
Joins two values valueInState1 and valueInState2 of corresponding SE
states state1 and state2 to a new value of a join state.
|
boolean |
requiresDistinguishablePathConditions() |
String |
toString() |
getJoinProcedures, getProcedureByName
private static JoinIfThenElseAntecedent INSTANCE
private static final String DISPLAY_NAME
public static JoinIfThenElseAntecedent instance()
public Triple<ImmutableSet<Term>,Term,ImmutableSet<Name>> joinValuesInStates(Term v, SymbolicExecutionState state1, Term valueInState1, SymbolicExecutionState state2, Term valueInState2, Term distinguishingFormula, Services services)
JoinProcedure
joinValuesInStates
in class JoinProcedure
v
- The variable for which the values should be joinedstate1
- 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 JoinProcedure
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.