public class Proof extends java.lang.Object implements Named
Goal
class represents
a goal with all needed extra information, and methods to apply
rules. Furthermore it offers services that deliver the open goals,
namespaces and several other informations about the current state
of the proof.Modifier and Type | Class and Description |
---|---|
private class |
Proof.ProofPruner
This class is responsible for pruning a proof tree at a certain cutting point.
|
Modifier and Type | Field and Description |
---|---|
private AbbrevMap |
abbreviations
maps the Abbreviations valid for this proof to their corresponding terms.
|
private Strategy |
activeStrategy |
private long |
autoModeTime |
private ImmutableList<Goal> |
closedGoals
list with the closed goals of the proof, needed to make pruning in closed branches
possible.
|
(package private) long |
creationTime
The time when the
Proof instance was created. |
private boolean |
disposed
Set to true if the proof has been abandoned and the dispose method has
been called on this object.
|
private ProofEnvironment |
env
the proof environment (optional)
|
private InitConfig |
initConfig
the logic configuration for this proof, i.e., logic signature, rules etc.
|
java.util.Vector<java.lang.String> |
keyVersionLog
when load and save a proof with different versions of key this vector
fills up with Strings containing the GIT versions.
|
private java.util.List<ProofTreeListener> |
listenerList
list with prooftree listeners of this proof
attention: firing events makes use of array list's random access
nature
|
private ProofCorrectnessMgt |
localMgt
the environment of the proof with specs and java model
|
private Name |
name
name of the proof
|
private ImmutableList<Goal> |
openGoals
list with the open goals of the proof
|
private ProofIndependentSettings |
pis |
private java.lang.String |
problemHeader
declarations &c, read from a problem file or otherwise
|
private java.util.List<ProofDisposedListener> |
proofDisposedListener
Contains all registered
ProofDisposedListener . |
private java.io.File |
proofFile
|
private Node |
root
the root of the proof
|
private java.util.List<RuleAppListener> |
ruleAppListenerList
list of rule app listeners
|
private SettingsListener |
settingsListener |
java.util.Vector<java.lang.String> |
userLog
when different users load and save a proof this vector fills up with
Strings containing the user names.
|
Modifier | Constructor and Description |
---|---|
private |
Proof(Name name,
InitConfig initConfig)
constructs a new empty proof with name
|
|
Proof(java.lang.String name,
InitConfig initConfig)
constructs a new empty proof with name
|
|
Proof(java.lang.String name,
Sequent sequent,
java.lang.String header,
TacletIndex rules,
BuiltInRuleIndex builtInRules,
InitConfig initConfig) |
private |
Proof(java.lang.String name,
Sequent problem,
TacletIndex rules,
BuiltInRuleIndex builtInRules,
InitConfig initConfig) |
|
Proof(java.lang.String name,
Term problem,
java.lang.String header,
InitConfig initConfig) |
Modifier and Type | Method and Description |
---|---|
AbbrevMap |
abbreviations() |
void |
add(Goal goal)
adds a new goal to the list of goals
|
void |
add(ImmutableList<Goal> goals)
adds a list with new goals to the list of open goals
|
void |
addAutoModeTime(long time) |
void |
addProofDisposedListener(ProofDisposedListener l)
Registers the given
ProofDisposedListener . |
void |
addProofTreeListener(ProofTreeListener listener)
adds a listener to the proof
|
void |
addRuleAppListener(RuleAppListener p) |
void |
breadthFirstSearch(Node startNode,
ProofVisitor visitor)
Makes a downwards directed breadth first search on the proof tree, starting with node
startNode . |
void |
clearAndDetachRuleAppIndexes() |
boolean |
closed()
returns true if the root node is marked as closed and all goals have been removed
|
void |
closeGoal(Goal p_goal)
Add the given constraint to the closure constraint of the given
goal, i.e. the given goal is closed if p_c is satisfied.
|
boolean |
containsProofTreeListener(ProofTreeListener listener) |
int |
countBranches()
retrieves number of branches
|
int |
countNodes()
retrieves number of nodes
|
void |
dispose()
Cut off all reference such that it does not lead to a big memory leak
if someone still holds a reference to this proof object.
|
private ImmutableList<Goal> |
filterEnabledGoals(ImmutableList<Goal> goals)
filter those goals from a list which are enabled
|
boolean |
find(Node node)
returns true iff the given node is found in the proof tree
|
protected void |
fireNotesChanged(Node node)
Fires the event
ProofTreeListener.notesChanged(ProofTreeEvent) to all listener. |
protected void |
fireProofClosed()
fires the event that the proof has closed.
|
protected void |
fireProofDisposed(ProofDisposedEvent e)
Fires the event
ProofDisposedListener.proofDisposed(ProofDisposedEvent) to all listener. |
protected void |
fireProofDisposing(ProofDisposedEvent e)
Fires the event
ProofDisposedListener.proofDisposing(ProofDisposedEvent) to all listener. |
void |
fireProofExpanded(Node node)
fires the event that the proof has been expanded at the given node
|
protected void |
fireProofGoalRemoved(Goal goal)
fires the event that a goal has been removed from the list of goals
|
protected void |
fireProofGoalsAdded(Goal goal)
fires the event that new goals have been added to the list of
goals
|
protected void |
fireProofGoalsAdded(ImmutableList<Goal> goals)
fires the event that new goals have been added to the list of
goals
|
void |
fireProofGoalsChanged()
fires the event that the proof has been restructured
|
protected void |
fireProofIsBeingPruned(Node below)
fires the event that the proof is being pruned at the given node
|
protected void |
fireProofPruned(Node below)
fires the event that the proof has been pruned at the given node
|
void |
fireProofStructureChanged()
fires the event that the proof has been restructured
|
protected void |
fireRuleApplied(ProofEvent p_e)
fires the event that a rule has been applied
|
Strategy |
getActiveStrategy() |
StrategyFactory |
getActiveStrategyFactory() |
long |
getAutoModeTime() |
Goal |
getClosedGoal(Node node)
Get the closed goal belonging to the given node if it exists.
|
ImmutableList<Goal> |
getClosedSubtreeGoals(Node node)
Returns a list of all (closed) goals of the closed subtree pending from this node.
|
ProofEnvironment |
getEnv() |
Goal |
getGoal(Node node)
returns the goal that belongs to the given node or null if the
node is an inner one
|
InitConfig |
getInitConfig() |
JavaInfo |
getJavaInfo()
returns the JavaInfo with the java type information
|
NamespaceSet |
getNamespaces()
returns a collection of the namespaces valid for this proof
|
ProofDisposedListener[] |
getProofDisposedListeners()
Returns all registered
ProofDisposedListener . |
java.io.File |
getProofFile()
Returns the
File under which the Proof was saved the last time if available. |
ProofIndependentSettings |
getProofIndependentSettings() |
Services |
getServices()
returns the Services with the java service classes
|
ProofSettings |
getSettings() |
Statistics |
getStatistics()
Retrieves a bunch of statistics to the proof tree.
|
ImmutableList<Goal> |
getSubtreeEnabledGoals(Node node)
get the list of goals of the subtree starting with node which are enabled.
|
ImmutableList<Goal> |
getSubtreeGoals(Node node)
returns the list of goals of the subtree starting with node.
|
java.lang.String |
header() |
private void |
initStrategy()
initialises the strategies
|
boolean |
isClosedGoal(Node node) |
boolean |
isDisposed()
Returns true if the proof has been abandoned and the dispose method has
been called on this object.
|
boolean |
isGoal(Node node)
returns true if the given node is part of a Goal
|
ProofCorrectnessMgt |
mgt() |
Name |
name()
returns the name of the proof.
|
ImmutableList<Goal> |
openEnabledGoals()
return the list of open and enabled goals
|
ImmutableList<Goal> |
openGoals()
returns the list of open goals
|
void |
pruneProof(Goal goal)
Performs an undo operation on the given goal.
|
ImmutableList<Node> |
pruneProof(Node cuttingPoint)
Prunes the subtree beneath the node
cuttingPoint , i.e. the node
cuttingPoint remains as the last node on the branch. |
ImmutableList<Node> |
pruneProof(Node cuttingPoint,
boolean fireChanges) |
private void |
remove(Goal goal)
removes the given goal from the list of open goals.
|
void |
removeProofDisposedListener(ProofDisposedListener l)
Unregisters the given
ProofDisposedListener . |
void |
removeProofTreeListener(ProofTreeListener listener)
removes a listener from the proof
|
void |
removeRuleAppListener(RuleAppListener p) |
void |
reOpenGoal(Goal p_goal)
Opens a previously closed node (the one corresponding to p_goal)
and all its closed parents.
|
void |
replace(Goal oldGoal,
ImmutableList<Goal> newGoals)
removes the given goal and adds the new goals in list
|
Node |
root()
returns the root node of the proof
|
void |
saveToFile(java.io.File file) |
void |
setActiveStrategy(Strategy activeStrategy) |
void |
setEnv(ProofEnvironment env) |
void |
setNamespaces(NamespaceSet ns)
sets the variable, function, sort, heuristics namespaces
|
void |
setProofFile(java.io.File proofFile)
Sets the
File under which the Proof was saved the last time. |
void |
setRoot(Node root)
sets the root of the proof
|
void |
setRuleAppIndexToAutoMode()
Currently the rule app index can either operate in interactive mode (and
contain applications of all existing taclets) or in automatic mode (and
only contain a restricted set of taclets that can possibly be applied
automated).
|
void |
setRuleAppIndexToInteractiveMode() |
java.lang.String |
toString()
toString
|
void |
traverseFromChildToParent(Node child,
Node parent,
ProofVisitor visitor) |
private void |
updateStrategyOnGoals() |
final long creationTime
Proof
instance was created.private final Name name
private Node root
private java.util.List<ProofTreeListener> listenerList
private ImmutableList<Goal> openGoals
private ImmutableList<Goal> closedGoals
private java.lang.String problemHeader
private ProofEnvironment env
private AbbrevMap abbreviations
private InitConfig initConfig
private ProofCorrectnessMgt localMgt
private ProofIndependentSettings pis
public java.util.Vector<java.lang.String> userLog
public java.util.Vector<java.lang.String> keyVersionLog
private long autoModeTime
private Strategy activeStrategy
private SettingsListener settingsListener
private boolean disposed
private java.util.List<RuleAppListener> ruleAppListenerList
private final java.util.List<ProofDisposedListener> proofDisposedListener
ProofDisposedListener
.private java.io.File proofFile
private Proof(Name name, InitConfig initConfig)
public Proof(java.lang.String name, InitConfig initConfig)
private Proof(java.lang.String name, Sequent problem, TacletIndex rules, BuiltInRuleIndex builtInRules, InitConfig initConfig)
public Proof(java.lang.String name, Term problem, java.lang.String header, InitConfig initConfig)
public Proof(java.lang.String name, Sequent sequent, java.lang.String header, TacletIndex rules, BuiltInRuleIndex builtInRules, InitConfig initConfig)
private void initStrategy()
public void dispose()
public boolean isDisposed()
public Name name()
public java.lang.String header()
public ProofCorrectnessMgt mgt()
public NamespaceSet getNamespaces()
public JavaInfo getJavaInfo()
public Services getServices()
public long getAutoModeTime()
public void addAutoModeTime(long time)
public void setNamespaces(NamespaceSet ns)
public ProofEnvironment getEnv()
public void setEnv(ProofEnvironment env)
public AbbrevMap abbreviations()
public Strategy getActiveStrategy()
public void setActiveStrategy(Strategy activeStrategy)
private void updateStrategyOnGoals()
public void clearAndDetachRuleAppIndexes()
public Node root()
public void setRoot(Node root)
public ProofSettings getSettings()
public ProofIndependentSettings getProofIndependentSettings()
public ImmutableList<Goal> openGoals()
public ImmutableList<Goal> openEnabledGoals()
private ImmutableList<Goal> filterEnabledGoals(ImmutableList<Goal> goals)
goals
- non-null list of goalsGoal.isAutomatic()
public void replace(Goal oldGoal, ImmutableList<Goal> newGoals)
oldGoal
- the old goal that has to be removed from listnewGoals
- the IListpublic void closeGoal(Goal p_goal)
public void reOpenGoal(Goal p_goal)
This is, for instance, needed for the MergeRule
: In
a situation where a merge node and its associated partners
have been closed and the merge node is then pruned away,
the partners have to be reopened again. Otherwise, we
have a soundness issue.
p_goal
- The goal to be opened again.private void remove(Goal goal)
goal
- the Goal to be removedpublic void add(Goal goal)
goal
- the Goal to be addedpublic void add(ImmutableList<Goal> goals)
goals
- the IListpublic boolean closed()
public void pruneProof(Goal goal)
goal
- the Goal where the last rule application gets undonepublic ImmutableList<Node> pruneProof(Node cuttingPoint)
cuttingPoint
, i.e. the node
cuttingPoint
remains as the last node on the branch. As a result,
an open goal is associated with this node.cuttingPoint
- public ImmutableList<Node> pruneProof(Node cuttingPoint, boolean fireChanges)
public void breadthFirstSearch(Node startNode, ProofVisitor visitor)
startNode
. The visited notes are reported to the object visitor
.
The first reported node is startNode
.public void traverseFromChildToParent(Node child, Node parent, ProofVisitor visitor)
public void fireProofExpanded(Node node)
protected void fireProofIsBeingPruned(Node below)
protected void fireProofPruned(Node below)
public void fireProofStructureChanged()
protected void fireProofGoalRemoved(Goal goal)
protected void fireProofGoalsAdded(ImmutableList<Goal> goals)
protected void fireProofGoalsAdded(Goal goal)
public void fireProofGoalsChanged()
protected void fireProofClosed()
protected void fireNotesChanged(Node node)
ProofTreeListener.notesChanged(ProofTreeEvent)
to all listener.node
- The changed Node
.public void addProofTreeListener(ProofTreeListener listener)
listener
- the ProofTreeListener to be addedpublic void removeProofTreeListener(ProofTreeListener listener)
listener
- the ProofTreeListener to be removedpublic boolean containsProofTreeListener(ProofTreeListener listener)
public boolean isGoal(Node node)
public Goal getGoal(Node node)
public boolean isClosedGoal(Node node)
node
- the Node which is checked for a corresponding closed goalpublic Goal getClosedGoal(Node node)
node
- the Node where a corresponding closed goal is searchedpublic ImmutableList<Goal> getSubtreeGoals(Node node)
node
- the Node where to start frompublic ImmutableList<Goal> getClosedSubtreeGoals(Node node)
node
- the root of the subtreepublic ImmutableList<Goal> getSubtreeEnabledGoals(Node node)
node
- the Node where to start frompublic boolean find(Node node)
node
- the Node to search forpublic int countNodes()
public void setRuleAppIndexToAutoMode()
public void setRuleAppIndexToInteractiveMode()
public int countBranches()
public Statistics getStatistics()
public java.lang.String toString()
toString
in class java.lang.Object
protected void fireRuleApplied(ProofEvent p_e)
public void addRuleAppListener(RuleAppListener p)
public void removeRuleAppListener(RuleAppListener p)
public void addProofDisposedListener(ProofDisposedListener l)
ProofDisposedListener
.l
- The ProofDisposedListener
to register.public void removeProofDisposedListener(ProofDisposedListener l)
ProofDisposedListener
.l
- The ProofDisposedListener
to unregister.public ProofDisposedListener[] getProofDisposedListeners()
ProofDisposedListener
.ProofDisposedListener
.protected void fireProofDisposed(ProofDisposedEvent e)
ProofDisposedListener.proofDisposed(ProofDisposedEvent)
to all listener.e
- The event to fire.protected void fireProofDisposing(ProofDisposedEvent e)
ProofDisposedListener.proofDisposing(ProofDisposedEvent)
to all listener.e
- The event to fire.public InitConfig getInitConfig()
public java.io.File getProofFile()
File
under which the Proof
was saved the last time if available.File
under which the Proof
was saved the last time or null
if not available.public void setProofFile(java.io.File proofFile)
File
under which the Proof
was saved the last time.proofFile
- The File
under which the Proof
was saved the last time.public void saveToFile(java.io.File file) throws java.io.IOException
java.io.IOException
public StrategyFactory getActiveStrategyFactory()