feat(library/blast): add target_updated event

src/library/blast/assert_cc_action.cpp

@@ -20,6 +20,7 @@ struct cc_branch_extension : public branch_extension {
     virtual ~cc_branch_extension() {}
     virtual branch_extension * clone() override { return new cc_branch_extension(*this); }
     virtual void initialized() override { m_cc.initialize(); }
+    virtual void target_updated() override { m_cc.internalize(curr_state().get_target()); }
 };
 
 void initialize_assert_cc_action() {
@@ -36,8 +37,6 @@ action_result assert_cc_action(hypothesis_idx hidx) {
     if (!get_config().m_cc)
         return action_result::failed();
     congruence_closure & cc = get_cc();
-    // TODO(Leo): consider a target_changed event for branch_extension.
-    cc.internalize(curr_state().get_target());
     cc.add(hidx);
     // cc.display();
     if (cc.is_inconsistent()) {

src/library/blast/state.cpp

@@ -733,6 +733,7 @@ branch_extension & state::get_extension(unsigned extid) {
                 hypothesis const & h = get_hypothesis_decl(hidx);
                 ext->hypothesis_activated(h, hidx);
             });
+        ext->target_updated();
         return *ext;
     } else {
         branch_extension * ext = get_extension_core(extid);
@@ -801,6 +802,11 @@ void state::set_target(expr const & t) {
                 }
             });
     }
+    unsigned n = get_extension_manager().get_num_extensions();
+    for (unsigned i = 0; i < n; i++) {
+        branch_extension * ext = get_extension_core(i);
+        if (ext) ext->target_updated();
+    }
 }
 
 struct expand_hrefs_fn : public replace_visitor {

src/library/blast/state.h

@@ -109,6 +109,8 @@ public:
     /** \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() {}
+    /** \brief This method is invoked whenever the target type in the current branch is updated. */
+    virtual void target_updated() {}
     /** \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) {}