public class ModalFormulaFactory
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
ModalFormulaProposition |
FALSE
The formula representing the propositional variable FALSE.
|
ModalFormulaProposition |
TRUE
The formula representing the propositional variable TRUE.
|
Constructor and Description |
---|
ModalFormulaFactory()
Constructs an instance of the factory using "false" and "true" as names for
true and false constants.
|
ModalFormulaFactory(java.lang.String falseName,
java.lang.String trueName)
Constructs an instance of the factory using the specified names for true
and false representation.
|
Modifier and Type | Method and Description |
---|---|
ModalFormulaProposition |
buildAtomic(java.lang.String name)
Builds the propositional modal formula with the specified name.
|
ModalFormula |
buildCompound(ModalConnective mainConnective,
ModalFormula... subFormulas)
Builds the formula having the specified logical constant as main connective
and the specified subformulas as direct subformulas.
|
ModalFormula |
buildFrom(BTModalFormula wff)
Build an instance of the specified
BTModalFormula . |
ModalFormula |
buildFrom(ModalFormula wff)
Build an instance of the specified
ModalFormula in this factory. |
ModalFormula |
buildFrom(org.antlr.v4.runtime.tree.ParseTree parseTree)
Build a modal formula from the specified parse-tree.
|
java.util.ArrayList<ModalFormula> |
generatedFormulas()
Returns a copy of the list of formulas generated by this factory.
|
ModalFormula |
getByIndex(int index)
Returns the formula with the specified index.
|
java.lang.String |
getDescription() |
ModalFormulaProposition |
getFalse()
Returns the formula modelling the propositional constant FALSE.
|
BitSetOfModalFormulas |
getGeneratedFormula()
Returns the set containing all the generated formulas.
|
BitSetOfModalFormulas |
getGeneratedFormulasOfType(ModalFormulaType type)
Returns the set containing all the generated formulas of the specified
type.
|
ModalFormulaProposition |
getTrue()
Returns the formula modelling the propositional constant TRUE.
|
int |
numberOfGeneratedFormulas()
The number of distinct formulas generated by this factory.
|
void |
setTranslateEquivalences(boolean b)
If
b is true equivalences
(A <-> B) are built as
(A -> B) & (B -> A) . |
java.lang.String |
toString() |
public final ModalFormulaProposition FALSE
public final ModalFormulaProposition TRUE
public ModalFormulaFactory(java.lang.String falseName, java.lang.String trueName)
ContractViolationImplementationError
is
thrown.falseName
- the name for the false constant.trueName
- the name for the true constant.public ModalFormulaFactory()
public int numberOfGeneratedFormulas()
public java.util.ArrayList<ModalFormula> generatedFormulas()
public ModalFormulaProposition getTrue()
public ModalFormulaProposition getFalse()
public BitSetOfModalFormulas getGeneratedFormula()
public BitSetOfModalFormulas getGeneratedFormulasOfType(ModalFormulaType type)
type
- the type of the formulas to return.public ModalFormulaProposition buildAtomic(java.lang.String name)
name
- the name of the proposition.public ModalFormula buildCompound(ModalConnective mainConnective, ModalFormula... subFormulas)
mainConnective
- the main connective (a logical constant).subFormulas
- the direct subformulas.public ModalFormula getByIndex(int index)
index
- the index of the formula.public ModalFormula buildFrom(ModalFormula wff)
ModalFormula
in this factory.wff
- the formula to build.public ModalFormula buildFrom(BTModalFormula wff)
BTModalFormula
.wff
- the formula to build.public ModalFormula buildFrom(org.antlr.v4.runtime.tree.ParseTree parseTree)
parseTree
- the parse tree.public void setTranslateEquivalences(boolean b)
b
is true
equivalences
(A <-> B)
are built as
(A -> B) & (B -> A)
.b
- if true
equivalences are translatedpublic java.lang.String toString()
toString
in class java.lang.Object
public java.lang.String getDescription()