mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-06 15:25:46 +00:00
Code Activity

Bug fix to spacer::sym_mux

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-03 16:32:06 -07:00
parent 38c2b56f0e
commit dd064bd8f9
2 changed files with 8 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/muz/spacer/spacer_sym_mux.cpp
View file

@ -57,7 +57,7 @@ void sym_mux::register_decl(func_decl *fdecl) {
m_muxes.insert(entry->m_variants.get(0), std::make_pair(entry, 0)); 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)); m_muxes.insert(entry->m_variants.get(1), std::make_pair(entry, 1));
} }
void sym_mux::ensure_capacity(sym_mux_entry &entry, unsigned sz) { void sym_mux::ensure_capacity(sym_mux_entry &entry, unsigned sz) const {
while (entry.m_variants.size() < sz) { while (entry.m_variants.size() < sz) {
unsigned idx = entry.m_variants.size(); unsigned idx = entry.m_variants.size();
entry.m_variants.push_back (mk_variant(entry.m_main, idx)); entry.m_variants.push_back (mk_variant(entry.m_main, idx));
@ -71,7 +71,7 @@ bool sym_mux::find_idx(func_decl * sym, unsigned & idx) const {
return false; return false;
} }
func_decl * sym_mux::find_by_decl(func_decl* fdecl, unsigned idx) { func_decl * sym_mux::find_by_decl(func_decl* fdecl, unsigned idx) const {
sym_mux_entry *entry = nullptr; sym_mux_entry *entry = nullptr;
if (m_entries.find(fdecl, entry)) { if (m_entries.find(fdecl, entry)) {
ensure_capacity(*entry, idx+1); ensure_capacity(*entry, idx+1);
@ -85,6 +85,7 @@ func_decl * sym_mux::shift_decl(func_decl * decl,
std::pair<sym_mux_entry*,unsigned> entry; std::pair<sym_mux_entry*,unsigned> entry;
if (m_muxes.find(decl, entry)) { if (m_muxes.find(decl, entry)) {
SASSERT(entry.second == src_idx); SASSERT(entry.second == src_idx);
ensure_capacity(*entry.first, tgt_idx + 1);
return entry.first->m_variants.get(tgt_idx); return entry.first->m_variants.get(tgt_idx);
} }
UNREACHABLE(); UNREACHABLE();

9
src/muz/spacer/spacer_sym_mux.h
View file

@ -42,11 +42,11 @@ private:
typedef obj_map<func_decl, std::pair<sym_mux_entry*, unsigned> > mux2entry_map; typedef obj_map<func_decl, std::pair<sym_mux_entry*, unsigned> > mux2entry_map;
ast_manager &m; ast_manager &m;
decl2entry_map m_entries; mutable decl2entry_map m_entries;
mux2entry_map m_muxes; mutable mux2entry_map m_muxes;
func_decl_ref mk_variant(func_decl *fdecl, unsigned i) const; func_decl_ref mk_variant(func_decl *fdecl, unsigned i) const;
void ensure_capacity(sym_mux_entry &entry, unsigned sz) ; void ensure_capacity(sym_mux_entry &entry, unsigned sz) const;
public: public:
sym_mux(ast_manager & m); sym_mux(ast_manager & m);
@ -58,12 +58,13 @@ public:
bool has_index(func_decl * sym, unsigned idx) const bool has_index(func_decl * sym, unsigned idx) const
{unsigned v; return find_idx(sym, v) && idx == v;} {unsigned v; return find_idx(sym, v) && idx == v;}
bool is_muxed(func_decl *fdecl) const {return m_muxes.contains(fdecl);}
/** /**
\brief Return symbol created from prefix, or 0 if the prefix \brief Return symbol created from prefix, or 0 if the prefix
was never used. was never used.
*/ */
func_decl * find_by_decl(func_decl* fdecl, unsigned idx); func_decl * find_by_decl(func_decl* fdecl, unsigned idx) const;
/** /**
\brief Return true if the only multiplexed symbols which e contains are \brief Return true if the only multiplexed symbols which e contains are