From 287c6f08e1250a610ad8d3a4e4821218a8652800 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 5 Apr 2018 20:31:45 +0100 Subject: [PATCH] Resolved merge conflict --- src/tactic/sine_filter.cpp | 149 ++++++++++++++++++++----------------- 1 file changed, 79 insertions(+), 70 deletions(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 88792e955..e67169a8e 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -35,25 +35,25 @@ class sine_tactic : public tactic { public: - sine_tactic(ast_manager& m, params_ref const& p): + sine_tactic(ast_manager& m, params_ref const& p): m(m), m_params(p) {} - - tactic * translate(ast_manager & m) override { + + virtual tactic * translate(ast_manager & m) { return alloc(sine_tactic, m, m_params); } - void updt_params(params_ref const & p) override { + virtual void updt_params(params_ref const & p) { } - void collect_param_descrs(param_descrs & r) override { + virtual void collect_param_descrs(param_descrs & r) { } - void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) override { - mc = nullptr; pc = nullptr; core = nullptr; + 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();); @@ -62,7 +62,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), nullptr, nullptr); + g->assert_expr(new_forms.get(i), 0, 0); } g->inc_depth(); g->updt_prec(goal::OVER); @@ -72,115 +72,120 @@ public: filter_model_converter * fmc = alloc(filter_model_converter, m); mc = fmc; } - - void cleanup() override { + + virtual void cleanup() { } private: typedef std::pair t_work_item; - t_work_item work_item(expr *e, expr *root) { + t_work_item work_item(expr * e, expr * root) { return std::pair(e, root); } - void find_constants(expr *e, obj_hashtable &consts) { + void find_constants(expr * e, obj_hashtable &consts) { ptr_vector stack; stack.push_back(e); - expr *curr; + expr * curr; while (!stack.empty()) { curr = stack.back(); stack.pop_back(); - if (is_app(curr)) { + if (is_app(curr) && is_uninterp(curr)) { app *a = to_app(curr); - if (is_uninterp(a)) { - func_decl *f = a->get_decl(); - consts.insert_if_not_there(f); - } + func_decl *f = a->get_decl(); + consts.insert_if_not_there(f); } } } - bool quantifier_matches(quantifier *q, + 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";); - } + TRACE("sine", + tout << "size of consts is "; tout << consts.size(); tout << "\n"; + obj_hashtable::iterator it = consts.begin(); + obj_hashtable::iterator end = consts.end(); + for (; it != end; it++) + tout << *it << "\n"; ); + bool matched = false; for (unsigned i = 0; i < q->get_num_patterns(); i++) { bool p_matched = true; ptr_vector stack; - expr *curr; + expr * curr; + // patterns are wrapped with "pattern" - if (!m.is_pattern(q->get_pattern(i), stack)) { + if (!m.is_pattern(q->get_pattern(i), stack)) continue; - } + while (!stack.empty()) { curr = stack.back(); stack.pop_back(); + if (is_app(curr)) { - app *a = to_app(curr); - func_decl *f = a->get_decl(); + app * a = to_app(curr); + func_decl * f = a->get_decl(); if (!consts.contains(f)) { TRACE("sine", tout << mk_pp(f, m) << "\n";); p_matched = false; next_consts.push_back(f); break; } - for (unsigned j = 0; j < a->get_num_args(); j++) { + for (unsigned 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 (unsigned i = 0; i < g->size(); i++) { - stack.push_back(work_item(g->form(i), g->form(i))); - } t_work_item curr; + + for (unsigned i = 0; i < g->size(); i++) + stack.push_back(work_item(g->form(i), g->form(i))); + while (!stack.empty()) { curr = stack.back(); stack.pop_back(); - if (is_app(curr.first)) { - app *a = to_app(curr.first); - if (is_uninterp(a)) { - func_decl *f = a->get_decl(); - 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 (is_app(curr.first) && is_uninterp(curr.first)) { + app * a = to_app(curr.first); + func_decl * f = a->get_decl(); + if (!consts.contains(f)) { + consts.insert(f); + if (const2quantifier.contains(f)) { + obj_pair_hashtable::iterator it = const2quantifier[f].begin(); + obj_pair_hashtable::iterator end = const2quantifier[f].end(); + for (; 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 (unsigned i = 0; i < a->get_num_args(); i++) { stack.push_back(work_item(a->get_arg(i), curr.second)); } @@ -214,28 +219,32 @@ private: } } } + // 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; + 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)) { + obj_hashtable::iterator it = exp2const[visiting].begin(); + obj_hashtable::iterator end = exp2const[visiting].end(); + for (; it != end; it++) { + obj_hashtable::iterator exprit = const2exp[*it].begin(); + obj_hashtable::iterator exprend = const2exp[*it].end(); + for (; exprit != exprend; exprit++) { + if (!visited.contains(*exprit)) to_visit.push_back(*exprit); - } } } } + for (unsigned i = 0; i < g->size(); i++) { - if (visited.contains(g->form(i))) { + if (visited.contains(g->form(i))) new_exprs.push_back(g->form(i)); - } } } };