public interface _BranchExistsRule extends _AbstractRule
nextBranchExistsSubgoal()
and hasNextBranchExistsSubgoal()
.
numberOfBranchExistsSubgoals()
returns a value grater than zero;
nextBranchExistsSubgoal()
can be safely invoked at least once
returning a non null value.
When the engine applies an instance of a branch-exists rule, it invokes
nextBranchExistsSubgoal()
to get the new goal, then it invokes
hasNextBranchExistsSubgoal()
to check if the rule has more subgoals.
If this is the case the engine stores the rule application in its internal
stack as an OR-branch point.
When a branch in the proof-search fails, the engine searches the stack for an
OR-branch-point. If the stack does not contain any backtrack point, the
engine stops and the proof-search is unsuccessful. Otherwise, the rule
application stored in the OR-branch point is restored. If the rule
application is an instance of _BranchExistsRule
, then the engine
invokes nextBranchExistsSubgoal()
to determine the new goal. Then
the engine invokes hasNextBranchExistsSubgoal()
to check if the rule
application has more subgoals. If this is the case the engine keeps the
OR-branch point in the stack otherwise it pop the OR-branch point from the
stack.
Modifier and Type | Method and Description |
---|---|
boolean |
hasNextBranchExistsSubgoal()
Returns true if this rule has a next subgoal.
|
_AbstractFormula |
mainFormula()
The main formula of this rule or
null if this rule does not
have a main formula. |
_AbstractGoal |
nextBranchExistsSubgoal()
Returns the next subgoal of this rule.
|
int |
numberOfBranchExistsSubgoals()
Returns the number of subgoals of this rule application.
|
name
int numberOfBranchExistsSubgoals()
_AbstractFormula mainFormula()
null
if this rule does not
have a main formula.null
._AbstractGoal nextBranchExistsSubgoal()
boolean hasNextBranchExistsSubgoal()