mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
some more string perf profiling
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
ab5905cf7f
commit
ba292346ae
|
|
@ -133,13 +133,14 @@ void theory_seq::solution_map::update(expr* e, expr* r, dependency* d) {
|
|||
return;
|
||||
}
|
||||
m_cache.reset();
|
||||
std::pair<expr*, dependency*> value;
|
||||
if (m_map.find(e, value)) {
|
||||
add_trail(DEL, e, value.first, value.second);
|
||||
expr_dep value;
|
||||
if (find(e, value)) {
|
||||
add_trail(DEL, e, value.e, value.d);
|
||||
}
|
||||
value.first = r;
|
||||
value.second = d;
|
||||
m_map.insert(e, value);
|
||||
value.v = e;
|
||||
value.e = r;
|
||||
value.d = d;
|
||||
insert(value);
|
||||
add_trail(INS, e, r, d);
|
||||
}
|
||||
|
||||
|
|
@ -151,7 +152,7 @@ void theory_seq::solution_map::add_trail(map_update op, expr* l, expr* r, depend
|
|||
}
|
||||
|
||||
bool theory_seq::solution_map::is_root(expr* e) const {
|
||||
return !m_map.contains(e);
|
||||
return e->get_id() >= m_map.size() || m_map[e->get_id()].e == nullptr;
|
||||
}
|
||||
|
||||
// e1 -> ... -> e2
|
||||
|
|
@ -159,22 +160,22 @@ bool theory_seq::solution_map::is_root(expr* e) const {
|
|||
// e1 -> .... -> e3
|
||||
|
||||
// e1 -> ... x, e2 -> ... x
|
||||
void theory_seq::solution_map::find_rec(expr* e, svector<std::pair<expr*, dependency*> >& finds) {
|
||||
void theory_seq::solution_map::find_rec(expr* e, svector<expr_dep >& finds) {
|
||||
dependency* d = nullptr;
|
||||
std::pair<expr*, dependency*> value(e, d);
|
||||
expr_dep value(e, e, d);
|
||||
do {
|
||||
e = value.first;
|
||||
d = m_dm.mk_join(d, value.second);
|
||||
e = value.e;
|
||||
d = m_dm.mk_join(d, value.d);
|
||||
finds.push_back(value);
|
||||
}
|
||||
while (m_map.find(e, value));
|
||||
while (find(e, value));
|
||||
}
|
||||
|
||||
bool theory_seq::solution_map::find1(expr* e, expr*& r, dependency*& d) {
|
||||
std::pair<expr*, dependency*> value;
|
||||
if (m_map.find(e, value)) {
|
||||
d = m_dm.mk_join(d, value.second);
|
||||
r = value.first;
|
||||
expr_dep value;
|
||||
if (find(e, value)) {
|
||||
d = m_dm.mk_join(d, value.d);
|
||||
r = value.e;
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
|
|
@ -183,22 +184,22 @@ bool theory_seq::solution_map::find1(expr* e, expr*& r, dependency*& d) {
|
|||
}
|
||||
|
||||
expr* theory_seq::solution_map::find(expr* e, dependency*& d) {
|
||||
std::pair<expr*, dependency*> value;
|
||||
expr_dep value;
|
||||
d = nullptr;
|
||||
expr* result = e;
|
||||
while (m_map.find(result, value)) {
|
||||
d = m_dm.mk_join(d, value.second);
|
||||
SASSERT(result != value.first);
|
||||
SASSERT(e != value.first);
|
||||
result = value.first;
|
||||
while (find(result, value)) {
|
||||
d = m_dm.mk_join(d, value.d);
|
||||
SASSERT(result != value.e);
|
||||
SASSERT(e != value.e);
|
||||
result = value.e;
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
expr* theory_seq::solution_map::find(expr* e) {
|
||||
std::pair<expr*, dependency*> value;
|
||||
while (m_map.find(e, value)) {
|
||||
e = value.first;
|
||||
expr_dep value;
|
||||
while (find(e, value)) {
|
||||
e = value.e;
|
||||
}
|
||||
return e;
|
||||
}
|
||||
|
|
@ -209,10 +210,11 @@ void theory_seq::solution_map::pop_scope(unsigned num_scopes) {
|
|||
unsigned start = m_limit[m_limit.size() - num_scopes];
|
||||
for (unsigned i = m_updates.size(); i-- > start; ) {
|
||||
if (m_updates[i] == INS) {
|
||||
m_map.remove(m_lhs.get(i));
|
||||
unsigned id = m_lhs.get(i)->get_id();
|
||||
if (id < m_map.size()) m_map[id] = expr_dep();
|
||||
}
|
||||
else {
|
||||
m_map.insert(m_lhs.get(i), std::make_pair(m_rhs.get(i), m_deps[i]));
|
||||
insert(expr_dep(m_lhs.get(i), m_rhs.get(i), m_deps[i]));
|
||||
}
|
||||
}
|
||||
m_updates.resize(start);
|
||||
|
|
@ -223,8 +225,8 @@ void theory_seq::solution_map::pop_scope(unsigned num_scopes) {
|
|||
}
|
||||
|
||||
void theory_seq::solution_map::display(std::ostream& out) const {
|
||||
for (auto const& kv : m_map) {
|
||||
out << mk_bounded_pp(kv.m_key, m, 2) << " |-> " << mk_bounded_pp(kv.m_value.first, m, 2) << "\n";
|
||||
for (auto const& ed : m_map) {
|
||||
if (ed.v) out << mk_bounded_pp(ed.v, m, 2) << " |-> " << mk_bounded_pp(ed.e, m, 2) << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -4313,6 +4315,7 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
app* theory_seq::mk_value(app* e) {
|
||||
expr_ref result(m);
|
||||
e = get_ite_value(e);
|
||||
|
|
@ -4489,10 +4492,10 @@ expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){
|
|||
expr_ref result(m);
|
||||
expr_dep ed;
|
||||
if (m_rep.find_cache(e, ed)) {
|
||||
if (e != ed.first) {
|
||||
eqs = m_dm.mk_join(eqs, ed.second);
|
||||
if (e != ed.e) {
|
||||
eqs = m_dm.mk_join(eqs, ed.d);
|
||||
}
|
||||
result = ed.first;
|
||||
result = ed.e;
|
||||
}
|
||||
else {
|
||||
m_expand_todo.push_back(e);
|
||||
|
|
@ -4626,8 +4629,8 @@ bool theory_seq::expand1(expr* e0, dependency*& eqs, expr_ref& result) {
|
|||
if (result == e0) {
|
||||
deps = nullptr;
|
||||
}
|
||||
expr_dep edr(result, deps);
|
||||
m_rep.add_cache(e0, edr);
|
||||
expr_dep edr(e0, result, deps);
|
||||
m_rep.add_cache(edr);
|
||||
eqs = m_dm.mk_join(eqs, deps);
|
||||
TRACE("seq_verbose", tout << mk_pp(e0, m) << " |--> " << result << "\n";
|
||||
if (eqs) display_deps(tout, eqs););
|
||||
|
|
|
|||
|
|
@ -45,8 +45,14 @@ namespace smt {
|
|||
typedef dependency_manager::dependency dependency;
|
||||
|
||||
typedef trail_stack<theory_seq> th_trail_stack;
|
||||
typedef std::pair<expr*, dependency*> expr_dep;
|
||||
typedef obj_map<expr, expr_dep> eqdep_map_t;
|
||||
struct expr_dep {
|
||||
expr* v;
|
||||
expr* e;
|
||||
dependency* d;
|
||||
expr_dep(expr* v, expr* e, dependency* d): v(v), e(e), d(d) {}
|
||||
expr_dep():v(nullptr), e(nullptr), d(nullptr) {}
|
||||
};
|
||||
typedef svector<expr_dep> eqdep_map_t;
|
||||
typedef union_find<theory_seq> th_union_find;
|
||||
|
||||
class seq_value_proc;
|
||||
|
|
@ -59,8 +65,15 @@ namespace smt {
|
|||
expr_ref_vector m_trail;
|
||||
public:
|
||||
eval_cache(ast_manager& m): m_trail(m) {}
|
||||
bool find(expr* v, expr_dep& r) const { return m_map.find(v, r); }
|
||||
void insert(expr* v, expr_dep& r) { m_trail.push_back(v); m_trail.push_back(r.first); m_map.insert(v, r); }
|
||||
bool find(expr* v, expr_dep& r) const {
|
||||
return v->get_id() < m_map.size() && m_map[v->get_id()].e && (r = m_map[v->get_id()], true);
|
||||
}
|
||||
void insert(expr_dep const& r) {
|
||||
m_trail.push_back(r.v);
|
||||
m_trail.push_back(r.e);
|
||||
m_map.reserve(2*r.v->get_id() + 1);
|
||||
m_map[r.v->get_id()] = r;
|
||||
}
|
||||
void reset() { m_map.reset(); m_trail.reset(); }
|
||||
};
|
||||
|
||||
|
|
@ -77,18 +90,25 @@ namespace smt {
|
|||
svector<map_update> m_updates;
|
||||
unsigned_vector m_limit;
|
||||
|
||||
bool find(expr* v, expr_dep& r) const {
|
||||
return v->get_id() < m_map.size() && m_map[v->get_id()].e && (r = m_map[v->get_id()], true);
|
||||
}
|
||||
void insert(expr_dep const& r) {
|
||||
m_map.reserve(2*r.v->get_id() + 1);
|
||||
m_map[r.v->get_id()] = r;
|
||||
}
|
||||
void add_trail(map_update op, expr* l, expr* r, dependency* d);
|
||||
public:
|
||||
solution_map(ast_manager& m, dependency_manager& dm):
|
||||
m(m), m_dm(dm), m_cache(m), m_lhs(m), m_rhs(m) {}
|
||||
bool empty() const { return m_map.empty(); }
|
||||
void update(expr* e, expr* r, dependency* d);
|
||||
void add_cache(expr* v, expr_dep& r) { m_cache.insert(v, r); }
|
||||
void add_cache(expr_dep& r) { m_cache.insert(r); }
|
||||
bool find_cache(expr* v, expr_dep& r) { return m_cache.find(v, r); }
|
||||
expr* find(expr* e, dependency*& d);
|
||||
expr* find(expr* e);
|
||||
bool find1(expr* a, expr*& b, dependency*& dep);
|
||||
void find_rec(expr* e, svector<std::pair<expr*, dependency*> >& finds);
|
||||
void find_rec(expr* e, svector<expr_dep>& finds);
|
||||
bool is_root(expr* e) const;
|
||||
void cache(expr* e, expr* r, dependency* d);
|
||||
void reset_cache() { m_cache.reset(); }
|
||||
|
|
|
|||
Loading…
Reference in a new issue