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 |
---|---|
private static java.lang.String |
DISPLAY_NAME |
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 |
private static java.lang.String |
MERGED_NODE_IS_WEAKENING_TITLE |
private static Name |
RULE_NAME |
Modifier | Constructor and Description |
---|---|
private |
CloseAfterMerge() |
Modifier and Type | Method and Description |
---|---|
private Term |
allClosure(Term term,
java.util.HashSet<Function> constsToReplace,
Services services)
Universally closes all logical variables in the given term.
|
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
|
private Term |
getSyntacticWeakeningFormula(CloseAfterMergeRuleBuiltInRuleApp closeApp,
Goal isWeakeningGoal)
Constructs the actual syntactic weakening formula \phi(s1, s2) expressing
that s2 is a weakening of s1.
|
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
|
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
private static final java.lang.String MERGED_NODE_IS_WEAKENING_TITLE
private static final java.lang.String DISPLAY_NAME
private static final Name RULE_NAME
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
private Term getSyntacticWeakeningFormula(CloseAfterMergeRuleBuiltInRuleApp closeApp, Goal isWeakeningGoal)
closeApp
- The rule application containing the required data.isWeakeningGoal
- The Proof
Goal
for the logical weakening
formula.CloseAfterMergeRuleBuiltInRuleApp
.private Term allClosure(Term term, java.util.HashSet<Function> constsToReplace, Services services)
term
- Term to universally close.constsToReplace
- Skolem constants to replace before the universal closure.services
- The services object.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
.