public class MergeWithPredicateAbstractionFactory extends MergeWithPredicateAbstraction
MergeWithPredicateAbstraction
which is itself a
MergeProcedure
. This class is used by the merge rule completion GUI
which needs in instance for every merge procedure (
MergeWithPredicateAbstraction
cannot be statically instantiated since
it depends on the list of predicates).
MergeWithPredicateAbstractionFactory
is a Singleton.MergeProcedure.ValuesMergeResult
Modifier and Type | Field and Description |
---|---|
private static MergeWithPredicateAbstractionFactory |
INSTANCE |
Modifier | Constructor and Description |
---|---|
private |
MergeWithPredicateAbstractionFactory()
Hidden constructor since this class is a Singleton.
|
Modifier and Type | Method and Description |
---|---|
boolean |
complete()
Similar to
AbstractBuiltInRuleApp.complete() . |
static MergeWithPredicateAbstractionFactory |
instance() |
MergeWithPredicateAbstraction |
instantiate(java.lang.Iterable<AbstractionPredicate> predicates,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> userChoices)
Creates a complete instance of
MergeWithPredicateAbstraction . |
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.
|
java.lang.String |
toString() |
addPredicate, addPredicates, getAbstractDomainForSort, getLatticeType, getPredicates, getUserChoices, instantiateAbstractDomain, setPredicates
requiresDistinguishablePathConditions
getMergeProcedures, getProcedureByName
private static final MergeWithPredicateAbstractionFactory INSTANCE
private MergeWithPredicateAbstractionFactory()
public static MergeWithPredicateAbstractionFactory instance()
MergeWithPredicateAbstractionFactory
.public MergeProcedure.ValuesMergeResult mergeValuesInStates(Term v, SymbolicExecutionState state1, Term valueInState1, SymbolicExecutionState state2, Term valueInState2, Term distinguishingFormula, Services services)
MergeProcedure
mergeValuesInStates
in class MergeWithLatticeAbstraction
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 complete()
MergeProcedure
AbstractBuiltInRuleApp.complete()
. Method was
introduced for predicate abstraction (which is not complete if the
abstraction predicates are not set).complete
in class MergeWithPredicateAbstraction
public MergeWithPredicateAbstraction instantiate(java.lang.Iterable<AbstractionPredicate> predicates, java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType, java.util.LinkedHashMap<ProgramVariable,AbstractDomainElement> userChoices)
MergeWithPredicateAbstraction
.predicates
- The predicates for the lattices to create.latticeType
- The concrete lattice type which determines how abstract
elements are generated from abstraction predicates.MergeWithPredicateAbstraction
.public java.lang.String toString()
toString
in class MergeWithPredicateAbstraction