| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
Mismatches are now allowed up to expressions not involving any of the bound
variables of the quantifier under inspection.
|
| |
|
|
| |
Again, spotted by Chris :)
|
| | |
|
| |
|
|
|
|
| |
Old is particular, because in old(g(f(x))), the triggers are old(g(x)) and
old(f(x)). This has a number of implications; see the new tests files for more
information.
|
| |
|
|
|
| |
Triggers themselves, however, are printed exactly as used. For example, a term
(x !in s) yields a trigger (x in s).
|
| |
|
|
| |
(compare by value, not by reference to boxed value)
|
| |
|
|
|
| |
In particular, start detecting loops between terms that don't look like each
other at the Dafny level, such as {a[x]} and {x in a} (when a is a multiset)
|
| |
|
|
|
|
|
|
|
| |
This requires rewriting the parts of the AST that contain these quantifiers. We
unfortunately don't have facilities to do such rewrites at the moment (and there
are loops in the AST, so it would be hard to write such a facility). As a
workaround, this commit introduces a field in quantifier expressions,
SplitQuantifiers. Code that manipulate triggers is expected to look for this
field, and ignore the other fields if that one is found.
|
| |
|
|
|
|
|
|
|
|
| |
Implementing loop detection between multiple triggers is much harder, as it
seems to require walking an exponentially sized graph. Self-loop detection is
still a net gain compared to the current situation: we used to not detect loops
in large quantifiers; not we break these apart, suppress the loops where we can
in the smaller parts, and report the ones that we can't suppress. It could be
that the broken-up quantifiers are mutually recursive, but these cases would
have already led to a loop in the past.
|
|
|
This new version will include a cleaner pipeline, and trigger splitting.
|
Clément Pit--Claudel