public class CloseAfterJoin extends Object implements BuiltInRule
TODO: If a user attempts to prune away a "closed" partner node, he/she should also be asked whether the corresponding join 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 join branch into master).
Modifier and Type | Field and Description |
---|---|
private static String |
DISPLAY_NAME |
static CloseAfterJoin |
INSTANCE |
private static String |
JOIN_GENERATE_IS_WEAKENING_GOAL_CFG |
private static String |
JOIN_GENERATE_IS_WEAKENING_GOAL_CFG_ON |
private static String |
JOINED_NODE_IS_WEAKENING_TITLE |
private static Name |
RULE_NAME |
Modifier | Constructor and Description |
---|---|
private |
CloseAfterJoin() |
Modifier and Type | Method and Description |
---|---|
private Term |
allClosure(Term term,
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.
|
CloseAfterJoinRuleBuiltInRuleApp |
createApp(PosInOccurrence pio,
Node thePartnerNode,
Node correspondingJoinNode,
SymbolicExecutionState joinNodeState,
SymbolicExecutionState partnerState,
Term pc)
Creates a complete CloseAfterJoinBuiltInRuleApp.
|
IBuiltInRuleApp |
createApp(PosInOccurrence pos,
TermServices services) |
String |
displayName()
returns the display name of the rule
|
private Term |
getSyntacticWeakeningFormula(Services services,
CloseAfterJoinRuleBuiltInRuleApp closeApp)
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
|
private static final String JOIN_GENERATE_IS_WEAKENING_GOAL_CFG
private static final String JOIN_GENERATE_IS_WEAKENING_GOAL_CFG_ON
private static final String JOINED_NODE_IS_WEAKENING_TITLE
private static final String DISPLAY_NAME
private static final Name RULE_NAME
public static final CloseAfterJoin INSTANCE
public 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(Services services, CloseAfterJoinRuleBuiltInRuleApp closeApp)
services
- The services object.closeApp
- The rule application containing the required data.private Term allClosure(Term term, 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 CloseAfterJoinRuleBuiltInRuleApp createApp(PosInOccurrence pio, Node thePartnerNode, Node correspondingJoinNode, SymbolicExecutionState joinNodeState, SymbolicExecutionState partnerState, Term pc)
pio
- Position of the Update-ProgramCounter formula.thePartnerNode
- The partner node to close.correspondingJoinNode
- The corresponding join 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.joinNodeState
- The SE state for the join node; needed for adding an
implicative premise ensuring the soundness of join 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).CloseAfterJoinRuleBuiltInRuleApp
.