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