- generateCombinations(CTreeNode, CollectionOfArrayOfNCTrees) - Method in class jtabwb.tracesupport.CollectionOfArrayOfNCTrees
-
- generatedFormulas() - Method in class jtabwbx.modal.formula.ModalFormulaFactory
-
Returns a copy of the list of formulas generated by this factory.
- generatedFormulas() - Method in class jtabwbx.prop.formula.FormulaFactory
-
Returns a copy of the list of formulas generated by this factory.
- generateFailureGoalAnnotations() - Method in interface jtabwb.tracesupport._LatexCTreeFormatter
-
If it returns true
the generator will print details about
failed goals of C-tree.
- generateLatex(PrintStream) - Method in class jtabwb.tracesupport.LatexTranslator
-
Generates the LaTeX proof and write it on the specified stream.
- generateNodeSetIndex() - Method in interface jtabwb.tracesupport._LatexCTreeFormatter
-
If it returns true
the generator will index the node-sets
occurring in the C-Tree
- generateRuleIndex() - Method in interface jtabwb.tracesupport._LatexCTreeFormatter
-
If it returns true
the generator will index the rule
applications occurring in the C-Tree
- getAllFormulas() - Method in interface jtabwbx.modal.basic._ModalFormulaSet
-
- getAllFormulas() - Method in class jtabwbx.modal.formula.BitSetOfModalFormulas
-
Returns the collection containing all the formulas in this set or null if
this set is empty.
- getAllFormulas(ModalFormulaType) - Method in class jtabwbx.modal.formula.BitSetOfModalFormulas
-
Returns a collection containing all formulas with the specified formula
type in this set or null if this set does not contain any formulas with the
specified formula type.
- getAllFormulas() - Method in interface jtabwbx.prop.formula._FormulaSet
-
Returns a collection containing all the formulas in this set or
null
if this set is empty.
- getAllFormulas() - Method in class jtabwbx.prop.formula.BitSetOfFormulas
-
Returns the collection containing all the formulas in this set or null if
this set is empty.
- getAllFormulas(FormulaType) - Method in class jtabwbx.prop.formula.BitSetOfFormulas
-
Returns a collection containing all formulas with the specified formula
type in this set or null if this set does not contain any formulas with the
specified formula type.
- getAllFormulas() - Method in class jtabwbx.prop.formula.FormulaSetOnHashSet
-
- getAllFormulas() - Method in class jtabwbx.prop.formula.FormulaSetOnList
-
- getAllLeftFormulas() - Method in interface jtabwbx.prop.formula._SingleSuccedentSequent
-
Returns the set containg all the formulas in the left hand side of this
sequent or null
if the left hand side of this sequent is
empty.
- getAllLeftFormulas(FormulaType) - Method in interface jtabwbx.prop.formula._SingleSuccedentSequent
-
Returns the collection of all the formulas in the left hand side of this
sequent with the specified type or null
if the left hand side
of this sequent does not contain any formula of the specified type.
- getAllLeftFormulas() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnArray
-
- getAllLeftFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnArray
-
- getAllLeftFormulas() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBitSet
-
- getAllLeftFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBitSet
-
- getAllLeftFormulas() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBSF
-
- getAllLeftFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBSF
-
- getAllLeftFormulas() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnLists
-
- getAllLeftFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnLists
-
- getAppliedRule() - Method in class jtabwb.engine.IterationInfo
-
Returns the rule applied in the last iteration or null
if no
rule has been applied in the last iteration of the engine.
- getAppliedRule() - Method in class jtabwb.engine.TraceNode
-
- getAppliedRule() - Method in class jtabwb.tracesupport.CTreeNode
-
- getATN() - Method in class jtabwbx.modal.parser.ModalWffLexer
-
- getATN() - Method in class jtabwbx.modal.parser.ModalWffParser
-
- getATN() - Method in class jtabwbx.prop.parser.FormulaLexer
-
- getATN() - Method in class jtabwbx.prop.parser.FormulaParser
-
- getAxioms() - Method in class jtabwbx.problems.ILTPProblem
-
- getBitsetOfAllFormulas(ModalFormulaType) - Method in class jtabwbx.modal.formula.BitSetOfModalFormulas
-
Returns bitset of all the formulas with the specified formula type in this
set or null if this set does not contain any formulas with the specified
formula type.
- getBitsetOfAllFormulas(FormulaType) - Method in class jtabwbx.prop.formula.BitSetOfFormulas
-
Returns bitset of all the formulas with the specified formula type in this
set or null if this set does not contain any formulas with the specified
formula type.
- getByIndex(int) - Method in class jtabwbx.modal.formula.ModalFormulaFactory
-
Returns the formula with the specified index.
- getByIndex(int) - Method in class jtabwbx.prop.formula.FormulaFactory
-
- getChildren() - Method in class jtabwb.engine.TraceNode
-
- getCmdLineOptionsManager() - Method in class jtabwb.launcher.Launcher
-
Returns the command line options manger used by this launcher.
- getCommandLine() - Method in class jtabwb.launcher.Launcher.LaunchConfiguration
-
Returns the list of atomic options and arguments parsed according to the
specified options.
- getConjecture() - Method in class jtabwbx.problems.ILTPProblem
-
- getConjecture() - Method in class jtabwbx.problems.JTabWbSimpleProblem
-
- getConjecture() - Method in class jtabwbx.problems.PlainProblemDescription
-
- getCurrentLauncherConfiguration() - Method in class jtabwb.launcher.Launcher
-
Return an object describing the relevant details about the configuration of
the launcher.
- getDescription() - Method in class jtabwb.engine.ProverName
-
- getDescription() - Method in interface jtabwb.launcher._ProblemReader
-
Returns a string describing this problem reader.
- getDescription() - Method in class jtabwb.launcher.ConfiguredProblemDescriptioReader
-
Returns the description given to the problem description reader in the
launcher configuration.
- getDescription() - Method in class jtabwb.launcher.ConfiguredTheoremProver
-
Returns the description given to the prover in the launcher configuration.
- getDescription() - Method in class jtabwbx.modal.btformula.BTModalFormulaFactory
-
- getDescription() - Method in class jtabwbx.modal.formula.ModalFormulaFactory
-
- getDescription() - Method in class jtabwbx.modal.parser.ModalFormulaParser
-
Returns a description of the parser.
- getDescription() - Method in class jtabwbx.problems.ILTPProblemReader
-
- getDescription() - Method in class jtabwbx.problems.JTabWbSimpleProblemReader
-
- getDescription() - Method in class jtabwbx.problems.PlainProblemReader
-
- getDescription() - Method in class jtabwbx.prop.btformula.BTPropositionalFormulaFactory
-
- getDescription() - Method in class jtabwbx.prop.formula.FormulaFactory
-
- getDescription() - Method in class jtabwbx.prop.parser.PropositionalFormulaParser
-
Returns a description of the parser.
- getDetailedName() - Method in class jtabwb.engine.ProverName
-
Returns the string done as follows:
- getDetails() - Method in interface jtabwb.engine._RuleWithDetails
-
A string providing some extra information about the rule application.
- getEndTime() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the end time of the proof-search or -1
if the
proof-search did not terminate.
- getExecutionTime() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the time required by the proof-search in milliseconds.
- getFactory() - Method in class jtabwbx.modal.formula.BitSetOfModalFormulas
-
- getFactory() - Method in class jtabwbx.modal.formula.ModalFormula
-
Returns the factory used to build this formula.
- getFactory() - Method in class jtabwbx.modal.formula.ModalFormulaProposition
-
- getFactory() - Method in class jtabwbx.prop.formula.BitSetOfFormulas
-
- getFactory() - Method in class jtabwbx.prop.formula.Formula
-
Returns the factory used to build this formula.
- getFactory() - Method in class jtabwbx.prop.formula.FormulaProposition
-
- getFalse() - Method in class jtabwbx.modal.formula.ModalFormulaFactory
-
Returns the formula modelling the propositional constant FALSE.
- getFalse() - Method in class jtabwbx.prop.formula.FormulaFactory
-
Returns the formula modelling the propositional constant FALSE.
- getFirst() - Method in interface jtabwbx.modal.basic._ModalFormulaSet
-
- getFirst() - Method in class jtabwbx.modal.formula.BitSetOfModalFormulas
-
- getFirst(ModalFormulaType) - Method in class jtabwbx.modal.formula.BitSetOfModalFormulas
-
- getFirst() - Method in interface jtabwbx.prop.formula._FormulaSet
-
Returns the first formula in this set or null
if this set is
empty.
- getFirst() - Method in class jtabwbx.prop.formula.BitSetOfFormulas
-
- getFirst(FormulaType) - Method in class jtabwbx.prop.formula.BitSetOfFormulas
-
- getFirst() - Method in class jtabwbx.prop.formula.FormulaSetOnHashSet
-
- getFirst() - Method in class jtabwbx.prop.formula.FormulaSetOnList
-
- getFirstAndRemove() - Method in class jtabwbx.modal.formula.BitSetOfModalFormulas
-
Returns the first formula in this bitset and removes it from the bitset.
- getFirstAndRemove(ModalFormulaType) - Method in class jtabwbx.modal.formula.BitSetOfModalFormulas
-
Returns the first formula with the specified type in this bitset and it
removes such a formula from the bitset.
- getFirstAndRemove() - Method in class jtabwbx.prop.formula.BitSetOfFormulas
-
Returns the first formula of this bitset and remove it from the bitset.
- getFirstAndRemove(FormulaType) - Method in class jtabwbx.prop.formula.BitSetOfFormulas
-
Returns the first formula with the specified type of this bitset and remove
it from the bitset.
- getFormulaFactory() - Method in class jtabwbx.prop.formula.SequentOnArray
-
- getFormulaFactory() - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- getFormulaFactory() - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- getFormulaFactory() - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- getFormulaFactory() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBSF
-
- getFormulasByRole(String) - Method in class jtabwb.launcher.ProblemDescription
-
Returns the list of the formulas in this problem description with the
specified role or null
if formula with the specified role is
defined for this problem.
- getFormulaType(ModalFormula) - Static method in enum jtabwbx.modal.basic.ModalFormulaType
-
Returns the type for the specified formula.
- getFormulaType() - Method in class jtabwbx.modal.formula.ModalFormula
-
Returns the formula type of this formula.
- getFormulaType() - Method in class jtabwbx.modal.formula.ModalFormulaProposition
-
- getFormulaType(_PropositionalFormula) - Static method in enum jtabwbx.prop.basic.FormulaType
-
Returns the type for the specified formula.
- getFormulaType() - Method in class jtabwbx.prop.formula.Formula
-
Returns the formula type of this formula.
- getFormulaType() - Method in class jtabwbx.prop.formula.FormulaProposition
-
- getGeneratedFormula() - Method in class jtabwbx.modal.formula.ModalFormulaFactory
-
Returns the set containing all the generated formulas.
- getGeneratedFormula() - Method in class jtabwbx.prop.formula.FormulaFactory
-
- getGeneratedFormulasOfType(ModalFormulaType) - Method in class jtabwbx.modal.formula.ModalFormulaFactory
-
Returns the set containing all the generated formulas of the specified
type.
- getGeneratedFormulasOfType(FormulaType) - Method in class jtabwbx.prop.formula.FormulaFactory
-
Returns the
BitSetOfFormulas
containing all the generated formulas
of the specified type.
- getGrammarFileName() - Method in class jtabwbx.modal.parser.ModalWffLexer
-
- getGrammarFileName() - Method in class jtabwbx.modal.parser.ModalWffParser
-
- getGrammarFileName() - Method in class jtabwbx.prop.parser.FormulaLexer
-
- getGrammarFileName() - Method in class jtabwbx.prop.parser.FormulaParser
-
- getId() - Method in class jtabwb.tracesupport.CTree
-
- getIncompatibleOptions() - Method in exception jtabwb.util.IncompatibleOptionsException
-
Returns the array containing the incompatible options which caused this
exception.
- getIndex() - Method in class jtabwbx.modal.formula.ModalFormula
-
Returns the index for this formula.
- getIndex() - Method in class jtabwbx.prop.formula.Formula
-
Returns the index for this formula.
- getInitialGoal() - Method in class jtabwb.engine.Engine
-
Returns the initial goal.
- getInitialNodeSet() - Method in class jtabwb.engine.Trace
-
Returns the initial node set (the node set at the root of the
proof-search).
- getIntialNodeSetConstructionTime() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the time required to build the initial node set.
- getIntro() - Method in interface jtabwb.tracesupport._LatexCTreeFormatter
-
Returns the text to add at the beginning of the LaTeX document; this text
is added immediately after "\begin{document}
".
- getIterationCounter() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the number of iterations performed by the engine during the
proof-search.
- getLastIterationInfo() - Method in class jtabwb.engine.Engine
-
Returns a bunch of detailed information on the last iteration performed by
the prover.
- getLastProofSearchData() - Method in class jtabwb.launcher.Launcher
-
Returns data about the last proof-search.
- getLatexProofFormatter() - Method in interface jtabwb.tracesupport._LatexSupport
-
Returns the LaTeX C-tree formatter.
- getLeft(FormulaType) - Method in interface jtabwbx.prop.formula._Sequent
-
Returns a formula of the specified type contained in the left hand side of
the sequent or null
if no formula of the specified type occurs
in this sequent.
- getLeft(FormulaType) - Method in interface jtabwbx.prop.formula._SingleSuccedentSequent
-
Returns a formula of the specified type contained in the left hand side of
the sequent or null
if no formula of the specified type occurs
in this sequent.
- getLeft() - Method in interface jtabwbx.prop.formula._SingleSuccedentSequent
-
Returns a formula from the left hand side of the sequent or
null
if le theft hand side is empty.
- getLeft(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnArray
-
- getLeft(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- getLeft(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- getLeft(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- getLeft(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnLists
-
- getLeft(FormulaType) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnArray
-
- getLeft() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnArray
-
- getLeft() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBitSet
-
- getLeft(FormulaType) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBitSet
-
- getLeft() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBSF
-
- getLeft(FormulaType) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBSF
-
- getLeft(FormulaType) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnLists
-
- getLeft() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnLists
-
- getLeftFormulas() - Method in interface jtabwbx.prop.formula._Sequent
-
Returns the set containg all the formulas in the left hand side of this
sequent or null
if the left hand side of this sequent is
empty.
- getLeftFormulas(FormulaType) - Method in interface jtabwbx.prop.formula._Sequent
-
Returns the collection of all the formulas in the left hand side of this
sequent with the specified type or null
if the left hand side
of this sequent does not contain any formula of the specified type.
- getLeftFormulas() - Method in class jtabwbx.prop.formula.SequentOnArray
-
- getLeftFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnArray
-
- getLeftFormulas() - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- getLeftFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- getLeftFormulas() - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- getLeftFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- getLeftFormulas() - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- getLeftFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- getLeftFormulas() - Method in class jtabwbx.prop.formula.SequentOnLists
-
- getLeftFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnLists
-
- getMaxNumberOfSuccessors() - Method in class jtabwb.engine.TraceNode
-
- getMaxStackSize() - Method in class jtabwb.engine.IterationInfo
-
Returns the maximum size of the stack up to this iteration.
- getMaxStackSize() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the maximum depth of the stack during the proof-search.
- getModeNames() - Method in class jtabwbx.modal.parser.ModalWffLexer
-
- getModeNames() - Method in class jtabwbx.prop.parser.FormulaLexer
-
- getMove() - Method in class jtabwb.engine.IterationInfo
-
Returns the move the engine performed in the last iteration.
- getName() - Method in interface jtabwb.launcher._ProblemReader
-
Returns the name of this problem reader.
- getName() - Method in class jtabwb.launcher.ConfiguredProblemDescriptioReader
-
Returns the name given to the problem description reader in the launcher
configuration.
- getName() - Method in class jtabwb.launcher.ConfiguredTheoremProver
-
Returns the name given to the prover in the launcher configuration.
- getName() - Method in enum jtabwbx.modal.basic.ModalConnective
-
- getName() - Method in class jtabwbx.modal.btformula.BTModalFormulaProposition
-
- getName() - Method in class jtabwbx.modal.formula.ModalFormulaProposition
-
- getName() - Method in class jtabwbx.modal.parser.ModalFormulaParser
-
Returns the parser name.
- getName() - Method in class jtabwbx.problems.ILTPProblemReader
-
- getName() - Method in class jtabwbx.problems.JTabWbSimpleProblemReader
-
- getName() - Method in class jtabwbx.problems.PlainProblemReader
-
- getName() - Method in enum jtabwbx.prop.basic.PropositionalConnective
-
- getName() - Method in class jtabwbx.prop.btformula.BTFormulaProposition
-
- getName() - Method in class jtabwbx.prop.formula.FormulaProposition
-
- getName() - Method in class jtabwbx.prop.parser.PropositionalFormulaParser
-
Returns the parser name.
- getNodeDeterminingPremise() - Method in class jtabwb.engine.TraceNode
-
- getNodeDeterminingPremiseTreatedConclusion() - Method in class jtabwb.engine.TraceNode
-
- getNodeSet() - Method in class jtabwb.tracesupport.CTreeNode
-
- getNumberOfConclusions() - Method in class jtabwb.engine.IterationInfo
-
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.
- getNumberOfGeneratedNodes() - Method in class jtabwb.engine.IterationInfo
-
Returns the number of node-sets generated up to this iteration.
- getNumberOfGeneratedNodes() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the number of node-sets generated during the proof-search.
- getNumberOfIterations() - Method in class jtabwb.engine.IterationInfo
-
Returns the number of iterations performed by the engine.
- getNumberOfRestoredBacktrackPoints() - Method in class jtabwb.engine.IterationInfo
-
Returns the number of times a backtrack-point has been restored up to this
iteration.
- getNumberOfRestoredBacktrackPoints() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the number of times a backtrack point has been restored from the
stack during the proof-search.
- getNumberOfRestoredBranchPoints() - Method in class jtabwb.engine.IterationInfo
-
Returns the number of times a branch-point has been restored up to this
iteration.
- getNumberOfRestoredBranchPoints() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the number of times a branch point has been restored from the stack
during the proof-search.
- getParent() - Method in class jtabwb.engine.TraceNode
-
- getParsingProblemTime() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the time required to parse the problem description in milliseconds.
- getPreamble() - Method in interface jtabwb.tracesupport._LatexCTreeFormatter
-
Returns the text to add to the preamble of the LaTeX file; in general it
contains local macro definitions.
- getPremise() - Method in class jtabwb.engine.TraceNode
-
- getProblemDescription() - Method in class jtabwb.launcher.ProofSearchData
-
- getProblemName() - Method in class jtabwb.launcher.ProblemDescription
-
- getProblemStatus() - Method in class jtabwb.launcher.ProblemDescription
-
- getProofSearchTree() - Method in class jtabwb.engine.Trace
-
Returns the root of the proof-search tree.
- getProperNoun() - Method in class jtabwb.engine.ProverName
-
- getProver() - Method in class jtabwb.engine.Trace
-
Returns the prover used to generate this trace.
- getProver() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the proved used to perform the proof-search.
- getProver() - Method in class jtabwb.tracesupport.CTree
-
Returns the prover that generated the C-tree.
- getProver() - Method in class jtabwb.tracesupport.TraceValidator
-
- getProverName() - Method in interface jtabwb.engine._Prover
-
Returns an object describing the detailed name of the prover.
- getProverName() - Method in class jtabwb.tracesupport.Validator
-
- getResult() - Method in class jtabwb.engine.Engine
-
Returns the result of the last proof-search.
- getResult() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the result of the proof-search.
- getRight(FormulaType) - Method in interface jtabwbx.prop.formula._Sequent
-
Returns the formula in the right hand side of this sequent or
null
if the formula in the right hand side does not have the
specified type.
- getRight() - Method in interface jtabwbx.prop.formula._SingleSuccedentSequent
-
Returns the formula in the right hand side of this sequent or
null
if the right hand side of this sequent is empty.
- getRight(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnArray
-
- getRight(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- getRight(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- getRight(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- getRight(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnLists
-
- getRight() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnArray
-
- getRight() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBitSet
-
- getRight() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBSF
-
- getRight() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnLists
-
- getRightFormulaOfType(FormulaType) - Method in interface jtabwbx.prop.formula._SingleSuccedentSequent
-
Returns the formula in the right hand side of this sequent if the formula
has the specified type or null
if the formula in the right
hand side does not have the specified type.
- getRightFormulaOfType(FormulaType) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnArray
-
- getRightFormulaOfType(FormulaType) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBitSet
-
- getRightFormulaOfType(FormulaType) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBSF
-
- getRightFormulaOfType(FormulaType) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnLists
-
- getRightFormulas() - Method in interface jtabwbx.prop.formula._Sequent
-
Returns the set containg all the formulas in the right hand side of this
sequent or null
if the right hand side of this sequent is
empty.
- getRightFormulas(FormulaType) - Method in interface jtabwbx.prop.formula._Sequent
-
Returns the collection of all the formulas in the right hand side of this
sequent with the specified type or null
if the right hand side
of this sequent does not contain any formula of the specified type.
- getRightFormulas() - Method in class jtabwbx.prop.formula.SequentOnArray
-
- getRightFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnArray
-
- getRightFormulas() - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- getRightFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- getRightFormulas() - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- getRightFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- getRightFormulas() - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- getRightFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- getRightFormulas() - Method in class jtabwbx.prop.formula.SequentOnLists
-
- getRightFormulas(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnLists
-
- getRoles() - Method in class jtabwb.launcher.ProblemDescription
-
Returns the roles for this problem description.
- getRoot() - Method in class jtabwb.tracesupport.CTree
-
Returns the node at the root of the C-tree.
- getRuleByName(String, _AbstractGoal, _AbstractFormula) - Method in interface jtabwb.tracesupport._TraceManager
-
Returns the instance of the rule with the specified name applied to the
specified arguments.
- getRuleIndex() - Method in class jtabwbx.modal.parser.ModalWffParser.ModalFormulaContext
-
- getRuleIndex() - Method in class jtabwbx.modal.parser.ModalWffParser.WffContext
-
- getRuleIndex() - Method in class jtabwbx.prop.parser.FormulaParser.FormulaContext
-
- getRuleIndex() - Method in class jtabwbx.prop.parser.FormulaParser.WffContext
-
- getRuleNames() - Method in class jtabwbx.modal.parser.ModalWffLexer
-
- getRuleNames() - Method in class jtabwbx.modal.parser.ModalWffParser
-
- getRuleNames() - Method in class jtabwbx.prop.parser.FormulaLexer
-
- getRuleNames() - Method in class jtabwbx.prop.parser.FormulaParser
-
- getRuleType() - Method in class jtabwb.engine.TraceNode
-
- getSelectedProver() - Method in class jtabwb.launcher.Launcher.LaunchConfiguration
-
- getSelectedReader() - Method in class jtabwb.launcher.Launcher.LaunchConfiguration
-
- getSerializedATN() - Method in class jtabwbx.modal.parser.ModalWffLexer
-
- getSerializedATN() - Method in class jtabwbx.modal.parser.ModalWffParser
-
- getSerializedATN() - Method in class jtabwbx.prop.parser.FormulaLexer
-
- getSerializedATN() - Method in class jtabwbx.prop.parser.FormulaParser
-
- getSource() - Method in class jtabwb.launcher.ProblemDescription
-
- getStackTrace() - Method in class jtabwb.engine.IterationInfo
-
Return the stack trace.
- getStartTime() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the start time of the proof-search.
- getStatus() - Method in class jtabwb.engine.Trace
-
Returns the status of the proof-search described by this trace.
- getStatus() - Method in class jtabwb.engine.TraceNode
-
- getStatus() - Method in class jtabwb.tracesupport.CTree
-
Returns the status of the C-tree.
- getStatus() - Method in class jtabwb.tracesupport.CTreeNode
-
- getStrategy() - Method in interface jtabwb.engine._Prover
-
Returns the strategy used by this prover.
- getStrategy() - Method in class jtabwb.tracesupport.Validator
-
- getSuccessors() - Method in class jtabwb.tracesupport.CTreeNode
-
- getTerminationStauts() - Method in class jtabwb.launcher.ProofSearchData
-
- getTokenNames() - Method in class jtabwbx.modal.parser.ModalWffLexer
-
Deprecated.
- getTokenNames() - Method in class jtabwbx.modal.parser.ModalWffParser
-
Deprecated.
- getTokenNames() - Method in class jtabwbx.prop.parser.FormulaLexer
-
Deprecated.
- getTokenNames() - Method in class jtabwbx.prop.parser.FormulaParser
-
Deprecated.
- getTrace() - Method in class jtabwb.engine.Engine
-
Returns the trace of the last proof-search or null if the engine has not
been executed in trace mode (see
Engine.ExecutionMode
).
- getTrace() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the trace of the proof-search if the trace option was set or
null
otherwise.
- getTrace() - Method in class jtabwb.tracesupport.TraceValidator
-
- getTraceManager() - Method in interface jtabwb.tracesupport._TraceSupport
-
- getTreatedConclusion() - Method in class jtabwb.engine.IterationInfo
-
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.
- getTreatedConclusion() - Method in class jtabwb.tracesupport.CTreeNode
-
- getTrue() - Method in class jtabwbx.modal.formula.ModalFormulaFactory
-
Returns the formula modelling the propositional constant TRUE.
- getTrue() - Method in class jtabwbx.prop.formula.FormulaFactory
-
Returns the formula modelling the propositional constant TRUE.
- getType(_AbstractRule) - Static method in enum jtabwb.engine.RuleType
-
Returns the type of the specified rule.
- getValue() - Method in class jtabwb.launcher.ConfiguredProblemDescriptioReader
-
Returns the class of the problem description reader.
- getValue() - Method in class jtabwb.launcher.ConfiguredTheoremProver
-
Returns the class of the prover.
- getVariant() - Method in class jtabwb.engine.ProverName
-
- getVersion() - Method in class jtabwb.engine.ProverName
-
- getVocabulary() - Method in class jtabwbx.modal.parser.ModalWffLexer
-
- getVocabulary() - Method in class jtabwbx.modal.parser.ModalWffParser
-
- getVocabulary() - Method in class jtabwbx.prop.parser.FormulaLexer
-
- getVocabulary() - Method in class jtabwbx.prop.parser.FormulaParser
-
- goal() - Method in interface jtabwb.engine._ClashDetectionRule
-
Returns the goal on which this this clash-detection rule act.
- goal() - Method in interface jtabwb.engine._MetaBacktrackRule
-
Returns the goal of this meta-backtrack rule application.
- goal() - Method in class jtabwb.engine.ForceBranchFailure
-
Returns the abstract node set on which the the proof-search failed.
- goal() - Method in class jtabwb.launcher.ProofSearchData
-
Returns the goal of the proof-search.