mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

add marker for top-level expression in rule.

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-24 15:20:44 +01:00
parent 61ab72b6a3
commit f639a7e1bc
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/muz/base/rule_properties.cpp
View file

@ -222,6 +222,7 @@ bool rule_properties::check_accessor(app* n) {
to_app(t)->get_arg(0) == n->get_arg(0) &&
m_dt.get_recognizer_constructor(to_app(t)->get_decl()) == c;
};
auto is_recognizer = [&](expr* t) {
if (m.is_and(t))
for (expr* arg : *to_app(t))
@ -240,6 +241,7 @@ bool rule_properties::check_accessor(app* n) {
obj_map<expr, ptr_vector<expr>> use_list;
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<expr>()).push_back(nullptr); // add marker for top-level expression.
for (expr* sub : subterms::all(expr_ref(t, m)))
if (is_app(sub))
for (expr* arg : *to_app(sub))
@ -254,6 +256,8 @@ 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)))