summaryrefslogtreecommitdiff
path: root/Source/Dafny/Triggers/TriggersCollector.cs
Commit message (Expand)AuthorAge
* Fix issue 124. Consider math operators that later turned into function callsGravatar qunyanm2016-02-08
* Fix issue 114. Do not export private terms for ComprehensionExpr in triggerGravatar qunyanm2015-12-08
* Fix issue 99. When annotate a quantifier expr that has a SplitQuantifier, weGravatar qunyanm2015-11-06
* Tiny cleanup in TriggersCollectorGravatar Clément Pit--Claudel2015-08-27
* Further relax the loop detection conditionsGravatar Clément Pit--Claudel2015-08-27
* Improve the redundancy detection algorithm used while constructing sets of termsGravatar Clément Pit--Claudel2015-08-26
* Allow MultiSelectExpr as quantifier headsGravatar Clément Pit--Claudel2015-08-23
* Make `old` a special case for trigger generation.Gravatar Clément Pit--Claudel2015-08-21
* Allow display expressions as trigger termsGravatar Clément Pit--Claudel2015-08-21
* Cleanup a number of FIXMEs that I had left in the codeGravatar Clément Pit--Claudel2015-08-20
* Implement the SelectTrigger method, removing redundant triggers.Gravatar Clément Pit--Claudel2015-08-20
* Print matches for triggers as they appear in the bufferGravatar Clément Pit--Claudel2015-08-19
* Collect ApplyExpr nodes when looking for trigger candidatesGravatar Clément Pit--Claudel2015-08-19
* Small cleanups, fixes, and refactoringsGravatar Clément Pit--Claudel2015-08-18
* Start committing split quantifiersGravatar Clément Pit--Claudel2015-08-14
* Implement self-loop detectionGravatar Clément Pit--Claudel2015-08-14
* Draft out a more advanced version of trigger generationGravatar Clément Pit--Claudel2015-08-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 16:49:37 +0000