mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
use ref-vector for shared occurrences to avoid hash-table overhead
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f8f3549c1c
commit
9bd4050e0c
|
@ -21,13 +21,11 @@ Revision History:
|
|||
#include "util/ref_util.h"
|
||||
|
||||
inline void shared_occs::insert(expr * t) {
|
||||
obj_hashtable<expr>::entry * dummy;
|
||||
if (m_shared.insert_if_not_there_core(t, dummy))
|
||||
m.inc_ref(t);
|
||||
m_shared.reserve(t->get_id() + 1);
|
||||
m_shared[t->get_id()] = t;
|
||||
}
|
||||
|
||||
void shared_occs::reset() {
|
||||
dec_ref_collection_values(m, m_shared);
|
||||
m_shared.reset();
|
||||
}
|
||||
|
||||
|
@ -132,9 +130,15 @@ void shared_occs::operator()(expr * t) {
|
|||
}
|
||||
|
||||
void shared_occs::display(std::ostream & out, ast_manager & m) const {
|
||||
iterator it = begin_shared();
|
||||
iterator end = end_shared();
|
||||
for (; it != end; ++it) {
|
||||
out << mk_ismt2_pp(*it, m) << "\n";
|
||||
for (expr* s : m_shared) {
|
||||
if (s) {
|
||||
out << mk_ismt2_pp(s, m) << "\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
unsigned shared_occs::num_shared() const{
|
||||
unsigned count = 0;
|
||||
for (expr* s : m_shared) if (s) count++;
|
||||
return count;
|
||||
}
|
||||
|
|
|
@ -53,7 +53,7 @@ class shared_occs {
|
|||
bool m_track_atomic;
|
||||
bool m_visit_quantifiers;
|
||||
bool m_visit_patterns;
|
||||
obj_hashtable<expr> m_shared;
|
||||
expr_ref_vector m_shared;
|
||||
typedef std::pair<expr*, unsigned> frame;
|
||||
svector<frame> m_stack;
|
||||
bool process(expr * t, shared_occs_mark & visited);
|
||||
|
@ -64,15 +64,14 @@ public:
|
|||
m(_m),
|
||||
m_track_atomic(track_atomic),
|
||||
m_visit_quantifiers(visit_quantifiers),
|
||||
m_visit_patterns(visit_patterns) {
|
||||
m_visit_patterns(visit_patterns),
|
||||
m_shared(m) {
|
||||
}
|
||||
~shared_occs();
|
||||
void operator()(expr * t);
|
||||
void operator()(expr * t, shared_occs_mark & visited);
|
||||
bool is_shared(expr * t) const { return m_shared.contains(t); }
|
||||
unsigned num_shared() const { return m_shared.size(); }
|
||||
iterator begin_shared() const { return m_shared.begin(); }
|
||||
iterator end_shared() const { return m_shared.end(); }
|
||||
bool is_shared(expr * t) const { return m_shared.get(t->get_id(), nullptr) != nullptr; }
|
||||
unsigned num_shared() const;
|
||||
void reset();
|
||||
void cleanup();
|
||||
void display(std::ostream & out, ast_manager & mgr) const;
|
||||
|
|
|
@ -77,30 +77,12 @@ BINARY_SYM_CMD(shift_vars_cmd,
|
|||
store_expr_ref(ctx, m_sym, r.get());
|
||||
});
|
||||
|
||||
UNARY_CMD(pp_shared_cmd, "dbg-pp-shared", "<term>", "display shared subterms of the given term", CPK_EXPR, expr *, {
|
||||
shared_occs s(ctx.m());
|
||||
s(arg);
|
||||
ctx.regular_stream() << "(shared";
|
||||
shared_occs::iterator it = s.begin_shared();
|
||||
shared_occs::iterator end = s.end_shared();
|
||||
for (; it != end; ++it) {
|
||||
expr * curr = *it;
|
||||
ctx.regular_stream() << std::endl << " ";
|
||||
ctx.display(ctx.regular_stream(), curr, 2);
|
||||
}
|
||||
ctx.regular_stream() << ")" << std::endl;
|
||||
});
|
||||
|
||||
UNARY_CMD(assert_not_cmd, "assert-not", "<term>", "assert negation", CPK_EXPR, expr *, {
|
||||
expr_ref ne(ctx.m().mk_not(arg), ctx.m());
|
||||
ctx.assert_expr(ne);
|
||||
});
|
||||
|
||||
UNARY_CMD(num_shared_cmd, "dbg-num-shared", "<term>", "return the number of shared subterms", CPK_EXPR, expr *, {
|
||||
shared_occs s(ctx.m());
|
||||
s(arg);
|
||||
ctx.regular_stream() << s.num_shared() << std::endl;
|
||||
});
|
||||
|
||||
UNARY_CMD(size_cmd, "dbg-size", "<term>", "return the size of the given term", CPK_EXPR, expr *, {
|
||||
ctx.regular_stream() << get_num_exprs(arg) << std::endl;
|
||||
|
@ -550,8 +532,6 @@ void install_dbg_cmds(cmd_context & ctx) {
|
|||
ctx.insert(alloc(set_cmd));
|
||||
ctx.insert(alloc(pp_var_cmd));
|
||||
ctx.insert(alloc(shift_vars_cmd));
|
||||
ctx.insert(alloc(pp_shared_cmd));
|
||||
ctx.insert(alloc(num_shared_cmd));
|
||||
ctx.insert(alloc(assert_not_cmd));
|
||||
ctx.insert(alloc(size_cmd));
|
||||
ctx.insert(alloc(subst_cmd));
|
||||
|
|
Loading…
Reference in a new issue