public class Sequent extends java.lang.Object implements java.lang.Iterable<SequentFormula>
A sequent is created either by using one of
the composition methods, that are
createSequent(de.uka.ilkd.key.logic.Semisequent, de.uka.ilkd.key.logic.Semisequent)
,
createAnteSequent(de.uka.ilkd.key.logic.Semisequent)
and
createSuccSequent(de.uka.ilkd.key.logic.Semisequent)
or by inserting formulas directly into EMPTY_SEQUENT
.
Modifier and Type | Class and Description |
---|---|
(package private) static class |
Sequent.NILSequent |
(package private) static class |
Sequent.SequentIterator |
Modifier and Type | Field and Description |
---|---|
private Semisequent |
antecedent |
static Sequent |
EMPTY_SEQUENT |
private Semisequent |
succedent |
Modifier | Constructor and Description |
---|---|
private |
Sequent()
must only be called by NILSequent
|
private |
Sequent(Semisequent antecedent,
Semisequent succedent)
creates new Sequent with antecedence and succedence
|
Modifier and Type | Method and Description |
---|---|
SequentChangeInfo |
addFormula(ImmutableList<SequentFormula> insertions,
boolean antec,
boolean first)
adds list of formulas to the antecedent (or succedent) of the
sequent.
|
SequentChangeInfo |
addFormula(ImmutableList<SequentFormula> insertions,
PosInOccurrence p)
adds the formulas of list insertions to the sequent starting at
position p.
|
SequentChangeInfo |
addFormula(SequentFormula cf,
boolean antec,
boolean first)
adds a formula to the antecedent (or succedent) of the
sequent.
|
SequentChangeInfo |
addFormula(SequentFormula cf,
PosInOccurrence p)
adds a formula to the sequent at the given
position.
|
Semisequent |
antecedent()
returns semisequent of the antecedent to work with
|
SequentChangeInfo |
changeFormula(ImmutableList<SequentFormula> replacements,
PosInOccurrence p)
replaces the formula at position p with the head of the given
list and adds the remaining list elements to the sequent
(NOTICE:Sequent determines
index using identity (==) not equality.)
|
SequentChangeInfo |
changeFormula(SequentFormula newCF,
PosInOccurrence p)
replaces the formula at the given position with another one
(NOTICE:Sequent determines
index using identity (==) not equality.)
|
private Sequent |
composeSequent(boolean antec,
Semisequent semiSeq)
replaces the antecedent (
antec is true) of this sequent by the given Semisequent
similar for the succedent if antec is false. |
boolean |
contains(SequentFormula form)
used to check whether this sequent contains a given sequent formula.
|
static Sequent |
createAnteSequent(Semisequent ante)
creates a new Sequent with empty succedent
|
static Sequent |
createSequent(Semisequent ante,
Semisequent succ)
creates a new Sequent
|
static Sequent |
createSuccSequent(Semisequent succ)
creates a new Sequent with empty antecedent
|
boolean |
equals(java.lang.Object o) |
int |
formulaNumberInSequent(boolean inAntec,
SequentFormula cfma) |
SequentFormula |
getFormulabyNr(int formulaNumber) |
private static java.util.Set<Name> |
getLabelsForTermRecursively(Term term) |
java.util.Set<Name> |
getOccuringTermLabels() |
private Semisequent |
getSemisequent(PosInOccurrence p)
returns the semisequent in which the SequentFormula described
by PosInOccurrence p lies
|
int |
hashCode() |
boolean |
isEmpty()
determines if the sequent is empty.
|
java.util.Iterator<SequentFormula> |
iterator()
returns iterator about all ConstrainedFormulae of the sequent
|
boolean |
numberInAntec(int formulaNumber) |
SequentChangeInfo |
removeFormula(PosInOccurrence p)
removes the formula at position p (NOTICE:Sequent determines
index using identity (==) not equality.)
|
int |
size() |
Semisequent |
succedent()
returns semisequent of the succedent to work with
|
java.lang.String |
toString()
String representation of the sequent
|
boolean |
varIsBound(QuantifiableVariable v)
returns true iff the given variable is bound in a formula of a
SequentFormula in this sequent.
|
public static final Sequent EMPTY_SEQUENT
private final Semisequent antecedent
private final Semisequent succedent
private Sequent()
private Sequent(Semisequent antecedent, Semisequent succedent)
public static Sequent createAnteSequent(Semisequent ante)
ante
- the Semisequent that plays the antecedent partpublic static Sequent createSequent(Semisequent ante, Semisequent succ)
ante
- the Semisequent that plays the antecedent partsucc
- the Semisequent that plays the succedent partpublic static Sequent createSuccSequent(Semisequent succ)
succ
- the Semisequent that plays the succedent partpublic SequentChangeInfo addFormula(SequentFormula cf, boolean antec, boolean first)
cf
- the SequentFormula to be addedantec
- boolean selecting the correct semisequent where to
insert the formulas. If set to true, the antecedent is taken
otherwise the succedent.first
- boolean if true the formula is added at the
beginning of the ante-/succedent, otherwise to the endpublic SequentChangeInfo addFormula(SequentFormula cf, PosInOccurrence p)
cf
- a SequentFormula to be addedp
- a PosInOccurrence describes position in the sequentpublic SequentChangeInfo addFormula(ImmutableList<SequentFormula> insertions, boolean antec, boolean first)
insertions
- the IListantec
- boolean selecting the correct semisequent where to
insert the formulas. If set to true, the antecedent is taken
otherwise the succedent.first
- boolean if true the formulas are added at the
beginning of the ante-/succedent, otherwise to the endpublic SequentChangeInfo addFormula(ImmutableList<SequentFormula> insertions, PosInOccurrence p)
insertions
- a IListp
- the PosInOccurrence describing the position where to
insert the formulaspublic Semisequent antecedent()
public SequentChangeInfo changeFormula(SequentFormula newCF, PosInOccurrence p)
newCF
- the SequentFormula replacing the old onep
- a PosInOccurrence describes position in the sequentpublic SequentChangeInfo changeFormula(ImmutableList<SequentFormula> replacements, PosInOccurrence p)
replacements
- the IListp
- a PosInOccurrence describing the position of the formula
to be replacedprivate Sequent composeSequent(boolean antec, Semisequent semiSeq)
antec
is true) of this sequent by the given Semisequent
similar for the succedent if antec
is false.antec
- if the antecedent or succedent shall be replacedsemiSeq
- the Semisequent
to usepublic boolean isEmpty()
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public int formulaNumberInSequent(boolean inAntec, SequentFormula cfma)
public SequentFormula getFormulabyNr(int formulaNumber)
private Semisequent getSemisequent(PosInOccurrence p)
public int hashCode()
hashCode
in class java.lang.Object
public java.util.Iterator<SequentFormula> iterator()
iterator
in interface java.lang.Iterable<SequentFormula>
public boolean numberInAntec(int formulaNumber)
public SequentChangeInfo removeFormula(PosInOccurrence p)
p
- a PosInOccurrence that describes position in the sequentpublic int size()
public Semisequent succedent()
public java.lang.String toString()
toString
in class java.lang.Object
public boolean varIsBound(QuantifiableVariable v)
v
- the bound variable to search forprivate static java.util.Set<Name> getLabelsForTermRecursively(Term term)
public java.util.Set<Name> getOccuringTermLabels()
public boolean contains(SequentFormula form)
form
- the given formula