mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

perf(datatype): improve caching in occurs_check

Browse source
This commit is contained in:
Simon Cruanes 2018-04-02 13:37:12 -05:00
parent 3b78bdc8e5
commit b5d531f079
2 changed files with 23 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/theory_datatype.cpp
View file

@ -389,12 +389,14 @@ namespace smt {
final_check_status theory_datatype::final_check_eh() { final_check_status theory_datatype::final_check_eh() {
int num_vars = get_num_vars(); int num_vars = get_num_vars();
final_check_status r = FC_DONE; final_check_status r = FC_DONE;
init_final_check();
for (int v = 0; v < num_vars; v++) { for (int v = 0; v < num_vars; v++) {
if (v == static_cast<int>(m_find.find(v))) { if (v == static_cast<int>(m_find.find(v))) {
enode * node = get_enode(v); enode * node = get_enode(v);
if (occurs_check(node)) { if (occurs_check(node)) {
// conflict was detected... // conflict was detected...
// return... // return...
cleanup_final_check();
return FC_CONTINUE; return FC_CONTINUE;
} }
if (m_params.m_dt_lazy_splits > 0) { if (m_params.m_dt_lazy_splits > 0) {
@ -407,6 +409,7 @@ namespace smt {
} }
} }
} }
cleanup_final_check();
return r; return r;
} }
@ -434,6 +437,8 @@ namespace smt {
tout << "eq: #" << p.first->get_owner_id() << " #" << p.second->get_owner_id() << "\n"; tout << "eq: #" << p.first->get_owner_id() << " #" << p.second->get_owner_id() << "\n";
tout << mk_bounded_pp(p.first->get_owner(), get_manager()) << " " << mk_bounded_pp(p.second->get_owner(), get_manager()) << "\n"; tout << mk_bounded_pp(p.first->get_owner(), get_manager()) << " " << mk_bounded_pp(p.second->get_owner(), get_manager()) << "\n";
}); });
} else {
oc_mark_cycle_free(n);
} }
return res; return res;
} }
@ -443,12 +448,11 @@ namespace smt {
TODO: improve performance. TODO: improve performance.
*/ */
bool theory_datatype::occurs_check_core(enode * app) { bool theory_datatype::occurs_check_core(enode * app) {
if (app->is_marked()) if (oc_cycle_free(app) || oc_explored(app))
return false; return false;
m_stats.m_occurs_check++; m_stats.m_occurs_check++;
app->set_mark(); oc_mark_explore(app);
m_to_unmark.push_back(app);
TRACE("datatype", tout << "occurs check_core: #" << app->get_owner_id() << " #" << m_main->get_owner_id() << "\n";); TRACE("datatype", tout << "occurs check_core: #" << app->get_owner_id() << " #" << m_main->get_owner_id() << "\n";);

16
src/smt/theory_datatype.h
View file

@ -74,8 +74,24 @@ namespace smt {
void sign_recognizer_conflict(enode * c, enode * r); void sign_recognizer_conflict(enode * c, enode * r);
ptr_vector<enode> m_to_unmark; ptr_vector<enode> m_to_unmark;
ptr_vector<enode> m_to_unmark2;
enode_pair_vector m_used_eqs; enode_pair_vector m_used_eqs;
enode * m_main; enode * m_main;
void oc_mark_explore(enode * n) { n->set_mark(); m_to_unmark.push_back(n); }
bool oc_explored(enode * n) const { n->is_marked(); }
void oc_mark_cycle_free(enode * n) { n->set_mark2(); m_to_unmark2.push_back(n); }
bool oc_cycle_free(enode * n) const { n->is_marked2(); }
void init_final_check() {
m_to_unmark2.reset();
}
void cleanup_final_check() {
unmark_enodes2(m_to_unmark2.size(), m_to_unmark2.c_ptr());
m_to_unmark2.reset();
}
bool occurs_check(enode * n); bool occurs_check(enode * n);
bool occurs_check_core(enode * n); bool occurs_check_core(enode * n);