public class IterationInfo
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
IterationInfo.Move
The possible moves performed by the engine.
|
Modifier and Type | Method and Description |
---|---|
boolean |
backtrackPointAdded()
Returns
true if the last rule application added a
backtrack-point to the stack. |
boolean |
branchPointAdded()
Returns
true if the last rule application added a branch-point
to the stack. |
_AbstractRule |
getAppliedRule()
Returns the rule applied in the last iteration or
null if no
rule has been applied in the last iteration of the engine. |
int |
getMaxStackSize()
Returns the maximum size of the stack up to this iteration.
|
IterationInfo.Move |
getMove()
Returns the move the engine performed in the last iteration.
|
int |
getNumberOfConclusions()
Returns the number of conclusions in the last rule application or -1 if
this information has no meaning for the move performed by the engine in the
last iteration.
|
long |
getNumberOfGeneratedNodes()
Returns the number of node-sets generated up to this iteration.
|
long |
getNumberOfIterations()
Returns the number of iterations performed by the engine.
|
long |
getNumberOfRestoredBacktrackPoints()
Returns the number of times a backtrack-point has been restored up to this
iteration.
|
long |
getNumberOfRestoredBranchPoints()
Returns the number of times a branch-point has been restored up to this
iteration.
|
java.lang.String |
getStackTrace()
Return the stack trace.
|
int |
getTreatedConclusion()
TODO: doc caso di meta-backtrack If in the last iteration the engine
applied a rule with conclusions, this method returns the index of the
conclusion that became the new goal of the engine, otherwise the method
returns -1.
|
public long getNumberOfIterations()
public _AbstractRule getAppliedRule()
null
if no
rule has been applied in the last iteration of the engine. In details,
according with the value returned by getMove()
:
IterationInfo.Move.INITIAL_STATE
: the method returns null
.IterationInfo.Move.REGULAR_RULE_APPLICATION
,
IterationInfo.Move.BRANCH_EXISTS_RULE_APPLICATION
,
IterationInfo.Move.META_RULE_APPLICATION
,
IterationInfo.Move.CLASH_DETECTION_RULE_APPLICATION
: the method returns the
instance of the applied rule.IterationInfo.Move.BACKTRACK_POINT_SEARCH
: if the stack contained a
backtrack-point the engine restored such a point, in this case the method
returns the instance of the rule restored from the stack. If the stack did
not contained a backtrack point, the method returns null
.IterationInfo.Move.BRANCH_POINT_SEARCH
: if the stack contained a branch-point
the engine restored such a point, in this case the method returns the
instance of the rule restored from the stack. If the stack did not
contained a branch-point, the method returns null
.null
if no rule has been applied in such an iteration.public IterationInfo.Move getMove()
IterationInfo.Move.INITIAL_STATE
if no iteration has been
performed by the engine.IterationInfo.Move.REGULAR_RULE_APPLICATION
,
IterationInfo.Move.BRANCH_EXISTS_RULE_APPLICATION
,
IterationInfo.Move.META_RULE_APPLICATION
, if this is the kind of the rule applied
in the last iteration.IterationInfo.Move.CLASH_DETECTION_RULE_APPLICATION
if the
rule applied in the last iteration was an instance of
_ClashDetectionRule
and the method
_ClashDetectionRule.status()
returned
ProofSearchResult.FAILURE
.IterationInfo.Move.BACKTRACK_POINT_SEARCH
if in the last
iteration the engine invoked
_Strategy.nextRule(_AbstractGoal, IterationInfo)
and such a
method returned null
. This means that the search for a proof
of the current goal failed and the engine searched the stack for a
backtrack-point.IterationInfo.Move.BRANCH_POINT_SEARCH
if the rule applied
in the last iteration was an instance of _ClashDetectionRule
and
the method _ClashDetectionRule.status()
returned
ProofSearchResult.SUCCESS
. In this case the engine query the stack
for a branch-point.public boolean backtrackPointAdded()
true
if the last rule application added a
backtrack-point to the stack. This happens if:
_BranchExistsRule
(hence getMove()
returns
IterationInfo.Move.BRANCH_EXISTS_RULE_APPLICATION
) and the invocation of
_BranchExistsRule.numberOfBranchExistsSubgoals()
on such an
instance returned a value greater than 1._MetaBacktrackRule
(hence getMove()
returns
IterationInfo.Move.META_RULE_APPLICATION
) and the invocation of
_MetaBacktrackRule.totalNumberOfRules()
on such an instance
returned a value greater than 1.true
if and only if, executing the last iteration, the
engine added a backtrack-point to the stack.public boolean branchPointAdded()
true
if the last rule application added a branch-point
to the stack. This happens if in the last iteration the engine applied an
instance of _RegularRule
(hence getMove()
returns
IterationInfo.Move.REGULAR_RULE_APPLICATION
) and the invocation of
_RegularRule.numberOfSubgoals()
on such an instance returned a
value greater than 1.true
if and only if, executing the last iteration, the
engine added a branch-point to the stack.public int getNumberOfConclusions()
_RegularRule
the method returns the result of the invocation of
_RegularRule.numberOfSubgoals()
on such an instance._BranchExistsRule
the method returns the values of the invocation
of _BranchExistsRule.numberOfBranchExistsSubgoals()
on such an
instance.public int getTreatedConclusion()
_RegularRule
, the method returns 0 (the index of the first
conclusion)._BranchExistsRule
, the method returns 0 (the index of the first
conclusion)._RegularRule
; the engine invoke
the method conclusion(i)
to get the new subgoal where i is the
index of the first non treated conclusion of the rule; in this case the
method returns i.public long getNumberOfGeneratedNodes()
public long getNumberOfRestoredBacktrackPoints()
public long getNumberOfRestoredBranchPoints()
public int getMaxStackSize()
public java.lang.String getStackTrace()