diff options
author | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-14 17:38:08 -0700 |
---|---|---|
committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-14 17:38:08 -0700 |
commit | a07b43ac03b38d4af575d1a1df48339ad228751a (patch) | |
tree | 0949d29186e9fdb9ee8caaefebe4653ac24bbedb /Source/Dafny/Rewriter.cs | |
parent | 22a997192baf246bd86031f319aac154c2ec05cb (diff) |
Start committing 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.
Diffstat (limited to 'Source/Dafny/Rewriter.cs')
-rw-r--r-- | Source/Dafny/Rewriter.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 0798510a..2c00e203 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -43,9 +43,9 @@ namespace Microsoft.Dafny Contract.Requires(reporter != null);
}
- internal override void PostResolve(ModuleDefinition m) {
+ internal override void PostCyclicityResolve(ModuleDefinition m) {
var finder = new Triggers.QuantifierCollectionsFinder(reporter);
-
+
foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
if (decl is Function) {
var function = (Function)decl;
|