Package | Description |
---|---|
de.uka.ilkd.key.gui.mergerule | |
de.uka.ilkd.key.gui.mergerule.predicateabstraction | |
de.uka.ilkd.key.rule.merge | |
de.uka.ilkd.key.util.mergerule |
Modifier and Type | Method and Description |
---|---|
ImmutableList<MergePartner> |
MergePartnerSelectionDialog.getChosenCandidates() |
Modifier and Type | Method and Description |
---|---|
abstract C |
MergeProcedureCompletion.complete(C proc,
Pair<Goal,PosInOccurrence> mergeGoalPio,
java.util.Collection<MergePartner> partners)
Completes the given merge procedure either automatically (if the procedure
is already complete) or by demanding input from the user in a GUI.
|
Constructor and Description |
---|
MergePartnerSelectionDialog(Goal mergeGoal,
PosInOccurrence pio,
ImmutableList<MergePartner> candidates,
Services services)
Creates a new merge partner selection dialog.
|
Modifier and Type | Method and Description |
---|---|
MergeWithPredicateAbstraction |
PredicateAbstractionCompletion.complete(MergeWithPredicateAbstraction proc,
Pair<Goal,PosInOccurrence> joinGoalPio,
java.util.Collection<MergePartner> partners) |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<MergePartner> |
MergeRule.findPotentialMergePartners(Goal goal,
PosInOccurrence pio)
Finds all suitable merge partners
|
ImmutableList<MergePartner> |
MergeRuleBuiltInRuleApp.getMergePartners() |
Modifier and Type | Method and Description |
---|---|
void |
MergeRuleBuiltInRuleApp.setMergePartners(ImmutableList<MergePartner> mergePartners) |
Constructor and Description |
---|
MergeRuleBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
Node mergeNode,
ImmutableList<MergePartner> mergePartners,
MergeProcedure concreteRule,
SymbolicExecutionStateWithProgCnt thisSEState,
ImmutableList<SymbolicExecutionState> mergePartnerStates,
Term distForm,
java.util.ArrayList<MergeRule.MergeRuleProgressListener> progressListeners) |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<SymbolicExecutionState> |
MergeRuleUtils.sequentsToSEPairs(java.lang.Iterable<MergePartner> sequentInfos)
Convenience method for converting a whole list of goal-pio combinations
to symbolic execution states; relies on
MergeRuleUtils.sequentToSETriple(Node, PosInOccurrence, Services) . |
Copyright © 2003-2019 The KeY-Project.