From 39dbbd687ba975f5f53b00b9f9f8a79179488e86 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 6 Dec 2015 14:12:44 -0800
Subject: [PATCH] feat(library/blast/strategy): add 'orelse' combinator

---
 src/library/blast/strategy.cpp | 9 +++++++++
 src/library/blast/strategy.h   | 2 ++
 2 files changed, 11 insertions(+)

diff --git a/src/library/blast/strategy.cpp b/src/library/blast/strategy.cpp
index dd4be53f45..c4a710cbd0 100644
--- a/src/library/blast/strategy.cpp
+++ b/src/library/blast/strategy.cpp
@@ -93,4 +93,13 @@ optional<expr> strategy_fn::search() {
         trace_curr_state_if(r);
     }
 }
+
+strategy operator|(strategy const & s1, strategy const & s2) {
+    return [=]() {
+        if (auto r = s1())
+            return r;
+        else
+            return s2();
+    }
+}
 }}
diff --git a/src/library/blast/strategy.h b/src/library/blast/strategy.h
index a542657578..55c46166ce 100644
--- a/src/library/blast/strategy.h
+++ b/src/library/blast/strategy.h
@@ -41,4 +41,6 @@ public:
     }
 
 typedef std::function<optional<expr>()> strategy;
+
+strategy operator|(strategy const & s1, strategy const & s2);
 }}