From 51ed13f96ad17e9aba9f06f0029b37cb6a41bd83 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Jun 2022 06:28:24 -0700 Subject: [PATCH] update topological sort to use arrays instead of hash tables, expose Context over Z3Object for programmability Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Z3Object.cs | 2 +- src/ast/ast.cpp | 8 +-- src/ast/ast.h | 7 ++- src/ast/euf/euf_egraph.cpp | 6 +- src/ast/euf/euf_enode.h | 4 +- src/ast/static_features.h | 2 +- src/ast/substitution/substitution_tree.cpp | 35 ++++------- src/model/model.cpp | 2 +- src/qe/mbp/mbp_term_graph.cpp | 4 +- src/sat/smt/array_model.cpp | 2 +- src/sat/smt/euf_proof.cpp | 2 +- src/sat/smt/q_mam.cpp | 20 +++--- src/smt/mam.cpp | 20 +++--- src/smt/smt_context.h | 8 +-- src/smt/smt_enode.h | 2 +- src/smt/smt_internalizer.cpp | 4 +- src/util/top_sort.h | 71 +++++++++++++--------- 17 files changed, 103 insertions(+), 96 deletions(-) diff --git a/src/api/dotnet/Z3Object.cs b/src/api/dotnet/Z3Object.cs index d25dfc25a..d385d9d62 100644 --- a/src/api/dotnet/Z3Object.cs +++ b/src/api/dotnet/Z3Object.cs @@ -113,7 +113,7 @@ namespace Microsoft.Z3 return s.NativeObject; } - internal Context Context + public Context Context { get { diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 9112d6dae..56a98b051 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -498,9 +498,9 @@ bool compare_nodes(ast const * n1, ast const * n2) { template inline unsigned ast_array_hash(T * const * array, unsigned size, unsigned init_value) { - if (size == 0) - return init_value; switch (size) { + case 0: + return init_value; case 1: return combine_hash(array[0]->hash(), init_value); case 2: @@ -993,7 +993,7 @@ sort * basic_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete } func_decl * basic_decl_plugin::mk_eq_decl_core(char const * name, decl_kind k, sort * s, ptr_vector & cache) { - unsigned id = s->get_decl_id(); + unsigned id = s->get_small_id(); force_ptr_array_size(cache, id + 1); if (cache[id] == 0) { sort * domain[2] = { s, s}; @@ -1009,7 +1009,7 @@ func_decl * basic_decl_plugin::mk_eq_decl_core(char const * name, decl_kind k, s } func_decl * basic_decl_plugin::mk_ite_decl(sort * s) { - unsigned id = s->get_decl_id(); + unsigned id = s->get_small_id(); force_ptr_array_size(m_ite_decls, id + 1); if (m_ite_decls[id] == 0) { sort * domain[3] = { m_bool_sort, s, s}; diff --git a/src/ast/ast.h b/src/ast/ast.h index 79a3cebc7..fe7586afa 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -572,7 +572,7 @@ protected: decl(ast_kind k, symbol const & name, decl_info * info):ast(k), m_name(name), m_info(info) {} public: - unsigned get_decl_id() const { SASSERT(get_id() >= c_first_decl_id); return get_id() - c_first_decl_id; } + unsigned get_small_id() const { SASSERT(get_id() >= c_first_decl_id); return get_id() - c_first_decl_id; } symbol const & get_name() const { return m_name; } decl_info * get_info() const { return m_info; } family_id get_family_id() const { return m_info == nullptr ? null_family_id : m_info->get_family_id(); } @@ -671,6 +671,9 @@ protected: public: sort* get_sort() const; + + unsigned get_small_id() const { return get_id(); } + }; // ----------------------------------- @@ -2573,7 +2576,7 @@ typedef ast_ref_fast_mark2 expr_ref_fast_mark2; when N is deleted. */ class ast_mark { - struct decl2uint { unsigned operator()(decl const & d) const { return d.get_decl_id(); } }; + struct decl2uint { unsigned operator()(decl const & d) const { return d.get_small_id(); } }; obj_mark m_expr_marks; obj_mark m_decl_marks; public: diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 5d0bd4b17..3820d2592 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -30,7 +30,7 @@ namespace euf { m_nodes.push_back(n); m_exprs.push_back(f); if (is_app(f) && num_args > 0) { - unsigned id = to_app(f)->get_decl()->get_decl_id(); + unsigned id = to_app(f)->get_decl()->get_small_id(); m_decl2enodes.reserve(id+1); m_decl2enodes[id].push_back(n); } @@ -60,7 +60,7 @@ namespace euf { enode_vector const& egraph::enodes_of(func_decl* f) { - unsigned id = f->get_decl_id(); + unsigned id = f->get_small_id(); if (id < m_decl2enodes.size()) return m_decl2enodes[id]; return m_empty_enodes; @@ -341,7 +341,7 @@ namespace euf { m_expr2enode[e->get_id()] = nullptr; n->~enode(); if (is_app(e) && n->num_args() > 0) - m_decl2enodes[to_app(e)->get_decl()->get_decl_id()].pop_back(); + m_decl2enodes[to_app(e)->get_decl()->get_small_id()].pop_back(); m_nodes.pop_back(); m_exprs.pop_back(); }; diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h index 7014223be..18a1a86af 100644 --- a/src/ast/euf/euf_enode.h +++ b/src/ast/euf/euf_enode.h @@ -162,7 +162,7 @@ namespace euf { bool merge_tf() const { return merge_enabled() && (class_size() > 1 || num_parents() > 0 || num_args() > 0); } enode* get_arg(unsigned i) const { SASSERT(i < num_args()); return m_args[i]; } - unsigned hash() const { return m_expr->hash(); } + unsigned hash() const { return m_expr->get_id(); } unsigned get_table_id() const { return m_table_id; } void set_table_id(unsigned t) { m_table_id = t; } @@ -204,6 +204,8 @@ namespace euf { app* get_app() const { return to_app(m_expr); } func_decl* get_decl() const { return is_app(m_expr) ? to_app(m_expr)->get_decl() : nullptr; } unsigned get_expr_id() const { return m_expr->get_id(); } + unsigned get_id() const { return m_expr->get_id(); } + unsigned get_small_id() const { return m_expr->get_small_id(); } unsigned get_root_id() const { return m_root->m_expr->get_id(); } bool children_are_roots() const; enode* get_next() const { return m_next; } diff --git a/src/ast/static_features.h b/src/ast/static_features.h index 40532f939..88e7934d4 100644 --- a/src/ast/static_features.h +++ b/src/ast/static_features.h @@ -162,7 +162,7 @@ struct static_features { bool arith_k_sum_is_small() const { return m_arith_k_sum < rational(INT_MAX / 8); } - void inc_num_apps(func_decl const * d) { unsigned id = d->get_decl_id(); m_num_apps.reserve(id+1, 0); m_num_apps[id]++; } + void inc_num_apps(func_decl const * d) { unsigned id = d->get_small_id(); m_num_apps.reserve(id+1, 0); m_num_apps[id]++; } void inc_theory_terms(family_id fid) { m_num_theory_terms.reserve(fid+1, 0); m_num_theory_terms[fid]++; } void inc_theory_atoms(family_id fid) { m_num_theory_atoms.reserve(fid+1, 0); m_num_theory_atoms[fid]++; } void inc_theory_constants(family_id fid) { m_num_theory_constants.reserve(fid+1, 0); m_num_theory_constants[fid]++; } diff --git a/src/ast/substitution/substitution_tree.cpp b/src/ast/substitution/substitution_tree.cpp index c0c3e5205..af2ca1039 100644 --- a/src/ast/substitution/substitution_tree.cpp +++ b/src/ast/substitution/substitution_tree.cpp @@ -137,10 +137,7 @@ void substitution_tree::reset_registers(unsigned old_size) { unsigned substitution_tree::get_compatibility_measure(svector const & sv) { unsigned old_size = m_todo.size(); unsigned measure = 0; - svector::const_iterator it = sv.begin(); - svector::const_iterator end = sv.end(); - for (; it != end; ++it) { - subst const & s = *it; + for (subst const& s : sv) { unsigned ireg = s.first->get_idx(); expr * out = s.second; expr * in = get_reg_value(ireg); @@ -254,7 +251,7 @@ void substitution_tree::insert(expr * new_expr) { else { SASSERT(is_var(new_expr)); sort * s = to_var(new_expr)->get_sort(); - unsigned id = s->get_decl_id(); + unsigned id = s->get_small_id(); if (id >= m_vars.size()) m_vars.resize(id+1); if (m_vars[id] == 0) @@ -274,7 +271,7 @@ void substitution_tree::insert(app * new_expr) { m_todo.push_back(0); func_decl * d = new_expr->get_decl(); - unsigned id = d->get_decl_id(); + unsigned id = d->get_small_id(); if (id >= m_roots.size()) m_roots.resize(id+1); @@ -439,7 +436,7 @@ void substitution_tree::erase(expr * e) { else { SASSERT(is_var(e)); sort * s = to_var(e)->get_sort(); - unsigned id = s->get_decl_id(); + unsigned id = s->get_small_id(); if (id >= m_vars.size() || m_vars[id] == 0) return; var_ref_vector * v = m_vars[id]; @@ -453,7 +450,7 @@ void substitution_tree::erase(expr * e) { */ void substitution_tree::erase(app * e) { func_decl * d = e->get_decl(); - unsigned id = d->get_decl_id(); + unsigned id = d->get_small_id(); if (id >= m_roots.size() || !m_roots[id]) return; @@ -732,7 +729,7 @@ bool substitution_tree::visit_vars(expr * e, st_visitor & st) { if (m_vars.empty()) return true; // continue sort * s = e->get_sort(); - unsigned s_id = s->get_decl_id(); + unsigned s_id = s->get_small_id(); if (s_id < m_vars.size()) { var_ref_vector * v = m_vars[s_id]; if (v && !v->empty()) { @@ -832,17 +829,14 @@ void substitution_tree::visit(expr * e, st_visitor & st, unsigned in_offset, uns if (visit_vars(e, st)) { if (is_app(e)) { func_decl * d = to_app(e)->get_decl(); - unsigned id = d->get_decl_id(); + unsigned id = d->get_small_id(); node * r = m_roots.get(id, 0); if (r) visit(e, st, r); } else { SASSERT(is_var(e)); - ptr_vector::iterator it = m_roots.begin(); - ptr_vector::iterator end = m_roots.end(); - for (; it != end; ++it) { - node * r = *it; + for (node* r : m_roots) { if (r != nullptr) { var * v = r->m_subst[0].first; if (v->get_sort() == to_var(e)->get_sort()) @@ -868,16 +862,11 @@ void substitution_tree::gen(expr * e, st_visitor & v, unsigned in_offset, unsign void substitution_tree::display(std::ostream & out) const { out << "substitution tree:\n"; - ptr_vector::const_iterator it = m_roots.begin(); - ptr_vector::const_iterator end = m_roots.end(); - for (; it != end; ++it) - if (*it) - display(out, *it, 0); + for (node* n : m_roots) + if (n) + display(out, n, 0); bool found_var = false; - ptr_vector::const_iterator it2 = m_vars.begin(); - ptr_vector::const_iterator end2 = m_vars.end(); - for (; it2 != end2; ++it2) { - var_ref_vector * v = *it2; + for (var_ref_vector* v : m_vars) { if (v == nullptr) continue; // m_vars may contain null pointers. See substitution_tree::insert. unsigned num = v->size(); diff --git a/src/model/model.cpp b/src/model/model.cpp index 21938766b..dfa76db68 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -476,7 +476,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition, // noop } else if (f->is_skolem() && can_inline_def(ts, f, force_inline) && (fi = get_func_interp(f)) && - fi->get_interp() && (!ts.partition_ids().find(f, pid) || pid != current_partition)) { + fi->get_interp() && (!ts.find(f, pid) || pid != current_partition)) { var_subst vs(m, false); new_t = vs(fi->get_interp(), args.size(), args.data()); } diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp index 52d633417..76b6a2b31 100644 --- a/src/qe/mbp/mbp_term_graph.cpp +++ b/src/qe/mbp/mbp_term_graph.cpp @@ -755,7 +755,7 @@ namespace mbp { app* a = to_app(e); func_decl* d = a->get_decl(); if (d->get_arity() == 0) continue; - unsigned id = d->get_decl_id(); + unsigned id = d->get_small_id(); m_decl2terms.reserve(id+1); if (m_decl2terms[id].empty()) m_decls.push_back(d); m_decl2terms[id].push_back(t); @@ -770,7 +770,7 @@ namespace mbp { // are distinct. // for (func_decl* d : m_decls) { - unsigned id = d->get_decl_id(); + unsigned id = d->get_small_id(); ptr_vector const& terms = m_decl2terms[id]; if (terms.size() <= 1) continue; unsigned arity = d->get_arity(); diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp index c437629f5..8b56ff3ae 100644 --- a/src/sat/smt/array_model.cpp +++ b/src/sat/smt/array_model.cpp @@ -54,7 +54,7 @@ namespace array { euf::enode* d = get_default(v); if (d) dep.add(n, d); - if (!dep.deps().contains(n)) + if (!dep.contains_dep(n)) dep.insert(n, nullptr); return true; } diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 8e5eb9dd7..c072022df 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -104,7 +104,7 @@ namespace euf { std::ostringstream strm; smt2_pp_environment_dbg env(m); ast_smt2_pp(strm, f, env); - get_drat().def_begin('f', f->get_decl_id(), strm.str()); + get_drat().def_begin('f', f->get_small_id(), strm.str()); get_drat().def_end(); } diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index d860b3c3c..4be554633 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -104,7 +104,7 @@ namespace q { public: unsigned char operator()(func_decl * lbl) { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); if (lbl_id >= m_lbl2hash.size()) m_lbl2hash.resize(lbl_id + 1, -1); if (m_lbl2hash[lbl_id] == -1) { @@ -2868,7 +2868,7 @@ namespace q { SASSERT(first_idx < mp->get_num_args()); app * p = to_app(mp->get_arg(first_idx)); func_decl * lbl = p->get_decl(); - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); m_trees.reserve(lbl_id+1, nullptr); if (m_trees[lbl_id] == nullptr) { m_trees[lbl_id] = m_compiler.mk_tree(qa, mp, first_idx, false); @@ -2898,7 +2898,7 @@ namespace q { } code_tree * get_code_tree_for(func_decl * lbl) const { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); if (lbl_id < m_trees.size()) return m_trees[lbl_id]; else @@ -3112,11 +3112,11 @@ namespace q { } bool is_plbl(func_decl * lbl) const { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); return lbl_id < m_is_plbl.size() && m_is_plbl[lbl_id]; } bool is_clbl(func_decl * lbl) const { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); return lbl_id < m_is_clbl.size() && m_is_clbl[lbl_id]; } @@ -3129,7 +3129,7 @@ namespace q { } void update_clbls(func_decl * lbl) { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); m_is_clbl.reserve(lbl_id+1, false); TRACE("trigger_bug", tout << "update_clbls: " << lbl->get_name() << " is already clbl: " << m_is_clbl[lbl_id] << "\n";); TRACE("mam_bug", tout << "update_clbls: " << lbl->get_name() << " is already clbl: " << m_is_clbl[lbl_id] << "\n";); @@ -3169,7 +3169,7 @@ namespace q { } void update_plbls(func_decl * lbl) { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); m_is_plbl.reserve(lbl_id+1, false); TRACE("trigger_bug", tout << "update_plbls: " << lbl->get_name() << " is already plbl: " << m_is_plbl[lbl_id] << ", lbl_id: " << lbl_id << "\n"; tout << "mam: " << this << "\n";); @@ -3698,7 +3698,7 @@ namespace q { app * p = to_app(mp->get_arg(0)); func_decl * lbl = p->get_decl(); if (!m_egraph.enodes_of(lbl).empty()) { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); m_tmp_trees.reserve(lbl_id+1, 0); if (m_tmp_trees[lbl_id] == 0) { m_tmp_trees[lbl_id] = m_compiler.mk_tree(qa, mp, 0, false); @@ -3711,7 +3711,7 @@ namespace q { } for (func_decl * lbl : m_tmp_trees_to_delete) { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); code_tree * tmp_tree = m_tmp_trees[lbl_id]; SASSERT(tmp_tree != 0); SASSERT(!m_egraph.enodes_of(lbl).empty()); @@ -3843,7 +3843,7 @@ namespace q { unsigned h = m_lbl_hasher(lbl); TRACE("trigger_bug", tout << "lbl: " << lbl->get_name() << " is_clbl(lbl): " << is_clbl(lbl) << ", is_plbl(lbl): " << is_plbl(lbl) << ", h: " << h << "\n"; - tout << "lbl_id: " << lbl->get_decl_id() << "\n";); + tout << "lbl_id: " << lbl->get_small_id() << "\n";); if (is_clbl(lbl)) update_lbls(n, h); if (is_plbl(lbl)) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 3d880aa80..ea335b1dc 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -78,7 +78,7 @@ namespace { public: unsigned char operator()(func_decl * lbl) { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); if (lbl_id >= m_lbl2hash.size()) m_lbl2hash.resize(lbl_id + 1, -1); if (m_lbl2hash[lbl_id] == -1) { @@ -2906,7 +2906,7 @@ namespace { SASSERT(first_idx < mp->get_num_args()); app * p = to_app(mp->get_arg(first_idx)); func_decl * lbl = p->get_decl(); - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); m_trees.reserve(lbl_id+1, nullptr); if (m_trees[lbl_id] == nullptr) { m_trees[lbl_id] = m_compiler.mk_tree(qa, mp, first_idx, false); @@ -2935,7 +2935,7 @@ namespace { } code_tree * get_code_tree_for(func_decl * lbl) const { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); if (lbl_id < m_trees.size()) return m_trees[lbl_id]; else @@ -3165,11 +3165,11 @@ namespace { } bool is_plbl(func_decl * lbl) const { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); return lbl_id < m_is_plbl.size() && m_is_plbl[lbl_id]; } bool is_clbl(func_decl * lbl) const { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); return lbl_id < m_is_clbl.size() && m_is_clbl[lbl_id]; } @@ -3182,7 +3182,7 @@ namespace { } void update_clbls(func_decl * lbl) { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); m_is_clbl.reserve(lbl_id+1, false); TRACE("trigger_bug", tout << "update_clbls: " << lbl->get_name() << " is already clbl: " << m_is_clbl[lbl_id] << "\n";); TRACE("mam_bug", tout << "update_clbls: " << lbl->get_name() << " is already clbl: " << m_is_clbl[lbl_id] << "\n";); @@ -3222,7 +3222,7 @@ namespace { } void update_plbls(func_decl * lbl) { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); m_is_plbl.reserve(lbl_id+1, false); TRACE("trigger_bug", tout << "update_plbls: " << lbl->get_name() << " is already plbl: " << m_is_plbl[lbl_id] << ", lbl_id: " << lbl_id << "\n"; tout << "mam: " << this << "\n";); @@ -3744,7 +3744,7 @@ namespace { app * p = to_app(mp->get_arg(0)); func_decl * lbl = p->get_decl(); if (m_context.get_num_enodes_of(lbl) > 0) { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); m_tmp_trees.reserve(lbl_id+1, 0); if (m_tmp_trees[lbl_id] == 0) { m_tmp_trees[lbl_id] = m_compiler.mk_tree(qa, mp, 0, false); @@ -3757,7 +3757,7 @@ namespace { } for (func_decl * lbl : m_tmp_trees_to_delete) { - unsigned lbl_id = lbl->get_decl_id(); + unsigned lbl_id = lbl->get_small_id(); code_tree * tmp_tree = m_tmp_trees[lbl_id]; SASSERT(tmp_tree != 0); SASSERT(m_context.get_num_enodes_of(lbl) > 0); @@ -3963,7 +3963,7 @@ namespace { unsigned h = m_lbl_hasher(lbl); TRACE("trigger_bug", tout << "lbl: " << lbl->get_name() << " is_clbl(lbl): " << is_clbl(lbl) << ", is_plbl(lbl): " << is_plbl(lbl) << ", h: " << h << "\n"; - tout << "lbl_id: " << lbl->get_decl_id() << "\n";); + tout << "lbl_id: " << lbl->get_small_id() << "\n";); if (is_clbl(lbl)) update_lbls(n, h); if (is_plbl(lbl)) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 696a5cc39..7c4989aca 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -531,22 +531,22 @@ namespace smt { } unsigned get_num_enodes_of(func_decl const * decl) const { - unsigned id = decl->get_decl_id(); + unsigned id = decl->get_small_id(); return id < m_decl2enodes.size() ? m_decl2enodes[id].size() : 0; } enode_vector const& enodes_of(func_decl const * d) const { - unsigned id = d->get_decl_id(); + unsigned id = d->get_small_id(); return id < m_decl2enodes.size() ? m_decl2enodes[id] : m_empty_vector; } enode_vector::const_iterator begin_enodes_of(func_decl const * decl) const { - unsigned id = decl->get_decl_id(); + unsigned id = decl->get_small_id(); return id < m_decl2enodes.size() ? m_decl2enodes[id].begin() : nullptr; } enode_vector::const_iterator end_enodes_of(func_decl const * decl) const { - unsigned id = decl->get_decl_id(); + unsigned id = decl->get_small_id(); return id < m_decl2enodes.size() ? m_decl2enodes[id].end() : nullptr; } diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 8995f7fba..196d28396 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -171,7 +171,7 @@ namespace smt { unsigned get_expr_id() const { return m_owner->get_id(); } func_decl * get_decl() const { return m_owner->get_decl(); } - unsigned get_decl_id() const { return m_owner->get_decl()->get_decl_id(); } + unsigned get_decl_id() const { return m_owner->get_decl()->get_small_id(); } sort* get_sort() const { return m_owner->get_sort(); } diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index eee811e62..2c1abec8a 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1010,7 +1010,7 @@ namespace smt { } } if (!e->is_eq()) { - unsigned decl_id = n->get_decl()->get_decl_id(); + unsigned decl_id = n->get_decl()->get_small_id(); if (decl_id >= m_decl2enodes.size()) m_decl2enodes.resize(decl_id+1); m_decl2enodes[decl_id].push_back(e); @@ -1054,7 +1054,7 @@ namespace smt { m_cg_table.erase(e); } if (e->get_num_args() > 0 && !e->is_eq()) { - unsigned decl_id = to_app(n)->get_decl()->get_decl_id(); + unsigned decl_id = to_app(n)->get_decl()->get_small_id(); SASSERT(decl_id < m_decl2enodes.size()); SASSERT(m_decl2enodes[decl_id].back() == e); m_decl2enodes[decl_id].pop_back(); diff --git a/src/util/top_sort.h b/src/util/top_sort.h index 8f9df7d52..46fe45446 100644 --- a/src/util/top_sort.h +++ b/src/util/top_sort.h @@ -24,39 +24,51 @@ Revision History: #include "util/obj_hashtable.h" #include "util/vector.h" #include "util/memory_manager.h" +#include "util/tptr.h" template class top_sort { typedef obj_hashtable T_set; - obj_map m_partition_id; - obj_map m_dfs_num; + unsigned_vector m_partition_id; + unsigned_vector m_dfs_num; ptr_vector m_top_sorted; ptr_vector m_stack_S; ptr_vector m_stack_P; unsigned m_next_preorder; - obj_map m_deps; + ptr_vector m_deps; + ptr_vector m_dep_keys; + + static T_set* add_tag(T_set* t) { return TAG(T_set*, t, 1); } + static T_set* del_tag(T_set* t) { return UNTAG(T_set*, t); } + T_set* get_dep(T* t) const { return del_tag(m_deps.get(t->get_small_id())); } + + + bool contains_partition(T* f) const { + return m_partition_id.get(f->get_small_id()) != UINT_MAX; + } + void traverse(T* f) { - unsigned p_id = 0; - if (m_dfs_num.find(f, p_id)) { - if (!m_partition_id.contains(f)) { - while (!m_stack_P.empty() && m_partition_id.contains(m_stack_P.back()) && m_partition_id[m_stack_P.back()] > p_id) { + unsigned p_id = m_dfs_num.get(f->get_small_id(), UINT_MAX); + if (p_id != UINT_MAX) { + if (!contains_partition(f)) { + while (!m_stack_P.empty() && contains_partition(m_stack_P.back()) && partition_id(m_stack_P.back()) > p_id) { m_stack_P.pop_back(); } } } - else if (!m_deps.contains(f)) { + else if (!contains_dep(f)) return; - } else { - m_dfs_num.insert(f, m_next_preorder++); + m_dfs_num.setx(f->get_small_id(), m_next_preorder, UINT_MAX); + ++m_next_preorder; m_stack_S.push_back(f); m_stack_P.push_back(f); - if (m_deps[f]) { - for (T* g : *m_deps[f]) { + T_set* ts = get_dep(f); + if (ts) { + for (T* g : *ts) traverse(g); - } } if (f == m_stack_P.back()) { p_id = m_top_sorted.size(); @@ -65,7 +77,7 @@ class top_sort { s_f = m_stack_S.back(); m_stack_S.pop_back(); m_top_sorted.push_back(s_f); - m_partition_id.insert(s_f, p_id); + m_partition_id.setx(s_f->get_small_id(), p_id, UINT_MAX); } while (s_f != f); m_stack_P.pop_back(); @@ -76,28 +88,29 @@ class top_sort { public: virtual ~top_sort() { - for (auto & kv : m_deps) dealloc(kv.m_value); + for (auto * t : m_dep_keys) + dealloc(get_dep(t)); } void topological_sort() { m_next_preorder = 0; m_partition_id.reset(); m_top_sorted.reset(); - for (auto & kv : m_deps) { - traverse(kv.m_key); - } + for (auto * t : m_dep_keys) + traverse(t); SASSERT(m_stack_S.empty()); SASSERT(m_stack_P.empty()); m_dfs_num.reset(); } - void insert(T* t, T_set* s) { - m_deps.insert(t, s); + void insert(T* t, T_set* s) { + m_deps.setx(t->get_small_id(), add_tag(s), nullptr); + m_dep_keys.push_back(t); } void add(T* t, T* s) { - T_set* tb = nullptr; - if (!m_deps.find(t, tb) || !tb) { + T_set* tb = get_dep(t); + if (!tb) { tb = alloc(T_set); insert(t, tb); } @@ -106,18 +119,18 @@ public: ptr_vector const& top_sorted() const { return m_top_sorted; } - obj_map const& partition_ids() const { return m_partition_id; } + unsigned partition_id(T* t) const { return m_partition_id[t->get_small_id()]; } - unsigned partition_id(T* t) const { return m_partition_id[t]; } + bool find(T* t, unsigned& p) const { p = m_partition_id.get(t->get_small_id(), UINT_MAX); return p != UINT_MAX; } + + bool contains_dep(T* t) const { return m_deps.get(t->get_small_id(), nullptr) != nullptr; } bool is_singleton_partition(T* f) const { - unsigned pid = m_partition_id[f]; + unsigned pid = m_partition_id(f); return f == m_top_sorted[pid] && - (pid == 0 || m_partition_id[m_top_sorted[pid-1]] != pid) && - (pid + 1 == m_top_sorted.size() || m_partition_id[m_top_sorted[pid+1]] != pid); + (pid == 0 || partition_id(m_top_sorted[pid-1]) != pid) && + (pid + 1 == m_top_sorted.size() || partition_id(m_top_sorted[pid+1]) != pid); } - obj_map const& deps() const { return m_deps; } - };