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 | Field and Description |
---|---|
static Sequent |
EMPTY_SEQUENT |
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
|
ImmutableList<SequentFormula> |
asList()
Returns a list containing every
SequentFormula in this sequent. |
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.)
|
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)
Computes the position of the given sequent formula on the proof sequent,
starting with one for the very first sequent formula.
|
SequentFormula |
getFormulabyNr(int formulaNumber) |
java.util.Set<Name> |
getOccuringTermLabels() |
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()
Computes the size of the proof sequent recursively (decends to antecedent and succedent).
|
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
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
replacedpublic boolean isEmpty()
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public int formulaNumberInSequent(boolean inAntec, SequentFormula cfma)
inAntec
- a boolean stating whether we search in the antecedent or the succedentcfma
- the given sequent formulapublic SequentFormula getFormulabyNr(int formulaNumber)
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 forpublic java.util.Set<Name> getOccuringTermLabels()
public boolean contains(SequentFormula form)
form
- the given formulapublic ImmutableList<SequentFormula> asList()
SequentFormula
in this sequent.SequentFormula
in this sequent.Copyright © 2003-2019 The KeY-Project.