Package | Description |
---|---|
jtabwb.engine |
Main classes implementing the engine; it specifies the interfaces with the
user defined prover.
|
jtabwb.tracesupport |
Some tool for managing traces and C-trees, including support for LaTeX source
generation.
|
Modifier and Type | Interface and Description |
---|---|
interface |
_BranchExistsRule
This interface describes a branch-exists rule, namely a backtrack rule that
succeeds if at least one of its subgoals succeeds.
|
interface |
_ClashDetectionRule
An object realizing a clash-detection rule.
|
interface |
_MetaBacktrackRule
A meta-backtrack rule specifies an enumeration of backtrack
rules to try in the proof-search.
|
interface |
_OnRuleCompletedListener
Specifies that the rule implementing this interface listens for the
on-rule-completed event.
|
interface |
_OnRuleResumedListener
Specifies that the rule implementing this interface listens for the
on-resume-event.
|
interface |
_RegularRule
A regular rule is a rule generating one or more sub-goals to solve.
|
Modifier and Type | Class and Description |
---|---|
class |
ForceBranchFailure
This rule force branch failure.
|
class |
ForceBranchSuccess
An final instance of
_ClashDetectionRule whose
_ClashDetectionRule.status() always returns
ProofSearchResult.SUCCESS . |
Modifier and Type | Method and Description |
---|---|
_AbstractRule |
TraceNode.getAppliedRule() |
_AbstractRule |
IterationInfo.getAppliedRule()
Returns the rule applied in the last iteration or
null if no
rule has been applied in the last iteration of the engine. |
_AbstractRule |
_Strategy.nextRule(_AbstractGoal currentGoal,
IterationInfo lastIteration)
This is a call-back method invoked by the engine when it needs to determine
the rule to to apply to
currentGoal ; doing this the engine
provides to the method as second argument a bunch of data describing the
last performed iteration. |
_AbstractRule |
_MetaBacktrackRule.nextRule()
Returns the next rule.
|
Modifier and Type | Method and Description |
---|---|
static RuleType |
RuleType.getType(_AbstractRule ruleToApply)
Returns the type of the specified rule.
|
Modifier and Type | Method and Description |
---|---|
_AbstractRule |
CTreeNode.getAppliedRule() |
_AbstractRule |
_TraceManager.getRuleByName(java.lang.String name,
_AbstractGoal premise,
_AbstractFormula mainFormula)
Returns the instance of the rule with the specified name applied to the
specified arguments.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
_LatexCTreeFormatter.formatRuleName(_AbstractRule rule)
Returns the LaTeX translation of the name of the rule.
|