From 03a0a6f6a13e1b3125f847b633db511074706eec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Mar 2016 15:53:02 -0800 Subject: [PATCH] refactor occurrence utility for common use (to be used in ctx_simplifier) per Nuno's suggestion Signed-off-by: Nikolaj Bjorner --- src/tactic/core/collect_occs.cpp | 97 +++++++++++++++++++++++++ src/tactic/core/collect_occs.h | 38 ++++++++++ src/tactic/core/elim_uncnstr_tactic.cpp | 85 +--------------------- 3 files changed, 138 insertions(+), 82 deletions(-) create mode 100644 src/tactic/core/collect_occs.cpp create mode 100644 src/tactic/core/collect_occs.h diff --git a/src/tactic/core/collect_occs.cpp b/src/tactic/core/collect_occs.cpp new file mode 100644 index 000000000..69c538db6 --- /dev/null +++ b/src/tactic/core/collect_occs.cpp @@ -0,0 +1,97 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + collect_cccs.cpp + +Abstract: + + Collect variables by occurrences. + +Author: + + Leonardo (leonardo) 2011-10-22 + +Notes: + +--*/ + +#include "ast.h" +#include "goal.h" +#include "hashtable.h" +#include "collect_occs.h" + +bool collect_occs::visit(expr * t) { + if (m_visited.is_marked(t)) { + if (is_uninterp_const(t)) + m_more_than_once.mark(t); + return true; + } + m_visited.mark(t); + if (is_uninterp_const(t)) { + m_vars.push_back(to_app(t)); + return true; + } + if (is_var(t)) + return true; + if (is_app(t) && to_app(t)->get_num_args() == 0) + return true; + m_stack.push_back(frame(t, 0)); + return false; +} + +void collect_occs::process(expr * t) { + SASSERT(m_stack.empty()); + if (visit(t)) + return; + SASSERT(!m_stack.empty()); + unsigned num; + expr * child; + while (!m_stack.empty()) { + start: + frame & fr = m_stack.back(); + expr * t = fr.first; + switch (t->get_kind()) { + case AST_APP: + num = to_app(t)->get_num_args(); + while (fr.second < num) { + child = to_app(t)->get_arg(fr.second); + fr.second++; + if (!visit(child)) + goto start; + } + m_stack.pop_back(); + break; + case AST_QUANTIFIER: + // don't need to visit patterns + child = to_quantifier(t)->get_expr(); + fr.second++; + if (!visit(child)) + goto start; + m_stack.pop_back(); + break; + default: + UNREACHABLE(); + } + } +} + + +void collect_occs::operator()(goal const & g, obj_hashtable & r) { + unsigned sz = g.size(); + for (unsigned i = 0; i < sz; i++) { + expr * t = g.form(i); + process(t); + } + + ptr_vector::const_iterator it = m_vars.begin(); + ptr_vector::const_iterator end = m_vars.end(); + for (; it != end; ++it) { + if (m_more_than_once.is_marked(*it)) + continue; + r.insert(*it); + } + m_visited.reset(); + m_more_than_once.reset(); +} diff --git a/src/tactic/core/collect_occs.h b/src/tactic/core/collect_occs.h new file mode 100644 index 000000000..7b42e44a6 --- /dev/null +++ b/src/tactic/core/collect_occs.h @@ -0,0 +1,38 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + collect_cccs.h + +Abstract: + + Collect variables by occurrences. + +Author: + + Leonardo (leonardo) 2011-10-22 + +Notes: + +--*/ +#ifndef COLLECT_OCCS_H_ +#define COLLECT_OCCS_H_ + +class collect_occs { + expr_fast_mark1 m_visited; + expr_fast_mark2 m_more_than_once; + typedef std::pair frame; + svector m_stack; + ptr_vector m_vars; + + bool visit(expr * t); + void process(expr * t); + +public: + + void operator()(goal const & g, obj_hashtable & r); + +}; + +#endif diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 538797ddf..156f69388 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -24,6 +24,7 @@ Notes: #include"bv_decl_plugin.h" #include"array_decl_plugin.h" #include"datatype_decl_plugin.h" +#include"collect_occs.h" #include"cooperate.h" #include"ast_smt2_pp.h" #include"ast_ll_pp.h" @@ -32,86 +33,6 @@ class elim_uncnstr_tactic : public tactic { struct imp { // unconstrained vars collector - struct collect { - expr_fast_mark1 m_visited; - expr_fast_mark2 m_more_than_once; - typedef std::pair frame; - svector m_stack; - ptr_vector m_vars; - - bool visit(expr * t) { - if (m_visited.is_marked(t)) { - if (is_uninterp_const(t)) - m_more_than_once.mark(t); - return true; - } - m_visited.mark(t); - if (is_uninterp_const(t)) { - m_vars.push_back(to_app(t)); - return true; - } - if (is_var(t)) - return true; - if (is_app(t) && to_app(t)->get_num_args() == 0) - return true; - m_stack.push_back(frame(t, 0)); - return false; - } - - void process(expr * t) { - SASSERT(m_stack.empty()); - if (visit(t)) - return; - SASSERT(!m_stack.empty()); - unsigned num; - expr * child; - while (!m_stack.empty()) { - start: - frame & fr = m_stack.back(); - expr * t = fr.first; - switch (t->get_kind()) { - case AST_APP: - num = to_app(t)->get_num_args(); - while (fr.second < num) { - child = to_app(t)->get_arg(fr.second); - fr.second++; - if (!visit(child)) - goto start; - } - m_stack.pop_back(); - break; - case AST_QUANTIFIER: - // don't need to visit patterns - child = to_quantifier(t)->get_expr(); - fr.second++; - if (!visit(child)) - goto start; - m_stack.pop_back(); - break; - default: - UNREACHABLE(); - } - } - } - - void operator()(goal const & g, obj_hashtable & r) { - unsigned sz = g.size(); - for (unsigned i = 0; i < sz; i++) { - expr * t = g.form(i); - process(t); - } - - ptr_vector::const_iterator it = m_vars.begin(); - ptr_vector::const_iterator end = m_vars.end(); - for (; it != end; ++it) { - if (m_more_than_once.is_marked(*it)) - continue; - r.insert(*it); - } - m_visited.reset(); - m_more_than_once.reset(); - } - }; typedef extension_model_converter mc; @@ -910,7 +831,7 @@ class elim_uncnstr_tactic : public tactic { TRACE("elim_uncnstr_bug", g->display(tout);); tactic_report report("elim-uncnstr-vars", *g); m_vars.reset(); - collect p; + collect_occs p; p(*g, m_vars); if (m_vars.empty()) { result.push_back(g.get()); @@ -977,7 +898,7 @@ class elim_uncnstr_tactic : public tactic { m_rw->reset(); // reset cache m_vars.reset(); { - collect p; + collect_occs p; p(*g, m_vars); } if (m_vars.empty())