public interface _RegularRule extends _AbstractRule
nextSubgoal()
and
hasNextSubgoal()
.
numberOfSubgoals()
returns a value grater than zero;nextSubgoal()
can be safely invoked at least once returning a
non null value.nextSubgoal()
method to get the new goal, then it invokes then it
invokes hasNextSubgoal()
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 AND-branch point.
When a branch in the proof-search succeeds, the engine searches for a
AND-branch point into the stack. If the stack does not contain any branch
point, the engine stops and the proof-search is successful. Otherwise, the
rule application stored in the AND-branch point is restored. If the rule
application is an instance of _RegularRule
, then the engine invokes
nextSubgoal()
to determine the new goal. Then the engine invokes
hasNextSubgoal()
to check if the rule application has more subgoals.
If this is the case the engine keeps the AND-branch point in the stack
otherwise it pop the AND-branch point from the stack.Modifier and Type | Method and Description |
---|---|
boolean |
hasNextSubgoal()
Returns true if this rule has a next subgoal.
|
_AbstractFormula |
mainFormula()
Returns the main formula of this rule or
null if this rule
does not have a main formula. |
_AbstractGoal |
nextSubgoal()
Returns the next subgoal of this rule.
|
int |
numberOfSubgoals()
Returns the number of subgoals of this rule.
|
name
int numberOfSubgoals()
_AbstractFormula mainFormula()
null
if this rule
does not have a main formula._AbstractGoal nextSubgoal()
boolean hasNextSubgoal()