From d833410f0d4ac1d2918319b143abb1edfc1844fb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 17 Nov 2015 19:06:23 -0800
Subject: [PATCH] feat(library/blast/congruence_closure): add proved/disproved
 aux methods

---
 src/library/blast/congruence_closure.cpp | 34 ++++++++++++++++++++++++
 src/library/blast/congruence_closure.h   |  8 ++++++
 2 files changed, 42 insertions(+)

diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp
index a67e84099..bd9125a04 100644
--- a/src/library/blast/congruence_closure.cpp
+++ b/src/library/blast/congruence_closure.cpp
@@ -320,6 +320,40 @@ optional<expr> congruence_closure::get_inconsistency_proof() const {
     }
 }
 
+bool congruence_closure::prove(expr const & e) const {
+    return is_eqv(get_iff_name(), e, mk_true());
+}
+
+optional<expr> congruence_closure::get_proof(expr const & e) const {
+    try {
+        app_builder & b = get_app_builder();
+        if (auto p = get_eqv_proof(get_iff_name(), e, mk_true())) {
+            return some_expr(b.mk_of_iff_true(*p));
+        } else {
+            return none_expr();
+        }
+    } catch (app_builder_exception &) {
+        return none_expr();
+    }
+}
+
+bool congruence_closure::disproved(expr const & e) const {
+    return is_eqv(get_iff_name(), e, mk_false());
+}
+
+optional<expr> congruence_closure::get_disproof(expr const & e) const {
+    try {
+        app_builder & b = get_app_builder();
+        if (auto p = get_eqv_proof(get_iff_name(), e, mk_false())) {
+            return some_expr(b.mk_not_of_iff_false(*p));
+        } else {
+            return none_expr();
+        }
+    } catch (app_builder_exception &) {
+        return none_expr();
+    }
+}
+
 bool congruence_closure::is_congr_root(name const & R, expr const & e) const {
     if (auto n = m_entries.find(eqc_key(R, e))) {
         return n->m_cg_root;
diff --git a/src/library/blast/congruence_closure.h b/src/library/blast/congruence_closure.h
index 60b055109..a83769a58 100644
--- a/src/library/blast/congruence_closure.h
+++ b/src/library/blast/congruence_closure.h
@@ -139,6 +139,14 @@ public:
     bool is_uneqv(name const & R, expr const & e1, expr const & e2) const;
     optional<expr> get_uneqv_proof(name const & R, expr const & e1, expr const & e2) const;
 
+    /** \brief Return true iff \c e has been proved by this module. That is, the proposition \c e is inhabited */
+    bool prove(expr const & e) const;
+    optional<expr> get_proof(expr const & e) const;
+
+    /** \brief Return true iff \c (not e) has been proved by this module. That is, the proposition \c (not e) is inhabited */
+    bool disproved(expr const & e) const;
+    optional<expr> get_disproof(expr const & e) const;
+
     bool is_congr_root(name const & R, expr const & e) const;
     bool is_root(name const & R, expr const & e) const { return get_root(R, e) == e; }
     expr get_root(name const & R, expr const & e) const;