diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp index 719bf7862..856207463 100644 --- a/src/muz/spacer/spacer_manager.cpp +++ b/src/muz/spacer/spacer_manager.cpp @@ -170,42 +170,25 @@ void inductive_property::display(datalog::rule_manager& rm, ptr_vector state_suffixes() { - std::vector res; - res.push_back("_n"); - return res; -} -manager::manager(ast_manager& manager) : - m(manager), m_mux(m, state_suffixes()) { -} +manager::manager(ast_manager& manager) : m(manager), m_mux(m) {} - -void manager::add_new_state(func_decl * s) -{ - SASSERT(s->get_arity() == 0); //we currently don't support non-constant states - decl_vector vect; - - SASSERT(o_index(0) == 1); //we assume this in the number of retrieved symbols - m_mux.create_tuple(s, s->get_arity(), s->get_domain(), s->get_range(), 2, vect); -} - -func_decl * manager::get_o_pred(func_decl* s, unsigned idx) -{ - func_decl * res = m_mux.try_get_by_prefix(s, o_index(idx)); - if (res) { return res; } - add_new_state(s); - res = m_mux.try_get_by_prefix(s, o_index(idx)); +func_decl * manager::get_o_pred(func_decl* s, unsigned idx) { + func_decl * res = m_mux.find_by_decl(s, o_index(idx)); + if (!res) { + m_mux.register_decl(s); + res = m_mux.find_by_decl(s, o_index(idx)); + } SASSERT(res); return res; } -func_decl * manager::get_n_pred(func_decl* s) -{ - func_decl * res = m_mux.try_get_by_prefix(s, n_index()); - if (res) { return res; } - add_new_state(s); - res = m_mux.try_get_by_prefix(s, n_index()); +func_decl * manager::get_n_pred(func_decl* s) { + func_decl * res = m_mux.find_by_decl(s, n_index()); + if (!res) { + m_mux.register_decl(s); + res = m_mux.find_by_decl(s, n_index()); + } SASSERT(res); return res; } diff --git a/src/muz/spacer/spacer_manager.h b/src/muz/spacer/spacer_manager.h index a73a9a63b..d592a30a8 100644 --- a/src/muz/spacer/spacer_manager.h +++ b/src/muz/spacer/spacer_manager.h @@ -83,8 +83,6 @@ class manager { unsigned n_index() const { return 0; } unsigned o_index(unsigned i) const { return i + 1; } - void add_new_state(func_decl * s); - public: manager(ast_manager & manager); @@ -100,27 +98,27 @@ public: {return m_mux.is_homogenous_formula(f, n_index());} func_decl * o2n(func_decl * p, unsigned o_idx) const - {return m_mux.conv(p, o_index(o_idx), n_index());} + {return m_mux.shift_decl(p, o_index(o_idx), n_index());} func_decl * o2o(func_decl * p, unsigned src_idx, unsigned tgt_idx) const - {return m_mux.conv(p, o_index(src_idx), o_index(tgt_idx));} + {return m_mux.shift_decl(p, o_index(src_idx), o_index(tgt_idx));} func_decl * n2o(func_decl * p, unsigned o_idx) const - {return m_mux.conv(p, n_index(), o_index(o_idx));} + {return m_mux.shift_decl(p, n_index(), o_index(o_idx));} 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);} + {m_mux.shift_expr(f, o_index(o_idx), n_index(), result, homogenous);} 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);} + {m_mux.shift_expr(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), + {m_mux.shift_expr(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), + {m_mux.shift_expr(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 776776188..5dfb3a531 100644 --- a/src/muz/spacer/spacer_sym_mux.cpp +++ b/src/muz/spacer/spacer_sym_mux.cpp @@ -1,5 +1,5 @@ /*++ -Copyright (c) 2011 Microsoft Corporation +Copyright (c) 2018 Arie Gurfinkel and Microsoft Corporation Module Name: @@ -7,10 +7,12 @@ 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: + Arie Gurfinkel Krystof Hoder (t-khoder) 2011-9-8. Revision History: @@ -22,166 +24,114 @@ Revision History: #include "ast/rewriter/rewriter.h" #include "ast/rewriter/rewriter_def.h" -#include "model/model.h" - #include "muz/spacer/spacer_util.h" #include "muz/spacer/spacer_sym_mux.h" using namespace spacer; -sym_mux::sym_mux(ast_manager & m, const std::vector & suffixes) - : m(m), m_ref_holder(m), m_next_sym_suffix_idx(0), m_suffixes(suffixes) -{ - for (std::string const& s : m_suffixes) { - m_used_suffixes.insert(symbol(s.c_str())); +sym_mux::sym_mux(ast_manager & m) : m(m) {} +sym_mux::~sym_mux() { + for (auto &entry : m_entries) { + dealloc(entry.m_value); } } -std::string sym_mux::get_suffix(unsigned i) const -{ - while (m_suffixes.size() <= i) { - std::string new_suffix; - symbol new_syffix_sym; - do { - std::stringstream stm; - stm << '_' << m_next_sym_suffix_idx; - m_next_sym_suffix_idx++; - new_suffix = stm.str(); - new_syffix_sym = symbol(new_suffix.c_str()); - } while (m_used_suffixes.contains(new_syffix_sym)); - m_used_suffixes.insert(new_syffix_sym); - m_suffixes.push_back(new_suffix); - } - return m_suffixes[i]; +func_decl_ref sym_mux::mk_variant(func_decl *fdecl, unsigned i) const { + func_decl_ref v(m); + std::string name = fdecl->get_name().str(); + std::string suffix = "_"; + suffix += i == 0 ? "n" : std::to_string(i - 1); + name += suffix; + v = m.mk_func_decl(symbol(name.c_str()), fdecl->get_arity(), + fdecl->get_domain(), fdecl->get_range()); + return v; } -/** - populates a vector called tuple with func_decl's - tuple[0] is called primary and is used as key in various maps - */ -void sym_mux::create_tuple(func_decl* prefix, unsigned arity, - sort * const * domain, sort * range, - unsigned tuple_length, decl_vector & tuple) -{ - SASSERT(tuple_length > 0); - while (tuple.size() < tuple_length) { - tuple.push_back(0); - } - SASSERT(tuple.size() == tuple_length); - for (unsigned i = 0; i < tuple_length; i++) { +void sym_mux::register_decl(func_decl *fdecl) { + sym_mux_entry *entry = alloc(sym_mux_entry, m); + entry->m_main = fdecl; + entry->m_variants.push_back(mk_variant(fdecl, 0)); + entry->m_variants.push_back(mk_variant(fdecl, 1)); - if (tuple[i] != 0) { - SASSERT(tuple[i]->get_arity() == arity); - SASSERT(tuple[i]->get_range() == range); - //domain should match as well, but we won't bother - //checking an array equality - } else { - std::string name = prefix->get_name().str(); - name += get_suffix(i); - tuple[i] = m.mk_func_decl(symbol(name.c_str()), arity, - domain, range); - } - m_ref_holder.push_back(tuple[i]); - m_sym2idx.insert(tuple[i], i); - m_sym2prim.insert(tuple[i], tuple[0]); - } - - m_prim2all.insert(tuple[0], tuple); - m_prefix2prim.insert(prefix, tuple[0]); - m_prim2prefix.insert(tuple[0], prefix); - m_ref_holder.push_back(prefix); + m_entries.insert(fdecl, entry); + m_muxes.insert(entry->m_variants.get(0), std::make_pair(entry, 0)); + m_muxes.insert(entry->m_variants.get(1), std::make_pair(entry, 1)); } - -/** - extends a tuple in which prim is primary to the given size -*/ -void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) const -{ - SASSERT(m_prim2all.contains(prim)); - decl_vector& tuple = m_prim2all.find_core(prim)->get_data().m_value; - SASSERT(tuple[0] == prim); - - if (sz <= tuple.size()) { return; } - - func_decl * prefix; - TRUSTME(m_prim2prefix.find(prim, prefix)); - std::string prefix_name = prefix->get_name().bare_str(); - for (unsigned i = tuple.size(); i < sz; ++i) { - std::string name = prefix_name + get_suffix(i); - func_decl * new_sym = - m.mk_func_decl(symbol(name.c_str()), prefix->get_arity(), - prefix->get_domain(), prefix->get_range()); - - tuple.push_back(new_sym); - m_ref_holder.push_back(new_sym); - m_sym2idx.insert(new_sym, i); - m_sym2prim.insert(new_sym, prim); +void sym_mux::ensure_capacity(sym_mux_entry &entry, unsigned sz) { + while (entry.m_variants.size() < sz) { + unsigned idx = entry.m_variants.size(); + entry.m_variants.push_back (mk_variant(entry.m_main, idx)); + m_muxes.insert(entry.m_variants.back(), std::make_pair(&entry, idx)); } } -/** given a func_decl with src_idx returns its version with tgt_idx */ -func_decl * sym_mux::conv(func_decl * sym, - unsigned src_idx, unsigned tgt_idx) const { - if (src_idx == tgt_idx) { return sym; } - func_decl * prim = (src_idx == 0) ? sym : get_primary(sym); - if (tgt_idx > src_idx) { - ensure_tuple_size(prim, tgt_idx + 1); - } - decl_vector & sym_vect = m_prim2all.find_core(prim)->get_data().m_value; - SASSERT(sym_vect[src_idx] == sym); - return sym_vect[tgt_idx]; +bool sym_mux::find_idx(func_decl * sym, unsigned & idx) const { + std::pair entry; + if (m_muxes.find(sym, entry)) {idx = entry.second; return true;} + return false; } +func_decl * sym_mux::find_by_decl(func_decl* fdecl, unsigned idx) { + sym_mux_entry *entry = nullptr; + if (m_entries.find(fdecl, entry)) { + ensure_capacity(*entry, idx+1); + return entry->m_variants.get(idx); + } + return nullptr; +} -struct sym_mux::formula_checker { +func_decl * sym_mux::shift_decl(func_decl * decl, + unsigned src_idx, unsigned tgt_idx) const { + std::pair entry; + if (m_muxes.find(decl, entry)) { + SASSERT(entry.second == src_idx); + return entry.first->m_variants.get(tgt_idx); + } + UNREACHABLE(); + return nullptr; +} + +namespace { +struct formula_checker { formula_checker(const sym_mux & parent, unsigned idx) : - m_parent(parent), m_idx(idx), - m_found_what_needed(false) {} + m_parent(parent), m_idx(idx), m_found(false) {} - void operator()(expr * e) - { - if (m_found_what_needed || !is_app(e)) { return; } + void operator()(expr * e) { + if (m_found || !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_parent.find_idx(sym, sym_idx)) { return; } bool have_idx = sym_idx == m_idx; - m_found_what_needed = !have_idx; - + m_found = !have_idx; } - bool all_have_idx() const {return !m_found_what_needed;} - + bool all_have_idx() const {return !m_found;} private: const sym_mux & m_parent; unsigned m_idx; - - /** - If we check whether all muxed symbols are of given index, we look for - counter-examples, checking whether form contains a muxed symbol of an index, - we look for symbol of index m_idx. - */ - bool m_found_what_needed; + bool m_found; }; - - -bool sym_mux::is_homogenous_formula(expr * e, unsigned idx) const -{ - expr_mark visited; - formula_checker chck(*this, idx); - for_each_expr(chck, visited, e); - return chck.all_have_idx(); } -struct sym_mux::conv_rewriter_cfg : public default_rewriter_cfg { +bool sym_mux::is_homogenous_formula(expr * e, unsigned idx) const { + expr_mark visited; + formula_checker fck(*this, idx); + for_each_expr(fck, visited, e); + return fck.all_have_idx(); +} + +namespace { +struct conv_rewriter_cfg : public default_rewriter_cfg { private: ast_manager & m; const sym_mux & m_parent; unsigned m_from_idx; unsigned m_to_idx; bool m_homogenous; + expr_ref_vector m_pinned; public: conv_rewriter_cfg(const sym_mux & parent, unsigned from_idx, unsigned to_idx, bool homogenous) @@ -189,7 +139,7 @@ public: m_parent(parent), m_from_idx(from_idx), m_to_idx(to_idx), - m_homogenous(homogenous) {} + m_homogenous(homogenous), m_pinned(m) {(void) m_homogenous;} bool get_subst(expr * s, expr * & t, proof * & t_pr) { @@ -197,24 +147,23 @@ public: app * a = to_app(s); func_decl * sym = a->get_decl(); if (!m_parent.has_index(sym, m_from_idx)) { - (void) m_homogenous; SASSERT(!m_homogenous || !m_parent.is_muxed(sym)); return false; } - func_decl * tgt = m_parent.conv(sym, m_from_idx, m_to_idx); - + func_decl * tgt = m_parent.shift_decl(sym, m_from_idx, m_to_idx); t = m.mk_app(tgt, a->get_args()); + m_pinned.push_back(t); return true; } }; - -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; - } - conv_rewriter_cfg r_cfg(*this, src_idx, tgt_idx, homogenous); - rewriter_tpl rwr(m, false, r_cfg); - rwr(f, res); +} + +void sym_mux::shift_expr(expr * f, unsigned src_idx, unsigned tgt_idx, + expr_ref & res, bool homogenous) const { + if (src_idx == tgt_idx) {res = f;} + else { + conv_rewriter_cfg r_cfg(*this, src_idx, tgt_idx, homogenous); + rewriter_tpl rwr(m, false, r_cfg); + rwr(f, res); + } } diff --git a/src/muz/spacer/spacer_sym_mux.h b/src/muz/spacer/spacer_sym_mux.h index 97e3459d7..9657b47d9 100644 --- a/src/muz/spacer/spacer_sym_mux.h +++ b/src/muz/spacer/spacer_sym_mux.h @@ -1,5 +1,5 @@ /*++ -Copyright (c) 2011 Microsoft Corporation +Copyright (c) 2018 Arie Gurfinkel and Microsoft Corporation Module Name: @@ -12,6 +12,7 @@ Abstract: Author: + Arie Gurfinkel Krystof Hoder (t-khoder) 2011-9-8. Revision History: @@ -21,144 +22,69 @@ Revision History: #ifndef _SYM_MUX_H_ #define _SYM_MUX_H_ -#include #include #include "ast/ast.h" #include "util/map.h" #include "util/vector.h" -class model_core; - namespace spacer { class sym_mux { private: - typedef obj_map sym2u; - typedef obj_map sym2dv; - typedef obj_map sym2sym; - typedef obj_map sym2pred; - typedef hashtable symbols; + class sym_mux_entry { + public: + func_decl_ref m_main; + func_decl_ref_vector m_variants; + sym_mux_entry(ast_manager &m) : m_main(m), m_variants(m) {}; + }; - ast_manager & m; - mutable ast_ref_vector m_ref_holder; + typedef obj_map decl2entry_map; + typedef obj_map > mux2entry_map; - mutable unsigned m_next_sym_suffix_idx; - mutable symbols m_used_suffixes; - /** Here we have default suffixes for each of the variants */ - mutable std::vector m_suffixes; + ast_manager &m; + decl2entry_map m_entries; + mux2entry_map m_muxes; + func_decl_ref mk_variant(func_decl *fdecl, unsigned i) const; + void ensure_capacity(sym_mux_entry &entry, unsigned sz) ; - /** - Primary symbol is the 0-th variant. This member maps from primary symbol - to vector of all its variants (including the primary variant). - */ - sym2dv m_prim2all; - - /** - For each symbol contains its variant index - */ - mutable sym2u m_sym2idx; - /** - For each symbol contains its primary variant - */ - mutable sym2sym m_sym2prim; - - /** - Maps prefixes passed to the create_tuple to - the primary symbol created from it. - */ - sym2pred m_prefix2prim; - - /** - Maps pripary symbols to prefixes that were used to create them. - */ - sym2sym m_prim2prefix; - - - - struct formula_checker; - struct conv_rewriter_cfg; - - 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; public: - sym_mux(ast_manager & m, const std::vector & suffixes); - + sym_mux(ast_manager & m); + ~sym_mux(); ast_manager & get_manager() const { return m; } - 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);} - + void register_decl(func_decl *fdecl); + bool find_idx(func_decl * sym, unsigned & idx) const; bool has_index(func_decl * sym, unsigned idx) const - { - unsigned actual_idx; - return try_get_index(sym, actual_idx) && idx == actual_idx; - } + {unsigned v; return find_idx(sym, v) && idx == v;} - /** Return primary symbol. sym must be muxed. */ - func_decl * get_primary(func_decl * sym) const - { - func_decl * prim; - TRUSTME(m_sym2prim.find(sym, prim)); - return prim; - } /** - Return primary symbol created from prefix, or 0 if the prefix was never used. + \brief Return symbol created from prefix, or 0 if the prefix + was never used. */ - func_decl * try_get_primary_by_prefix(func_decl* prefix) const - { - func_decl * res; - if(!m_prefix2prim.find(prefix, res)) { - return nullptr; - } - return res; - } + func_decl * find_by_decl(func_decl* fdecl, unsigned idx); /** - Return symbol created from prefix, or 0 if the prefix was never used. - */ - func_decl * try_get_by_prefix(func_decl* prefix, unsigned idx) const - { - func_decl * prim = try_get_primary_by_prefix(prefix); - if(!prim) { - return nullptr; - } - return conv(prim, 0, idx); - } - - /** - Create a multiplexed tuple of propositional constants. - Symbols may be suplied in the tuple vector, - those beyond the size of the array and those with corresponding positions - assigned to zero will be created using prefix. - Tuple length must be at least one. - */ - void create_tuple(func_decl* prefix, unsigned arity, sort * const * domain, sort * range, - unsigned tuple_length, decl_vector & tuple); - - /** - Return true if the only multiplexed symbols which e contains are of index idx. + \brief Return true if the only multiplexed symbols which e contains are + of index idx. */ bool is_homogenous_formula(expr * e, unsigned idx) const; /** - Convert symbol sym which has to be of src_idx variant into variant tgt_idx. + \brief Convert symbol sym which has to be of src_idx variant + into variant tgt_idx. */ - func_decl * conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx) const; - + func_decl * shift_decl(func_decl * sym, unsigned src_idx, unsigned tgt_idx) const; /** - Convert src_idx symbols in formula f variant into tgt_idx. - If homogenous is true, formula cannot contain symbols of other variants. + \brief 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 shift_expr(expr * f, unsigned src_idx, unsigned tgt_idx, + expr_ref & res, bool homogenous = true) const; };