public class SimplifyIfThenElseUpdateCondition extends java.lang.Object implements VariableCondition
Modifier and Type | Class and Description |
---|---|
private static class |
SimplifyIfThenElseUpdateCondition.ElementaryUpdateWrapper |
Modifier and Type | Field and Description |
---|---|
private FormulaSV |
commonFormula |
private FormulaSV |
phi |
private SchemaVariable |
result |
private UpdateSV |
u1 |
private UpdateSV |
u2 |
Constructor and Description |
---|
SimplifyIfThenElseUpdateCondition(FormulaSV phi,
UpdateSV u1,
UpdateSV u2,
FormulaSV commonFormula,
SchemaVariable result) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
private boolean |
collect(java.util.TreeMap<UpdateableOperator,SimplifyIfThenElseUpdateCondition.ElementaryUpdateWrapper> map,
Term update,
boolean firstTerm,
TermServices services) |
private void |
collectSingleTerm(java.util.TreeMap<UpdateableOperator,SimplifyIfThenElseUpdateCondition.ElementaryUpdateWrapper> map,
Term update,
boolean firstTerm,
TermServices services) |
private java.util.TreeMap<UpdateableOperator,SimplifyIfThenElseUpdateCondition.ElementaryUpdateWrapper> |
createMap() |
private java.util.TreeSet<UpdateableOperator> |
createTree() |
private Term |
simplify(Term phi,
Term u1,
Term u2,
Term t,
TermServices services) |
private final FormulaSV phi
private final UpdateSV u1
private final UpdateSV u2
private final FormulaSV commonFormula
private final SchemaVariable result
public SimplifyIfThenElseUpdateCondition(FormulaSV phi, UpdateSV u1, UpdateSV u2, FormulaSV commonFormula, SchemaVariable result)
private java.util.TreeMap<UpdateableOperator,SimplifyIfThenElseUpdateCondition.ElementaryUpdateWrapper> createMap()
private java.util.TreeSet<UpdateableOperator> createTree()
private void collectSingleTerm(java.util.TreeMap<UpdateableOperator,SimplifyIfThenElseUpdateCondition.ElementaryUpdateWrapper> map, Term update, boolean firstTerm, TermServices services)
private boolean collect(java.util.TreeMap<UpdateableOperator,SimplifyIfThenElseUpdateCondition.ElementaryUpdateWrapper> map, Term update, boolean firstTerm, TermServices services)
public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc, Services services)
VariableCondition
check
in interface VariableCondition
var
- the SchemaVariable to be instantiatedinstCandidate
- the SVSubstitute (e.g. Term, ProgramElement) to be mapped to varmc
- the MatchCondition with the current matching state and in particular
the SVInstantiations that are already known to be neededservices
- the program information objectnull
otherwise