michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/blast/state): document branch extension methods

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-18 17:29:01 -08:00
parent 70a1aebfe3
commit 5251752b9c
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/blast/state.h
View file

@ -103,12 +103,21 @@ class branch_extension {
void dealloc() { delete this; } void dealloc() { delete this; }
public: public:
virtual ~branch_extension() {} virtual ~branch_extension() {}
/** \brief Return a copy of this object */
virtual branch_extension * clone() = 0; virtual branch_extension * clone() = 0;
/** \brief This method is invoked the first time an extension is used in a branch
The system guarantees this object is not shared, and destructive updates are allowed. */
virtual void initialized() {} virtual void initialized() {}
/** \brief This method is invoked when the given hypothesis is initialized in the current branch.
The system guarantees this object is not shared, and destructive updates are allowed. */
virtual void hypothesis_activated(hypothesis const &, hypothesis_idx) {} virtual void hypothesis_activated(hypothesis const &, hypothesis_idx) {}
/** \brief This method is invoked when the given hypothesis is deleted from the current branch.
The system guarantees this object is not shared, and destructive updates are allowed. */
virtual void hypothesis_deleted(hypothesis const &, hypothesis_idx) {} virtual void hypothesis_deleted(hypothesis const &, hypothesis_idx) {}
}; };
/** \brief This procedure must be invoke at Lean initialization time for each branch extension.
The unique id returned should be used to retrieve the branch extension associated with the current state */
unsigned register_branch_extension(branch_extension * initial); unsigned register_branch_extension(branch_extension * initial);
/** \brief Information associated with the current branch of the proof state. /** \brief Information associated with the current branch of the proof state.