public class DependencyContractCompletion extends java.lang.Object implements InteractiveRuleApplicationCompletion
Modifier and Type | Class and Description |
---|---|
static class |
DependencyContractCompletion.TermStringWrapper |
Constructor and Description |
---|
DependencyContractCompletion() |
Modifier and Type | Method and Description |
---|---|
boolean |
canComplete(IBuiltInRuleApp app)
checks if this instance is responsible for the given app
|
static boolean |
checkCanComplete(IBuiltInRuleApp app)
Checks if the app is supported.
|
IBuiltInRuleApp |
complete(IBuiltInRuleApp app,
Goal goal,
boolean forced)
method called to complete the given builtin rule application
|
static void |
extractHeaps(java.util.List<LocationVariable> heapContext,
java.util.List<PosInOccurrence> steps,
DependencyContractCompletion.TermStringWrapper[] heaps,
LogicPrinter lp) |
static PosInOccurrence |
findCorrespondingStep(java.util.List<PosInOccurrence> steps,
Term[] resultHeaps) |
private static PosInOccurrence |
letUserChooseStep(java.util.List<LocationVariable> heapContext,
java.util.List<PosInOccurrence> steps,
boolean forced,
Services services)
collects all possible heaps and presents them to the user for selection.
|
public IBuiltInRuleApp complete(IBuiltInRuleApp app, Goal goal, boolean forced)
InteractiveRuleApplicationCompletion
complete
in interface InteractiveRuleApplicationCompletion
app
- the app to completegoal
- the goal where the app will be appliedforced
- a boolean indicating if the user shall be bothered if the instantiation is unique or
can be chosen in a reasonable way as if uniqueprivate static PosInOccurrence letUserChooseStep(java.util.List<LocationVariable> heapContext, java.util.List<PosInOccurrence> steps, boolean forced, Services services)
steps
- forced
- services
- public static PosInOccurrence findCorrespondingStep(java.util.List<PosInOccurrence> steps, Term[] resultHeaps)
public static void extractHeaps(java.util.List<LocationVariable> heapContext, java.util.List<PosInOccurrence> steps, DependencyContractCompletion.TermStringWrapper[] heaps, LogicPrinter lp)
public boolean canComplete(IBuiltInRuleApp app)
InteractiveRuleApplicationCompletion
canComplete
in interface InteractiveRuleApplicationCompletion
app
- the rule apppublic static boolean checkCanComplete(IBuiltInRuleApp app)