| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
as candidates for triggers.
|
| |
|
|
| |
collectors.
|
| |
|
|
|
| |
need exclude the private terms (the ones that includes the quantifier expr's bv)
from it exported terms.
|
| | |
|
| |
|
|
|
| |
Mismatches are now allowed up to expressions not involving any of the bound
variables of the quantifier under inspection.
|
| |
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
| |
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 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.
|
qunyanm
Clément Pit--Claudel