mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

update topological sort to use arrays instead of hash tables, expose Context over Z3Object for programmability

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-06-08 06:28:24 -07:00
parent 0e6c64510a
commit 51ed13f96a
17 changed files with 103 additions and 96 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/dotnet/Z3Object.cs
View file

@ -113,7 +113,7 @@ namespace Microsoft.Z3
return s.NativeObject; return s.NativeObject;
} }
internal Context Context public Context Context
{ {
get get
{ {

8
src/ast/ast.cpp
View file

@ -498,9 +498,9 @@ bool compare_nodes(ast const * n1, ast const * n2) {
template<typename T> template<typename T>
inline unsigned ast_array_hash(T * const * array, unsigned size, unsigned init_value) { inline unsigned ast_array_hash(T * const * array, unsigned size, unsigned init_value) {
if (size == 0)
return init_value;
switch (size) { switch (size) {
case 0:
return init_value;
case 1: case 1:
return combine_hash(array[0]->hash(), init_value); return combine_hash(array[0]->hash(), init_value);
case 2: 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<func_decl> & cache) { func_decl * basic_decl_plugin::mk_eq_decl_core(char const * name, decl_kind k, sort * s, ptr_vector<func_decl> & cache) {
unsigned id = s->get_decl_id(); unsigned id = s->get_small_id();
force_ptr_array_size(cache, id + 1); force_ptr_array_size(cache, id + 1);
if (cache[id] == 0) { if (cache[id] == 0) {
sort * domain[2] = { s, s}; 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) { 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); force_ptr_array_size(m_ite_decls, id + 1);
if (m_ite_decls[id] == 0) { if (m_ite_decls[id] == 0) {
sort * domain[3] = { m_bool_sort, s, s}; sort * domain[3] = { m_bool_sort, s, s};

7
src/ast/ast.h
View file

@ -572,7 +572,7 @@ protected:
decl(ast_kind k, symbol const & name, decl_info * info):ast(k), m_name(name), m_info(info) {} decl(ast_kind k, symbol const & name, decl_info * info):ast(k), m_name(name), m_info(info) {}
public: 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; } symbol const & get_name() const { return m_name; }
decl_info * get_info() const { return m_info; } 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(); } family_id get_family_id() const { return m_info == nullptr ? null_family_id : m_info->get_family_id(); }
@ -671,6 +671,9 @@ protected:
public: public:
sort* get_sort() const; 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. when N is deleted.
*/ */
class ast_mark { 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<expr> m_expr_marks; obj_mark<expr> m_expr_marks;
obj_mark<decl, bit_vector, decl2uint> m_decl_marks; obj_mark<decl, bit_vector, decl2uint> m_decl_marks;
public: public:

6
src/ast/euf/euf_egraph.cpp
View file

@ -30,7 +30,7 @@ namespace euf {
m_nodes.push_back(n); m_nodes.push_back(n);
m_exprs.push_back(f); m_exprs.push_back(f);
if (is_app(f) && num_args > 0) { 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.reserve(id+1);
m_decl2enodes[id].push_back(n); m_decl2enodes[id].push_back(n);
} }
@ -60,7 +60,7 @@ namespace euf {
enode_vector const& egraph::enodes_of(func_decl* f) { 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()) if (id < m_decl2enodes.size())
return m_decl2enodes[id]; return m_decl2enodes[id];
return m_empty_enodes; return m_empty_enodes;
@ -341,7 +341,7 @@ namespace euf {
m_expr2enode[e->get_id()] = nullptr; m_expr2enode[e->get_id()] = nullptr;
n->~enode(); n->~enode();
if (is_app(e) && n->num_args() > 0) 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_nodes.pop_back();
m_exprs.pop_back(); m_exprs.pop_back();
}; };

4
src/ast/euf/euf_enode.h
View file

@ -162,7 +162,7 @@ namespace euf {
bool merge_tf() const { return merge_enabled() && (class_size() > 1 || num_parents() > 0 || num_args() > 0); } 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]; } 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; } unsigned get_table_id() const { return m_table_id; }
void set_table_id(unsigned t) { m_table_id = t; } 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); } 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; } 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_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(); } unsigned get_root_id() const { return m_root->m_expr->get_id(); }
bool children_are_roots() const; bool children_are_roots() const;
enode* get_next() const { return m_next; } enode* get_next() const { return m_next; }

2
src/ast/static_features.h
View file

@ -162,7 +162,7 @@ struct static_features {
bool arith_k_sum_is_small() const { return m_arith_k_sum < rational(INT_MAX / 8); } 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_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_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]++; } void inc_theory_constants(family_id fid) { m_num_theory_constants.reserve(fid+1, 0); m_num_theory_constants[fid]++; }

35
src/ast/substitution/substitution_tree.cpp
View file

@ -137,10 +137,7 @@ void substitution_tree::reset_registers(unsigned old_size) {
unsigned substitution_tree::get_compatibility_measure(svector<subst> const & sv) { unsigned substitution_tree::get_compatibility_measure(svector<subst> const & sv) {
unsigned old_size = m_todo.size(); unsigned old_size = m_todo.size();
unsigned measure = 0; unsigned measure = 0;
svector<subst>::const_iterator it = sv.begin(); for (subst const& s : sv) {
svector<subst>::const_iterator end = sv.end();
for (; it != end; ++it) {
subst const & s = *it;
unsigned ireg = s.first->get_idx(); unsigned ireg = s.first->get_idx();
expr * out = s.second; expr * out = s.second;
expr * in = get_reg_value(ireg); expr * in = get_reg_value(ireg);
@ -254,7 +251,7 @@ void substitution_tree::insert(expr * new_expr) {
else { else {
SASSERT(is_var(new_expr)); SASSERT(is_var(new_expr));
sort * s = to_var(new_expr)->get_sort(); 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()) if (id >= m_vars.size())
m_vars.resize(id+1); m_vars.resize(id+1);
if (m_vars[id] == 0) if (m_vars[id] == 0)
@ -274,7 +271,7 @@ void substitution_tree::insert(app * new_expr) {
m_todo.push_back(0); m_todo.push_back(0);
func_decl * d = new_expr->get_decl(); func_decl * d = new_expr->get_decl();
unsigned id = d->get_decl_id(); unsigned id = d->get_small_id();
if (id >= m_roots.size()) if (id >= m_roots.size())
m_roots.resize(id+1); m_roots.resize(id+1);
@ -439,7 +436,7 @@ void substitution_tree::erase(expr * e) {
else { else {
SASSERT(is_var(e)); SASSERT(is_var(e));
sort * s = to_var(e)->get_sort(); 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) if (id >= m_vars.size() || m_vars[id] == 0)
return; return;
var_ref_vector * v = m_vars[id]; var_ref_vector * v = m_vars[id];
@ -453,7 +450,7 @@ void substitution_tree::erase(expr * e) {
*/ */
void substitution_tree::erase(app * e) { void substitution_tree::erase(app * e) {
func_decl * d = e->get_decl(); 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]) if (id >= m_roots.size() || !m_roots[id])
return; return;
@ -732,7 +729,7 @@ bool substitution_tree::visit_vars(expr * e, st_visitor & st) {
if (m_vars.empty()) if (m_vars.empty())
return true; // continue return true; // continue
sort * s = e->get_sort(); 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()) { if (s_id < m_vars.size()) {
var_ref_vector * v = m_vars[s_id]; var_ref_vector * v = m_vars[s_id];
if (v && !v->empty()) { if (v && !v->empty()) {
@ -832,17 +829,14 @@ void substitution_tree::visit(expr * e, st_visitor & st, unsigned in_offset, uns
if (visit_vars<Mode>(e, st)) { if (visit_vars<Mode>(e, st)) {
if (is_app(e)) { if (is_app(e)) {
func_decl * d = to_app(e)->get_decl(); 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); node * r = m_roots.get(id, 0);
if (r) if (r)
visit<Mode>(e, st, r); visit<Mode>(e, st, r);
} }
else { else {
SASSERT(is_var(e)); SASSERT(is_var(e));
ptr_vector<node>::iterator it = m_roots.begin(); for (node* r : m_roots) {
ptr_vector<node>::iterator end = m_roots.end();
for (; it != end; ++it) {
node * r = *it;
if (r != nullptr) { if (r != nullptr) {
var * v = r->m_subst[0].first; var * v = r->m_subst[0].first;
if (v->get_sort() == to_var(e)->get_sort()) 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 { void substitution_tree::display(std::ostream & out) const {
out << "substitution tree:\n"; out << "substitution tree:\n";
ptr_vector<node>::const_iterator it = m_roots.begin(); for (node* n : m_roots)
ptr_vector<node>::const_iterator end = m_roots.end(); if (n)
for (; it != end; ++it) display(out, n, 0);
if (*it)
display(out, *it, 0);
bool found_var = false; bool found_var = false;
ptr_vector<var_ref_vector>::const_iterator it2 = m_vars.begin(); for (var_ref_vector* v : m_vars) {
ptr_vector<var_ref_vector>::const_iterator end2 = m_vars.end();
for (; it2 != end2; ++it2) {
var_ref_vector * v = *it2;
if (v == nullptr) if (v == nullptr)
continue; // m_vars may contain null pointers. See substitution_tree::insert. continue; // m_vars may contain null pointers. See substitution_tree::insert.
unsigned num = v->size(); unsigned num = v->size();

2
src/model/model.cpp
View file

@ -476,7 +476,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition,
// noop // noop
} }
else if (f->is_skolem() && can_inline_def(ts, f, force_inline) && (fi = get_func_interp(f)) && 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); var_subst vs(m, false);
new_t = vs(fi->get_interp(), args.size(), args.data()); new_t = vs(fi->get_interp(), args.size(), args.data());
} }

4
src/qe/mbp/mbp_term_graph.cpp
View file

@ -755,7 +755,7 @@ namespace mbp {
app* a = to_app(e); app* a = to_app(e);
func_decl* d = a->get_decl(); func_decl* d = a->get_decl();
if (d->get_arity() == 0) continue; if (d->get_arity() == 0) continue;
unsigned id = d->get_decl_id(); unsigned id = d->get_small_id();
m_decl2terms.reserve(id+1); m_decl2terms.reserve(id+1);
if (m_decl2terms[id].empty()) m_decls.push_back(d); if (m_decl2terms[id].empty()) m_decls.push_back(d);
m_decl2terms[id].push_back(t); m_decl2terms[id].push_back(t);
@ -770,7 +770,7 @@ namespace mbp {
// are distinct. // are distinct.
// //
for (func_decl* d : m_decls) { for (func_decl* d : m_decls) {
unsigned id = d->get_decl_id(); unsigned id = d->get_small_id();
ptr_vector<term> const& terms = m_decl2terms[id]; ptr_vector<term> const& terms = m_decl2terms[id];
if (terms.size() <= 1) continue; if (terms.size() <= 1) continue;
unsigned arity = d->get_arity(); unsigned arity = d->get_arity();

2
src/sat/smt/array_model.cpp
View file

@ -54,7 +54,7 @@ namespace array {
euf::enode* d = get_default(v); euf::enode* d = get_default(v);
if (d) if (d)
dep.add(n, d); dep.add(n, d);
if (!dep.deps().contains(n)) if (!dep.contains_dep(n))
dep.insert(n, nullptr); dep.insert(n, nullptr);
return true; return true;
} }

2
src/sat/smt/euf_proof.cpp
View file

@ -104,7 +104,7 @@ namespace euf {
std::ostringstream strm; std::ostringstream strm;
smt2_pp_environment_dbg env(m); smt2_pp_environment_dbg env(m);
ast_smt2_pp(strm, f, env); 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(); get_drat().def_end();
} }

20
src/sat/smt/q_mam.cpp
View file

@ -104,7 +104,7 @@ namespace q {
public: public:
unsigned char operator()(func_decl * lbl) { 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()) if (lbl_id >= m_lbl2hash.size())
m_lbl2hash.resize(lbl_id + 1, -1); m_lbl2hash.resize(lbl_id + 1, -1);
if (m_lbl2hash[lbl_id] == -1) { if (m_lbl2hash[lbl_id] == -1) {
@ -2868,7 +2868,7 @@ namespace q {
SASSERT(first_idx < mp->get_num_args()); SASSERT(first_idx < mp->get_num_args());
app * p = to_app(mp->get_arg(first_idx)); app * p = to_app(mp->get_arg(first_idx));
func_decl * lbl = p->get_decl(); 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); m_trees.reserve(lbl_id+1, nullptr);
if (m_trees[lbl_id] == nullptr) { if (m_trees[lbl_id] == nullptr) {
m_trees[lbl_id] = m_compiler.mk_tree(qa, mp, first_idx, false); 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 { 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()) if (lbl_id < m_trees.size())
return m_trees[lbl_id]; return m_trees[lbl_id];
else else
@ -3112,11 +3112,11 @@ namespace q {
} }
bool is_plbl(func_decl * lbl) const { 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]; return lbl_id < m_is_plbl.size() && m_is_plbl[lbl_id];
} }
bool is_clbl(func_decl * lbl) const { 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]; return lbl_id < m_is_clbl.size() && m_is_clbl[lbl_id];
} }
@ -3129,7 +3129,7 @@ namespace q {
} }
void update_clbls(func_decl * lbl) { 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); 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("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";); 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) { 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); 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"; 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";); tout << "mam: " << this << "\n";);
@ -3698,7 +3698,7 @@ namespace q {
app * p = to_app(mp->get_arg(0)); app * p = to_app(mp->get_arg(0));
func_decl * lbl = p->get_decl(); func_decl * lbl = p->get_decl();
if (!m_egraph.enodes_of(lbl).empty()) { 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); m_tmp_trees.reserve(lbl_id+1, 0);
if (m_tmp_trees[lbl_id] == 0) { if (m_tmp_trees[lbl_id] == 0) {
m_tmp_trees[lbl_id] = m_compiler.mk_tree(qa, mp, 0, false); 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) { 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]; code_tree * tmp_tree = m_tmp_trees[lbl_id];
SASSERT(tmp_tree != 0); SASSERT(tmp_tree != 0);
SASSERT(!m_egraph.enodes_of(lbl).empty()); SASSERT(!m_egraph.enodes_of(lbl).empty());
@ -3843,7 +3843,7 @@ namespace q {
unsigned h = m_lbl_hasher(lbl); unsigned h = m_lbl_hasher(lbl);
TRACE("trigger_bug", tout << "lbl: " << lbl->get_name() << " is_clbl(lbl): " << is_clbl(lbl) TRACE("trigger_bug", tout << "lbl: " << lbl->get_name() << " is_clbl(lbl): " << is_clbl(lbl)
<< ", is_plbl(lbl): " << is_plbl(lbl) << ", h: " << h << "\n"; << ", 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)) if (is_clbl(lbl))
update_lbls(n, h); update_lbls(n, h);
if (is_plbl(lbl)) if (is_plbl(lbl))

20
src/smt/mam.cpp
View file

@ -78,7 +78,7 @@ namespace {
public: public:
unsigned char operator()(func_decl * lbl) { 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()) if (lbl_id >= m_lbl2hash.size())
m_lbl2hash.resize(lbl_id + 1, -1); m_lbl2hash.resize(lbl_id + 1, -1);
if (m_lbl2hash[lbl_id] == -1) { if (m_lbl2hash[lbl_id] == -1) {
@ -2906,7 +2906,7 @@ namespace {
SASSERT(first_idx < mp->get_num_args()); SASSERT(first_idx < mp->get_num_args());
app * p = to_app(mp->get_arg(first_idx)); app * p = to_app(mp->get_arg(first_idx));
func_decl * lbl = p->get_decl(); 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); m_trees.reserve(lbl_id+1, nullptr);
if (m_trees[lbl_id] == nullptr) { if (m_trees[lbl_id] == nullptr) {
m_trees[lbl_id] = m_compiler.mk_tree(qa, mp, first_idx, false); 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 { 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()) if (lbl_id < m_trees.size())
return m_trees[lbl_id]; return m_trees[lbl_id];
else else
@ -3165,11 +3165,11 @@ namespace {
} }
bool is_plbl(func_decl * lbl) const { 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]; return lbl_id < m_is_plbl.size() && m_is_plbl[lbl_id];
} }
bool is_clbl(func_decl * lbl) const { 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]; return lbl_id < m_is_clbl.size() && m_is_clbl[lbl_id];
} }
@ -3182,7 +3182,7 @@ namespace {
} }
void update_clbls(func_decl * lbl) { 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); 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("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";); 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) { 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); 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"; 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";); tout << "mam: " << this << "\n";);
@ -3744,7 +3744,7 @@ namespace {
app * p = to_app(mp->get_arg(0)); app * p = to_app(mp->get_arg(0));
func_decl * lbl = p->get_decl(); func_decl * lbl = p->get_decl();
if (m_context.get_num_enodes_of(lbl) > 0) { 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); m_tmp_trees.reserve(lbl_id+1, 0);
if (m_tmp_trees[lbl_id] == 0) { if (m_tmp_trees[lbl_id] == 0) {
m_tmp_trees[lbl_id] = m_compiler.mk_tree(qa, mp, 0, false); 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) { 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]; code_tree * tmp_tree = m_tmp_trees[lbl_id];
SASSERT(tmp_tree != 0); SASSERT(tmp_tree != 0);
SASSERT(m_context.get_num_enodes_of(lbl) > 0); SASSERT(m_context.get_num_enodes_of(lbl) > 0);
@ -3963,7 +3963,7 @@ namespace {
unsigned h = m_lbl_hasher(lbl); unsigned h = m_lbl_hasher(lbl);
TRACE("trigger_bug", tout << "lbl: " << lbl->get_name() << " is_clbl(lbl): " << is_clbl(lbl) TRACE("trigger_bug", tout << "lbl: " << lbl->get_name() << " is_clbl(lbl): " << is_clbl(lbl)
<< ", is_plbl(lbl): " << is_plbl(lbl) << ", h: " << h << "\n"; << ", 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)) if (is_clbl(lbl))
update_lbls(n, h); update_lbls(n, h);
if (is_plbl(lbl)) if (is_plbl(lbl))

8
src/smt/smt_context.h
View file

@ -531,22 +531,22 @@ namespace smt {
} }
unsigned get_num_enodes_of(func_decl const * decl) const { 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; return id < m_decl2enodes.size() ? m_decl2enodes[id].size() : 0;
} }
enode_vector const& enodes_of(func_decl const * d) const { 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; return id < m_decl2enodes.size() ? m_decl2enodes[id] : m_empty_vector;
} }
enode_vector::const_iterator begin_enodes_of(func_decl const * decl) const { 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; return id < m_decl2enodes.size() ? m_decl2enodes[id].begin() : nullptr;
} }
enode_vector::const_iterator end_enodes_of(func_decl const * decl) const { 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; return id < m_decl2enodes.size() ? m_decl2enodes[id].end() : nullptr;
} }

2
src/smt/smt_enode.h
View file

@ -171,7 +171,7 @@ namespace smt {
unsigned get_expr_id() const { return m_owner->get_id(); } unsigned get_expr_id() const { return m_owner->get_id(); }
func_decl * get_decl() const { return m_owner->get_decl(); } 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(); } sort* get_sort() const { return m_owner->get_sort(); }

4
src/smt/smt_internalizer.cpp
View file

@ -1010,7 +1010,7 @@ namespace smt {
} }
} }
if (!e->is_eq()) { 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()) if (decl_id >= m_decl2enodes.size())
m_decl2enodes.resize(decl_id+1); m_decl2enodes.resize(decl_id+1);
m_decl2enodes[decl_id].push_back(e); m_decl2enodes[decl_id].push_back(e);
@ -1054,7 +1054,7 @@ namespace smt {
m_cg_table.erase(e); m_cg_table.erase(e);
} }
if (e->get_num_args() > 0 && !e->is_eq()) { 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(decl_id < m_decl2enodes.size());
SASSERT(m_decl2enodes[decl_id].back() == e); SASSERT(m_decl2enodes[decl_id].back() == e);
m_decl2enodes[decl_id].pop_back(); m_decl2enodes[decl_id].pop_back();

71
src/util/top_sort.h
View file

@ -24,39 +24,51 @@ Revision History:
#include "util/obj_hashtable.h" #include "util/obj_hashtable.h"
#include "util/vector.h" #include "util/vector.h"
#include "util/memory_manager.h" #include "util/memory_manager.h"
#include "util/tptr.h"
template<typename T> template<typename T>
class top_sort { class top_sort {
typedef obj_hashtable<T> T_set; typedef obj_hashtable<T> T_set;
obj_map<T, unsigned> m_partition_id; unsigned_vector m_partition_id;
obj_map<T, unsigned> m_dfs_num; unsigned_vector m_dfs_num;
ptr_vector<T> m_top_sorted; ptr_vector<T> m_top_sorted;
ptr_vector<T> m_stack_S; ptr_vector<T> m_stack_S;
ptr_vector<T> m_stack_P; ptr_vector<T> m_stack_P;
unsigned m_next_preorder; unsigned m_next_preorder;
obj_map<T, T_set*> m_deps; ptr_vector<T_set> m_deps;
ptr_vector<T> 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) { void traverse(T* f) {
unsigned p_id = 0; unsigned p_id = m_dfs_num.get(f->get_small_id(), UINT_MAX);
if (m_dfs_num.find(f, p_id)) { if (p_id != UINT_MAX) {
if (!m_partition_id.contains(f)) { if (!contains_partition(f)) {
while (!m_stack_P.empty() && m_partition_id.contains(m_stack_P.back()) && m_partition_id[m_stack_P.back()] > p_id) { while (!m_stack_P.empty() && contains_partition(m_stack_P.back()) && partition_id(m_stack_P.back()) > p_id) {
m_stack_P.pop_back(); m_stack_P.pop_back();
} }
} }
} }
else if (!m_deps.contains(f)) { else if (!contains_dep(f))
return; return;
}
else { 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_S.push_back(f);
m_stack_P.push_back(f); m_stack_P.push_back(f);
if (m_deps[f]) { T_set* ts = get_dep(f);
for (T* g : *m_deps[f]) { if (ts) {
for (T* g : *ts)
traverse(g); traverse(g);
}
} }
if (f == m_stack_P.back()) { if (f == m_stack_P.back()) {
p_id = m_top_sorted.size(); p_id = m_top_sorted.size();
@ -65,7 +77,7 @@ class top_sort {
s_f = m_stack_S.back(); s_f = m_stack_S.back();
m_stack_S.pop_back(); m_stack_S.pop_back();
m_top_sorted.push_back(s_f); 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); while (s_f != f);
m_stack_P.pop_back(); m_stack_P.pop_back();
@ -76,28 +88,29 @@ class top_sort {
public: public:
virtual ~top_sort() { 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() { void topological_sort() {
m_next_preorder = 0; m_next_preorder = 0;
m_partition_id.reset(); m_partition_id.reset();
m_top_sorted.reset(); m_top_sorted.reset();
for (auto & kv : m_deps) { for (auto * t : m_dep_keys)
traverse(kv.m_key); traverse(t);
}
SASSERT(m_stack_S.empty()); SASSERT(m_stack_S.empty());
SASSERT(m_stack_P.empty()); SASSERT(m_stack_P.empty());
m_dfs_num.reset(); m_dfs_num.reset();
} }
void insert(T* t, T_set* s) { void insert(T* t, T_set* s) {
m_deps.insert(t, s); m_deps.setx(t->get_small_id(), add_tag(s), nullptr);
m_dep_keys.push_back(t);
} }
void add(T* t, T* s) { void add(T* t, T* s) {
T_set* tb = nullptr; T_set* tb = get_dep(t);
if (!m_deps.find(t, tb) || !tb) { if (!tb) {
tb = alloc(T_set); tb = alloc(T_set);
insert(t, tb); insert(t, tb);
} }
@ -106,18 +119,18 @@ public:
ptr_vector<T> const& top_sorted() const { return m_top_sorted; } ptr_vector<T> const& top_sorted() const { return m_top_sorted; }
obj_map<T, unsigned> 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 { 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] && return f == m_top_sorted[pid] &&
(pid == 0 || 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() || m_partition_id[m_top_sorted[pid+1]] != pid); (pid + 1 == m_top_sorted.size() || partition_id(m_top_sorted[pid+1]) != pid);
} }
obj_map<T, T_set*> const& deps() const { return m_deps; }
}; };