From a9d61d48ae5c21ee6bfafbd6baa244f8cbb53a1d Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Fri, 21 Oct 2016 12:08:46 -0700 Subject: [PATCH 1/9] Add basic Sine Qua Non filtering --- contrib/cmake/src/tactic/CMakeLists.txt | 1 + src/tactic/sine_filter.cpp | 252 ++++++++++++++++++++++++ src/tactic/sine_filter.h | 28 +++ 3 files changed, 281 insertions(+) create mode 100644 src/tactic/sine_filter.cpp create mode 100644 src/tactic/sine_filter.h diff --git a/contrib/cmake/src/tactic/CMakeLists.txt b/contrib/cmake/src/tactic/CMakeLists.txt index 318803cd2..324d8089b 100644 --- a/contrib/cmake/src/tactic/CMakeLists.txt +++ b/contrib/cmake/src/tactic/CMakeLists.txt @@ -12,6 +12,7 @@ z3_add_component(tactic probe.cpp proof_converter.cpp replace_proof_converter.cpp + sine_filter.cpp tactical.cpp tactic.cpp COMPONENT_DEPENDENCIES diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp new file mode 100644 index 000000000..15f0fca7a --- /dev/null +++ b/src/tactic/sine_filter.cpp @@ -0,0 +1,252 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + sine_filter.cpp + +Abstract: + + Tactic that performs Sine Qua Non premise selection + +Revision History: +--*/ + +#include "sine_filter.h" +#include "tactical.h" +#include "filter_model_converter.h" +#include "datatype_decl_plugin.h" +#include "rewriter_def.h" +#include "filter_model_converter.h" +#include "extension_model_converter.h" +#include "var_subst.h" +#include "ast_util.h" +#include "obj_pair_hashtable.h" + +#if 0 +TODO documentation here +#endif + + +class sine_tactic : public tactic { + + ast_manager& m; + params_ref m_params; + datatype_util m_dt; + ref m_ext; + ref m_filter; + unsigned m_num_transformed; + +public: + + sine_tactic(ast_manager& m, params_ref const& p): + m(m), m_params(p), m_dt(m) {} + + virtual tactic * translate(ast_manager & m) { + return alloc(sine_tactic, m, m_params); + } + + virtual void updt_params(params_ref const & p) { + } + + virtual void collect_param_descrs(param_descrs & r) { + } + + virtual void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + mc = 0; pc = 0; core = 0; + + TRACE("sine", g->display(tout);); + TRACE("sine", tout << g->size();); + ptr_vector new_forms; + filter_expressions(g, new_forms); + TRACE("sine", tout << new_forms.size();); + g->reset(); + for (unsigned i = 0; i < new_forms.size(); i++) { + g->assert_expr(new_forms.get(i), 0, 0); + } + g->inc_depth(); + g->updt_prec(goal::OVER); + result.push_back(g.get()); + TRACE("sine", result[0]->display(tout);); + SASSERT(g->is_well_sorted()); + filter_model_converter * fmc = alloc(filter_model_converter, m); + mc = fmc; + } + + virtual void cleanup() { + } + +private: + + // is this a user-defined symbol name? + bool is_name(func_decl * f) { + return f->get_family_id() < 0; + } + + typedef std::pair t_work_item; + + t_work_item work_item(expr *e, expr *root) { + return std::pair(e, root); + } + + void find_constants(expr *e, obj_hashtable &consts) { + ptr_vector stack; + stack.push_back(e); + expr *curr; + while (!stack.empty()) { + curr = stack.back(); + stack.pop_back(); + if (is_app(curr)) { + app *a = to_app(curr); + func_decl *f = a->get_decl(); + if (is_name(f) && !consts.contains(f)) { + consts.insert(f); + } + } + } + } + + bool quantifier_matches(quantifier *q, + obj_hashtable const & consts, + ptr_vector & next_consts) { + TRACE("sine", tout << "size of consts is "; tout << consts.size(); tout << "\n";); + for (obj_hashtable::iterator constit = consts.begin(), constend = consts.end(); constit != constend; constit++) { + TRACE("sine", tout << *constit; tout << "\n";); + } + bool matched = false; + for (int i = 0; i < q->get_num_patterns(); i++) { + bool p_matched = true; + vector stack; + expr *curr; + // patterns are wrapped with "pattern" + stack.push_back(to_app(q->get_pattern(i))->get_arg(0)); + while (!stack.empty()) { + curr = stack.back(); + stack.pop_back(); + if (is_app(curr)) { + app *a = to_app(curr); + func_decl *f = a->get_decl(); + if (!consts.contains(f)) { + TRACE("sine", tout << f; tout << "\n";); + p_matched = false; + next_consts.push_back(f); + break; + } + for (int j = 0; j < a->get_num_args(); j++) { + stack.push_back(a->get_arg(j)); + } + } + } + if (p_matched) { + matched = true; + break; + } + } + return matched; + } + + void filter_expressions(goal_ref const & g, ptr_vector & new_exprs) { + obj_map > const2exp; + obj_map > exp2const; + obj_map > const2quantifier; + obj_hashtable consts; + vector stack; + for (int i = 0; i < g->size(); i++) { + stack.push_back(work_item(g->form(i), g->form(i))); + } + t_work_item curr; + while (!stack.empty()) { + curr = stack.back(); + stack.pop_back(); + if (is_app(curr.first)) { + app *a = to_app(curr.first); + func_decl *f = a->get_decl(); + if (is_name(f)) { + if (!consts.contains(f)) { + consts.insert(f); + if (const2quantifier.contains(f)) { + for (obj_pair_hashtable::iterator it = const2quantifier[f].begin(), end = const2quantifier[f].end(); it != end; it++) { + stack.push_back(*it); + } + const2quantifier.remove(f); + } + } + if (!const2exp.contains(f)) { + const2exp.insert(f, obj_hashtable()); + } + if (!const2exp[f].contains(curr.second)) { + const2exp[f].insert(curr.second); + } + if (!exp2const.contains(curr.second)) { + exp2const.insert(curr.second, obj_hashtable()); + } + if (!exp2const[curr.second].contains(f)) { + exp2const[curr.second].insert(f); + } + } + for (int i = 0; i < a->get_num_args(); i++) { + stack.push_back(work_item(a->get_arg(i), curr.second)); + } + } + else if (is_quantifier(curr.first)) { + quantifier *q = to_quantifier(curr.first); + if (q->is_forall()) { + if (q->has_patterns()) { + ptr_vector next_consts; + if (quantifier_matches(q, consts, next_consts)) { + stack.push_back(work_item(q->get_expr(), curr.second)); + } + else { + for (unsigned i = 0; i < next_consts.size(); i++) { + func_decl *c = next_consts.get(i); + if (!const2quantifier.contains(c)) { + const2quantifier.insert(c, obj_pair_hashtable()); + } + if (!const2quantifier[c].contains(curr)) { + const2quantifier[c].insert(curr); + } + } + } + } + else { + stack.push_back(work_item(q->get_expr(), curr.second)); + } + } + else if (q->is_exists()) { + stack.push_back(work_item(q->get_expr(), curr.second)); + } + } + } + // ok, now we just need to find the connected component of the last term + + obj_hashtable visited; + ptr_vector to_visit; + to_visit.push_back(g->form(g->size() - 1)); + expr *visiting; + while (!to_visit.empty()) { + visiting = to_visit.back(); + to_visit.pop_back(); + visited.insert(visiting); + for (obj_hashtable::iterator constit = exp2const[visiting].begin(), constend = exp2const[visiting].end(); constit != constend; constit++) { + for (obj_hashtable::iterator exprit = const2exp[*constit].begin(), exprend = const2exp[*constit].end(); exprit != exprend; exprit++) { + if (!visited.contains(*exprit)) { + to_visit.push_back(*exprit); + } + } + } + } + for (int i = 0; i < g->size(); i++) { + if (visited.contains(g->form(i))) { + new_exprs.push_back(g->form(i)); + } + } + } +}; + +tactic * mk_sine_tactic(ast_manager & m, params_ref const & p) { + return alloc(sine_tactic, m, p); +} diff --git a/src/tactic/sine_filter.h b/src/tactic/sine_filter.h new file mode 100644 index 000000000..9b9e279a4 --- /dev/null +++ b/src/tactic/sine_filter.h @@ -0,0 +1,28 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + sine_filter.h + +Abstract: + + Tactic that performs Sine Qua Non premise selection + +Revision History: + +--*/ +#ifndef SINE_TACTIC_H_ +#define SINE_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_sine_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("sine-filter", "eliminate premises using Sine Qua Non", "mk_sine_tactic(m, p)") +*/ + +#endif From b00c4d2e64ad0aaa15f8a7dc5252ead76eac7a08 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Mon, 30 Jan 2017 20:54:24 -0800 Subject: [PATCH 2/9] add name --- src/tactic/sine_filter.cpp | 4 ++++ src/tactic/sine_filter.h | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 15f0fca7a..2052035f7 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -9,6 +9,10 @@ Abstract: Tactic that performs Sine Qua Non premise selection +Author: + + Doug Woos + Revision History: --*/ diff --git a/src/tactic/sine_filter.h b/src/tactic/sine_filter.h index 9b9e279a4..769ef474f 100644 --- a/src/tactic/sine_filter.h +++ b/src/tactic/sine_filter.h @@ -9,6 +9,10 @@ Abstract: Tactic that performs Sine Qua Non premise selection +Author: + + Doug Woos + Revision History: --*/ From da63f6b0ffce1b11260bc505cbfa01efb66b1ecf Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Mon, 30 Jan 2017 20:54:33 -0800 Subject: [PATCH 3/9] delete comment --- src/tactic/sine_filter.cpp | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 2052035f7..d76e8f6b5 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -27,11 +27,6 @@ Revision History: #include "ast_util.h" #include "obj_pair_hashtable.h" -#if 0 -TODO documentation here -#endif - - class sine_tactic : public tactic { ast_manager& m; From c0bb6dd2be9cabb4cc774babb6bae9a530298161 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Mon, 30 Jan 2017 20:54:40 -0800 Subject: [PATCH 4/9] delete unused args --- src/tactic/sine_filter.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index d76e8f6b5..60482d86e 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -31,15 +31,11 @@ class sine_tactic : public tactic { ast_manager& m; params_ref m_params; - datatype_util m_dt; - ref m_ext; - ref m_filter; - unsigned m_num_transformed; public: sine_tactic(ast_manager& m, params_ref const& p): - m(m), m_params(p), m_dt(m) {} + m(m), m_params(p) {} virtual tactic * translate(ast_manager & m) { return alloc(sine_tactic, m, m_params); From 89ba99918eed693a97b4378b448726e1758e2e90 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Mon, 30 Jan 2017 21:02:09 -0800 Subject: [PATCH 5/9] reindent --- src/tactic/sine_filter.cpp | 302 ++++++++++++++++++------------------- 1 file changed, 151 insertions(+), 151 deletions(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 60482d86e..f5ecc36a3 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -3,15 +3,15 @@ Copyright (c) 2016 Microsoft Corporation Module Name: - sine_filter.cpp + sine_filter.cpp Abstract: - Tactic that performs Sine Qua Non premise selection + Tactic that performs Sine Qua Non premise selection Author: - Doug Woos + Doug Woos Revision History: --*/ @@ -35,7 +35,7 @@ class sine_tactic : public tactic { public: sine_tactic(ast_manager& m, params_ref const& p): - m(m), m_params(p) {} + m(m), m_params(p) {} virtual tactic * translate(ast_manager & m) { return alloc(sine_tactic, m, m_params); @@ -61,7 +61,7 @@ public: TRACE("sine", tout << new_forms.size();); g->reset(); for (unsigned i = 0; i < new_forms.size(); i++) { - g->assert_expr(new_forms.get(i), 0, 0); + g->assert_expr(new_forms.get(i), 0, 0); } g->inc_depth(); g->updt_prec(goal::OVER); @@ -77,169 +77,169 @@ public: private: - // is this a user-defined symbol name? - bool is_name(func_decl * f) { - return f->get_family_id() < 0; - } + // is this a user-defined symbol name? + bool is_name(func_decl * f) { + return f->get_family_id() < 0; + } - typedef std::pair t_work_item; + typedef std::pair t_work_item; - t_work_item work_item(expr *e, expr *root) { - return std::pair(e, root); - } + t_work_item work_item(expr *e, expr *root) { + return std::pair(e, root); + } - void find_constants(expr *e, obj_hashtable &consts) { - ptr_vector stack; - stack.push_back(e); - expr *curr; - while (!stack.empty()) { - curr = stack.back(); - stack.pop_back(); - if (is_app(curr)) { - app *a = to_app(curr); - func_decl *f = a->get_decl(); - if (is_name(f) && !consts.contains(f)) { - consts.insert(f); + void find_constants(expr *e, obj_hashtable &consts) { + ptr_vector stack; + stack.push_back(e); + expr *curr; + while (!stack.empty()) { + curr = stack.back(); + stack.pop_back(); + if (is_app(curr)) { + app *a = to_app(curr); + func_decl *f = a->get_decl(); + if (is_name(f) && !consts.contains(f)) { + consts.insert(f); + } + } } - } } - } - bool quantifier_matches(quantifier *q, - obj_hashtable const & consts, - ptr_vector & next_consts) { - TRACE("sine", tout << "size of consts is "; tout << consts.size(); tout << "\n";); - for (obj_hashtable::iterator constit = consts.begin(), constend = consts.end(); constit != constend; constit++) { - TRACE("sine", tout << *constit; tout << "\n";); - } - bool matched = false; - for (int i = 0; i < q->get_num_patterns(); i++) { - bool p_matched = true; - vector stack; - expr *curr; - // patterns are wrapped with "pattern" - stack.push_back(to_app(q->get_pattern(i))->get_arg(0)); - while (!stack.empty()) { - curr = stack.back(); - stack.pop_back(); - if (is_app(curr)) { - app *a = to_app(curr); - func_decl *f = a->get_decl(); - if (!consts.contains(f)) { - TRACE("sine", tout << f; tout << "\n";); - p_matched = false; - next_consts.push_back(f); - break; - } - for (int j = 0; j < a->get_num_args(); j++) { - stack.push_back(a->get_arg(j)); - } + bool quantifier_matches(quantifier *q, + obj_hashtable const & consts, + ptr_vector & next_consts) { + TRACE("sine", tout << "size of consts is "; tout << consts.size(); tout << "\n";); + for (obj_hashtable::iterator constit = consts.begin(), constend = consts.end(); constit != constend; constit++) { + TRACE("sine", tout << *constit; tout << "\n";); } - } - if (p_matched) { - matched = true; - break; - } + bool matched = false; + for (int i = 0; i < q->get_num_patterns(); i++) { + bool p_matched = true; + vector stack; + expr *curr; + // patterns are wrapped with "pattern" + stack.push_back(to_app(q->get_pattern(i))->get_arg(0)); + while (!stack.empty()) { + curr = stack.back(); + stack.pop_back(); + if (is_app(curr)) { + app *a = to_app(curr); + func_decl *f = a->get_decl(); + if (!consts.contains(f)) { + TRACE("sine", tout << f; tout << "\n";); + p_matched = false; + next_consts.push_back(f); + break; + } + for (int j = 0; j < a->get_num_args(); j++) { + stack.push_back(a->get_arg(j)); + } + } + } + if (p_matched) { + matched = true; + break; + } + } + return matched; } - return matched; - } - void filter_expressions(goal_ref const & g, ptr_vector & new_exprs) { - obj_map > const2exp; - obj_map > exp2const; - obj_map > const2quantifier; - obj_hashtable consts; - vector stack; - for (int i = 0; i < g->size(); i++) { - stack.push_back(work_item(g->form(i), g->form(i))); - } - t_work_item curr; - while (!stack.empty()) { - curr = stack.back(); - stack.pop_back(); - if (is_app(curr.first)) { - app *a = to_app(curr.first); - func_decl *f = a->get_decl(); - if (is_name(f)) { - if (!consts.contains(f)) { - consts.insert(f); - if (const2quantifier.contains(f)) { - for (obj_pair_hashtable::iterator it = const2quantifier[f].begin(), end = const2quantifier[f].end(); it != end; it++) { - stack.push_back(*it); - } - const2quantifier.remove(f); - } - } - if (!const2exp.contains(f)) { - const2exp.insert(f, obj_hashtable()); - } - if (!const2exp[f].contains(curr.second)) { - const2exp[f].insert(curr.second); - } - if (!exp2const.contains(curr.second)) { - exp2const.insert(curr.second, obj_hashtable()); - } - if (!exp2const[curr.second].contains(f)) { - exp2const[curr.second].insert(f); - } + void filter_expressions(goal_ref const & g, ptr_vector & new_exprs) { + obj_map > const2exp; + obj_map > exp2const; + obj_map > const2quantifier; + obj_hashtable consts; + vector stack; + for (int i = 0; i < g->size(); i++) { + stack.push_back(work_item(g->form(i), g->form(i))); } - for (int i = 0; i < a->get_num_args(); i++) { - stack.push_back(work_item(a->get_arg(i), curr.second)); - } - } - else if (is_quantifier(curr.first)) { - quantifier *q = to_quantifier(curr.first); - if (q->is_forall()) { - if (q->has_patterns()) { - ptr_vector next_consts; - if (quantifier_matches(q, consts, next_consts)) { - stack.push_back(work_item(q->get_expr(), curr.second)); - } - else { - for (unsigned i = 0; i < next_consts.size(); i++) { - func_decl *c = next_consts.get(i); - if (!const2quantifier.contains(c)) { - const2quantifier.insert(c, obj_pair_hashtable()); + t_work_item curr; + while (!stack.empty()) { + curr = stack.back(); + stack.pop_back(); + if (is_app(curr.first)) { + app *a = to_app(curr.first); + func_decl *f = a->get_decl(); + if (is_name(f)) { + if (!consts.contains(f)) { + consts.insert(f); + if (const2quantifier.contains(f)) { + for (obj_pair_hashtable::iterator it = const2quantifier[f].begin(), end = const2quantifier[f].end(); it != end; it++) { + stack.push_back(*it); + } + const2quantifier.remove(f); + } + } + if (!const2exp.contains(f)) { + const2exp.insert(f, obj_hashtable()); + } + if (!const2exp[f].contains(curr.second)) { + const2exp[f].insert(curr.second); + } + if (!exp2const.contains(curr.second)) { + exp2const.insert(curr.second, obj_hashtable()); + } + if (!exp2const[curr.second].contains(f)) { + exp2const[curr.second].insert(f); + } } - if (!const2quantifier[c].contains(curr)) { - const2quantifier[c].insert(curr); + for (int i = 0; i < a->get_num_args(); i++) { + stack.push_back(work_item(a->get_arg(i), curr.second)); + } + } + else if (is_quantifier(curr.first)) { + quantifier *q = to_quantifier(curr.first); + if (q->is_forall()) { + if (q->has_patterns()) { + ptr_vector next_consts; + if (quantifier_matches(q, consts, next_consts)) { + stack.push_back(work_item(q->get_expr(), curr.second)); + } + else { + for (unsigned i = 0; i < next_consts.size(); i++) { + func_decl *c = next_consts.get(i); + if (!const2quantifier.contains(c)) { + const2quantifier.insert(c, obj_pair_hashtable()); + } + if (!const2quantifier[c].contains(curr)) { + const2quantifier[c].insert(curr); + } + } + } + } + else { + stack.push_back(work_item(q->get_expr(), curr.second)); + } + } + else if (q->is_exists()) { + stack.push_back(work_item(q->get_expr(), curr.second)); } - } } - } - else { - stack.push_back(work_item(q->get_expr(), curr.second)); - } } - else if (q->is_exists()) { - stack.push_back(work_item(q->get_expr(), curr.second)); - } - } - } - // ok, now we just need to find the connected component of the last term + // ok, now we just need to find the connected component of the last term - obj_hashtable visited; - ptr_vector to_visit; - to_visit.push_back(g->form(g->size() - 1)); - expr *visiting; - while (!to_visit.empty()) { - visiting = to_visit.back(); - to_visit.pop_back(); - visited.insert(visiting); - for (obj_hashtable::iterator constit = exp2const[visiting].begin(), constend = exp2const[visiting].end(); constit != constend; constit++) { - for (obj_hashtable::iterator exprit = const2exp[*constit].begin(), exprend = const2exp[*constit].end(); exprit != exprend; exprit++) { - if (!visited.contains(*exprit)) { - to_visit.push_back(*exprit); - } + obj_hashtable visited; + ptr_vector to_visit; + to_visit.push_back(g->form(g->size() - 1)); + expr *visiting; + while (!to_visit.empty()) { + visiting = to_visit.back(); + to_visit.pop_back(); + visited.insert(visiting); + for (obj_hashtable::iterator constit = exp2const[visiting].begin(), constend = exp2const[visiting].end(); constit != constend; constit++) { + for (obj_hashtable::iterator exprit = const2exp[*constit].begin(), exprend = const2exp[*constit].end(); exprit != exprend; exprit++) { + if (!visited.contains(*exprit)) { + to_visit.push_back(*exprit); + } + } + } + } + for (int i = 0; i < g->size(); i++) { + if (visited.contains(g->form(i))) { + new_exprs.push_back(g->form(i)); + } } - } } - for (int i = 0; i < g->size(); i++) { - if (visited.contains(g->form(i))) { - new_exprs.push_back(g->form(i)); - } - } - } }; tactic * mk_sine_tactic(ast_manager & m, params_ref const & p) { From d9e43f0e6d592d6b385b673a3c1dc8e12ca753c4 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Tue, 31 Jan 2017 11:47:44 -0800 Subject: [PATCH 6/9] use insert_if_not_there --- src/tactic/sine_filter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index f5ecc36a3..71ae58f8c 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -98,8 +98,8 @@ private: if (is_app(curr)) { app *a = to_app(curr); func_decl *f = a->get_decl(); - if (is_name(f) && !consts.contains(f)) { - consts.insert(f); + if (is_name(f)) { + consts.insert_if_not_there(f); } } } From a147e2bc3530da587c4128eeae020cd33e3bbdaf Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Wed, 1 Feb 2017 16:20:40 -0800 Subject: [PATCH 7/9] use is_uninterp --- src/tactic/sine_filter.cpp | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 71ae58f8c..43c15bf74 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -77,11 +77,6 @@ public: private: - // is this a user-defined symbol name? - bool is_name(func_decl * f) { - return f->get_family_id() < 0; - } - typedef std::pair t_work_item; t_work_item work_item(expr *e, expr *root) { @@ -97,8 +92,8 @@ private: stack.pop_back(); if (is_app(curr)) { app *a = to_app(curr); - func_decl *f = a->get_decl(); - if (is_name(f)) { + if (is_uninterp(a)) { + func_decl *f = a->get_decl(); consts.insert_if_not_there(f); } } @@ -159,8 +154,8 @@ private: stack.pop_back(); if (is_app(curr.first)) { app *a = to_app(curr.first); - func_decl *f = a->get_decl(); - if (is_name(f)) { + if (is_uninterp(a)) { + func_decl *f = a->get_decl(); if (!consts.contains(f)) { consts.insert(f); if (const2quantifier.contains(f)) { From 44c417904b268c6bbb175082c81f58c0ada1a422 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Wed, 1 Feb 2017 16:21:01 -0800 Subject: [PATCH 8/9] correctly pretty-print --- src/tactic/sine_filter.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 43c15bf74..059608b4c 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -26,6 +26,7 @@ Revision History: #include "var_subst.h" #include "ast_util.h" #include "obj_pair_hashtable.h" +#include "ast_pp.h" class sine_tactic : public tactic { @@ -121,7 +122,7 @@ private: app *a = to_app(curr); func_decl *f = a->get_decl(); if (!consts.contains(f)) { - TRACE("sine", tout << f; tout << "\n";); + TRACE("sine", tout << mk_pp(f, m) << "\n";); p_matched = false; next_consts.push_back(f); break; From d6fbfe401e282f3a86abbe21a5363256996e3ea6 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Wed, 1 Feb 2017 16:21:15 -0800 Subject: [PATCH 9/9] add and use new is_pattern recognizer --- src/ast/ast.cpp | 16 ++++++++++++++++ src/ast/ast.h | 2 ++ src/tactic/sine_filter.cpp | 6 ++++-- 3 files changed, 22 insertions(+), 2 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 440179ba8..7be7300a2 100644 --- a/src/ast/ast.cpp +++ b/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 &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, diff --git a/src/ast/ast.h b/src/ast/ast.h index 47ea0f812..9259d5431 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1840,6 +1840,8 @@ public: bool is_pattern(expr const * n) const; + bool is_pattern(expr const *n, ptr_vector &args); + public: quantifier * mk_quantifier(bool forall, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 059608b4c..e180eea5e 100644 --- a/src/tactic/sine_filter.cpp +++ b/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 stack; + ptr_vector 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();