From 9260be01b252ff8b4ba2add31927a41e05bb9ac5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Nov 2015 10:56:52 -0700
Subject: [PATCH] feat(library/blast): add blast.backward option for
 disabling/enabling backward chaining

---
 src/library/blast/backward/backward_strategy.cpp |  2 ++
 src/library/blast/options.cpp                    | 12 ++++++++++++
 src/library/blast/options.h                      |  1 +
 3 files changed, 15 insertions(+)

diff --git a/src/library/blast/backward/backward_strategy.cpp b/src/library/blast/backward/backward_strategy.cpp
index 128dc106c..1233e0bc2 100644
--- a/src/library/blast/backward/backward_strategy.cpp
+++ b/src/library/blast/backward/backward_strategy.cpp
@@ -76,6 +76,8 @@ class backward_strategy : public strategy {
 };
 
 optional<expr> apply_backward_strategy() {
+    if (!get_config().m_backward)
+        return none_expr();
     flet<bool> disable_show_failure(get_config().m_show_failure, false);
     return backward_strategy()();
 }
diff --git a/src/library/blast/options.cpp b/src/library/blast/options.cpp
index 33217f631..8c1a15585 100644
--- a/src/library/blast/options.cpp
+++ b/src/library/blast/options.cpp
@@ -41,6 +41,9 @@ Author: Leonardo de Moura
 #ifndef LEAN_DEFAULT_BLAST_EMATCH
 #define LEAN_DEFAULT_BLAST_EMATCH false
 #endif
+#ifndef LEAN_DEFAULT_BLAST_BACKWARD
+#define LEAN_DEFAULT_BLAST_BACKWARD true
+#endif
 
 
 namespace lean {
@@ -56,6 +59,7 @@ static name * g_blast_cc           = nullptr;
 static name * g_blast_trace_cc     = nullptr;
 static name * g_blast_recursor     = nullptr;
 static name * g_blast_ematch       = nullptr;
+static name * g_blast_backward     = nullptr;
 static name * g_blast_show_failure = nullptr;
 
 unsigned get_blast_max_depth(options const & o) {
@@ -88,6 +92,9 @@ bool get_blast_recursor(options const & o) {
 bool get_blast_ematch(options const & o) {
     return o.get_bool(*g_blast_ematch, LEAN_DEFAULT_BLAST_EMATCH);
 }
+bool get_blast_backward(options const & o) {
+    return o.get_bool(*g_blast_backward, LEAN_DEFAULT_BLAST_BACKWARD);
+}
 bool get_blast_show_failure(options const & o) {
     return o.get_bool(*g_blast_show_failure, LEAN_DEFAULT_BLAST_SHOW_FAILURE);
 }
@@ -103,6 +110,7 @@ config::config(options const & o) {
     m_trace_cc          = get_blast_trace_cc(o);
     m_recursor          = get_blast_recursor(o);
     m_ematch            = get_blast_ematch(o);
+    m_backward          = get_blast_backward(o);
     m_show_failure      = get_blast_show_failure(o);
     m_pattern_max_steps = get_pattern_max_steps(o);
 }
@@ -135,6 +143,7 @@ void initialize_options() {
     g_blast_trace_cc     = new name{"blast", "trace_cc"};
     g_blast_recursor     = new name{"blast", "recursor"};
     g_blast_ematch       = new name{"blast", "ematch"};
+    g_blast_backward     = new name{"blast", "backward"};
     g_blast_show_failure = new name{"blast", "show_failure"};
 
     register_unsigned_option(*blast::g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH,
@@ -157,6 +166,8 @@ void initialize_options() {
                          "(blast) enable recursor action");
     register_bool_option(*blast::g_blast_ematch, LEAN_DEFAULT_BLAST_EMATCH,
                          "(blast) enable heuristic instantiation based on e-matching");
+    register_bool_option(*blast::g_blast_ematch, LEAN_DEFAULT_BLAST_BACKWARD,
+                         "(blast) enable backward chaining");
     register_bool_option(*blast::g_blast_show_failure, LEAN_DEFAULT_BLAST_SHOW_FAILURE,
                          "(blast) show failure state");
 }
@@ -171,6 +182,7 @@ void finalize_options() {
     delete g_blast_trace_cc;
     delete g_blast_recursor;
     delete g_blast_ematch;
+    delete g_blast_backward;
     delete g_blast_show_failure;
 }
 }}
diff --git a/src/library/blast/options.h b/src/library/blast/options.h
index f950b99b5..a55da8fdf 100644
--- a/src/library/blast/options.h
+++ b/src/library/blast/options.h
@@ -20,6 +20,7 @@ struct config {
     bool                       m_recursor;
     bool                       m_ematch;
     bool                       m_cc;
+    bool                       m_backward;
     bool                       m_trace_cc;
     bool                       m_show_failure;
     unsigned                   m_pattern_max_steps;