From b5d531f079d6b678dc8accf6fd165185361c18d6 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 2 Apr 2018 13:37:12 -0500 Subject: [PATCH 01/11] perf(datatype): improve caching in occurs_check --- src/smt/theory_datatype.cpp | 10 +++++++--- src/smt/theory_datatype.h | 16 ++++++++++++++++ 2 files changed, 23 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 3d3d56055..a3c0ecc96 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -389,12 +389,14 @@ namespace smt { final_check_status theory_datatype::final_check_eh() { int num_vars = get_num_vars(); final_check_status r = FC_DONE; + init_final_check(); for (int v = 0; v < num_vars; v++) { if (v == static_cast(m_find.find(v))) { enode * node = get_enode(v); if (occurs_check(node)) { // conflict was detected... // return... + cleanup_final_check(); return FC_CONTINUE; } if (m_params.m_dt_lazy_splits > 0) { @@ -407,6 +409,7 @@ namespace smt { } } } + cleanup_final_check(); return r; } @@ -434,6 +437,8 @@ namespace smt { 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"; }); + } else { + oc_mark_cycle_free(n); } return res; } @@ -443,12 +448,11 @@ namespace smt { TODO: improve performance. */ bool theory_datatype::occurs_check_core(enode * app) { - if (app->is_marked()) + if (oc_cycle_free(app) || oc_explored(app)) return false; m_stats.m_occurs_check++; - app->set_mark(); - m_to_unmark.push_back(app); + oc_mark_explore(app); TRACE("datatype", tout << "occurs check_core: #" << app->get_owner_id() << " #" << m_main->get_owner_id() << "\n";); diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index 2337fd0ea..1ccc15314 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -74,8 +74,24 @@ namespace smt { void sign_recognizer_conflict(enode * c, enode * r); ptr_vector m_to_unmark; + ptr_vector m_to_unmark2; enode_pair_vector m_used_eqs; 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_core(enode * n); From 2ee1e358b6cb3aa03c63580d656499106ae4c4a2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 2 Apr 2018 15:10:08 -0500 Subject: [PATCH 02/11] chore: add definition for `enode_tbl` --- src/smt/smt_types.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/smt_types.h b/src/smt/smt_types.h index 6300bd43c..17b99c8b2 100644 --- a/src/smt/smt_types.h +++ b/src/smt/smt_types.h @@ -21,6 +21,7 @@ Revision History: #include "util/list.h" #include "util/vector.h" +#include "util/hashtable.h" #include "util/lbool.h" class model; @@ -46,6 +47,7 @@ namespace smt { typedef ptr_vector enode_vector; typedef std::pair enode_pair; typedef svector enode_pair_vector; + typedef ptr_hashtable, deref_eq > enode_tbl; class context; From 9df140343a9565cbdae2fdf39b876882add46933 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 2 Apr 2018 17:17:21 -0500 Subject: [PATCH 03/11] perf(datatype): whole-graph implementation of occurs_check --- src/smt/smt_enode.h | 7 ++ src/smt/smt_types.h | 1 - src/smt/theory_datatype.cpp | 136 ++++++++++++++++++++++-------------- src/smt/theory_datatype.h | 61 +++++++++++----- 4 files changed, 135 insertions(+), 70 deletions(-) diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index df6309424..ba13a31bb 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -171,6 +171,9 @@ namespace smt { m_interpreted = true; } + inline bool equal(const enode & other) const { + return m_owner == other.m_owner; + } void del_eh(ast_manager & m, bool update_children_parent = true); @@ -423,5 +426,9 @@ namespace smt { }; +inline bool operator==(const smt::enode & e1, const smt::enode & e2) { + return e1.equal(e2); +} + #endif /* SMT_ENODE_H_ */ diff --git a/src/smt/smt_types.h b/src/smt/smt_types.h index 17b99c8b2..e062a4ad6 100644 --- a/src/smt/smt_types.h +++ b/src/smt/smt_types.h @@ -47,7 +47,6 @@ namespace smt { typedef ptr_vector enode_vector; typedef std::pair enode_pair; typedef svector enode_pair_vector; - typedef ptr_hashtable, deref_eq > enode_tbl; class context; diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index a3c0ecc96..b3c6ffadf 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -389,14 +389,13 @@ namespace smt { final_check_status theory_datatype::final_check_eh() { int num_vars = get_num_vars(); final_check_status r = FC_DONE; - init_final_check(); + final_check_st _guard(this); // RAII for managing state for (int v = 0; v < num_vars; v++) { if (v == static_cast(m_find.find(v))) { enode * node = get_enode(v); if (occurs_check(node)) { // conflict was detected... // return... - cleanup_final_check(); return FC_CONTINUE; } if (m_params.m_dt_lazy_splits > 0) { @@ -409,10 +408,62 @@ namespace smt { } } } - cleanup_final_check(); return r; } + // explain the cycle root -> … -> app -> root + void theory_datatype::occurs_check_explain(enode * app, enode * const root) { + TRACE("datatype", tout << "occurs_check_explain " << mk_bounded_pp(app->get_owner(), get_manager()) << " <-> " << mk_bounded_pp(root->get_owner(), get_manager()) << "\n";); + enode* app_parent = nullptr; + + while (app->get_root() != root->get_root()) { + theory_var v = app->get_root()->get_th_var(get_id()); + SASSERT(v != null_theory_var); + v = m_find.find(v); + var_data * d = m_var_data[v]; + SASSERT(d->m_constructor); + if (app != d->m_constructor) + m_used_eqs.push_back(enode_pair(app, d->m_constructor)); + bool found = m_parent.find(app, app_parent); + SASSERT(found); + app = app_parent; + } + + SASSERT(app->get_root() == root->get_root()); + if (app != root) + m_used_eqs.push_back(enode_pair(app, root)); + } + + // start exploring subgraph below `app` + bool theory_datatype::occurs_check_enter(enode * app) { + oc_mark_on_stack(app); + theory_var v = app->get_root()->get_th_var(get_id()); + if (v != null_theory_var) { + v = m_find.find(v); + var_data * d = m_var_data[v]; + if (d->m_constructor) { + unsigned num_args = d->m_constructor->get_num_args(); + for (unsigned i = 0; i < num_args; i++) { + enode * arg = d->m_constructor->get_arg(i); + if (oc_cycle_free(arg)) { + return false; + } + if (oc_on_stack(arg)) { + // arg was explored before app, and is still on the stack: cycle + occurs_check_explain(app, arg); + return true; + } + // explore `arg` (with parent `app`) + if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) { + m_parent.insert(arg, app); + oc_push_stack(arg); + } + } + } + } + return false; + } + /** \brief Check if n can be reached starting from n and following equalities and constructors. For example, occur_check(a1) returns true in the following set of equalities: @@ -421,68 +472,47 @@ namespace smt { a3 = cons(v3, a1) */ bool theory_datatype::occurs_check(enode * n) { - TRACE("datatype", tout << "occurs check: #" << n->get_owner_id() << "\n";); - m_to_unmark.reset(); - m_used_eqs.reset(); - m_main = n; - bool res = occurs_check_core(m_main); - unmark_enodes(m_to_unmark.size(), m_to_unmark.c_ptr()); + TRACE("datatype", tout << "occurs check: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), get_manager()) << "\n";); + m_stats.m_occurs_check++; + + bool res = false; + oc_push_stack(n); + + // DFS traversal from `n`. Look at top element and explore it. + while (!res && !m_stack.empty()) { + stack_op op = m_stack.back().first; + enode * app = m_stack.back().second; + m_stack.pop_back(); + + if (oc_cycle_free(app)) continue; + + TRACE("datatype", tout << "occurs check loop: #" << app->get_owner_id() << " " << mk_bounded_pp(app->get_owner(), get_manager()) << (op==ENTER?" enter":" exit")<< "\n";); + + switch (op) { + case ENTER: + res = occurs_check_enter(app) || res; + break; + + case EXIT: + oc_mark_cycle_free(app); + break; + } + } + if (res) { + // m_used_eqs should contain conflict context & ctx = get_context(); region & r = ctx.get_region(); ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, nullptr, m_used_eqs.size(), m_used_eqs.c_ptr()))); - TRACE("occurs_check", + TRACE("datatype", tout << "occurs_check: true\n"; for (enode_pair const& p : m_used_eqs) { 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"; }); - } else { - oc_mark_cycle_free(n); } return res; } - - /** - \brief Auxiliary method for occurs_check. - TODO: improve performance. - */ - bool theory_datatype::occurs_check_core(enode * app) { - if (oc_cycle_free(app) || oc_explored(app)) - return false; - - m_stats.m_occurs_check++; - oc_mark_explore(app); - - TRACE("datatype", tout << "occurs check_core: #" << app->get_owner_id() << " #" << m_main->get_owner_id() << "\n";); - - theory_var v = app->get_root()->get_th_var(get_id()); - if (v != null_theory_var) { - v = m_find.find(v); - var_data * d = m_var_data[v]; - if (d->m_constructor) { - if (app != d->m_constructor) - m_used_eqs.push_back(enode_pair(app, d->m_constructor)); - unsigned num_args = d->m_constructor->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - enode * arg = d->m_constructor->get_arg(i); - if (arg->get_root() == m_main->get_root()) { - if (arg != m_main) - m_used_eqs.push_back(enode_pair(arg, m_main)); - return true; - } - if (m_util.is_datatype(get_manager().get_sort(arg->get_owner())) && occurs_check_core(arg)) - return true; - } - if (app != d->m_constructor) { - SASSERT(m_used_eqs.back().first == app); - SASSERT(m_used_eqs.back().second == d->m_constructor); - m_used_eqs.pop_back(); - } - } - } - return false; - } void theory_datatype::reset_eh() { m_trail_stack.reset(); diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index 1ccc15314..fe8396fc5 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -26,7 +26,6 @@ Revision History: #include "smt/proto_model/datatype_factory.h" namespace smt { - class theory_datatype : public theory { typedef trail_stack th_trail_stack; typedef union_find th_union_find; @@ -73,27 +72,57 @@ namespace smt { void propagate_recognizer(theory_var v, enode * r); void sign_recognizer_conflict(enode * c, enode * r); - ptr_vector m_to_unmark; - ptr_vector m_to_unmark2; - enode_pair_vector m_used_eqs; - enode * m_main; + typedef enum { ENTER, EXIT } stack_op; + typedef map, deref_eq > parent_tbl; + typedef std::pair stack_entry; - void oc_mark_explore(enode * n) { n->set_mark(); m_to_unmark.push_back(n); } - bool oc_explored(enode * n) const { n->is_marked(); } + ptr_vector m_to_unmark; + ptr_vector m_to_unmark2; + enode_pair_vector m_used_eqs; // conflict, if any + parent_tbl m_parent; // parent explanation for occurs_check + svector m_stack; // stack for DFS for occurs_check - 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 oc_mark_on_stack(enode * n) { + n = n->get_root(); + n->set_mark(); + m_to_unmark.push_back(n); } + bool oc_on_stack(enode * n) const { return n->get_root()->is_marked(); } - 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(); + void oc_mark_cycle_free(enode * n) { + n = n->get_root(); + n->set_mark2(); + m_to_unmark2.push_back(n); } + bool oc_cycle_free(enode * n) const { return n->get_root()->is_marked2(); } + + void oc_push_stack(enode * n) { + m_stack.push_back(std::make_pair(EXIT, n)); + m_stack.push_back(std::make_pair(ENTER, n)); } + // class for managing state of final_check + class final_check_st { + theory_datatype * th; + public: + final_check_st(theory_datatype * th) : th(th) { + th->m_to_unmark2.reset(); + th->m_to_unmark.reset(); + th->m_used_eqs.reset(); + th->m_stack.reset(); + th->m_parent.reset(); + } + ~final_check_st() { + unmark_enodes(th->m_to_unmark.size(), th->m_to_unmark.c_ptr()); + unmark_enodes2(th->m_to_unmark2.size(), th->m_to_unmark2.c_ptr()); + th->m_to_unmark.reset(); + th->m_to_unmark2.reset(); + th->m_stack.reset(); + th->m_parent.reset(); + } + }; + bool occurs_check(enode * n); - bool occurs_check_core(enode * n); + bool occurs_check_enter(enode * n); + void occurs_check_explain(enode * top, enode * root); void mk_split(theory_var v); From fa10e510bba1647a00807a04cb7bdff73acf0dea Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 3 Apr 2018 11:53:29 -0500 Subject: [PATCH 04/11] fix(datatype): only use pointer equality for enode_tbl --- src/smt/smt_enode.h | 7 ------- src/smt/theory_datatype.h | 2 +- 2 files changed, 1 insertion(+), 8 deletions(-) diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index ba13a31bb..df6309424 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -171,9 +171,6 @@ namespace smt { m_interpreted = true; } - inline bool equal(const enode & other) const { - return m_owner == other.m_owner; - } void del_eh(ast_manager & m, bool update_children_parent = true); @@ -426,9 +423,5 @@ namespace smt { }; -inline bool operator==(const smt::enode & e1, const smt::enode & e2) { - return e1.equal(e2); -} - #endif /* SMT_ENODE_H_ */ diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index fe8396fc5..4dc99f774 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -73,7 +73,7 @@ namespace smt { void sign_recognizer_conflict(enode * c, enode * r); typedef enum { ENTER, EXIT } stack_op; - typedef map, deref_eq > parent_tbl; + typedef map, ptr_eq > parent_tbl; typedef std::pair stack_entry; ptr_vector m_to_unmark; From e535cad48004e027f97f1d37bf341c61ec4eab4b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 3 Apr 2018 12:12:09 -0500 Subject: [PATCH 05/11] chore(datatype): small improvements --- src/smt/theory_datatype.cpp | 2 +- src/smt/theory_datatype.h | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index b3c6ffadf..fb817502b 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -393,7 +393,7 @@ namespace smt { for (int v = 0; v < num_vars; v++) { if (v == static_cast(m_find.find(v))) { enode * node = get_enode(v); - if (occurs_check(node)) { + if (!oc_cycle_free(node) && occurs_check(node)) { // conflict was detected... // return... return FC_CONTINUE; diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index 4dc99f774..29799910b 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -104,8 +104,8 @@ namespace smt { theory_datatype * th; public: final_check_st(theory_datatype * th) : th(th) { - th->m_to_unmark2.reset(); th->m_to_unmark.reset(); + th->m_to_unmark2.reset(); th->m_used_eqs.reset(); th->m_stack.reset(); th->m_parent.reset(); @@ -115,6 +115,7 @@ namespace smt { unmark_enodes2(th->m_to_unmark2.size(), th->m_to_unmark2.c_ptr()); th->m_to_unmark.reset(); th->m_to_unmark2.reset(); + th->m_used_eqs.reset(); th->m_stack.reset(); th->m_parent.reset(); } From 433f487ff2d2dcb8d4c4427169b46e8db3b34c82 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 3 Apr 2018 18:30:09 -0500 Subject: [PATCH 06/11] fix(datatype): always use root nodes for the `parent` table --- src/smt/theory_datatype.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index fb817502b..68ebb60e6 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -424,7 +424,7 @@ namespace smt { SASSERT(d->m_constructor); if (app != d->m_constructor) m_used_eqs.push_back(enode_pair(app, d->m_constructor)); - bool found = m_parent.find(app, app_parent); + bool found = m_parent.find(app->get_root(), app_parent); SASSERT(found); app = app_parent; } @@ -455,7 +455,7 @@ namespace smt { } // explore `arg` (with parent `app`) if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) { - m_parent.insert(arg, app); + m_parent.insert(arg->get_root(), app); oc_push_stack(arg); } } From d973b0824745ba97ebeb0259d250cc1ad78a4899 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 4 Apr 2018 10:41:40 -0500 Subject: [PATCH 07/11] fix(datatypes): update following @nikolajbjorner 's review --- src/smt/theory_datatype.cpp | 5 ++--- src/smt/theory_datatype.h | 4 ++-- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 68ebb60e6..e21067a56 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -412,7 +412,7 @@ namespace smt { } // explain the cycle root -> … -> app -> root - void theory_datatype::occurs_check_explain(enode * app, enode * const root) { + void theory_datatype::occurs_check_explain(enode * app, enode * root) { TRACE("datatype", tout << "occurs_check_explain " << mk_bounded_pp(app->get_owner(), get_manager()) << " <-> " << mk_bounded_pp(root->get_owner(), get_manager()) << "\n";); enode* app_parent = nullptr; @@ -424,8 +424,7 @@ namespace smt { SASSERT(d->m_constructor); if (app != d->m_constructor) m_used_eqs.push_back(enode_pair(app, d->m_constructor)); - bool found = m_parent.find(app->get_root(), app_parent); - SASSERT(found); + app_parent = m_parent[app->get_root()]; app = app_parent; } diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index 29799910b..77da52360 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -104,8 +104,8 @@ namespace smt { theory_datatype * th; public: final_check_st(theory_datatype * th) : th(th) { - th->m_to_unmark.reset(); - th->m_to_unmark2.reset(); + SASSERT(th->m_to_unmark.empty()); + SASSERT(th->m_to_unmark2.empty()); th->m_used_eqs.reset(); th->m_stack.reset(); th->m_parent.reset(); From bf6928fec0bfa273201ecc6d3c0f07706e82a9b5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 6 Apr 2018 11:13:53 -0500 Subject: [PATCH 08/11] fix(datatypes): additional explanation in occurs_check --- src/smt/theory_datatype.cpp | 36 +++++++++++++++++++++++++++++------- src/smt/theory_datatype.h | 1 + 2 files changed, 30 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index e21067a56..f17bdc3d6 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -411,19 +411,41 @@ namespace smt { return r; } + // Assuming `app` is equal to a constructor term, return the constructor enode + inline enode * theory_datatype::oc_get_cstor(enode * app) { + theory_var v = app->get_root()->get_th_var(get_id()); + SASSERT(v != null_theory_var); + v = m_find.find(v); + var_data * d = m_var_data[v]; + SASSERT(d->m_constructor); + return d->m_constructor; + } + // explain the cycle root -> … -> app -> root void theory_datatype::occurs_check_explain(enode * app, enode * root) { TRACE("datatype", tout << "occurs_check_explain " << mk_bounded_pp(app->get_owner(), get_manager()) << " <-> " << mk_bounded_pp(root->get_owner(), get_manager()) << "\n";); enode* app_parent = nullptr; + // first: explain that root=v, given that app=cstor(…,v,…) + { + enode * app_cstor = oc_get_cstor(app); + unsigned n_args_app = app_cstor->get_num_args(); + for (unsigned i=0; i < n_args_app; ++i) { + enode * arg = app_cstor->get_arg(i); + // found an argument which is equal to root + if (arg->get_root() == root->get_root()) { + if (arg != root) + m_used_eqs.push_back(enode_pair(arg, root)); + break; + } + } + } + + // now explain app=cstor(…,v,…) where v=root, and recurse with parent of app while (app->get_root() != root->get_root()) { - theory_var v = app->get_root()->get_th_var(get_id()); - SASSERT(v != null_theory_var); - v = m_find.find(v); - var_data * d = m_var_data[v]; - SASSERT(d->m_constructor); - if (app != d->m_constructor) - m_used_eqs.push_back(enode_pair(app, d->m_constructor)); + enode * app_cstor = oc_get_cstor(app); + if (app != app_cstor) + m_used_eqs.push_back(enode_pair(app, app_cstor)); app_parent = m_parent[app->get_root()]; app = app_parent; } diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index 77da52360..020949296 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -121,6 +121,7 @@ namespace smt { } }; + enode * oc_get_cstor(enode * n); bool occurs_check(enode * n); bool occurs_check_enter(enode * n); void occurs_check_explain(enode * top, enode * root); From 8fd2d8a636b65ca9e5d13bcc7f327e34ec40a09f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 6 Apr 2018 15:56:05 -0500 Subject: [PATCH 09/11] chore(datatype): small fixes --- src/smt/theory_datatype.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index f17bdc3d6..825856e37 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -452,7 +452,7 @@ namespace smt { SASSERT(app->get_root() == root->get_root()); if (app != root) - m_used_eqs.push_back(enode_pair(app, root)); + m_used_eqs.push_back(enode_pair(app, root)); } // start exploring subgraph below `app` @@ -511,7 +511,7 @@ namespace smt { switch (op) { case ENTER: - res = occurs_check_enter(app) || res; + res = occurs_check_enter(app); break; case EXIT: From ac881d949d69db7bf83df9dd861526f64c5a3deb Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 6 Apr 2018 17:19:06 -0500 Subject: [PATCH 10/11] style(datatype): use modern iteration --- src/smt/theory_datatype.cpp | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 825856e37..147067d61 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -429,9 +429,7 @@ namespace smt { // first: explain that root=v, given that app=cstor(…,v,…) { enode * app_cstor = oc_get_cstor(app); - unsigned n_args_app = app_cstor->get_num_args(); - for (unsigned i=0; i < n_args_app; ++i) { - enode * arg = app_cstor->get_arg(i); + for (enode * arg : enode::args(app_cstor)) { // found an argument which is equal to root if (arg->get_root() == root->get_root()) { if (arg != root) @@ -463,9 +461,7 @@ namespace smt { v = m_find.find(v); var_data * d = m_var_data[v]; if (d->m_constructor) { - unsigned num_args = d->m_constructor->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - enode * arg = d->m_constructor->get_arg(i); + for (enode * arg : enode::args(d->m_constructor)) { if (oc_cycle_free(arg)) { return false; } From 66b85e000b419ba414939eeb9fa4e146bbebdfd0 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 7 Apr 2018 01:25:19 -0500 Subject: [PATCH 11/11] fix in occurs_check (early exit) --- src/smt/theory_datatype.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 147067d61..da18460f4 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -463,7 +463,7 @@ namespace smt { if (d->m_constructor) { for (enode * arg : enode::args(d->m_constructor)) { if (oc_cycle_free(arg)) { - return false; + continue; } if (oc_on_stack(arg)) { // arg was explored before app, and is still on the stack: cycle