From 6464468cd89d9ebedfbf147f768d7a393c4d97d7 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 2 Jun 2018 22:57:22 -0700 Subject: [PATCH] Remove dead code --- src/muz/spacer/spacer_manager.h | 41 +--- src/muz/spacer/spacer_sym_mux.cpp | 391 +----------------------------- src/muz/spacer/spacer_sym_mux.h | 107 +------- 3 files changed, 21 insertions(+), 518 deletions(-) diff --git a/src/muz/spacer/spacer_manager.h b/src/muz/spacer/spacer_manager.h index 2149395ef..a73a9a63b 100644 --- a/src/muz/spacer/spacer_manager.h +++ b/src/muz/spacer/spacer_manager.h @@ -96,35 +96,6 @@ public: func_decl * get_o_pred(func_decl * s, unsigned idx); func_decl * get_n_pred(func_decl * s); - void get_o_index(func_decl* p, unsigned& idx) const { - m_mux.try_get_index(p, idx); - SASSERT(idx != n_index()); - idx--; // m_mux has indices starting at 1 - } - - bool is_o(func_decl * p, unsigned idx) const - {return m_mux.has_index(p, o_index(idx));} - bool is_o(func_decl * p) const { - unsigned idx; - return m_mux.try_get_index(p, idx) && idx != n_index(); - } - bool is_o(expr* e) const - {return is_app(e) && is_o(to_app(e)->get_decl());} - bool is_o(expr* e, unsigned idx) const - {return is_app(e) && is_o(to_app(e)->get_decl(), idx);} - bool is_n(func_decl * p) const - {return m_mux.has_index(p, n_index());} - bool is_n(expr* e) const - {return is_app(e) && is_n(to_app(e)->get_decl());} - - - /** true if f doesn't contain any n predicates */ - bool is_o_formula(expr * f) const - {return !m_mux.contains(f, n_index());} - /** true if f contains only o state preds of index o_idx */ - bool is_o_formula(expr * f, unsigned o_idx) const - {return m_mux.is_homogenous_formula(f, o_index(o_idx));} - /** true if f doesn't contain any o predicates */ bool is_n_formula(expr * f) const {return m_mux.is_homogenous_formula(f, n_index());} @@ -135,18 +106,22 @@ public: func_decl * n2o(func_decl * p, unsigned o_idx) const {return m_mux.conv(p, n_index(), o_index(o_idx));} - void formula_o2n(expr * f, expr_ref & result, unsigned o_idx, bool homogenous = true) const + void formula_o2n(expr * f, expr_ref & result, unsigned o_idx, + bool homogenous = true) const {m_mux.conv_formula(f, o_index(o_idx), n_index(), result, homogenous);} - void formula_n2o(expr * f, expr_ref & result, unsigned o_idx, bool homogenous = true) const + void formula_n2o(expr * f, expr_ref & result, unsigned o_idx, + bool homogenous = true) const {m_mux.conv_formula(f, n_index(), o_index(o_idx), result, homogenous);} void formula_n2o(unsigned o_idx, bool homogenous, expr_ref & result) const - {m_mux.conv_formula(result.get(), n_index(), o_index(o_idx), result, homogenous);} + {m_mux.conv_formula(result.get(), n_index(), o_index(o_idx), + result, homogenous);} void formula_o2o(expr * src, expr_ref & tgt, unsigned src_idx, unsigned tgt_idx, bool homogenous = true) const - {m_mux.conv_formula(src, o_index(src_idx), o_index(tgt_idx), tgt, homogenous);} + {m_mux.conv_formula(src, o_index(src_idx), o_index(tgt_idx), + tgt, homogenous);} }; diff --git a/src/muz/spacer/spacer_sym_mux.cpp b/src/muz/spacer/spacer_sym_mux.cpp index ee1d3726d..9426ddcf7 100644 --- a/src/muz/spacer/spacer_sym_mux.cpp +++ b/src/muz/spacer/spacer_sym_mux.cpp @@ -82,7 +82,6 @@ void sym_mux::create_tuple(func_decl* prefix, unsigned arity, sort * const * dom m_prim2all.insert(tuple[0], tuple); m_prefix2prim.insert(prefix, tuple[0]); m_prim2prefix.insert(tuple[0], prefix); - m_prim_preds.push_back(tuple[0]); m_ref_holder.push_back(prefix); } @@ -122,32 +121,7 @@ func_decl * sym_mux::conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx) c } -func_decl * sym_mux::get_or_create_symbol_by_prefix(func_decl* prefix, unsigned idx, - unsigned arity, sort * const * domain, sort * range) -{ - func_decl * prim = try_get_primary_by_prefix(prefix); - if (prim) { - SASSERT(prim->get_arity() == arity); - SASSERT(prim->get_range() == range); - //domain should match as well, but we won't bother checking an array equality - return conv(prim, 0, idx); - } - - decl_vector syms; - create_tuple(prefix, arity, domain, range, idx + 1, syms); - return syms[idx]; -} - -bool sym_mux::is_muxed_lit(expr * e, unsigned idx) const -{ - if (!is_app(e)) { return false; } - app * a = to_app(e); - if (m.is_not(a) && is_app(a->get_arg(0))) { - a = to_app(a->get_arg(0)); - } - return is_muxed(a->get_decl()); -} struct sym_mux::formula_checker { @@ -198,155 +172,15 @@ private: bool m_found_what_needed; }; -bool sym_mux::contains(expr * e, unsigned idx) const -{ - formula_checker chck(*this, false, idx); - for_each_expr(chck, m_visited, e); - m_visited.reset(); - return chck.some_with_idx(); -} bool sym_mux::is_homogenous_formula(expr * e, unsigned idx) const { + expr_mark visited; formula_checker chck(*this, true, idx); - for_each_expr(chck, m_visited, e); - m_visited.reset(); + for_each_expr(chck, visited, e); return chck.all_have_idx(); } -bool sym_mux::is_homogenous(const expr_ref_vector & vect, unsigned idx) const -{ - expr * const * begin = vect.c_ptr(); - expr * const * end = begin + vect.size(); - for (expr * const * it = begin; it != end; it++) { - if (!is_homogenous_formula(*it, idx)) { - return false; - } - } - return true; -} - -class sym_mux::index_collector { - sym_mux const& m_parent; - svector m_indices; -public: - index_collector(sym_mux const& s): - m_parent(s) {} - - void operator()(expr * e) - { - if (is_app(e)) { - func_decl * sym = to_app(e)->get_decl(); - unsigned idx; - if (m_parent.try_get_index(sym, idx)) { - SASSERT(idx > 0); - --idx; - if (m_indices.size() <= idx) { - m_indices.resize(idx + 1, false); - } - m_indices[idx] = true; - } - } - } - - void extract(unsigned_vector& indices) - { - for (unsigned i = 0; i < m_indices.size(); ++i) { - if (m_indices[i]) { - indices.push_back(i); - } - } - } -}; - - - -void sym_mux::collect_indices(expr* e, unsigned_vector& indices) const -{ - indices.reset(); - index_collector collector(*this); - for_each_expr(collector, m_visited, e); - m_visited.reset(); - collector.extract(indices); -} - -class sym_mux::variable_collector { - sym_mux const& m_parent; - vector >& m_vars; -public: - variable_collector(sym_mux const& s, vector >& vars): - m_parent(s), m_vars(vars) {} - - void operator()(expr * e) - { - if (is_app(e)) { - func_decl * sym = to_app(e)->get_decl(); - unsigned idx; - if (m_parent.try_get_index(sym, idx)) { - SASSERT(idx > 0); - --idx; - if (m_vars.size() <= idx) { - m_vars.resize(idx + 1, ptr_vector()); - } - m_vars[idx].push_back(to_app(e)); - } - } - } -}; - -void sym_mux::collect_variables(expr* e, vector >& vars) const -{ - vars.reset(); - variable_collector collector(*this, vars); - for_each_expr(collector, m_visited, e); - m_visited.reset(); -} - -class sym_mux::hmg_checker { - const sym_mux & m_parent; - - bool m_found_idx; - unsigned m_idx; - bool m_multiple_indexes; - -public: - hmg_checker(const sym_mux & parent) : - m_parent(parent), m_found_idx(false), m_multiple_indexes(false) - { - } - - void operator()(expr * e) - { - if (m_multiple_indexes || !is_app(e)) { return; } - - func_decl * sym = to_app(e)->get_decl(); - unsigned sym_idx; - if (!m_parent.try_get_index(sym, sym_idx)) { return; } - - if (!m_found_idx) { - m_found_idx = true; - m_idx = sym_idx; - return; - } - if (m_idx == sym_idx) { return; } - m_multiple_indexes = true; - } - - bool has_multiple_indexes() const - { - return m_multiple_indexes; - } -}; - -bool sym_mux::is_homogenous_formula(expr * e) const -{ - hmg_checker chck(*this); - for_each_expr(chck, m_visited, e); - m_visited.reset(); - return !chck.has_multiple_indexes(); -} - - struct sym_mux::conv_rewriter_cfg : public default_rewriter_cfg { private: ast_manager & m; @@ -379,8 +213,8 @@ public: } }; -void sym_mux::conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous) const -{ +void sym_mux::conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, + expr_ref & res, bool homogenous) const { if (src_idx == tgt_idx) { res = f; return; @@ -389,220 +223,3 @@ void sym_mux::conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_re rewriter_tpl rwr(m, false, r_cfg); rwr(f, res); } - -struct sym_mux::shifting_rewriter_cfg : public default_rewriter_cfg { -private: - ast_manager & m; - const sym_mux & m_parent; - int m_shift; -public: - shifting_rewriter_cfg(const sym_mux & parent, int shift) - : m(parent.get_manager()), - m_parent(parent), - m_shift(shift) {} - - bool get_subst(expr * s, expr * & t, proof * & t_pr) - { - if (!is_app(s)) { return false; } - app * a = to_app(s); - func_decl * sym = a->get_decl(); - - unsigned idx; - if (!m_parent.try_get_index(sym, idx)) { - return false; - } - SASSERT(static_cast(idx) + m_shift >= 0); - func_decl * tgt = m_parent.conv(sym, idx, idx + m_shift); - t = m.mk_app(tgt, a->get_args()); - return true; - } -}; - -void sym_mux::shift_formula(expr * f, int dist, expr_ref & res) const -{ - if (dist == 0) { - res = f; - return; - } - shifting_rewriter_cfg r_cfg(*this, dist); - rewriter_tpl rwr(m, false, r_cfg); - rwr(f, res); -} - -void sym_mux::conv_formula_vector(const expr_ref_vector & vect, unsigned src_idx, unsigned tgt_idx, - expr_ref_vector & res) const -{ - res.reset(); - expr * const * begin = vect.c_ptr(); - expr * const * end = begin + vect.size(); - for (expr * const * it = begin; it != end; it++) { - expr_ref converted(m); - conv_formula(*it, src_idx, tgt_idx, converted); - res.push_back(converted); - } -} - -void sym_mux::filter_idx(expr_ref_vector & vect, unsigned idx) const -{ - unsigned i = 0; - while (i < vect.size()) { - expr* e = vect[i].get(); - if (contains(e, idx) && is_homogenous_formula(e, idx)) { - i++; - } else { - //we don't allow mixing states inside vector elements - SASSERT(!contains(e, idx)); - vect[i] = vect.back(); - vect.pop_back(); - } - } -} - -void sym_mux::partition_o_idx( - expr_ref_vector const& lits, - expr_ref_vector& o_lits, - expr_ref_vector& other, unsigned idx) const -{ - - for (unsigned i = 0; i < lits.size(); ++i) { - if (contains(lits[i], idx) && is_homogenous_formula(lits[i], idx)) { - o_lits.push_back(lits[i]); - } else { - other.push_back(lits[i]); - } - } -} - - - -class sym_mux::nonmodel_sym_checker { - const sym_mux & m_parent; - - bool m_found; -public: - nonmodel_sym_checker(const sym_mux & parent) : - m_parent(parent), m_found(false) - { - } - - void operator()(expr * e) - { - if (m_found || !is_app(e)) { return; } - - func_decl * sym = to_app(e)->get_decl(); - - if (m_parent.is_non_model_sym(sym)) { - m_found = true; - } - } - - bool found() const - { - return m_found; - } -}; - -bool sym_mux::has_nonmodel_symbol(expr * e) const -{ - nonmodel_sym_checker chck(*this); - for_each_expr(chck, e); - return chck.found(); -} - -void sym_mux::filter_non_model_lits(expr_ref_vector & vect) const -{ - unsigned i = 0; - while (i < vect.size()) { - if (!has_nonmodel_symbol(vect[i].get())) { - i++; - continue; - } - vect[i] = vect.back(); - vect.pop_back(); - } -} - -class sym_mux::decl_idx_comparator { - const sym_mux & m_parent; -public: - decl_idx_comparator(const sym_mux & parent) - : m_parent(parent) - { } - - bool operator()(func_decl * sym1, func_decl * sym2) - { - unsigned idx1, idx2; - if (!m_parent.try_get_index(sym1, idx1)) { idx1 = UINT_MAX; } - if (!m_parent.try_get_index(sym2, idx2)) { idx2 = UINT_MAX; } - - if (idx1 != idx2) { return idx1 < idx2; } - return lt(sym1->get_name(), sym2->get_name()); - } -}; - -std::string sym_mux::pp_model(const model_core & mdl) const -{ - decl_vector consts; - unsigned sz = mdl.get_num_constants(); - for (unsigned i = 0; i < sz; i++) { - func_decl * d = mdl.get_constant(i); - consts.push_back(d); - } - - std::sort(consts.begin(), consts.end(), decl_idx_comparator(*this)); - - std::stringstream res; - - decl_vector::iterator end = consts.end(); - for (decl_vector::iterator it = consts.begin(); it != end; it++) { - func_decl * d = *it; - std::string name = d->get_name().str(); - const char * arrow = " -> "; - res << name << arrow; - unsigned indent = static_cast(name.length() + strlen(arrow)); - res << mk_pp(mdl.get_const_interp(d), m, indent) << "\n"; - - if (it + 1 != end) { - unsigned idx1, idx2; - if (!try_get_index(*it, idx1)) { idx1 = UINT_MAX; } - if (!try_get_index(*(it + 1), idx2)) { idx2 = UINT_MAX; } - if (idx1 != idx2) { res << "\n"; } - } - } - return res.str(); -} - - -#if 0 - -class sym_mux::index_renamer_cfg : public default_rewriter_cfg { - const sym_mux & m_parent; - unsigned m_idx; - -public: - index_renamer_cfg(const sym_mux & p, unsigned idx) : m_parent(p), m_idx(idx) {} - - bool get_subst(expr * s, expr * & t, proof * & t_pr) - { - if (!is_app(s)) { return false; } - app * a = to_app(s); - if (a->get_family_id() != null_family_id) { - return false; - } - func_decl * sym = a->get_decl(); - unsigned idx; - if (!m_parent.try_get_index(sym, idx)) { - return false; - } - if (m_idx == idx) { - return false; - } - ast_manager& m = m_parent.get_manager(); - symbol name = symbol((sym->get_name().str() + "!").c_str()); - func_decl * tgt = m.mk_func_decl(name, sym->get_arity(), sym->get_domain(), sym->get_range()); - t = m.mk_app(tgt, a->get_num_args(), a->get_args()); - return true; - } -}; - -#endif diff --git a/src/muz/spacer/spacer_sym_mux.h b/src/muz/spacer/spacer_sym_mux.h index a4d10971a..97e3459d7 100644 --- a/src/muz/spacer/spacer_sym_mux.h +++ b/src/muz/spacer/spacer_sym_mux.h @@ -7,7 +7,8 @@ Module Name: Abstract: - A symbol multiplexer that helps with having multiple versions of each of a set of symbols. + A symbol multiplexer that helps with having multiple versions of + each of a set of symbols. Author: @@ -20,18 +21,17 @@ Revision History: #ifndef _SYM_MUX_H_ #define _SYM_MUX_H_ +#include +#include + #include "ast/ast.h" #include "util/map.h" #include "util/vector.h" -#include class model_core; namespace spacer { class sym_mux { -public: - typedef ptr_vector app_vector; - typedef ptr_vector decl_vector; private: typedef obj_map sym2u; typedef obj_map sym2dv; @@ -41,7 +41,6 @@ private: ast_manager & m; mutable ast_ref_vector m_ref_holder; - mutable expr_mark m_visited; mutable unsigned m_next_sym_suffix_idx; mutable symbols m_used_suffixes; @@ -75,24 +74,15 @@ private: */ sym2sym m_prim2prefix; - decl_vector m_prim_preds; - obj_hashtable m_non_model_syms; struct formula_checker; struct conv_rewriter_cfg; - struct shifting_rewriter_cfg; - class decl_idx_comparator; - class hmg_checker; - class nonmodel_sym_checker; - class index_renamer_cfg; - class index_collector; - class variable_collector; std::string get_suffix(unsigned i) const; void ensure_tuple_size(func_decl * prim, unsigned sz) const; - expr_ref isolate_o_idx(expr* e, unsigned idx) const; + // expr_ref isolate_o_idx(expr* e, unsigned idx) const; public: sym_mux(ast_manager & m, const std::vector & suffixes); @@ -101,9 +91,7 @@ public: bool is_muxed(func_decl * sym) const { return m_sym2idx.contains(sym); } bool try_get_index(func_decl * sym, unsigned & idx) const - { - return m_sym2idx.find(sym, idx); - } + {return m_sym2idx.find(sym, idx);} bool has_index(func_decl * sym, unsigned idx) const { @@ -143,30 +131,6 @@ public: return conv(prim, 0, idx); } - /** - Marks symbol as non-model which means it will not appear in models collected by - get_muxed_cube_from_model function. - This is to take care of auxiliary symbols introduced by the disjunction relations - to relativize lemmas coming from disjuncts. - */ - void mark_as_non_model(func_decl * sym) - { - SASSERT(is_muxed(sym)); - m_non_model_syms.insert(get_primary(sym)); - } - - func_decl * get_or_create_symbol_by_prefix(func_decl* prefix, unsigned idx, - unsigned arity, sort * const * domain, sort * range); - - - - bool is_muxed_lit(expr * e, unsigned idx) const; - - bool is_non_model_sym(func_decl * s) const - { - return is_muxed(s) && m_non_model_syms.contains(get_primary(s)); - } - /** Create a multiplexed tuple of propositional constants. Symbols may be suplied in the tuple vector, @@ -181,27 +145,7 @@ public: Return true if the only multiplexed symbols which e contains are of index idx. */ bool is_homogenous_formula(expr * e, unsigned idx) const; - bool is_homogenous(const expr_ref_vector & vect, unsigned idx) const; - /** - Return true if all multiplexed symbols which e contains are of one index. - */ - bool is_homogenous_formula(expr * e) const; - - /** - Return true if expression e contains a muxed symbol of index idx. - */ - bool contains(expr * e, unsigned idx) const; - - /** - Collect indices used in expression. - */ - void collect_indices(expr* e, unsigned_vector& indices) const; - - /** - Collect used variables of each index. - */ - void collect_variables(expr* e, vector >& vars) const; /** Convert symbol sym which has to be of src_idx variant into variant tgt_idx. @@ -213,43 +157,10 @@ public: Convert src_idx symbols in formula f variant into tgt_idx. If homogenous is true, formula cannot contain symbols of other variants. */ - void conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous = true) const; - void conv_formula_vector(const expr_ref_vector & vect, unsigned src_idx, unsigned tgt_idx, - expr_ref_vector & res) const; + void conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, + expr_ref & res, bool homogenous = true) const; - /** - Shifts the muxed symbols in f by dist. Dist can be negative, but it should never shift - symbol index to a negative value. - */ - void shift_formula(expr * f, int dist, expr_ref & res) const; - /** - Remove from vect literals (atoms or negations of atoms) of symbols - that contain multiplexed symbols with indexes other than idx. - - Each of the literals can contain only symbols multiplexed with one index - (this trivially holds if the literals are propositional). - - Order of elements in vect may be modified by this function - */ - void filter_idx(expr_ref_vector & vect, unsigned idx) const; - - /** - Partition literals into o_literals and others. - */ - void partition_o_idx(expr_ref_vector const& lits, - expr_ref_vector& o_lits, - expr_ref_vector& other, unsigned idx) const; - - bool has_nonmodel_symbol(expr * e) const; - void filter_non_model_lits(expr_ref_vector & vect) const; - - func_decl * const * begin_prim_preds() const { return m_prim_preds.begin(); } - func_decl * const * end_prim_preds() const { return m_prim_preds.end(); } - - void get_muxed_cube_from_model(const model_core & model, expr_ref_vector & res) const; - - std::string pp_model(const model_core & mdl) const; }; }