feat(library/blast/congruence_closure): avoid unnecessary propagations in the congruence closure module

src/library/blast/blast.cpp

@@ -1157,10 +1157,12 @@ void initialize_blast() {
     register_trace_class_alias("app_builder", name({"blast", "event"}));
     register_trace_class_alias(name({"simplifier", "failure"}), name({"blast", "event"}));
 
+    register_trace_class_alias(name({"cc", "propagation"}), "blast");
+
     register_trace_class_alias("blast", "blast_detailed");
     register_trace_class_alias("app_builder", "blast_detailed");
     register_trace_class_alias(name({"simplifier", "failure"}), "blast_detailed");
-    register_trace_class_alias(name({"congruence_closure", "merge"}), "blast_detailed");
+    register_trace_class_alias(name({"cc", "merge"}), "blast_detailed");
 
     blast::g_prefix                  = new name(name::mk_internal_unique_name());
     blast::g_tmp_prefix              = new name(name::mk_internal_unique_name());

src/library/blast/congruence_closure.cpp

@@ -632,7 +632,7 @@ void congruence_closure::internalize(name const & R, expr const & e, bool toplev
     flet<congruence_closure *> set_cc(g_cc, this);
     bool to_propagate = false; // We don't need to mark units for propagation
     internalize_core(R, e, toplevel, to_propagate);
-    process_todo();
+    process_todo(none_expr());
 }
 
 void congruence_closure::internalize(expr const & e) {
@@ -716,7 +716,9 @@ static bool is_true_or_false(expr const & e) {
     return is_constant(e, get_true_name()) || is_constant(e, get_false_name());
 }
 
-void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr const & H) {
+/* Remark: If added_prop is not none, then it contains the proposition provided to ::add.
+   We use it here to avoid an unnecessary propagation back to the current_state. */
+void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr const & H, optional<expr> const & added_prop) {
     auto n1 = m_entries.find(eqc_key(R, e1));
     auto n2 = m_entries.find(eqc_key(R, e2));
     if (!n1 || !n2)
@@ -834,6 +836,7 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
         for (expr const & e : to_propagate) {
             lean_assert(R == get_iff_name());
             expr type = e;
+            if ((!added_prop || *added_prop != type) && !s.contains_hypothesis(type)) {
                 expr pr   = *get_eqv_proof(R, e, e2_root);
                 if (is_true) {
                     pr = b.mk_of_iff_true(pr);
@@ -841,29 +844,32 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
                     type = b.mk_not(e);
                     pr   = b.mk_not_of_iff_false(pr);
                 }
-            s.mk_hypothesis(type, pr);
+                expr H = s.mk_hypothesis(type, pr);
+                lean_trace(name({"cc", "propagation"}),
+                           tout() << ppb(H) << " : " << ppb(infer_type(H)) << "\n";);
+            }
         }
     }
 
     update_mt(R, e2_root);
 
-    lean_trace(name({"congruence_closure", "merge"}), tout() << ppb(e1) << " [" << R << "] " << ppb(e2) << "\n";);
+    lean_trace(name({"cc", "merge"}), tout() << ppb(e1) << " [" << R << "] " << ppb(e2) << "\n";);
-    lean_trace(name({"congruence_closure", "state"}), trace(););
+    lean_trace(name({"cc", "state"}), trace(););
 }
 
