Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Handle additional cases in rule_properties::check_accessor #5821

Merged
merged 2 commits into from
Mar 7, 2022
Merged

Handle additional cases in rule_properties::check_accessor #5821

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5e0e2cc
Handle additional cases in rule_properties::check_accessor
wert310 Feb 7, 2022
dda2002
Walk parents depth first in rule_properties::check_accessor
wert310 Feb 11, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
74 changes: 60 additions & 14 deletions src/muz/base/rule_properties.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<expr> 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))
Expand All @@ -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<expr, ptr_vector<expr>> use_list;
Expand All @@ -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<func_decl> 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<func_decl> 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)))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Leaves some room as the ite condition could be conjunctive. So an abstraction of this test could be to extract 'must' recognizers from an expression. Overall, a more satisfactory approach would address complete patterns for nested cases which this code doesn't address.

match (x, y) with
    a::as, [] -> 
    [], b::bs -> 
    [], [] -> 
    _, _ -> body with hd(x), tl(y)....

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is another bug: e could be in both branches of the ite.
Then checking that it is in the if-branch and continuing masks that it is in the else branch.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Leaves some room as the ite condition could be conjunctive

If I understand correctly, the smtlib match syntax disallows nested patterns Sec 3.6.1, Remark 4 of SMT-LIB 2.6 Standard. So such a pattern matching expression would not be possible unless it is desugared "externally" into ites with conjunctive conditions.

In our WebSpec project, we compile nested patterns into nested smtlib match expressions, so we handle this case by first desugaring it into standard smtlib expressions and then run Z3.

Does Z3 support nested patterns by creating a match expression using another frontend/API?

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)))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This allows formulas like (==> (is_cons x) (= y (tail x)) . I don’t consider this guarded because the second literal could be set to true even when the first is set to false. Please comment on why this is considered guarded.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this should be fine. It is de-morgan dual to conjunction and context based.
dually, there could be a conjunction (not (and (is_cons x) (not (= y (tail x))))
The context-sensitive analysis determines that the conjunction is true only if (is_cons x)

goto _continue;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the goto really required? It looks to me that you can just use continue

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I need to skip the todo.push_back, so just continue from the inner for is not enough.
I'm not really happy about using goto, to remove it I could:

  1. use std::any_of and continue 
    if (m.is_or(parent)) {
    for (expr* arg : *to_app(parent))
        add_recognizer(arg);
    if (std::any_of(to_app(parent)->begin(), to_app(parent)->end(),
                    [&](expr *arg) { return m.is_not(arg, arg) && is_recognizer(arg); }))
        continue;
}
    But this would loop twice over args
  2. use a boolean flag and then continue if the flag is true
  3. include the "or not" case in is_recognizer

Probably (1) is the cleaner one, even if it requires an additional loop/lambda.
I noticed that goto is used more than std::any_of in the codebase, so let me know which one you prefer for consistency.

}
}
}
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) {
Expand Down