public class Semisequent extends java.lang.Object implements java.lang.Iterable<SequentFormula>
Modifier and Type | Class and Description |
---|---|
private static class |
Semisequent.Empty |
Modifier and Type | Field and Description |
---|---|
static Semisequent |
EMPTY_SEMISEQUENT
the empty semisequent (using singleton pattern)
|
private ImmutableList<SequentFormula> |
seqList
list with the
SequentFormula s of the Semisequent |
Modifier | Constructor and Description |
---|---|
private |
Semisequent()
used by inner class Empty
|
(package private) |
Semisequent(ImmutableList<SequentFormula> seqList)
creates a new Semisequent with the Semisequent elements in
seqList; the provided list must be redundance free, i.e.,
the created sequent must be exactly the same as when creating the sequent
by subsequently inserting all formulas
|
|
Semisequent(SequentFormula seqFormula)
creates a new Semisequent with the Semisequent elements in
seqList
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<SequentFormula> |
asList() |
private SemisequentChangeInfo |
complete(SemisequentChangeInfo semiCI)
Deprecated.
Use
de.uka.ilkd.key.logic.SemisequentChangeInfo#complete(de.uka.ilkd.key.logic.Semisequent) instead |
boolean |
contains(SequentFormula sequentFormula)
checks if the
SequentFormula occurs in this
Semisequent (identity check) |
boolean |
containsEqual(SequentFormula sequentFormula)
checks if a
SequentFormula is in this Semisequent
(equality check) |
boolean |
equals(java.lang.Object o) |
SequentFormula |
get(int idx)
gets the element at a specific index
|
SequentFormula |
getFirst() |
int |
hashCode() |
int |
indexOf(SequentFormula sequentFormula)
returns the index of the given
SequentFormula or -1
if the sequent formula is not found. |
SemisequentChangeInfo |
insert(int idx,
ImmutableList<SequentFormula> insertionList)
inserts the elements of the list at the specified index
performing redundancy checks
|
SemisequentChangeInfo |
insert(int idx,
SequentFormula sequentFormula)
inserts an element at a specified index performing redundancy
checks, this may result in returning same semisequent if
inserting would create redundancies
|
private SemisequentChangeInfo |
insertAndRemoveRedundancy(int idx,
ImmutableList<SequentFormula> sequentFormulasToBeInserted,
SemisequentChangeInfo sci)
.
|
private SemisequentChangeInfo |
insertAndRemoveRedundancyHelper(int idx,
SequentFormula sequentFormula,
SemisequentChangeInfo semiCI,
FormulaChangeInfo fci)
inserts new SequentFormula at index idx and removes
duplicates, perform simplifications etc.
|
SemisequentChangeInfo |
insertFirst(ImmutableList<SequentFormula> insertions)
inserts element at index 0 performing redundancy
checks, this may result in returning same semisequent if
inserting would create redundancies
|
SemisequentChangeInfo |
insertFirst(SequentFormula sequentFormula)
inserts element at index 0 performing redundancy
checks, this may result in returning same semisequent if
inserting would create redundancies
|
SemisequentChangeInfo |
insertLast(ImmutableList<SequentFormula> insertions)
inserts the formulas of the list at the end of the semisequent
performing redundancy checks, this may result in returning same
semisequent if inserting would create redundancies
|
SemisequentChangeInfo |
insertLast(SequentFormula sequentFormula)
inserts element at the end of the semisequent performing
redundancy checks, this may result in returning same
semisequent if inserting would create redundancies
|
boolean |
isEmpty()
is this a semisequent that contains no formulas
|
java.util.Iterator<SequentFormula> |
iterator()
returns iterator about the elements of the sequent
|
SemisequentChangeInfo |
remove(int idx)
removes an element
|
private SemisequentChangeInfo |
removeRedundance(int idx,
ImmutableList<SequentFormula> sequentFormula)
.
|
private SemisequentChangeInfo |
removeRedundance(int idx,
SequentFormula sequentFormula)
.
|
SemisequentChangeInfo |
replace(int idx,
ImmutableList<SequentFormula> replacements)
replaces the formula at position
idx by the given list of formulas |
SemisequentChangeInfo |
replace(int idx,
SequentFormula sequentFormula)
replaces the idx-th formula by sequentFormula
|
SemisequentChangeInfo |
replace(PosInOccurrence pos,
ImmutableList<SequentFormula> replacements)
replaces the element at place idx with the first element of the
given list and adds the rest of the list to the semisequent
behind the replaced formula
|
SemisequentChangeInfo |
replace(PosInOccurrence pos,
SequentFormula sequentFormula)
replaces the element at place idx with sequentFormula
|
int |
size() |
java.lang.String |
toString() |
public static final Semisequent EMPTY_SEMISEQUENT
private final ImmutableList<SequentFormula> seqList
SequentFormula
s of the Semisequentprivate Semisequent()
Semisequent(ImmutableList<SequentFormula> seqList)
public Semisequent(SequentFormula seqFormula)
public SemisequentChangeInfo insert(int idx, SequentFormula sequentFormula)
idx
- int encoding the place the element has to be putsequentFormula
- SequentFormula
to be insertedpublic SemisequentChangeInfo insert(int idx, ImmutableList<SequentFormula> insertionList)
idx
- int encoding the place where the insertion startsinsertionList
- IListpublic SemisequentChangeInfo insertFirst(SequentFormula sequentFormula)
sequentFormula
- SequentFormula to be insertedpublic SemisequentChangeInfo insertFirst(ImmutableList<SequentFormula> insertions)
insertions
- IListpublic SemisequentChangeInfo insertLast(SequentFormula sequentFormula)
sequentFormula
- SequentFormula
to be insertedpublic SemisequentChangeInfo insertLast(ImmutableList<SequentFormula> insertions)
insertions
- the IListpublic boolean isEmpty()
private SemisequentChangeInfo insertAndRemoveRedundancyHelper(int idx, SequentFormula sequentFormula, SemisequentChangeInfo semiCI, FormulaChangeInfo fci)
fci
- null if the formula to be added is new, otherwise an
object telling which formula is replaced with the new formula
sequentFormula
, and what are the differences between the
two formulasprivate SemisequentChangeInfo insertAndRemoveRedundancy(int idx, ImmutableList<SequentFormula> sequentFormulasToBeInserted, SemisequentChangeInfo sci)
sequentFormulasToBeInserted
- the ImmutableList
to be inserted at position idxidx
- an int that means insert sequentFormula at the idx-th
position in the semisequentprivate SemisequentChangeInfo removeRedundance(int idx, ImmutableList<SequentFormula> sequentFormula)
sequentFormula
- the IListidx
- an int that means insert sequentFormula at the idx-th
position in the semisequentprivate SemisequentChangeInfo removeRedundance(int idx, SequentFormula sequentFormula)
idx
and removes duplicates, perform simplifications etc.sequentFormula
- the SequentFormula to be inserted at position idxidx
- an int that means insert sequentFormula at the idx-th
position in the semisequentpublic SemisequentChangeInfo replace(PosInOccurrence pos, SequentFormula sequentFormula)
pos
- the PosInOccurrence describing the position of and within the
formula below which the formula differs from the new formula
sequentFormula
sequentFormula
- the SequentFormula replacing the old element at index idxpublic SemisequentChangeInfo replace(int idx, SequentFormula sequentFormula)
idx
- the int with the position of the formula to be replacedsequentFormula
- the SequentFormula replacing the formula at the given positionpublic SemisequentChangeInfo replace(PosInOccurrence pos, ImmutableList<SequentFormula> replacements)
pos
- the formula to be replacedreplacements
- the IListpublic SemisequentChangeInfo replace(int idx, ImmutableList<SequentFormula> replacements)
idx
by the given list of formulasidx
- the positionreplacements
- the new formulaspublic int size()
@Deprecated private SemisequentChangeInfo complete(SemisequentChangeInfo semiCI)
de.uka.ilkd.key.logic.SemisequentChangeInfo#complete(de.uka.ilkd.key.logic.Semisequent)
insteadpublic SemisequentChangeInfo remove(int idx)
idx
- int being the index of the element that has to
be removedpublic int indexOf(SequentFormula sequentFormula)
SequentFormula
or -1
if the sequent formula is not found. Equality of sequent formulas
is checked sing the identy check (i.e.,==
)sequentFormula
- the SequentFormula
to look forpublic SequentFormula get(int idx)
idx
- int representing the index of the element we
want to haveSequentFormula
found at index idxjava.lang.IndexOutOfBoundsException
- if idx is negative or
greater or equal to Sequent.size()
public SequentFormula getFirst()
SequentFormula
of this Semisequentpublic boolean contains(SequentFormula sequentFormula)
SequentFormula
occurs in this
Semisequent (identity check)sequentFormula
- the SequentFormula
to look forpublic boolean containsEqual(SequentFormula sequentFormula)
SequentFormula
is in this Semisequent
(equality check)sequentFormula
- the SequentFormula
to look forpublic java.util.Iterator<SequentFormula> iterator()
iterator
in interface java.lang.Iterable<SequentFormula>
public ImmutableList<SequentFormula> asList()
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public java.lang.String toString()
toString
in class java.lang.Object