Added has_quantifier probe

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);
+}
+
+
+

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);