Handle additional cases in rule_properties::check_accessor

[wert310]

This PR adds additional safe accessor patterns to the previously accepted ones.

Instead of only allowing guarded accessors, this patch allows for an accessor to be used unguarded if all other recognizers are used in the other paths (so the only possible value at that point of the expression is the last remaining constructor). These new accepted patterns should cover all possible ways a match expression is desugared:

• guarded branch with correct recognizer (as before)
• if all other recognizes have been used negated in a rule the remaining unguarded accessor is safe
• and: if all branches except for one have negated recognizers, then the remaining one is safe
• or: if all branches except for one have recognizers the remaining one is safe
• or: if one branch has a negated recognizer (for the current case) access in another branch is safe
• ite: if the recognizer is in the condition, access in "then" branch is safe; the "else" branch is safe if all recognizers except for one have been used in the condition of an ite in the path to the current accessor
• any combination of the above

This PR improves the fix of #4869 by allowing pattern matching expressions where the last branch accesses the constructor arguments. The previous version of check_accessor incorrectly returned false for the example of #4869 if the cases of the match expression are swapped:

(define-fun getValueDefault ((opt OptionInt) (default Int)) Int
 (match opt
  ((NoneInt default)
   ((SomeInt int) int))))

In that example, the match is desugared as:

(ite ((_ is (NoneInt () OptionInt)) (:var 0)) (:var 2) (valueInt (:var 0)))

where (valueInt (:var 0)) is a safe (but unguarded) accessor because it is in the else branch and it is the only remaining constructor. The previous check would not allow this accessor because it is unguarded.

(Edit: clarified second case in the above list)

[ghost]

All CLA requirements met.

[hgvk94]

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

[wert310]

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.

[hgvk94]

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.

[NikolajBjorner]

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)

[NikolajBjorner]

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)....

[NikolajBjorner]

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.

[wert310]

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?

[wert310]

Thanks for your comments!

I've modified the loop to do a full depth first search over all parents, keeping track of the size of the ctors array across each expression (so that I can remove the elements when backtracking). The search starts with ctors containing all global constructors, then for each path it should contain only the "local" constructors.

I'm using an std::tuple in the todo stack to avoid creating multiple vectors/maps. In particular I use the last element of the tuple to keep track of the visited nodes in the tree. I noticed that elsewhere in the code you are using an ast_mark: do you prefer that I edit the current solution to use an additional ast_mark for consistency, or is this solution ok?