public class Semisequent extends java.lang.Object implements java.lang.Iterable<SequentFormula>
Modifier and Type | Field and Description |
---|---|
static Semisequent |
EMPTY_SEMISEQUENT
the empty semisequent (using singleton pattern)
|
Constructor and Description |
---|
Semisequent(SequentFormula seqFormula)
creates a new Semisequent with the Semisequent elements in
seqList
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<SequentFormula> |
asList() |
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
|
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
|
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
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()
public 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()
public 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
Copyright © 2003-2019 The KeY-Project.