From cb2bf482549f91a05752bdd091e0709d672c9fed Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 30 Mar 2016 15:22:53 +0100
Subject: [PATCH] Added has_quantifier probe

---
 src/tactic/probe.cpp | 33 +++++++++++++++++++++++++++++++++
 src/tactic/probe.h   |  9 ++++++++-
 2 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp
index 3473d33d9..ecc27eccf 100644
--- a/src/tactic/probe.cpp
+++ b/src/tactic/probe.cpp
@@ -533,3 +533,36 @@ public:
 probe * mk_has_pattern_probe() {
     return alloc(has_pattern_probe);
 }
+
+
+struct has_quantifier_probe : public probe {
+    struct found {};
+
+    struct proc {
+        void operator()(var * n) {}
+        void operator()(app * n) {}
+        void operator()(quantifier * n) { throw found(); }
+    };
+public:
+    virtual result operator()(goal const & g) {
+        try {
+            expr_fast_mark1 visited;
+            proc p;
+            unsigned sz = g.size();
+            for (unsigned i = 0; i < sz; i++) {
+                quick_for_each_expr(p, visited, g.form(i));
+            }
+            return false;
+        }
+        catch (found) {
+            return true;
+        }
+    }
+};
+
+probe * mk_has_quantifier_probe() {
+    return alloc(has_quantifier_probe);
+}
+
+
+
diff --git a/src/tactic/probe.h b/src/tactic/probe.h
index b5be1cc8e..8894a75d8 100644
--- a/src/tactic/probe.h
+++ b/src/tactic/probe.h
@@ -84,7 +84,6 @@ probe * mk_num_bv_consts_probe();
 probe * mk_produce_proofs_probe();
 probe * mk_produce_models_probe();
 probe * mk_produce_unsat_cores_probe();
-probe * mk_has_pattern_probe();
 
 /*
   ADD_PROBE("produce-proofs", "true if proof generation is enabled for the given goal.", "mk_produce_proofs_probe()")
@@ -93,6 +92,14 @@ probe * mk_has_pattern_probe();
   ADD_PROBE("has-patterns", "true if the goal contains quantifiers with patterns.", "mk_has_pattern_probe()")
 */
 
+probe * mk_has_quantifier_probe();
+probe * mk_has_pattern_probe();
+
+/*
+  ADD_PROBE("has-quantifier", "true if the goal contains quantifiers.", "mk_has_quantifier_probe()")
+  ADD_PROBE("has-patterns", "true if the goal contains quantifiers with patterns.", "mk_has_pattern_probe()")
+*/
+
 // Some basic combinators for probes
 probe * mk_not(probe * p1);
 probe * mk_and(probe * p1, probe * p2);