public class SingleSuccedentSequentOnArray extends java.lang.Object implements _SingleSuccedentSequent, java.lang.Cloneable
_SingleSuccedentSequent
interface using an
array of integers to represents the sequent.Constructor and Description |
---|
SingleSuccedentSequentOnArray(FormulaFactory factory) |
Modifier and Type | Method and Description |
---|---|
void |
addLeft(Formula wff)
Add the specified formula to the left hand side of this sequent.
|
void |
addRight(Formula wff)
This method add the specified formula in the right hand side of this
sequent.
|
static SingleSuccedentSequentOnArray |
buildArraySequent(FormulaFactory factory,
java.util.Collection<Formula> leftFormulas,
Formula rightFormula) |
SingleSuccedentSequentOnArray |
clone()
Returns a fresh copy of this sequent.
|
boolean |
containsLeft(Formula wff)
Returns
true if this sequent contains the specified formula in
the left hand side and false otherwise. |
java.lang.String |
format()
Returns a string describing this goal
|
java.util.Collection<Formula> |
getAllLeftFormulas()
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. |
java.util.Collection<Formula> |
getAllLeftFormulas(FormulaType formulaType)
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. |
Formula |
getLeft()
Returns a formula from the left hand side of the sequent or
null if le theft hand side is empty. |
Formula |
getLeft(FormulaType formulaType)
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. |
Formula |
getRight()
Returns the formula in the right hand side of this sequent or
null if the right hand side of this sequent is empty. |
Formula |
getRightFormulaOfType(FormulaType formulaType)
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. |
boolean |
isIdentityAxiom()
Returns
true iff this is an identity axiom, that is a sequent
of the kind S,H ==> H . |
boolean |
removeLeft(Formula wff)
Removes the specified formula from the left hand side of this sequent, if
it is present.
|
boolean |
removeRight()
Removes the right formula form this sequent.
|
java.lang.String |
toString() |
public SingleSuccedentSequentOnArray(FormulaFactory factory)
public java.util.Collection<Formula> getAllLeftFormulas()
_SingleSuccedentSequent
null
if the left hand side of this sequent is
empty.getAllLeftFormulas
in interface _SingleSuccedentSequent
null
.public java.util.Collection<Formula> getAllLeftFormulas(FormulaType formulaType)
_SingleSuccedentSequent
null
if the left hand side
of this sequent does not contain any formula of the specified type.getAllLeftFormulas
in interface _SingleSuccedentSequent
formulaType
- the type of the formulas.null
if the left hand side of the sequent does not contain any
formula of the sepcified type.public Formula getRight()
_SingleSuccedentSequent
null
if the right hand side of this sequent is empty.getRight
in interface _SingleSuccedentSequent
null
.public void addLeft(Formula wff)
_SingleSuccedentSequent
addLeft
in interface _SingleSuccedentSequent
wff
- the formula to add.public void addRight(Formula wff)
_SingleSuccedentSequent
addRight
in interface _SingleSuccedentSequent
wff
- the formula to add in the right hand side of the sequent.public Formula getLeft(FormulaType formulaType)
_SingleSuccedentSequent
null
if no formula of the specified type occurs
in this sequent.getLeft
in interface _SingleSuccedentSequent
formulaType
- the type of the formula to be returnednull
.public Formula getLeft()
_SingleSuccedentSequent
null
if le theft hand side is empty.getLeft
in interface _SingleSuccedentSequent
null
.public Formula getRightFormulaOfType(FormulaType formulaType)
_SingleSuccedentSequent
null
if the formula in the right
hand side does not have the specified type.getRightFormulaOfType
in interface _SingleSuccedentSequent
formulaType
- the type of the formula to be returnednull
if the type of the formula in the right hand
side is different from the specified type.public boolean removeLeft(Formula wff)
_SingleSuccedentSequent
removeLeft
in interface _SingleSuccedentSequent
wff
- the formula to remove.true
if this sequent contained the specified element.public boolean removeRight()
_SingleSuccedentSequent
removeRight
in interface _SingleSuccedentSequent
true
if this sequent contained a formula in the
right-hand side.public boolean isIdentityAxiom()
_SingleSuccedentSequent
true
iff this is an identity axiom, that is a sequent
of the kind S,H ==> H
.isIdentityAxiom
in interface _SingleSuccedentSequent
true
iff this is an identity axiom.public boolean containsLeft(Formula wff)
_SingleSuccedentSequent
true
if this sequent contains the specified formula in
the left hand side and false otherwise.containsLeft
in interface _SingleSuccedentSequent
wff
- the formula to searchtrue
if the right hand side of the sequent contains
the specifiedpublic SingleSuccedentSequentOnArray clone()
_SingleSuccedentSequent
clone
in interface _AbstractGoal
clone
in interface _SingleSuccedentSequent
clone
in class java.lang.Object
public java.lang.String format()
_AbstractGoal
format
in interface _AbstractGoal
public java.lang.String toString()
toString
in class java.lang.Object
public static SingleSuccedentSequentOnArray buildArraySequent(FormulaFactory factory, java.util.Collection<Formula> leftFormulas, Formula rightFormula)