de.uka.ilkd.key.logic

Class Semisequent

java.lang.Object

de.uka.ilkd.key.logic.Semisequent

All Implemented Interfaces:

java.lang.Iterable<SequentFormula>

Direct Known Subclasses:

Semisequent.Empty

public class Semisequent
extends java.lang.Object
implements java.lang.Iterable<SequentFormula>

This class represents the succedent or antecendent part of a sequent. It is more or less a list without duplicates and subsumed formulas. This is ensured using method removeRedundancy. In future versions it can be enhanced to do other simplifications. A sequent and so a semisequent has to be immutable.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	Semisequent.Empty

Field Summary

Fields

Modifier and Type	Field and Description
static Semisequent	EMPTY_SEMISEQUENT the empty semisequent (using singleton pattern)
private ImmutableList<SequentFormula>	seqList list with the SequentFormulas of the Semisequent

Constructor Summary

Constructors

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

Method Summary

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()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Field Detail

EMPTY_SEMISEQUENT

public static final Semisequent EMPTY_SEMISEQUENT

the empty semisequent (using singleton pattern)

seqList

private final ImmutableList<SequentFormula> seqList

list with the SequentFormulas of the Semisequent

Constructor Detail

Semisequent

private Semisequent()

used by inner class Empty

Semisequent

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

public Semisequent(SequentFormula seqFormula)

creates a new Semisequent with the Semisequent elements in seqList

Method Detail

insert

public 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

Parameters:

idx - int encoding the place the element has to be put

sequentFormula - SequentFormula to be inserted

Returns:

a semi sequent change information object with the new semisequent and information which formulas have been added or removed

insert

public SemisequentChangeInfo insert(int idx,
                                    ImmutableList<SequentFormula> insertionList)

inserts the elements of the list at the specified index performing redundancy checks

Parameters:

idx - int encoding the place where the insertion starts

insertionList - IList to be inserted starting at idx

Returns:

a semi sequent change information object with the new semisequent and information which formulas have been added or removed

insertFirst

public SemisequentChangeInfo insertFirst(SequentFormula sequentFormula)

inserts element at index 0 performing redundancy checks, this may result in returning same semisequent if inserting would create redundancies

Parameters:

sequentFormula - SequentFormula to be inserted

Returns:

a semi sequent change information object with the new semisequent and information which formulas have been added or removed

insertFirst

public 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

Parameters:

insertions - IList to be inserted

Returns:

a semi sequent change information object with the new semisequent and information which formulas have been added or removed

insertLast

public 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

Parameters:

sequentFormula - SequentFormula to be inserted

Returns:

a semi sequent change information object with the new semisequent and information which formulas have been added or removed

insertLast

public 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

Parameters:

insertions - the IList to be inserted

Returns:

a semi sequent change information object with the new semisequent and information which formulas have been added or removed

isEmpty

public boolean isEmpty()

is this a semisequent that contains no formulas

Returns:

true if the semisequent contains no formulas

insertAndRemoveRedundancyHelper

private SemisequentChangeInfo insertAndRemoveRedundancyHelper(int idx,
                                                              SequentFormula sequentFormula,
                                                              SemisequentChangeInfo semiCI,
                                                              FormulaChangeInfo fci)

inserts new SequentFormula at index idx and removes duplicates, perform simplifications etc.

Parameters:

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 formulas

Returns:

a semi sequent change information object with the new semisequent and information which formulas have been added or removed

insertAndRemoveRedundancy

private SemisequentChangeInfo insertAndRemoveRedundancy(int idx,
                                                        ImmutableList<SequentFormula> sequentFormulasToBeInserted,
                                                        SemisequentChangeInfo sci)

. inserts new ConstrainedFormulas starting at index idx and removes duplicates, perform simplifications etc.

Parameters:

sequentFormulasToBeInserted - the ImmutableList to be inserted at position idx

idx - an int that means insert sequentFormula at the idx-th position in the semisequent

Returns:

a semi sequent change information object with the new semisequent and information which formulas have been added or removed

removeRedundance

