| java.lang.Object
 de.uka.ilkd.key.logic.Sequent
| Inner Class :static class NILSequent extends Sequent | |
| Inner Class :static class SequentIterator implements IteratorOfConstrainedFormula | |
| Method Summary | |
| public SequentChangeInfo | addFormula(ConstrainedFormula cf, boolean antec, boolean first)
adds a formula to the antecedent (or succedent) of the
sequent. | | public SequentChangeInfo | addFormula(ConstrainedFormula cf, PosInOccurrence p)
adds a formula to the sequent at the given
position. | | public SequentChangeInfo | addFormula(ListOfConstrainedFormula insertions, boolean antec, boolean first)
adds list of formulas to the antecedent (or succedent) of the
sequent. | | public SequentChangeInfo | addFormula(ListOfConstrainedFormula insertions, PosInOccurrence p)
adds the formulas of list insertions to the sequent starting at
position p. | | public Semisequent | antecedent()
| | public SequentChangeInfo | changeFormula(ConstrainedFormula newCF, PosInOccurrence p)
| | public SequentChangeInfo | changeFormula(ListOfConstrainedFormula replacements, PosInOccurrence p)
| | public static Sequent | createAnteSequent(Semisequent ante)
| | public static Sequent | createSequent(Semisequent ante, Semisequent succ)
| | public static Sequent | createSuccSequent(Semisequent succ)
| | public boolean | equals(Object o)
| | public int | formulaNumberInSequent(boolean inAntec, ConstrainedFormula cfma)
| | public ConstrainedFormula | getFormulabyNr(int formulaNumber)
| | public int | hashCode()
| | public boolean | isEmpty()
determines if the sequent is empty. | | public IteratorOfConstrainedFormula | iterator()
| | public boolean | numberInAntec(int formulaNumber)
| | public void | prettyprint(de.uka.ilkd.key.pp.LogicPrinter printer)
| | public void | prettyprint(de.uka.ilkd.key.pp.LogicPrinter printer, SequentPrintFilter filter)
| | public StringBuffer | prettyprint(Services services)
| | public SequentChangeInfo | removeFormula(PosInOccurrence p)
| | public int | size()
| | public Semisequent | succedent()
| | public String | toString()
| | public boolean | varIsBound(QuantifiableVariable v)
returns true iff the given variable is bound in a formula of a
ConstrainedFormula in this sequent. |
| addFormula | | public SequentChangeInfo addFormula(ConstrainedFormula cf, boolean antec, boolean first)(Code) | | adds a formula to the antecedent (or succedent) of the
sequent. Depending on the value of first the formulas are
inserted at the beginning or end of the ante-/succedent.
(NOTICE:Sequent determines
index using identy (==) not equality.)
Parameters:
cf - the ConstrainedFormula to be added
Parameters:
antec - boolean selecting the correct semisequent where toinsert the formulas. If set to true, the antecedent is takenotherwise the succedent.
Parameters:
first - boolean if true the formula is added at thebeginning of the ante-/succedent, otherwise to the end a SequentChangeInfo which contains the new sequent andinformation which formulas have been added or removed |
| addFormula | | public SequentChangeInfo addFormula(ConstrainedFormula cf, PosInOccurrence p)(Code) | | adds a formula to the sequent at the given
position. (NOTICE:Sequent determines
index using identy (==) not equality.)
Parameters:
cf - a ConstrainedFormula to be added
Parameters:
p - a PosInOccurrence describes position in the sequent a SequentChangeInfo which contains the new sequent andinformation which formulas have been added or removed |
| addFormula | | public SequentChangeInfo addFormula(ListOfConstrainedFormula insertions, boolean antec, boolean first)(Code) | | adds list of formulas to the antecedent (or succedent) of the
sequent. Depending on the value of first the formulas are
inserted at the beginning or end of the ante-/succedent.
(NOTICE:Sequent determines
index using identity (==) not equality.)
Parameters:
insertions - the ListOfConstrainedFormula to be added
Parameters:
antec - boolean selecting the correct semisequent where toinsert the formulas. If set to true, the antecedent is takenotherwise the succedent.
Parameters:
first - boolean if true the formulas are added at thebeginning of the ante-/succedent, otherwise to the end a SequentChangeInfo which contains the new sequent andinformation which formulas have been added or removed |
| addFormula | | public SequentChangeInfo addFormula(ListOfConstrainedFormula insertions, PosInOccurrence p)(Code) | | adds the formulas of list insertions to the sequent starting at
position p. (NOTICE:Sequent determines
index using identy (==) not equality.)
Parameters:
insertions - a ListOfConstrainedFormula with the formulas to be added
Parameters:
p - the PosInOccurrence describing the position where toinsert the formulas a SequentChangeInfo which contains the new sequent andinformation which formulas have been added or removed |
| antecedent | | public Semisequent antecedent()(Code) | | returns semisequent of the antecedent to work with
|
| changeFormula | | public SequentChangeInfo changeFormula(ConstrainedFormula newCF, PosInOccurrence p)(Code) | | replaces the formula at the given position with another one
(NOTICE:Sequent determines
index using identity (==) not equality.)
Parameters:
newCF - the ConstrainedFormula replacing the old one
Parameters:
p - a PosInOccurrence describes position in the sequent a SequentChangeInfo which contains the new sequent andinformation which formulas have been added or removed |
| changeFormula | | public SequentChangeInfo changeFormula(ListOfConstrainedFormula replacements, PosInOccurrence p)(Code) | | 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.)
Parameters:
replacements - the ListOfConstrainedFormula whose headreplaces the formula at position p and adds the rest of the listbehind the changed formula
Parameters:
p - a PosInOccurrence describing the position of the formulato be replaced a SequentChangeInfo which contains the new sequent andinformation which formulas have been added or removed |
| createAnteSequent | | public static Sequent createAnteSequent(Semisequent ante)(Code) | | creates a new Sequent with empty succedent
Parameters:
ante - the Semisequent that plays the antecedent part the new sequent or the EMPTY_SEQUENT if both antec and succare same as EMPTY_SEMISEQUENT |
| createSequent | | public static Sequent createSequent(Semisequent ante, Semisequent succ)(Code) | | creates a new Sequent
Parameters:
ante - the Semisequent that plays the antecedent part
Parameters:
succ - the Semisequent that plays the succedent part the new sequent or the EMPTY_SEQUENT if both antec and succare same as EMPTY_SEMISEQUENT |
| createSuccSequent | | public static Sequent createSuccSequent(Semisequent succ)(Code) | | creates a new Sequent with empty antecedent
Parameters:
succ - the Semisequent that plays the succedent part the new sequent or the EMPTY_SEQUENT if both antec and succare same as EMPTY_SEMISEQUENT |
| hashCode | | public int hashCode()(Code) | | |
| isEmpty | | public boolean isEmpty()(Code) | | determines if the sequent is empty.
true iff the sequent consists of two instances ofSemisequent.EMPTY_SEMISEQUENT |
| iterator | | public IteratorOfConstrainedFormula iterator()(Code) | | returns iterator about all ConstrainedFormulae of the sequent
iterator about all ConstrainedFormulae of the sequent |
| numberInAntec | | public boolean numberInAntec(int formulaNumber)(Code) | | |
| removeFormula | | public SequentChangeInfo removeFormula(PosInOccurrence p)(Code) | | removes the formula at position p (NOTICE:Sequent determines
index using identity (==) not equality.)
Parameters:
p - a PosInOccurrence that describes position in the sequent a SequentChangeInfo which contains the new sequent andinformation which formulas have been added or removed |
| succedent | | public Semisequent succedent()(Code) | | returns semisequent of the succedent to work with
|
| toString | | public String toString()(Code) | | String representation of the sequent
String representation of the sequent |
| varIsBound | | public boolean varIsBound(QuantifiableVariable v)(Code) | | returns true iff the given variable is bound in a formula of a
ConstrainedFormula in this sequent.
Parameters:
v - the bound variable to search for |
|
|