-void congruence_closure::process_todo() {
+void congruence_closure::process_todo(optional<expr> const & added_prop) {
     auto & todo = get_todo();
     while (!todo.empty()) {
         name R; expr lhs, rhs, H;
         std::tie(R, lhs, rhs, H) = todo.back();
         todo.pop_back();
-        add_eqv_step(R, lhs, rhs, H);
+        add_eqv_step(R, lhs, rhs, H, added_prop);
     }
 }
 
-void congruence_closure::add_eqv_core(name const & R, expr const & lhs, expr const & rhs, expr const & H) {
+void congruence_closure::add_eqv_core(name const & R, expr const & lhs, expr const & rhs, expr const & H, optional<expr> const & added_prop) {
     push_todo(R, lhs, rhs, H);
-    process_todo();
+    process_todo(added_prop);
 }
 
 void congruence_closure::add_eqv(name const & R, expr const & lhs, expr const & rhs, expr const & H) {
@@ -874,7 +880,7 @@ void congruence_closure::add_eqv(name const & R, expr const & lhs, expr const &
     bool toplevel = false; bool to_propagate = false;
     internalize_core(R, lhs, toplevel, to_propagate);
     internalize_core(R, rhs, toplevel, to_propagate);
-    add_eqv_core(R, lhs, rhs, H);
+    add_eqv_core(R, lhs, rhs, H, none_expr());
 }
 
 void congruence_closure::add(hypothesis_idx hidx) {
@@ -911,20 +917,20 @@ void congruence_closure::add(expr const & type, expr const & proof) {
         if (is_neg) {
             bool toplevel = true; bool to_propagate = false;
             internalize_core(get_iff_name(), p, toplevel, to_propagate);
-            add_eqv_core(get_iff_name(), p, mk_false(), mk_iff_false_intro(proof));
+            add_eqv_core(get_iff_name(), p, mk_false(), mk_iff_false_intro(proof), some_expr(type));
         } else {
             bool toplevel = false; bool to_propagate = false;
             internalize_core(R, lhs, toplevel, to_propagate);
             internalize_core(R, rhs, toplevel, to_propagate);
-            add_eqv_core(R, lhs, rhs, proof);
+            add_eqv_core(R, lhs, rhs, proof, some_expr(type));
         }
     } else if (is_prop(p)) {
         bool toplevel = true; bool to_propagate = false;
         internalize_core(get_iff_name(), p, toplevel, to_propagate);
         if (is_neg) {
-            add_eqv_core(get_iff_name(), p, mk_false(), mk_iff_false_intro(proof));
+            add_eqv_core(get_iff_name(), p, mk_false(), mk_iff_false_intro(proof), some_expr(type));
         } else {
-            add_eqv_core(get_iff_name(), p, mk_true(), mk_iff_true_intro(proof));
+            add_eqv_core(get_iff_name(), p, mk_true(), mk_iff_true_intro(proof), some_expr(type));
         }
     }
 }
@@ -1375,9 +1381,10 @@ congruence_closure & get_cc() {
 }
 
 void initialize_congruence_closure() {
-    register_trace_class("congruence_closure");
+    register_trace_class("cc");
-    register_trace_class({"congruence_closure", "state"});
+    register_trace_class({"cc", "state"});
-    register_trace_class({"congruence_closure", "merge"});
+    register_trace_class({"cc", "propagation"});
+    register_trace_class({"cc", "merge"});
     g_ext_id = register_branch_extension(new cc_branch_extension());
     name prefix = name::mk_internal_unique_name();
     g_congr_mark    = new expr(mk_constant(name(prefix, "[congruence]")));

src/library/blast/congruence_closure.h

@@ -117,7 +117,7 @@ class congruence_closure {
 
     void register_to_propagate(expr const & e);
     void internalize_core(name const & R, expr const & e, bool toplevel, bool to_propagate);
-    void process_todo();
+    void process_todo(optional<expr> const & added_prop);
 
     int compare_symm(name const & R, expr lhs1, expr rhs1, expr lhs2, expr rhs2) const;
     int compare_root(name const & R, expr e1, expr e2) const;
@@ -136,8 +136,8 @@ class congruence_closure {
     void update_mt(name const & R, expr const & e);
     expr mk_iff_false_intro(expr const & proof);
     expr mk_iff_true_intro(expr const & proof);
-    void add_eqv_step(name const & R, expr e1, expr e2, expr const & H);
+    void add_eqv_step(name const & R, expr e1, expr e2, expr const & H, optional<expr> const & added_prop);
-    void add_eqv_core(name const & R, expr const & lhs, expr const & rhs, expr const & H);
+    void add_eqv_core(name const & R, expr const & lhs, expr const & rhs, expr const & H, optional<expr> const & added_prop);
 
     expr mk_congr_proof_core(name const & R, expr const & lhs, expr const & rhs) const;
     expr mk_congr_proof(name const & R, expr const & lhs, expr const & rhs) const;

src/library/blast/state.cpp

@@ -756,6 +756,15 @@ list<hypothesis_idx> state::get_head_related() const {
         return list<hypothesis_idx>();
 }
 
+optional<hypothesis_idx> state::contains_hypothesis(expr const & type) const {
+    for (auto hidx : get_occurrences_of(head_index(type))) {
+        hypothesis const & h = get_hypothesis_decl(hidx);
+        if (h.get_type() == type)
+            return optional<hypothesis_idx>(hidx);
+    }
+    return optional<hypothesis_idx>();
+}
+
 branch_extension * state::get_extension_core(unsigned i) {
     branch_extension * ext = m_branch.m_extensions[i];
     if (ext && ext->get_rc() > 1) {
@@ -844,6 +853,7 @@ void state::activate_hypothesis(hypothesis_idx hidx) {
     lean_trace_search(
         hypothesis const & h = get_hypothesis_decl(hidx);
         tout() << "activate " << h.get_name() << " : " << ppb(h.get_type()) << "\n";);
+    lean_assert(!get_hypothesis_decl(hidx).is_dead());
     m_branch.m_active.insert(hidx);
     update_indices(hidx);
 }

src/library/blast/state.h

@@ -324,6 +324,9 @@ public:
     /** \brief Return (active) hypotheses whose head symbol is equal to target or it is the negation of */
     list<hypothesis_idx> get_head_related() const;
 
+    /** \brief If there is an hypothesis with the given type (return it), otherwise return none */
+    optional<hypothesis_idx> contains_hypothesis(expr const & type) const;
+
     /************************
        Abstracting hypotheses
     *************************/

src/library/blast/strategy.cpp

@@ -20,7 +20,8 @@ action_result strategy_fn::activate_hypothesis() {
     auto hidx = curr_state().select_hypothesis_to_activate();
     if (!hidx) return action_result::failed();
     auto r    = hypothesis_pre_activation(*hidx);
-    if (!solved(r) && !failed(r)) {
+    // The pre-activation may delete the hypothesis (e.g., subsumption)
+    if (!solved(r) && !failed(r) && !curr_state().get_hypothesis_decl(*hidx).is_dead()) {
         curr_state().activate_hypothesis(*hidx);
         return hypothesis_post_activation(*hidx);
     } else {