public class FormulaFactory
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
FormulaProposition |
FALSE
The formula representing the propositional variable FALSE.
|
FormulaProposition |
TRUE
The formula representing the propositional variable TRUE.
|
Constructor and Description |
---|
FormulaFactory()
Constructs an instance of the factory using "false" and "true" as names for
true and false constants.
|
FormulaFactory(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 |
---|---|
FormulaProposition |
buildAtomic(java.lang.String name) |
Formula |
buildCompound(PropositionalConnective mainConnective,
Formula... subFormulas)
Builds the formula having the specified logical constant as main connective
and the specified subformulas as direct subformulas.
|
Formula |
buildFrom(BTFormula wff)
Build an instance of the specified
BTFormula . |
Formula |
buildFrom(Formula wff)
Build an instance of the specified formula in this factory.
|
Formula |
buildFrom(org.antlr.v4.runtime.tree.ParseTree parseTree)
Build a formula from the specified parse-tree.
|
java.util.ArrayList<Formula> |
generatedFormulas()
Returns a copy of the list of formulas generated by this factory.
|
Formula |
getByIndex(int index) |
java.lang.String |
getDescription() |
FormulaProposition |
getFalse()
Returns the formula modelling the propositional constant FALSE.
|
BitSetOfFormulas |
getGeneratedFormula()
Returns the
BitSetOfFormulas containing all the generated formulas. |
BitSetOfFormulas |
getGeneratedFormulasOfType(FormulaType type)
Returns the
BitSetOfFormulas containing all the generated formulas
of the specified type. |
FormulaProposition |
getTrue()
Returns the formula modelling the propositional constant TRUE.
|
BitSetOfFormulas |
intuitionisticNonLocalFormulas()
Returns the bitset containing the intuitionistic NON local formulas in this
factory.
|
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) . |
void |
setTranslateImplisesFalse(boolean b)
If
b is true implications of the kind
A -> false are built as ~ A . |
void |
setTranslateNegations(boolean b)
If
b is true negated formulas (~ A) are built as
(A -> FALSE) . |
java.lang.String |
toString() |
public final FormulaProposition FALSE
public final FormulaProposition TRUE
public FormulaFactory(java.lang.String falseName, java.lang.String trueName)
ContractViolationImplementationError
is
thrown.falseName
- the name of the false constant.trueName
- the name of the true constant.public FormulaFactory()
public int numberOfGeneratedFormulas()
public java.util.ArrayList<Formula> generatedFormulas()
public FormulaProposition getTrue()
public FormulaProposition getFalse()
public BitSetOfFormulas getGeneratedFormula()
BitSetOfFormulas
containing all the generated formulas.public BitSetOfFormulas getGeneratedFormulasOfType(FormulaType type)
BitSetOfFormulas
containing all the generated formulas
of the specified type.type
- the type of the formulas to return.public FormulaProposition buildAtomic(java.lang.String name)
public Formula buildCompound(PropositionalConnective mainConnective, Formula... subFormulas)
mainConnective
- the main connective (a logical constant).subFormulas
- the direct subformulas.public Formula getByIndex(int index)
public Formula buildFrom(Formula wff)
wff
- the formula to build.public Formula buildFrom(BTFormula wff)
BTFormula
.wff
- the formula to build.public Formula buildFrom(org.antlr.v4.runtime.tree.ParseTree parseTree)
parseTree
- the parse tree.public BitSetOfFormulas intuitionisticNonLocalFormulas()
public java.lang.String getDescription()
public void setTranslateNegations(boolean b)
b
is true
negated formulas (~ A) are built as
(A -> FALSE)
.b
- if true
negations are translatedpublic void setTranslateEquivalences(boolean b)
b
is true
equivalences
(A <-> B)
are built as
(A -> B) & (B -> A)
.b
- if true
equivalences are translatedpublic void setTranslateImplisesFalse(boolean b)
b
is true
implications of the kind
A -> false
are built as ~ A
.b
- if true the translation is applied.public java.lang.String toString()
toString
in class java.lang.Object