public class SemisequentChangeInfo
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private ImmutableList<SequentFormula> |
added
contains the added formulas to the semisequent
|
private int |
lastFormulaIndex |
private ImmutableList<FormulaChangeInfo> |
modified
contains the modified formulas from the semisequent
|
private ImmutableList<SequentFormula> |
modifiedSemisequent
stores the redundance free formula list of the semisequent
|
private ImmutableList<SequentFormula> |
rejected
contains formulas that have been tried to add, but which have been rejected due to
already existing formulas in the sequent subsuming these formulas
|
private ImmutableList<SequentFormula> |
removed
contains the removed formulas from the semisequent
|
Constructor and Description |
---|
SemisequentChangeInfo() |
SemisequentChangeInfo(ImmutableList<SequentFormula> formulas) |
Modifier and Type | Method and Description |
---|---|
void |
addedFormula(int idx,
SequentFormula cf)
logs an added formula at position idx
|
ImmutableList<SequentFormula> |
addedFormulas()
returns the list of all added constrained formulas
|
void |
combine(SemisequentChangeInfo succ)
This method combines this change information from this info and its successor.
|
ImmutableList<SequentFormula> |
getFormulaList()
returns the list of constrained formula of the new semisequent
|
int |
getIndex()
returns the index of the last added formula
|
boolean |
hasChanged()
returns true if the semisequent has changed
|
void |
modifiedFormula(int idx,
FormulaChangeInfo fci)
logs a modified formula at position idx
|
ImmutableList<FormulaChangeInfo> |
modifiedFormulas()
returns the list of all modification positions
|
void |
rejectedFormula(SequentFormula f)
adding formula f to the semisequent failed due to
a redundance check.
|
ImmutableList<SequentFormula> |
rejectedFormulas()
returns a list of formulas that have been tried to add to
the semisequent but got rejected as they were redundant
|
void |
removedFormula(int idx,
SequentFormula cf)
logs an added formula at position idx
|
ImmutableList<SequentFormula> |
removedFormulas()
returns the list of all removed constrained formulas
|
Semisequent |
semisequent()
returns the semisequent that is the result of the change
operation
|
void |
setFormulaList(ImmutableList<SequentFormula> list)
sets the list of constrained formula containing all formulas of
the semisequent after the operation
|
java.lang.String |
toString()
toString
|
private ImmutableList<SequentFormula> added
private ImmutableList<SequentFormula> removed
private ImmutableList<FormulaChangeInfo> modified
private ImmutableList<SequentFormula> modifiedSemisequent
private ImmutableList<SequentFormula> rejected
private int lastFormulaIndex
public SemisequentChangeInfo()
public SemisequentChangeInfo(ImmutableList<SequentFormula> formulas)
public boolean hasChanged()
public void setFormulaList(ImmutableList<SequentFormula> list)
public ImmutableList<SequentFormula> getFormulaList()
public void addedFormula(int idx, SequentFormula cf)
public void modifiedFormula(int idx, FormulaChangeInfo fci)
public ImmutableList<SequentFormula> addedFormulas()
public ImmutableList<SequentFormula> removedFormulas()
public ImmutableList<SequentFormula> rejectedFormulas()
public void rejectedFormula(SequentFormula f)
f
- the SequentFormulapublic ImmutableList<FormulaChangeInfo> modifiedFormulas()
public void removedFormula(int idx, SequentFormula cf)
public void combine(SemisequentChangeInfo succ)
succ
and does not release it. This means
when invoking the method it must be snsured that succ is never used afterwards.public int getIndex()
public Semisequent semisequent()
public java.lang.String toString()
toString
in class java.lang.Object