- calculateBooleanSimplification() - Method in class jtabwbx.prop.formula.Formula
-
Returns the formula obtained by applying boolean simplifications on this
formula.
- calculateBooleanSimplification() - Method in class jtabwbx.prop.formula.FormulaProposition
-
- cardinality() - Method in interface jtabwbx.modal.basic._ModalFormulaSet
-
- cardinality() - Method in interface jtabwbx.prop.formula._FormulaSet
-
The number of elements in this set.
- cardinality() - Method in class jtabwbx.prop.formula.FormulaSetOnHashSet
-
- cardinality() - Method in class jtabwbx.prop.formula.FormulaSetOnList
-
- CASE_NOT_IMPLEMENTED - Static variable in exception jtabwb.util.ImplementationError
-
- CaseNotImplementedImplementationError - Exception in jtabwb.util
-
- CaseNotImplementedImplementationError() - Constructor for exception jtabwb.util.CaseNotImplementedImplementationError
-
- CaseNotImplementedImplementationError(String) - Constructor for exception jtabwb.util.CaseNotImplementedImplementationError
-
- checkConfiguration() - Method in class jtabwb.launcher.Launcher.LaunchConfiguration
-
- ChildrenWithCtreeNodes - Class in jtabwb.tracesupport
-
- ChildrenWithCtreeNodes(LinkedList<TraceNode>) - Constructor for class jtabwb.tracesupport.ChildrenWithCtreeNodes
-
- clearLeft() - Method in interface jtabwbx.prop.formula._Sequent
-
- clearLeft() - Method in class jtabwbx.prop.formula.SequentOnArray
-
- clearLeft() - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- clearLeft() - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- clearLeft() - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- clearLeft() - Method in class jtabwbx.prop.formula.SequentOnLists
-
- clearLeft() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBSF
-
- clearRight() - Method in interface jtabwbx.prop.formula._Sequent
-
- clearRight() - Method in class jtabwbx.prop.formula.SequentOnArray
-
- clearRight() - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- clearRight() - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- clearRight() - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- clearRight() - Method in class jtabwbx.prop.formula.SequentOnLists
-
- clearRight() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBSF
-
- clone() - Method in interface jtabwb.engine._AbstractGoal
-
Returns a fresh copy of this goal
- clone() - Method in interface jtabwbx.modal.basic._ModalFormulaSet
-
- clone() - Method in class jtabwbx.modal.formula.BitSetOfModalFormulas
-
- clone() - Method in interface jtabwbx.prop.formula._FormulaSet
-
Returns a fresh copy of this set.
- clone() - Method in interface jtabwbx.prop.formula._Sequent
-
Returns a fresh copy of this sequent.
- clone() - Method in interface jtabwbx.prop.formula._SingleSuccedentSequent
-
Returns a fresh copy of this sequent.
- clone() - Method in class jtabwbx.prop.formula.BitSetOfFormulas
-
- clone() - Method in class jtabwbx.prop.formula.FormulaSetOnHashSet
-
- clone() - Method in class jtabwbx.prop.formula.FormulaSetOnList
-
- clone() - Method in class jtabwbx.prop.formula.SequentOnArray
-
- clone() - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- clone() - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- clone() - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- clone() - Method in class jtabwbx.prop.formula.SequentOnLists
-
- clone() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnArray
-
- clone() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBitSet
-
- clone() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBSF
-
- clone() - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnLists
-
- ClosedFactoryException - Exception in jtabwbx.modal.formula
-
- ClosedFactoryException() - Constructor for exception jtabwbx.modal.formula.ClosedFactoryException
-
- ClosedFactoryException(String, Throwable, boolean, boolean) - Constructor for exception jtabwbx.modal.formula.ClosedFactoryException
-
- ClosedFactoryException(String, Throwable) - Constructor for exception jtabwbx.modal.formula.ClosedFactoryException
-
- ClosedFactoryException(String) - Constructor for exception jtabwbx.modal.formula.ClosedFactoryException
-
- ClosedFactoryException(Throwable) - Constructor for exception jtabwbx.modal.formula.ClosedFactoryException
-
- ClosedFactoryException - Exception in jtabwbx.prop.formula
-
- ClosedFactoryException() - Constructor for exception jtabwbx.prop.formula.ClosedFactoryException
-
- ClosedFactoryException(String, Throwable, boolean, boolean) - Constructor for exception jtabwbx.prop.formula.ClosedFactoryException
-
- ClosedFactoryException(String, Throwable) - Constructor for exception jtabwbx.prop.formula.ClosedFactoryException
-
- ClosedFactoryException(String) - Constructor for exception jtabwbx.prop.formula.ClosedFactoryException
-
- ClosedFactoryException(Throwable) - Constructor for exception jtabwbx.prop.formula.ClosedFactoryException
-
- CollectionOfArrayOfNCTrees - Class in jtabwb.tracesupport
-
- CollectionOfArrayOfNCTrees(int) - Constructor for class jtabwb.tracesupport.CollectionOfArrayOfNCTrees
-
- compareTo(ProverName) - Method in class jtabwb.engine.ProverName
-
- configInitialNodeSetBuilder(ProblemDescription, Launcher.LaunchConfiguration) - Method in interface jtabwb.launcher._SingleExecutionConfigurator
-
- configInitialNodeSetBuilder(_InitialGoalBuilder) - Method in class jtabwb.launcher.Launcher
-
Defines the initial node set builder to use.
- configLauncherName(String) - Method in class jtabwb.launcher.Launcher
-
Defines the name of the class using this launcher to execute a prover.
- configProblemDescriptionReader(String, Class<T>) - Method in class jtabwb.launcher.Launcher
-
Adds a problem description reader with the specified name and
implementation to this launcher.
- configProblemDescriptionReader(String, Class<T>, boolean) - Method in class jtabwb.launcher.Launcher
-
Adds a problem description reader with the specified name and
implementation to this launcher specifying if it is (
isDefault==true
) or not (isDefault==false
) the
default problem description reader for this launcher.
- configProblemReader(_ProblemReader, Launcher.LaunchConfiguration) - Method in interface jtabwb.launcher._SingleExecutionConfigurator
-
- configProver(_Prover, _AbstractGoal, Launcher.LaunchConfiguration) - Method in interface jtabwb.launcher._SingleExecutionConfigurator
-
- configStandardInputReader(_ProblemReader) - Method in class jtabwb.launcher.Launcher
-
Defines the reader used to parse a problem from standard input when
-i
option is set.
- configTheoremProver(String, Class<T>) - Method in class jtabwb.launcher.Launcher
-
Adds to this launcher a theorem prover with the specified name and
implementation.
- configTheoremProver(String, Class<T>, boolean) - Method in class jtabwb.launcher.Launcher
-
Adds a theorem prover with the specified name and implementation to this
launcher specifying if it is ( isDefault==true
) or not (
isDefault==false
) the default prover for this launcher.
- ConfiguredProblemDescriptioReader - Class in jtabwb.launcher
-
An object of this class describes a problem description reader added to the
configuration of the current launcher.
- ConfiguredProblemDescriptioReader(String, String, Class<_ProblemReader>) - Constructor for class jtabwb.launcher.ConfiguredProblemDescriptioReader
-
- ConfiguredTheoremProver - Class in jtabwb.launcher
-
An object of this class describes a theorem prover added to the configuration
of the current launcher.
- ConfiguredTheoremProver(String, String, Class<_Prover>) - Constructor for class jtabwb.launcher.ConfiguredTheoremProver
-
- contains(ModalFormula) - Method in interface jtabwbx.modal.basic._ModalFormulaSet
-
- contains(ModalFormula) - Method in class jtabwbx.modal.formula.BitSetOfModalFormulas
-
- contains(Formula) - Method in interface jtabwbx.prop.formula._FormulaSet
-
Returns true
if and only if this set contains the specified
formula.
- contains(Formula) - Method in class jtabwbx.prop.formula.BitSetOfFormulas
-
- contains(Formula) - Method in class jtabwbx.prop.formula.FormulaSetOnHashSet
-
- contains(Formula) - Method in class jtabwbx.prop.formula.FormulaSetOnList
-
- contains(SingleSuccedentSequentOnBitSet) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBitSet
-
Returns true if this sequent is contained in the one specifed as agrument;
this holds if this
and other
have the same
formula in the right-hand side and the set of formulas in the left-hand
side of this
includes the set of formulas in the left-hand
side of other
.
- containsFalse() - Method in class jtabwbx.modal.formula.ModalFormula
-
Returns true
iff this formula contains the propositional
constant FALSE as subformula.
- containsFalse() - Method in class jtabwbx.modal.formula.ModalFormulaProposition
-
- containsFalse() - Method in class jtabwbx.prop.formula.Formula
-
Returns true
iff this formula contains the propositional
constant FALSE as subformula.
- containsFalse() - Method in class jtabwbx.prop.formula.FormulaProposition
-
- containsFormulaOfType(ModalFormulaType) - Method in class jtabwbx.modal.formula.BitSetOfModalFormulas
-
- containsFormulaOfType(FormulaType) - Method in class jtabwbx.prop.formula.BitSetOfFormulas
-
- containsLeft(Formula) - Method in interface jtabwbx.prop.formula._Sequent
-
Returns true
if this sequent contains the specified formula in
the left hand side and false
otherwise.
- containsLeft(FormulaType) - Method in interface jtabwbx.prop.formula._Sequent
-
Returns true
if this sequent contains at least a formula of
the specified type in the left-hand side.
- containsLeft(Formula) - Method in interface jtabwbx.prop.formula._SingleSuccedentSequent
-
Returns true
if this sequent contains the specified formula in
the left hand side and false otherwise.
- containsLeft(Formula) - Method in class jtabwbx.prop.formula.SequentOnArray
-
- containsLeft(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnArray
-
- containsLeft(Formula) - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- containsLeft(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- containsLeft(Formula) - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- containsLeft(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- containsLeft(Formula) - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- containsLeft(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- containsLeft(Formula) - Method in class jtabwbx.prop.formula.SequentOnLists
-
- containsLeft(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnLists
-
- containsLeft(Formula) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnArray
-
- containsLeft(Formula) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBitSet
-
- containsLeft(Formula) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnBSF
-
- containsLeft(Formula) - Method in class jtabwbx.prop.formula.SingleSuccedentSequentOnLists
-
- containsProposition(ModalFormulaProposition) - Method in class jtabwbx.modal.formula.ModalFormulaProposition
-
- containsProposition(FormulaProposition) - Method in class jtabwbx.prop.formula.FormulaProposition
-
- containsRight(Formula) - Method in interface jtabwbx.prop.formula._Sequent
-
Returns true
if this sequent contains the specified formula in
the right hand side and false
otherwise.
- containsRight(FormulaType) - Method in interface jtabwbx.prop.formula._Sequent
-
Returns true
if this sequent contains at least a formula of
the specified type in the right-hand side.
- containsRight(Formula) - Method in class jtabwbx.prop.formula.SequentOnArray
-
- containsRight(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnArray
-
- containsRight(Formula) - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- containsRight(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBitSet
-
- containsRight(Formula) - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- containsRight(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBSF
-
- containsRight(Formula) - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- containsRight(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnBSFWithFormulasByType
-
- containsRight(Formula) - Method in class jtabwbx.prop.formula.SequentOnLists
-
- containsRight(FormulaType) - Method in class jtabwbx.prop.formula.SequentOnLists
-
- containsTrue() - Method in class jtabwbx.modal.formula.ModalFormula
-
Returns true
iff this formula contains the propositional
constant TRUE as subfromula.
- containsTrue() - Method in class jtabwbx.modal.formula.ModalFormulaProposition
-
- containsTrue() - Method in class jtabwbx.prop.formula.Formula
-
Returns true
iff this formula contains the propositional
constant TRUE as subfromula.
- containsTrue() - Method in class jtabwbx.prop.formula.FormulaProposition
-
- CONTRACT_VIOLATION - Static variable in exception jtabwb.util.ImplementationError
-
- ContractViolationImplementationError - Exception in jtabwb.util
-
- ContractViolationImplementationError() - Constructor for exception jtabwb.util.ContractViolationImplementationError
-
- ContractViolationImplementationError(String) - Constructor for exception jtabwb.util.ContractViolationImplementationError
-
- convertToCNF() - Method in class jtabwbx.modal.btformula.BTModalFormula
-
- convertToCNF() - Method in class jtabwbx.modal.btformula.BTModalFormulaCompound
-
- convertToCNF() - Method in class jtabwbx.modal.btformula.BTModalFormulaProposition
-
- copyFrom(ModalWffParser.WffContext) - Method in class jtabwbx.modal.parser.ModalWffParser.WffContext
-
- copyFrom(FormulaParser.WffContext) - Method in class jtabwbx.prop.parser.FormulaParser.WffContext
-
- CTree - Class in jtabwb.tracesupport
-
An object of this class represents a C-Tree.
- CTreeNode - Class in jtabwb.tracesupport
-
An object of this class represents a node of a C-tree.