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 | 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
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
Copyright © 2003-2019 The KeY-Project.