public class FormulaTagManager
extends java.lang.Object
Goal
class, and are
not immutableModifier and Type | Class and Description |
---|---|
private static class |
FormulaTagManager.FormulaInfo
Class that holds information about a formula, namely the current position
(
PosInOccurrence ) as well as a list of the modifications
that have been applied to the formula so far. |
Modifier and Type | Field and Description |
---|---|
private FormulaTagManager.FormulaInfo |
lastQueryResult |
private FormulaTag |
lastTagQueried |
private java.util.HashMap<PosInOccurrence,FormulaTag> |
pioToTag
Key: PosInOccurrence Value: FormulaTag
|
private java.util.HashMap<FormulaTag,FormulaTagManager.FormulaInfo> |
tagToFormulaInfo
Key: FormulaTag Value: FormulaInfo
|
Modifier | Constructor and Description |
---|---|
(package private) |
FormulaTagManager(Goal p_goal)
Create a new manager that is initialised with the formulas of the given
sequent
|
private |
FormulaTagManager(java.util.HashMap<FormulaTag,FormulaTagManager.FormulaInfo> p_tagToPIO,
java.util.HashMap<PosInOccurrence,FormulaTag> p_pioToTag) |
Modifier and Type | Method and Description |
---|---|
private void |
addTags(SequentChangeInfo sci,
boolean p_antec,
Goal p_goal) |
java.lang.Object |
clone() |
FormulaTagManager |
copy() |
private void |
createNewTag(PosInOccurrence p_pio,
Goal p_goal)
Add a new tag to the maps
|
private void |
createNewTags(Goal p_goal)
Create new tags for all formulas of a sequent
|
private void |
createNewTags(Goal p_goal,
boolean p_antec)
Create new tags for all formulas of a semisequent
|
long |
getAgeForTag(FormulaTag p_tag) |
private FormulaTagManager.FormulaInfo |
getFormulaInfo(FormulaTag p_tag) |
ImmutableList<FormulaChangeInfo> |
getModifications(FormulaTag p_tag) |
PosInOccurrence |
getPosForTag(FormulaTag p_tag) |
FormulaTag |
getTagForPos(PosInOccurrence p_pio) |
private void |
putInQueryCache(FormulaTag p_tag,
FormulaTagManager.FormulaInfo p_info) |
private void |
removeTag(PosInOccurrence p_pio)
Remove the entries for the given formulas from the maps
|
private void |
removeTags(SequentChangeInfo sci,
boolean p_antec,
Goal p_goal) |
void |
sequentChanged(Goal source,
SequentChangeInfo sci) |
private void |
updateTag(FormulaChangeInfo p_info,
Sequent p_newSeq,
Goal p_goal) |
private void |
updateTags(SequentChangeInfo sci,
boolean p_antec,
Goal p_goal) |
private final java.util.HashMap<FormulaTag,FormulaTagManager.FormulaInfo> tagToFormulaInfo
private final java.util.HashMap<PosInOccurrence,FormulaTag> pioToTag
private FormulaTag lastTagQueried
private FormulaTagManager.FormulaInfo lastQueryResult
FormulaTagManager(Goal p_goal)
private FormulaTagManager(java.util.HashMap<FormulaTag,FormulaTagManager.FormulaInfo> p_tagToPIO, java.util.HashMap<PosInOccurrence,FormulaTag> p_pioToTag)
public FormulaTag getTagForPos(PosInOccurrence p_pio)
public PosInOccurrence getPosForTag(FormulaTag p_tag)
PosInOccurrence
can
be obsolete and refer to a previous node. If no formula is assigned to
the given tag, null
is returnedpublic long getAgeForTag(FormulaTag p_tag)
Goal.getTime()
) of the
formula, i.e. the time when the formula was introduced resp. when
the last modification was applied to the formula. If no formula
is assigned to the given tag, 0
is returnedpublic ImmutableList<FormulaChangeInfo> getModifications(FormulaTag p_tag)
public void sequentChanged(Goal source, SequentChangeInfo sci)
private void updateTags(SequentChangeInfo sci, boolean p_antec, Goal p_goal)
private void addTags(SequentChangeInfo sci, boolean p_antec, Goal p_goal)
private void removeTags(SequentChangeInfo sci, boolean p_antec, Goal p_goal)
public java.lang.Object clone()
clone
in class java.lang.Object
public FormulaTagManager copy()
private void createNewTags(Goal p_goal)
p_goal
- The sequentprivate void createNewTags(Goal p_goal, boolean p_antec)
p_goal
- The sequent that contains the semisequentp_antec
- true iff the formulas of the antecedent should be addedprivate void createNewTag(PosInOccurrence p_pio, Goal p_goal)
p_pio
- The formula for which a new tag is supposed to be createdprivate void removeTag(PosInOccurrence p_pio)
private void updateTag(FormulaChangeInfo p_info, Sequent p_newSeq, Goal p_goal)
private void putInQueryCache(FormulaTag p_tag, FormulaTagManager.FormulaInfo p_info)
private FormulaTagManager.FormulaInfo getFormulaInfo(FormulaTag p_tag)