| 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 :)
|
| |
|
|
|
|
|
|
| |
Based on an issue noted by Chris with redundancy removal resuls being dependent
on the order of the terms. Interestingly, one of our tests already had an
instance of that problem.
Also fix the issue with nested quantifiers getting redundant triggers.
|
| | |
|
| |
|
|
| |
This fixes a bug that affected Monad.dfy
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
The idea is that we define an partial order on triggers (which may contain
multiple terms), and find all the maximal elements. The algorithm as
implemented is rather inefficient; in particular, is does not look at the
structure of the graph of the relation (thus is does many redundant
comparisons). See triggers/useless-triggers-are-removed.dfy for an example
where such a filter is useful.
|
| |
|
|
| |
This indentation is just needed by CLI-based clients
|
| | |
|
| | |
|
| |
|
|
|
| |
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)
|
| |
|
|
|
|
| |
The new 'quantifiers' list keeps track of the quantifiers that have already been
seen, so that they are not added both as a member of a collection and as a
single quantifier.
|
| | |
|
| |
|
|
|
| |
This allows it to report the source of the error, giving better feedback to the
user about which precondition to a function failed to hold, for example.
|
| | |
|
| |
|
|
|
| |
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 is useful because trigger-related messages can contain quite a bit of
information, especially if they include info about multiple split quantifiers.
|
| |
|
|
|
|
|
|
|
| |
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