private SemisequentChangeInfo removeRedundance(int idx,
                                               ImmutableList<SequentFormula> sequentFormula)

. inserts new ConstrainedFormulas starting at index idx and removes duplicates, perform simplifications etc.

Parameters:

sequentFormula - the IList to be inserted at position idx

idx - an int that means insert sequentFormula at the idx-th position in the semisequent

Returns:

a semi sequent change information object with the new semisequent and information which formulas have been added or removed

removeRedundance

private SemisequentChangeInfo removeRedundance(int idx,
                                               SequentFormula sequentFormula)

. inserts new SequentFormula at index idx and removes duplicates, perform simplifications etc.

Parameters:

sequentFormula - the SequentFormula to be inserted at position idx

idx - an int that means insert sequentFormula at the idx-th position in the semisequent

Returns:

new Semisequent with sequentFormula at index idx and removed redundancies

replace

public SemisequentChangeInfo replace(PosInOccurrence pos,
                                     SequentFormula sequentFormula)

replaces the element at place idx with sequentFormula

Parameters:

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 idx

Returns:

a semi sequent change information object with the new semisequent and information which formulas have been added or removed

replace

public SemisequentChangeInfo replace(int idx,
                                     SequentFormula sequentFormula)

replaces the idx-th formula by sequentFormula

Parameters:

idx - the int with the position of the formula to be replaced

sequentFormula - the SequentFormula replacing the formula at the given position

Returns:

a SemisequentChangeInfo containing the new sequent and a diff to the old one

replace

public 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

Parameters:

pos - the formula to be replaced

replacements - the IList whose head replaces the element at index idx and the tail is added to the semisequent

Returns:

a semi sequent change information object with the new semisequent and information which formulas have been added or removed

replace

public SemisequentChangeInfo replace(int idx,
                                     ImmutableList<SequentFormula> replacements)

replaces the formula at position idx by the given list of formulas

Parameters:

idx - the position

replacements - the new formulas

Returns:

change information including the resulting semisequent after the replacement

size

public int size()

Returns:

int counting the elements of this semisequent

complete

@Deprecated
private SemisequentChangeInfo complete(SemisequentChangeInfo semiCI)

Deprecated. Use de.uka.ilkd.key.logic.SemisequentChangeInfo#complete(de.uka.ilkd.key.logic.Semisequent) instead

creates a semisequent out of the semisequent change info (semiCI) object and hands it over to semiCI

remove

public SemisequentChangeInfo remove(int idx)

removes an element

Parameters:

idx - int being the index of the element that has to be removed

Returns:

a semi sequent change information object with the new semisequent and information which formulas have been added or removed

indexOf

public int indexOf(SequentFormula sequentFormula)

returns the index of the given SequentFormula or -1 if the sequent formula is not found. Equality of sequent formulas is checked sing the identy check (i.e.,==)

Parameters:

sequentFormula - the SequentFormula to look for

Returns:

index of sequentFormula (-1 if not found)

get

public SequentFormula get(int idx)

gets the element at a specific index

Parameters:

idx - int representing the index of the element we want to have

Returns:

SequentFormula found at index idx

Throws:

java.lang.IndexOutOfBoundsException - if idx is negative or greater or equal to Sequent.size()

getFirst

public SequentFormula getFirst()

Returns:

the first SequentFormula of this Semisequent

contains

public boolean contains(SequentFormula sequentFormula)

checks if the SequentFormula occurs in this Semisequent (identity check)

Parameters:

sequentFormula - the SequentFormula to look for

Returns:

true iff. sequentFormula has been found in this Semisequent

containsEqual

public boolean containsEqual(SequentFormula sequentFormula)

checks if a SequentFormula is in this Semisequent (equality check)

Parameters:

sequentFormula - the SequentFormula to look for

Returns:

true iff. sequentFormula has been found in this Semisequent

iterator

public java.util.Iterator<SequentFormula> iterator()

returns iterator about the elements of the sequent

Specified by:

iterator in interface java.lang.Iterable<SequentFormula>

Returns:

Iterator

asList

public ImmutableList<SequentFormula> asList()

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

Returns:

String representation of this Semisequent