add and use new is_pattern recognizer

src/ast/ast.cpp

@@ -2326,6 +2326,22 @@ bool ast_manager::is_pattern(expr const * n) const {
     return true;
 }
 
+
+bool ast_manager::is_pattern(expr const * n, ptr_vector<expr> &args) {
+    if (!is_app_of(n, m_pattern_family_id, OP_PATTERN)) {
+        return false;
+    }
+    for (unsigned i = 0; i < to_app(n)->get_num_args(); ++i) {
+        expr *arg = to_app(n)->get_arg(i);
+        if (!is_app(arg)) {
+            return false;
+        }
+        args.push_back(arg);
+    }
+    return true;
+}
+
+
 quantifier * ast_manager::mk_quantifier(bool forall, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names,
                                         expr * body, int weight , symbol const & qid, symbol const & skid,
                                         unsigned num_patterns, expr * const * patterns,

src/ast/ast.h

@@ -1840,6 +1840,8 @@ public:
 
     bool is_pattern(expr const * n) const;
 
+    bool is_pattern(expr const *n, ptr_vector<expr> &args);
+
 public:
 
     quantifier * mk_quantifier(bool forall, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,

src/tactic/sine_filter.cpp

@@ -111,10 +111,12 @@ private:
         bool matched = false;
         for (int i = 0; i < q->get_num_patterns(); i++) {
             bool p_matched = true;
-            vector<expr *> stack;
+            ptr_vector<expr> stack;
             expr *curr;
             // patterns are wrapped with "pattern"
-            stack.push_back(to_app(q->get_pattern(i))->get_arg(0));
+            if (!m.is_pattern(q->get_pattern(i), stack)) {
+                continue;
+            }
             while (!stack.empty()) {
                 curr = stack.back();
                 stack.pop_back();