| java.lang.Object
 de.uka.ilkd.key.logic.SemisequentChangeInfo
| SemisequentChangeInfo | | public class SemisequentChangeInfo implements java.io.Serializable(Code) | | Records the changes made to a semisequent. Keeps track of added and
removed formula to the semisequents.
|
| Field Summary | |
| public ListOfConstrainedFormula | rejected
|
| rejected | | public ListOfConstrainedFormula rejected(Code) | | contains formulas that have been tried to add, but which have been rejected due to
already existing formulas in the sequent subsuming these formulas
|
| SemisequentChangeInfo | | public SemisequentChangeInfo()(Code) | | |
| SemisequentChangeInfo | | public SemisequentChangeInfo(ListOfConstrainedFormula formulas)(Code) | | |
| addedFormulas | | public ListOfConstrainedFormula addedFormulas()(Code) | | returns the list of all added constrained formulas
ListOfConstrainedFormula added to the semisequent |
| getFormulaList | | public ListOfConstrainedFormula getFormulaList()(Code) | | returns the list of constrained formula of the new semisequent
|
| getIndex | | public int getIndex()(Code) | | returns the index of the last added formula
|
| hasChanged | | public boolean hasChanged()(Code) | | returns true if the semisequent has changed
|
| modifiedFormula | | public void modifiedFormula(int idx, FormulaChangeInfo fci)(Code) | | logs a modified formula at position idx
|
| modifiedFormulas | | public ListOfFormulaChangeInfo modifiedFormulas()(Code) | | returns the list of all modification positions
ListOfConstrainedFormula modified within thesemisequent |
| rejectedFormula | | public void rejectedFormula(ConstrainedFormula f)(Code) | | adding formula f to the semisequent failed due to
a redundance check. This means an equal or stronger formula
is already present in the semisequent
Parameters:
f - the ConstrainedFormula |
| rejectedFormulas | | public ListOfConstrainedFormula rejectedFormulas()(Code) | | returns a list of formulas that have been tried to add to
the semisequent but got rejected as they were redundant
list of formulas rejected due to redundancy |
| removedFormulas | | public ListOfConstrainedFormula removedFormulas()(Code) | | returns the list of all removed constrained formulas
ListOfConstrainedFormula removed from the semisequent |
| semisequent | | public Semisequent semisequent()(Code) | | returns the semisequent that is the result of the change
operation
|
| setFormulaList | | public void setFormulaList(ListOfConstrainedFormula list)(Code) | | sets the list of constrained formula containing all formulas of
the semisequent after the operation
|
| setSemisequent | | public void setSemisequent(Semisequent semisequent)(Code) | | sets the resulting semisequent
|
|
|