public class SingleSuccedentSequentOnBitSet extends java.lang.Object implements _SingleSuccedentSequent, java.lang.Cloneable
_Sequent
interface on Formula
using a
BitSet to represent the left-hand side of the sequent.Constructor and Description |
---|
SingleSuccedentSequentOnBitSet(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 SingleSuccedentSequentOnBitSet |
buildArraySequent(FormulaFactory factory,
java.util.Collection<Formula> leftFormulas,
Formula rightFormula) |
SingleSuccedentSequentOnBitSet |
clone()
Returns a fresh copy of this sequent.
|
boolean |
contains(SingleSuccedentSequentOnBitSet other)
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 . |
boolean |
containsLeft(Formula wff)
Returns
true if this sequent contains the specified formula in
the left hand side and false otherwise. |
boolean |
equals(java.lang.Object obj) |
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. |
int |
hashCode() |
boolean |
isContained(SingleSuccedentSequentOnBitSet other)
Returns
true if this sequent is contained in the other. |
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 SingleSuccedentSequentOnBitSet(FormulaFactory factory)
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 static SingleSuccedentSequentOnBitSet buildArraySequent(FormulaFactory factory, java.util.Collection<Formula> leftFormulas, Formula rightFormula)
public SingleSuccedentSequentOnBitSet clone()
_SingleSuccedentSequent
clone
in interface _AbstractGoal
clone
in interface _SingleSuccedentSequent
clone
in class java.lang.Object
public boolean contains(SingleSuccedentSequentOnBitSet other)
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
.other
- the other sequent.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 java.lang.String format()
_AbstractGoal
format
in interface _AbstractGoal
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 getLeft()
_SingleSuccedentSequent
null
if le theft hand side is empty.getLeft
in interface _SingleSuccedentSequent
null
.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 getRight()
_SingleSuccedentSequent
null
if the right hand side of this sequent is empty.getRight
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 isContained(SingleSuccedentSequentOnBitSet other)
true
if this sequent is contained in the other.other
- the other sequent.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 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 java.lang.String toString()
toString
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public boolean equals(java.lang.Object obj)
equals
in class java.lang.Object