From 83b9769225cd4a7b796e1e979568d38fbe4fefae Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 4 Dec 2015 08:13:19 -0800
Subject: [PATCH] fix(library/blast): init_classical_flag

The procedure get_namespaces does not return the set of opened
namespaces. I added a comment there to clarify that.
---
 src/library/blast/blast.cpp | 14 +++++++++-----
 src/library/constants.cpp   |  4 ++++
 src/library/constants.h     |  1 +
 src/library/constants.txt   |  1 +
 4 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index b1e00b739..2928902cb 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -466,20 +466,24 @@ public:
     }
 
     void init_classical_flag() {
-        for_each(get_namespaces(m_env), [&](name const & ns) {
-                if (m_classical) return;
-                if (ns == get_classical_name()) m_classical = true;
-            });
+        if (is_standard(env())) {
+            expr p     = m_tmp_ctx->mk_tmp_local(mk_Prop());
+            expr dec_p = mk_app(mk_constant(get_decidable_name()), p);
+            if (m_tmp_ctx->mk_class_instance(dec_p)) {
+                m_classical = true;
+            }
+            m_tmp_ctx->clear_cache();
+        }
     }
 
     bool classical() { return m_classical; }
 
     void init_state(goal const & g) {
         init_curr_state(g);
-        init_classical_flag();
         save_initial_context();
         m_tctx.set_local_instances(m_initial_context);
         m_tmp_ctx->set_local_instances(m_initial_context);
+        init_classical_flag();
     }
 
     optional<expr> operator()(goal const & g) {
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 3f06c5ec7..d370ba550 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -23,6 +23,7 @@ name const * g_classical = nullptr;
 name const * g_congr = nullptr;
 name const * g_congr_arg = nullptr;
 name const * g_congr_fun = nullptr;
+name const * g_decidable = nullptr;
 name const * g_dite = nullptr;
 name const * g_div = nullptr;
 name const * g_empty = nullptr;
@@ -201,6 +202,7 @@ void initialize_constants() {
     g_congr = new name{"congr"};
     g_congr_arg = new name{"congr_arg"};
     g_congr_fun = new name{"congr_fun"};
+    g_decidable = new name{"decidable"};
     g_dite = new name{"dite"};
     g_div = new name{"div"};
     g_empty = new name{"empty"};
@@ -380,6 +382,7 @@ void finalize_constants() {
     delete g_congr;
     delete g_congr_arg;
     delete g_congr_fun;
+    delete g_decidable;
     delete g_dite;
     delete g_div;
     delete g_empty;
@@ -558,6 +561,7 @@ name const & get_classical_name() { return *g_classical; }
 name const & get_congr_name() { return *g_congr; }
 name const & get_congr_arg_name() { return *g_congr_arg; }
 name const & get_congr_fun_name() { return *g_congr_fun; }
+name const & get_decidable_name() { return *g_decidable; }
 name const & get_dite_name() { return *g_dite; }
 name const & get_div_name() { return *g_div; }
 name const & get_empty_name() { return *g_empty; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 72fdf951c..924c60665 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -25,6 +25,7 @@ name const & get_classical_name();
 name const & get_congr_name();
 name const & get_congr_arg_name();
 name const & get_congr_fun_name();
+name const & get_decidable_name();
 name const & get_dite_name();
 name const & get_div_name();
 name const & get_empty_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index de5c80358..eb44192ec 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -18,6 +18,7 @@ classical
 congr
 congr_arg
 congr_fun
+decidable
 dite
 div
 empty