public class CloseAfterMerge extends java.lang.Object implements BuiltInRule
TODO: If a user attempts to prune away a "closed" partner node, he/she should also be asked whether the corresponding merge node should also be pruned. Otherwise, the user might accidentally make it harder to close the whole proof (Add this to the bug tracker after merging the merge branch into master).
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
FINAL_WEAKENING_TERM_HINT
Hint to refactor the final weakening term.
|
static CloseAfterMerge |
INSTANCE |
static java.lang.String |
MERGE_GENERATE_IS_WEAKENING_GOAL_CFG |
static java.lang.String |
MERGE_GENERATE_IS_WEAKENING_GOAL_CFG_ON |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
CloseAfterMergeRuleBuiltInRuleApp |
createApp(PosInOccurrence pio,
Node thePartnerNode,
Node correspondingMergeNode,
SymbolicExecutionState mergeNodeState,
SymbolicExecutionState partnerState,
Term pc,
java.util.Set<Name> newNames)
Creates a complete CloseAfterMergeBuiltInRuleApp.
|
IBuiltInRuleApp |
createApp(PosInOccurrence pos,
TermServices services) |
java.lang.String |
displayName()
returns the display name of the rule
|
boolean |
isApplicable(Goal goal,
PosInOccurrence pio)
returns true iff a rule is applicable at the given
position.
|
boolean |
isApplicableOnSubTerms() |
Name |
name()
the name of the rule
|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getOrigin
public static final java.lang.String MERGE_GENERATE_IS_WEAKENING_GOAL_CFG
public static final java.lang.String MERGE_GENERATE_IS_WEAKENING_GOAL_CFG_ON
public static final CloseAfterMerge INSTANCE
public static final java.lang.String FINAL_WEAKENING_TERM_HINT
public java.lang.String displayName()
Rule
displayName
in interface Rule
public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp) throws RuleAbortException
Rule
apply
in interface Rule
goal
- the Goal on which to apply ruleAppservices
- the Services with the necessary information
about the java programsruleApp
- the rule application to be executedRuleAbortException
public boolean isApplicable(Goal goal, PosInOccurrence pio)
BuiltInRule
isApplicable
in interface BuiltInRule
public boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule
public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services)
createApp
in interface BuiltInRule
public CloseAfterMergeRuleBuiltInRuleApp createApp(PosInOccurrence pio, Node thePartnerNode, Node correspondingMergeNode, SymbolicExecutionState mergeNodeState, SymbolicExecutionState partnerState, Term pc, java.util.Set<Name> newNames)
pio
- Position of the Update-ProgramCounter formula.thePartnerNode
- The partner node to close.correspondingMergeNode
- The corresponding merge node that is not closed. This is
needed to add a reference to its parent in the partner goal at
the place of this rule application.mergeNodeState
- The SE state for the merge node; needed for adding an
implicative premise ensuring the soundness of merge rules.partnerState
- The SE state for the partner node.pc
- The program counter common to the two states -- a formula of
the form U\<{...}\> PHI, where U is an update in normal form
and PHI is a DL formula).newNames
- The set of new names (of Skolem constants) introduced in the
merge.CloseAfterMergeRuleBuiltInRuleApp
.Copyright © 2003-2019 The KeY-Project.