From c50d7ac4b8fd2e833459f59da3ef9f0a3a7eb1c2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Nov 2015 15:21:28 -0800
Subject: [PATCH] feat(library/blast/congruence_closure): add add/assume API

---
 src/library/blast/congruence_closure.cpp | 70 ++++++++++++++----------
 src/library/blast/congruence_closure.h   |  6 ++
 2 files changed, 48 insertions(+), 28 deletions(-)

diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp
index 75eb9162f..31904c71a 100644
--- a/src/library/blast/congruence_closure.cpp
+++ b/src/library/blast/congruence_closure.cpp
@@ -884,41 +884,55 @@ void congruence_closure::add_eqv(name const & R, expr const & lhs, expr const &
 }
 
 void congruence_closure::add(hypothesis_idx hidx) {
+    state & s            = curr_state();
+    hypothesis const & h = s.get_hypothesis_decl(hidx);
+    add(h.get_type(), h.get_self());
+}
+
+void congruence_closure::assume(expr const & type) {
+    lean_assert(m_froze_partitions);
+    expr dummy = mk_true_intro();
+    add(type, dummy);
+}
+
+expr congruence_closure::mk_iff_false_intro(expr const & proof) {
+    return m_froze_partitions ? proof : get_app_builder().mk_iff_false_intro(proof);
+}
+
+expr congruence_closure::mk_iff_true_intro(expr const & proof) {
+    return m_froze_partitions ? proof : get_app_builder().mk_iff_true_intro(proof);
+}
+
+void congruence_closure::add(expr const & type, expr const & proof) {
     if (is_inconsistent())
         return;
     flet<congruence_closure *> set_cc(g_cc, this);
     clear_todo();
-    state & s       = curr_state();
-    app_builder & b = get_app_builder();
-    hypothesis const & h = s.get_hypothesis_decl(hidx);
-    try {
-        expr const & type = h.get_type();
-        expr p      = type;
-        bool is_neg = is_not(type, p);
-        if (is_neg && !is_standard(env()))
-            return;
-        name R; expr lhs, rhs;
-        if (is_relation_app(p, R, lhs, rhs)) {
-            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(), b.mk_iff_false_intro(h.get_self()));
-            } 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, h.get_self());
-            }
-        } else if (is_prop(p)) {
+    expr p      = type;
+    bool is_neg = is_not(type, p);
+    if (is_neg && !is_standard(env()))
+        return;
+    name R; expr lhs, rhs;
+    if (is_relation_app(p, R, lhs, rhs)) {
+        if (is_neg) {
             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(), b.mk_iff_false_intro(h.get_self()));
-            } else {
-                add_eqv_core(get_iff_name(), p, mk_true(), b.mk_iff_true_intro(h.get_self()));
-            }
+            add_eqv_core(get_iff_name(), p, mk_false(), mk_iff_false_intro(proof));
+        } 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);
         }
-    } catch (app_builder_exception &) {}
+    } 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));
+        } else {
+            add_eqv_core(get_iff_name(), p, mk_true(), mk_iff_true_intro(proof));
+        }
+    }
 }
 
 bool congruence_closure::is_eqv(name const & R, expr const & e1, expr const & e2) const {
diff --git a/src/library/blast/congruence_closure.h b/src/library/blast/congruence_closure.h
index 2c680fa2c..14c54f18d 100644
--- a/src/library/blast/congruence_closure.h
+++ b/src/library/blast/congruence_closure.h
@@ -133,6 +133,8 @@ class congruence_closure {
     void remove_parents(name const & R, expr const & e);
     void reinsert_parents(name const & R, expr const & e);
     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_core(name const & R, expr const & lhs, expr const & rhs, expr const & H);
 
@@ -171,6 +173,10 @@ public:
 
         If H is none of the forms above, this method does nothing. */
     void add(hypothesis_idx hidx);
+    void add(expr const & type, expr const & proof);
+    /** \brief Similar to \c add but asserts the given type without proof
+        \pre It can only be used after \c freeze_partitions has been invoked (i.e., proof extraction has been disabled). */
+    void assume(expr const & type);
 
     /** \brief Assert the equivalence (R a b) with proof H. */
     void add_eqv(name const & R, expr const & a, expr const & b, expr const & H);