diff --git a/src/library/blast/recursor_action.cpp b/src/library/blast/recursor_action.cpp index 385a0a7e7..c943c682f 100644 --- a/src/library/blast/recursor_action.cpp +++ b/src/library/blast/recursor_action.cpp @@ -20,8 +20,6 @@ struct recursor_branch_extension : public branch_extension { recursor_branch_extension(recursor_branch_extension const & b):m_rec_queue(b.m_rec_queue) {} virtual ~recursor_branch_extension() {} virtual branch_extension * clone() { return new recursor_branch_extension(*this); } - virtual void hypothesis_activated(hypothesis const &, hypothesis_idx) {} - virtual void hypothesis_deleted(hypothesis const &, hypothesis_idx) {} }; void initialize_recursor_action() { diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 672d35a6f..af45c44ae 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -712,6 +712,7 @@ branch_extension & state::get_extension(unsigned extid) { ext->inc_ref(); m_branch.m_extensions[extid] = ext; lean_assert(ext.get_rc() == 1); + ext->initialized(); m_branch.m_active.for_each([&](hypothesis_idx hidx) { hypothesis const * h = get_hypothesis_decl(hidx); lean_assert(h); diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 8bae1a751..7811260fc 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -104,8 +104,9 @@ class branch_extension { public: virtual ~branch_extension() {} virtual branch_extension * clone() = 0; - virtual void hypothesis_activated(hypothesis const & h, hypothesis_idx hidx) = 0; - virtual void hypothesis_deleted(hypothesis const & h, hypothesis_idx hidx) = 0; + virtual void initialized() {} + virtual void hypothesis_activated(hypothesis const &, hypothesis_idx) {} + virtual void hypothesis_deleted(hypothesis const &, hypothesis_idx) {} }; unsigned register_branch_extension(branch_extension * initial);