From 5e0e2cc6dac099262f308018bafb45d1b83b7068 Mon Sep 17 00:00:00 2001 From: wert310 <310wert@gmail.com> Date: Mon, 7 Feb 2022 14:57:06 +0100 Subject: [PATCH 1/2] Handle additional cases in rule_properties::check_accessor --- src/muz/base/rule_properties.cpp | 74 ++++++++++++++++++++++++++------ 1 file changed, 60 insertions(+), 14 deletions(-) diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 991ca716eee..eb89d2c4279 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -210,19 +210,19 @@ bool rule_properties::check_accessor(app* n) { SASSERT(m_dt.is_datatype(s)); if (m_dt.get_datatype_constructors(s)->size() <= 1) return true; - func_decl* f = n->get_decl(); func_decl * c = m_dt.get_accessor_constructor(f); unsigned ut_size = m_rule->get_uninterpreted_tail_size(); unsigned t_size = m_rule->get_tail_size(); + ptr_vector recognizers; auto is_recognizer_base = [&](expr* t) { return m_dt.is_recognizer(t) && to_app(t)->get_arg(0) == n->get_arg(0) && m_dt.get_recognizer_constructor(to_app(t)->get_decl()) == c; }; - + // t is a recognizer for n auto is_recognizer = [&](expr* t) { if (m.is_and(t)) for (expr* arg : *to_app(t)) @@ -231,11 +231,13 @@ bool rule_properties::check_accessor(app* n) { return is_recognizer_base(t); }; - - for (unsigned i = ut_size; i < t_size; ++i) - if (is_recognizer(m_rule->get_tail(i))) + for (unsigned i = ut_size; i < t_size; ++i) { + auto *tail = m_rule->get_tail(i); + if (is_recognizer(tail)) return true; - + if (m.is_not(tail) && m_dt.is_recognizer(to_app(tail)->get_arg(0))) + recognizers.push_back(to_app(tail)->get_arg(0)); + } // create parent use list for every sub-expression in the rule obj_map> use_list; @@ -256,18 +258,62 @@ bool rule_properties::check_accessor(app* n) { if (!use_list.contains(e)) return false; for (expr* parent : use_list[e]) { - if (!parent) - return false; // top-level expressions are not guarded - if (is_recognizer(parent)) - continue; - if (m.is_ite(parent) && to_app(parent)->get_arg(1) == e && is_recognizer(to_app(parent)->get_arg(0))) + if (!parent) { // top-level expression + // check if n is an unguarded "else" branch + ptr_vector ctors; + for (auto *rc : recognizers) + if (to_app(rc)->get_arg(0) == n->get_arg(0)) + ctors.push_back(m_dt.get_recognizer_constructor(to_app(rc)->get_decl())); + ptr_vector diff; + for (auto *dtc : *m_dt.get_datatype_constructors(s)) + if (std::find(ctors.begin(), ctors.end(), dtc) == ctors.end()) + diff.push_back(dtc); + // the only unguarded constructor for s is c: + // all the others are guarded and we are in an "else" branch so the accessor is safe + if (diff.size() == 1 && diff[0] == c) + continue; + return false; // the accessor is not safe + } + if (is_recognizer_base(parent)) continue; - todo.push_back(parent); + if (m.is_ite(parent)) { + if (to_app(parent)->get_arg(1) == e && is_recognizer(to_app(parent)->get_arg(0))) + continue; // e is guarded + else + if (m_dt.is_recognizer(to_app(parent)->get_arg(0))) + recognizers.push_back(to_app(parent)->get_arg(0)); // e is in the else branch of the ite + } + if (m.is_or(parent)) { + for (expr *arg : *to_app(parent)) { + // if all branches are guarded the remaining one might be safe + if (m_dt.is_recognizer(arg)) + recognizers.push_back(arg); + // if one branch is not(recognizer) then the accessor is safe + if (m.is_not(arg)) { + if (is_recognizer(to_app(arg)->get_arg(0))) + goto _continue; + } + } + } + if (m.is_and(parent)) { + for (expr *arg : *to_app(parent)) { + // if one branch is guarded the accessor is safe + if (is_recognizer(arg)) + goto _continue; + // if all branches are not(recognizer) the remaining one might be safe + if (m.is_not(arg)) { + auto *neg_rec = to_app(arg)->get_arg(0); + if (m_dt.is_recognizer(neg_rec)) + recognizers.push_back(neg_rec); + } + } + } + todo.push_back(parent); + _continue:; } } - + return true; - } void rule_properties::operator()(app* n) { From dda20025e1a69c01afc5003ad30e236e1f32cff0 Mon Sep 17 00:00:00 2001 From: wert310 <310wert@gmail.com> Date: Fri, 11 Feb 2022 12:10:57 +0100 Subject: [PATCH 2/2] Walk parents depth first in rule_properties::check_accessor --- src/muz/base/rule_properties.cpp | 101 ++++++++++++++++--------------- 1 file changed, 53 insertions(+), 48 deletions(-) diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index eb89d2c4279..7632a0c2fa4 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -212,17 +212,33 @@ bool rule_properties::check_accessor(app* n) { return true; func_decl* f = n->get_decl(); - func_decl * c = m_dt.get_accessor_constructor(f); + func_decl* c = m_dt.get_accessor_constructor(f); unsigned ut_size = m_rule->get_uninterpreted_tail_size(); unsigned t_size = m_rule->get_tail_size(); - ptr_vector recognizers; + ptr_vector ctors; + + // add recognizer constructor to ctors + auto add_recognizer = [&](expr* r) { + if (!m_dt.is_recognizer(r)) + return; + if (n->get_arg(0) != to_app(r)->get_arg(0)) + return; + auto* c2 = m_dt.get_recognizer_constructor(to_app(r)->get_decl()); + if (c == c2) + return; + ctors.push_back(c2); + }; + auto add_not_recognizer = [&](expr* r) { + if (m.is_not(r, r)) + add_recognizer(r); + }; + // t is a recognizer for n auto is_recognizer_base = [&](expr* t) { return m_dt.is_recognizer(t) && to_app(t)->get_arg(0) == n->get_arg(0) && m_dt.get_recognizer_constructor(to_app(t)->get_decl()) == c; }; - // t is a recognizer for n auto is_recognizer = [&](expr* t) { if (m.is_and(t)) for (expr* arg : *to_app(t)) @@ -232,11 +248,10 @@ bool rule_properties::check_accessor(app* n) { }; for (unsigned i = ut_size; i < t_size; ++i) { - auto *tail = m_rule->get_tail(i); + auto* tail = m_rule->get_tail(i); if (is_recognizer(tail)) return true; - if (m.is_not(tail) && m_dt.is_recognizer(to_app(tail)->get_arg(0))) - recognizers.push_back(to_app(tail)->get_arg(0)); + add_not_recognizer(tail); } // create parent use list for every sub-expression in the rule @@ -244,29 +259,32 @@ bool rule_properties::check_accessor(app* n) { for (unsigned i = ut_size; i < t_size; ++i) { app* t = m_rule->get_tail(i); use_list.insert_if_not_there(t, ptr_vector()).push_back(nullptr); // add marker for top-level expression. - for (expr* sub : subterms::all(expr_ref(t, m))) + for (expr* sub : subterms::all(expr_ref(t, m))) if (is_app(sub)) for (expr* arg : *to_app(sub)) use_list.insert_if_not_there(arg, ptr_vector()).push_back(sub); } - // walk parents of n to check that each path is guarded by a recognizer. - ptr_vector todo; - todo.push_back(n); - for (unsigned i = 0; i < todo.size(); ++i) { - expr* e = todo[i]; + // walk parents of n depth first to check that each path is guarded by a recognizer. + vector> todo; + todo.push_back({n, ctors.size(), false}); + while(!todo.empty()) { + auto [e, ctors_size, visited] = todo.back(); + if (visited) { + todo.pop_back(); + while (ctors.size() > ctors_size) ctors.pop_back(); + continue; + } + std::get<2>(todo.back()) = true; // set visited + if (!use_list.contains(e)) return false; for (expr* parent : use_list[e]) { if (!parent) { // top-level expression // check if n is an unguarded "else" branch - ptr_vector ctors; - for (auto *rc : recognizers) - if (to_app(rc)->get_arg(0) == n->get_arg(0)) - ctors.push_back(m_dt.get_recognizer_constructor(to_app(rc)->get_decl())); ptr_vector diff; - for (auto *dtc : *m_dt.get_datatype_constructors(s)) - if (std::find(ctors.begin(), ctors.end(), dtc) == ctors.end()) + for (auto* dtc : *m_dt.get_datatype_constructors(s)) + if (!ctors.contains(dtc)) diff.push_back(dtc); // the only unguarded constructor for s is c: // all the others are guarded and we are in an "else" branch so the accessor is safe @@ -274,41 +292,28 @@ bool rule_properties::check_accessor(app* n) { continue; return false; // the accessor is not safe } - if (is_recognizer_base(parent)) + if (is_recognizer(parent)) continue; - if (m.is_ite(parent)) { - if (to_app(parent)->get_arg(1) == e && is_recognizer(to_app(parent)->get_arg(0))) - continue; // e is guarded - else - if (m_dt.is_recognizer(to_app(parent)->get_arg(0))) - recognizers.push_back(to_app(parent)->get_arg(0)); // e is in the else branch of the ite - } - if (m.is_or(parent)) { - for (expr *arg : *to_app(parent)) { - // if all branches are guarded the remaining one might be safe - if (m_dt.is_recognizer(arg)) - recognizers.push_back(arg); - // if one branch is not(recognizer) then the accessor is safe - if (m.is_not(arg)) { - if (is_recognizer(to_app(arg)->get_arg(0))) - goto _continue; - } + + expr *cnd, *thn, *els; + if (m.is_ite(parent, cnd, thn, els)) { + if (thn == e) { + if (is_recognizer(cnd) && els != e) + continue; // e is guarded } + add_recognizer(cnd); } - if (m.is_and(parent)) { - for (expr *arg : *to_app(parent)) { - // if one branch is guarded the accessor is safe - if (is_recognizer(arg)) + if (m.is_and(parent)) + for (expr* arg : *to_app(parent)) + add_not_recognizer(arg); + if (m.is_or(parent)) + for (expr* arg : *to_app(parent)) { + add_recognizer(arg); + // if one branch is not(recognizer) then the accessor is safe + if (m.is_not(arg, arg) && is_recognizer(arg)) goto _continue; - // if all branches are not(recognizer) the remaining one might be safe - if (m.is_not(arg)) { - auto *neg_rec = to_app(arg)->get_arg(0); - if (m_dt.is_recognizer(neg_rec)) - recognizers.push_back(neg_rec); - } } - } - todo.push_back(parent); + todo.push_back({parent, ctors.size(), false}); _continue:; } }