Merge

41 files changed, 768 insertions, 144 deletions

diff --git a/Source/Dafny.sln b/Source/Dafny.sln
index db035b4a..3e71a2a4 100644
--- a/Source/Dafny.sln
+++ b/Source/Dafny.sln
@@ -6,6 +6,9 @@ EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyPipeline", "Dafny\DafnyPipeline.csproj", "{FE44674A-1633-4917-99F4-57635E6FA740}"

 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyServer", "DafnyServer\DafnyServer.csproj", "{AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}"

+	ProjectSection(ProjectDependencies) = postProject

+		{FE44674A-1633-4917-99F4-57635E6FA740} = {FE44674A-1633-4917-99F4-57635E6FA740}

+	EndProjectSection

 EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index d78ae170..5943e8e4 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -7764,6 +7764,33 @@ namespace Microsoft.Dafny {
     public void Visit(IEnumerable<MaybeFreeExpression> exprs) {

       exprs.Iter(Visit);

     }

+    public void Visit(IEnumerable<FrameExpression> exprs) {

+      exprs.Iter(Visit);

+    }

+    public void Visit(ICallable decl) {

+      if (decl is Function) {

+        Visit((Function)decl);

+      } else if (decl is Method) {

+        Visit((Method)decl);

+      }

+      //FIXME More?

+    }

+    public void Visit(Method method) {

+      Visit(method.Ens);

+      Visit(method.Req);

+      Visit(method.Mod.Expressions);

+      Visit(method.Decreases.Expressions);

+      if (method.Body != null) { Visit(method.Body); }

+      //FIXME More?

+    }

+    public void Visit(Function function) {

+      Visit(function.Ens);

+      Visit(function.Req);

+      Visit(function.Reads);

+      Visit(function.Decreases.Expressions);

+      if (function.Body != null) { Visit(function.Body); }

+      //FIXME More?

+    }

     protected virtual void VisitOneExpr(Expression expr) {

       Contract.Requires(expr != null);

       // by default, do nothing

@@ -7810,6 +7837,33 @@ namespace Microsoft.Dafny {
     public void Visit(IEnumerable<MaybeFreeExpression> exprs, State st) {

       exprs.Iter(e => Visit(e, st));

     }

+    public void Visit(IEnumerable<FrameExpression> exprs, State st) {

+      exprs.Iter(e => Visit(e, st));

+    }

+    public void Visit(ICallable decl, State st) {

+      if (decl is Function) {

+        Visit((Function)decl, st);

+      } else if (decl is Method) {

+        Visit((Method)decl, st);

+      }

+      //FIXME More?

+    }

+    public void Visit(Method method, State st) {

+      Visit(method.Ens, st);

+      Visit(method.Req, st);

+      Visit(method.Mod.Expressions, st);

+      Visit(method.Decreases.Expressions, st);

+      if (method.Body != null) { Visit(method.Body, st); }

+      //FIXME More?

+    }

+    public void Visit(Function function, State st) {

+      Visit(function.Ens, st);

+      Visit(function.Req, st);

+      Visit(function.Reads, st);

+      Visit(function.Decreases.Expressions, st);

+      if (function.Body != null) { Visit(function.Body, st); }

+      //FIXME More?

+    }

     /// <summary>

     /// Visit one expression proper.  This method is invoked before it is invoked on the

     /// sub-parts (sub-expressions and sub-statements).  A return value of "true" says to

diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs
index c3797574..4cfbf20e 100644
--- a/Source/Dafny/Reporting.cs
+++ b/Source/Dafny/Reporting.cs
@@ -34,21 +34,14 @@ namespace Microsoft.Dafny {
       AllMessages[ErrorLevel.Info] = new List<ErrorMessage>();

     }

 

-    protected bool ShouldDiscard(MessageSource source, ErrorLevel level) {

-      return ((ErrorsOnly && level != ErrorLevel.Error) ||

-              (!DafnyOptions.O.PrintTooltips && level == ErrorLevel.Info));

-    }

-

     // This is the only thing that needs to be overriden

     public virtual bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {

-      var discard = ShouldDiscard(source, level);

-

+      bool discard = (ErrorsOnly && level != ErrorLevel.Error) || // Discard non-errors if ErrorsOnly is set

+                     (tok is TokenWrapper && !(tok is NestedToken)); // Discard wrapped tokens, except for nested ones

       if (!discard) {

         AllMessages[level].Add(new ErrorMessage { token = tok, message = msg });

-        return true;

       }

-

-      return false;

+      return !discard;

     }

 

     public int Count(ErrorLevel level) {

@@ -122,15 +115,15 @@ namespace Microsoft.Dafny {
       Info(source, tok, String.Format(msg, args));

     }

 

-    public string ErrorToString(ErrorLevel header, IToken tok, string msg) {

+    public static string ErrorToString(ErrorLevel header, IToken tok, string msg) {

       return ErrorToString_Internal(": " + header.ToString(), tok.filename, tok.line, tok.col, ": " + msg);

     }

 

-    public string ErrorToString(ErrorLevel header, string filename, int oneBasedLine, int oneBasedColumn, string msg) {

+    public static string ErrorToString(ErrorLevel header, string filename, int oneBasedLine, int oneBasedColumn, string msg) {

       return ErrorToString_Internal(": " + header.ToString(), filename, oneBasedLine, oneBasedColumn, ": " + msg);

     }

 

-    public string ErrorToString_Internal(string header, string filename, int oneBasedLine, int oneBasedColumn, string msg) {

+    public static string ErrorToString_Internal(string header, string filename, int oneBasedLine, int oneBasedColumn, string msg) {

       return String.Format("{0}({1},{2}){3}{4}", filename, oneBasedLine, oneBasedColumn - 1, header, msg ?? "");

     }

   }

@@ -150,7 +143,10 @@ namespace Microsoft.Dafny {
     }

 

     public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {

-      if (base.Message(source, level, tok, msg)) {

+      if (base.Message(source, level, tok, msg) && (DafnyOptions.O.PrintTooltips || level != ErrorLevel.Info)) {

+        // Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI

+        msg = msg.Replace(Environment.NewLine, Environment.NewLine + " ");

+

         ConsoleColor previousColor = Console.ForegroundColor;

         Console.ForegroundColor = ColorForLevel(level);

         Console.WriteLine(ErrorToString(level, tok, msg));

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 83f49a12..230d9349 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -47,21 +47,7 @@ namespace Microsoft.Dafny
       var finder = new Triggers.QuantifierCollector(reporter);

         

       foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {

-        if (decl is Function) {

-          var function = (Function)decl;

-          finder.Visit(function.Ens, null);

-          finder.Visit(function.Req, null);

-          if (function.Body != null) {

-            finder.Visit(function.Body, null);

-          }

-        } else if (decl is Method) {

-          var method = (Method)decl;

-          finder.Visit(method.Ens, null);

-          finder.Visit(method.Req, null);

-          if (method.Body != null) {

-            finder.Visit(method.Body, null);

-          }

-        }

+        finder.Visit(decl, null);

       }

       

       var triggersCollector = new Triggers.TriggersCollector();

@@ -80,21 +66,7 @@ namespace Microsoft.Dafny
     internal override void PostResolve(ModuleDefinition m) {

       var splitter = new Triggers.QuantifierSplitter();

       foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {

-        if (decl is Function) {

-          var function = (Function)decl;

-          splitter.Visit(function.Ens);

-          splitter.Visit(function.Req);

-          if (function.Body != null) {

-            splitter.Visit(function.Body);

-          }

-        } else if (decl is Method) {

-          var method = (Method)decl;

-          splitter.Visit(method.Ens);

-          splitter.Visit(method.Req);

-          if (method.Body != null) {

-            splitter.Visit(method.Body);

-          }

-        }

+        splitter.Visit(decl);

       }

     }

   }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 8cc32e18..8200f254 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3585,7 +3585,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

       Contract.Ensures(Contract.Result<Bpl.Cmd>() != null);

       var col = tok.col + (isEndToken ? tok.val.Length : 0);

-      string description = reporter.ErrorToString_Internal(additionalInfo == null ? "" : ": ", tok.filename, tok.line, tok.col, additionalInfo ?? "");

+      string description = ErrorReporter.ErrorToString_Internal(additionalInfo == null ? "" : ": ", tok.filename, tok.line, tok.col, additionalInfo ?? "");

       QKeyValue kv = new QKeyValue(tok, "captureState", new List<object>() { description }, null);

       return new Bpl.AssumeCmd(tok, Bpl.Expr.True, kv);

     }

@@ -11524,56 +11524,60 @@ namespace Microsoft.Dafny {
           return TrExpr(((NamedExpr)expr).Body);

         } else if (expr is QuantifierExpr) {

           QuantifierExpr e = (QuantifierExpr)expr;

-          List<Variable> tyvars = translator.MkTyParamBinders(e.TypeArgs);

-          List<Variable> bvars = new List<Variable>();

 

-          var initEtran = this;

-          var bodyEtran = this;

-          bool _scratch = true;

+          if (e.SplitQuantifier != null) {

+            return TrExpr(e.SplitQuantifierExpression);

+          } else {

+            List<Variable> tyvars = translator.MkTyParamBinders(e.TypeArgs);

+            List<Variable> bvars = new List<Variable>();

 

-          Bpl.Expr antecedent = Bpl.Expr.True;

+            var initEtran = this;

+            var bodyEtran = this;

+            bool _scratch = true;

 

-          if (Attributes.ContainsBool(e.Attributes, "layerQuantifier", ref _scratch)) {

-            // If this is a layer quantifier, quantify over layers here, and use $LS(ly) layers in the translation of the body

-            var ly = BplBoundVar(e.Refresh("q$ly#", translator.CurrentIdGenerator), predef.LayerType, bvars);

-            bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, new FuelSetting(translator, 1, ly), new FuelSetting(translator, 1, ly), modifiesFrame, stripLits);

-          }

-          if (Attributes.ContainsBool(e.Attributes, "heapQuantifier", ref _scratch)) {

-            var h = BplBoundVar(e.Refresh("q$heap#", translator.CurrentIdGenerator), predef.HeapType, bvars);

-            bodyEtran = new ExpressionTranslator(bodyEtran, h);

-            antecedent = BplAnd(new List<Bpl.Expr> {

+            Bpl.Expr antecedent = Bpl.Expr.True;

+

+            if (Attributes.ContainsBool(e.Attributes, "layerQuantifier", ref _scratch)) {

+              // If this is a layer quantifier, quantify over layers here, and use $LS(ly) layers in the translation of the body

+              var ly = BplBoundVar(e.Refresh("q$ly#", translator.CurrentIdGenerator), predef.LayerType, bvars);

+              bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, new FuelSetting(translator, 1, ly), new FuelSetting(translator, 1, ly), modifiesFrame, stripLits);

+            }

+            if (Attributes.ContainsBool(e.Attributes, "heapQuantifier", ref _scratch)) {

+              var h = BplBoundVar(e.Refresh("q$heap#", translator.CurrentIdGenerator), predef.HeapType, bvars);

+              bodyEtran = new ExpressionTranslator(bodyEtran, h);

+              antecedent = BplAnd(new List<Bpl.Expr> {

               antecedent,

               translator.FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, h),

               translator.HeapSameOrSucc(initEtran.HeapExpr, h)

             });

-          }

+            }

 

-          antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars));

+            antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars));

 

-          Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger");

-          Bpl.Trigger tr = null;

-          var argsEtran = bodyEtran.WithNoLits();

-          foreach (var aa in e.Attributes.AsEnumerable()) {

-            if (aa.Name == "trigger") {

-              List<Bpl.Expr> tt = new List<Bpl.Expr>();

-              foreach (var arg in aa.Args) {

-                tt.Add(argsEtran.TrExpr(arg));

+            Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger");

+            Bpl.Trigger tr = null;

+            var argsEtran = bodyEtran.WithNoLits();

+            foreach (var aa in e.Attributes.AsEnumerable()) {

+              if (aa.Name == "trigger") {

+                List<Bpl.Expr> tt = new List<Bpl.Expr>();

+                foreach (var arg in aa.Args) {

+                  tt.Add(argsEtran.TrExpr(arg));

+                }

+                tr = new Bpl.Trigger(expr.tok, true, tt, tr);

               }

-              tr = new Bpl.Trigger(expr.tok, true, tt, tr);

             }

-          }

-          if (e.Range != null) {

-            antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range));

-          }

-          Bpl.Expr body = bodyEtran.TrExpr(e.Term);

-          

-          if (e is ForallExpr) {

-            return new Bpl.ForallExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.Imp(antecedent, body));

-          } else {

-            Contract.Assert(e is ExistsExpr);

-            return new Bpl.ExistsExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.And(antecedent, body));

-          }

+            if (e.Range != null) {

+              antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range));

+            }

+            Bpl.Expr body = bodyEtran.TrExpr(e.Term);

 

+            if (e is ForallExpr) {

+              return new Bpl.ForallExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.Imp(antecedent, body));

+            } else {

+              Contract.Assert(e is ExistsExpr);

+              return new Bpl.ExistsExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.And(antecedent, body));

+            }

+          }

         } else if (expr is SetComprehension) {

           var e = (SetComprehension)expr;

           // Translate "set xs | R :: T" into "lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T))".

@@ -13090,13 +13094,7 @@ namespace Microsoft.Dafny {
 

     private bool CanSafelyInline(FunctionCallExpr fexp, Function f) {

       var visitor = new TriggersExplorer();

-

-      visitor.Visit(f.Body);

-      foreach (var expr in f.Ens) { visitor.Visit(expr); }

-      foreach (var expr in f.Req) { visitor.Visit(expr); }

-      foreach (var expr in f.Reads) { visitor.Visit(expr); }

-      foreach (var expr in f.Decreases.Expressions) { visitor.Visit(expr); }

-

+      visitor.Visit(f);

       return f.Formals.Zip(fexp.Args).All(formal_concrete => CanSafelySubstitute(visitor.TriggerVariables, formal_concrete.Item1, formal_concrete.Item2));

     }

 

diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs
index 4b223856..c50bc9c6 100644
--- a/Source/Dafny/Triggers/QuantifierSplitter.cs
+++ b/Source/Dafny/Triggers/QuantifierSplitter.cs
@@ -85,10 +85,12 @@ namespace Microsoft.Dafny.Triggers {
 

     protected override void VisitOneExpr(Expression expr) {

       var quantifier = expr as QuantifierExpr;

-      if (quantifier != null) {

-        var split = SplitQuantifier(quantifier).ToList();

-        quantifier.SplitQuantifier = split;

-        //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| "));

+      if (quantifier != null && quantifier.SplitQuantifier == null) {

+        bool splitAttr = true;

+        if (!Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr) {

+          var split = SplitQuantifier(quantifier).ToList();

+          quantifier.SplitQuantifier = split;

+        }

       }

     }

   }

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index a6340f10..bfa90d81 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -7,7 +7,6 @@ using System.Text;
 using Microsoft.Boogie;

 using System.Diagnostics.Contracts;

 

-//FIXME Generated triggers should be _triggers

 //FIXME: When scoring, do not consider old(x) to be higher than x.

 

 namespace Microsoft.Dafny.Triggers {

@@ -28,7 +27,7 @@ namespace Microsoft.Dafny.Triggers {
     internal void TrimInvalidTriggers() {

       Contract.Requires(CandidateTerms != null);

       Contract.Requires(Candidates != null);

-      Candidates = TriggerUtils.Filter(Candidates, tr => tr.MentionsAll(quantifier.BoundVars), tr => { }).ToList();

+      Candidates = TriggerUtils.Filter(Candidates, tr => tr, (tr, _) => tr.MentionsAll(quantifier.BoundVars), (tr, _) => { }).ToList();

     }

   }

 

@@ -60,7 +59,13 @@ namespace Microsoft.Dafny.Triggers {
       return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any();

     }

 

-    //FIXME document that this assumes that the quantifiers live in the same context and share the same variables

+    /// <summary>

+    /// Collect triggers from the body of each quantifier, and share them

+    /// between all quantifiers. This method assumes that all quantifiers

+    /// actually come from the same context, and were the result of a split that

+    /// gave them all the same variables.

+    /// </summary>

+    /// <param name="triggersCollector"></param>

     void CollectAndShareTriggers(TriggersCollector triggersCollector) {

       var pool = quantifiers.SelectMany(q => triggersCollector.CollectTriggers(q.quantifier));

       var distinctPool = pool.Deduplicate(TriggerTerm.Eq);

@@ -79,13 +84,10 @@ namespace Microsoft.Dafny.Triggers {
     }

 

     void BuildDependenciesGraph() {

-      // FIXME: Think more about multi-quantifier dependencies

-      //class QuantifierDependency {

-      //  QuantifierWithTriggers Cause;

-      //  QuantifierWithTriggers Consequence;

-      //  List<TriggerCandidate> Triggers;

-      //  List<Expression> MatchingTerm;

-      //}

+      // The problem of finding matching loops between multiple-triggers is hard; it

+      // seems to require one to track exponentially-sized dependencies between parts

+      // of triggers and quantifiers. For now, we only do single-quantifier loop

+      // detection

     }

 

     void SuppressMatchingLoops() {

@@ -111,14 +113,14 @@ namespace Microsoft.Dafny.Triggers {
 

       foreach (var q in quantifiers) {

         var looping = new List<TriggerCandidate>();

-        var loopingSubterms = q.Candidates.ToDictionary(candidate => candidate, candidate => candidate.LoopingSubterms(q.quantifier).ToList());

 

         var safe = TriggerUtils.Filter(

           q.Candidates,

-          c => !loopingSubterms[c].Any(),

-          c => {

-            looping.Add(c);

-            c.Annotation = "loops with " + loopingSubterms[c].MapConcat(t => Printer.ExprToString(t.Expr), ", ");

+          candidate => candidate.LoopingSubterms(q.quantifier).ToList(),

+          (candidate, loopingSubterms) => !loopingSubterms.Any(),

+          (candidate, loopingSubterms) => {

+            looping.Add(candidate);

+            candidate.Annotation = "loops with " + loopingSubterms.MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", ");

           }).ToList();

 

         q.CouldSuppressLoops = safe.Count > 0;

@@ -131,15 +133,23 @@ namespace Microsoft.Dafny.Triggers {
     }

 

     void SelectTriggers() {

-      //FIXME

+      foreach (var q in quantifiers) { //FIXME Check whether this makes verification faster

+        q.Candidates = TriggerUtils.Filter(q.Candidates,

+          candidate => q.Candidates.Where(candidate.IsStrongerThan).ToList(),

+          (candidate, weakerCandidates) => !weakerCandidates.Any(),

+          (candidate, weakerCandidates) => {

+            q.RejectedCandidates.Add(candidate);

+            candidate.Annotation = "stronger than " + String.Join(", ", weakerCandidates);

+          }).ToList();

+      }

     }

 

     private void CommitOne(QuantifierWithTriggers q, bool addHeader) {

       var errorLevel = ErrorLevel.Info;

       var msg = new StringBuilder();

-      var indent = addHeader ? "   " : " "; //FIXME if multiline messages were properly supported, this indentation wouldn't be needed

+      var indent = addHeader ? "  " : "";

 

-      if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop and autotriggers attributes are passed down to Boogie

+      if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop, split and autotriggers attributes are passed down to Boogie

         msg.AppendFormat("Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); 

         // FIXME This shouldn't be printed for autoReqs. (see autoReq.dfy)

         // FIXME typeQuantifier?

@@ -156,7 +166,7 @@ namespace Microsoft.Dafny.Triggers {
         AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true);

 

 #if QUANTIFIER_WARNINGS

-        string WARN = (msg.Length > 0 ? indent : "") + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) ");

+        string WARN = indent + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) ");

         if (!q.CandidateTerms.Any()) {

           errorLevel = ErrorLevel.Warning;

           msg.Append(WARN).AppendLine("No terms found to trigger on.");

@@ -171,7 +181,8 @@ namespace Microsoft.Dafny.Triggers {
       }

       

       if (msg.Length > 0) {

-        reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msg.ToString().TrimEnd("\r\n".ToCharArray()));

+        var msgStr = msg.ToString().TrimEnd("\r\n ".ToCharArray());

+        reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msgStr);

       }

     }

 

diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs
index a49ed13a..6c3f4ee7 100644
--- a/Source/Dafny/Triggers/TriggerExtensions.cs
+++ b/Source/Dafny/Triggers/TriggerExtensions.cs
@@ -24,6 +24,7 @@ namespace Microsoft.Dafny.Triggers {
 

   internal struct TriggerMatch {

     internal Expression Expr;

+    internal Expression OriginalExpr;

     internal Dictionary<IVariable, Expression> Bindings;

 

     internal static bool Eq(TriggerMatch t1, TriggerMatch t2) {

@@ -110,10 +111,10 @@ namespace Microsoft.Dafny.Triggers {
       return ShallowEq_Top(expr, trigger) && TriggerUtils.SameLists(expr.SubExpressions, trigger.SubExpressions, (e1, e2) => MatchesTrigger(e1, e2, holes, bindings));

     }

 

-    private static TriggerMatch? MatchAgainst(this Expression expr, Expression trigger, IEnumerable<BoundVar> holes) {

+    private static TriggerMatch? MatchAgainst(this Expression expr, Expression trigger, IEnumerable<BoundVar> holes, Expression originalExpr) {

       var bindings = new Dictionary<IVariable, Expression>();

       if (expr.MatchesTrigger(trigger, new HashSet<BoundVar>(holes), bindings)) {

-        return new TriggerMatch { Expr = expr, Bindings = bindings };

+        return new TriggerMatch { Expr = expr, OriginalExpr = originalExpr ?? expr, Bindings = bindings };

       } else {

         return null;

       }

@@ -121,7 +122,7 @@ namespace Microsoft.Dafny.Triggers {
 

     internal static IEnumerable<TriggerMatch> SubexpressionsMatchingTrigger(this QuantifierExpr quantifier, Expression trigger) {

       return quantifier.Term.AllSubExpressions()

-        .Select(e => TriggerUtils.CleanupExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars))

+        .Select(e => TriggerUtils.CleanupExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars, e))

         .Where(e => e.HasValue).Select(e => e.Value);

     }

 

diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index 9ebcf846..6f76464b 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -76,13 +76,14 @@ namespace Microsoft.Dafny.Triggers {
       return it1_has == it2_has && acc;

     }

 

-    internal static IEnumerable<T> Filter<T>(IEnumerable<T> elements, Func<T, bool> predicate, Action<T> reject) {

+    internal static IEnumerable<T> Filter<T, U>(IEnumerable<T> elements, Func<T, U> Converter, Func<T, U, bool> predicate, Action<T, U> reject) {

       var positive = new List<T>();

-      foreach (var c in elements) {

-        if (predicate(c)) {

-          yield return c;

+      foreach (var elem in elements) {

+        var conv = Converter(elem);

+        if (predicate(elem, conv)) {

+          yield return elem;

         } else {

-          reject(c);

+          reject(elem, conv);

         }

       }

     }

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index 08d33af6..3b2853ed 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -13,7 +13,25 @@ namespace Microsoft.Dafny.Triggers {
     internal ISet<IVariable> Variables { get; set; }

 

     public override string ToString() {

-      return Printer.ExprToString(OriginalExpr);

+      return Printer.ExprToString(Expr); 

+      // NOTE: Using OriginalExpr here could cause some confusion: 

+      // for example, {a !in b} is a binary expression, yielding 

+      // trigger {a in b}. Saying the trigger is a !in b would be 

+      // rather misleading.

+    }

+

+    internal enum TermComparison {

+      SameStrength = 0, Stronger = 1, NotStronger = -1

+    }

+

+    internal TermComparison CompareTo(TriggerTerm other) {

+      if (this == other) {

+        return TermComparison.SameStrength;

+      } else if (Expr.AllSubExpressions(true).Any(other.Expr.ExpressionEq)) {

+        return TermComparison.Stronger;

+      } else {

+        return TermComparison.NotStronger;

+      }

     }

 

     internal static bool Eq(TriggerTerm t1, TriggerTerm t2) {

@@ -37,7 +55,7 @@ namespace Microsoft.Dafny.Triggers {
       return vars.All(x => Terms.Any(term => term.Variables.Contains(x)));

     }

 

-    private string Repr { get { return String.Join(", ", Terms); } }

+    internal string Repr { get { return String.Join(", ", Terms); } }

 

     public override string ToString() {

       return "{" + Repr + "}" + (String.IsNullOrWhiteSpace(Annotation) ? "" : " (" + Annotation + ")");

@@ -45,7 +63,7 @@ namespace Microsoft.Dafny.Triggers {
 

     internal IEnumerable<TriggerMatch> LoopingSubterms(QuantifierExpr quantifier) {

       Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier

-      var matchingSubterms = MatchingSubterms(quantifier);

+      var matchingSubterms = this.MatchingSubterms(quantifier);

       return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms));

     }

 

@@ -54,8 +72,23 @@ namespace Microsoft.Dafny.Triggers {
       return Terms.SelectMany(term => quantifier.SubexpressionsMatchingTrigger(term.Expr)).Deduplicate(TriggerMatch.Eq);

     }

 

-    public String AsDafnyAttributeString() {

-      return "{:trigger " + Repr + "}";

+    internal bool IsStrongerThan(TriggerCandidate that) {

+      if (this == that) {

+        return false; 

+      }

+

+      var hasStrictlyStrongerTerm = false;

+      foreach (var t in Terms) {

+        var comparison = that.Terms.Select(t.CompareTo).Max();

+

+        // All terms of `this` must be at least as strong as a term of `that`

+        if (comparison == TriggerTerm.TermComparison.NotStronger) { return false; }

+

+        // Did we find a strictly stronger term?

+        hasStrictlyStrongerTerm = hasStrictlyStrongerTerm || comparison == TriggerTerm.TermComparison.Stronger;

+      }

+

+      return hasStrictlyStrongerTerm;

     }

   }

 

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 13991496..5b70329d 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -15,7 +15,6 @@ using Microsoft.VisualStudio.Text.Tagging;
 using Microsoft.VisualStudio.Utilities;

 using Bpl = Microsoft.Boogie;

 

-

 namespace DafnyLanguage

 {

 

@@ -136,8 +135,7 @@ namespace DafnyLanguage
 

       List<IdRegion> newRegions = new List<IdRegion>();

 

-      foreach (var info in program.reporter.AllMessages[ErrorLevel.Info])

-      {

+      foreach (var info in program.reporter.AllMessages[ErrorLevel.Info]) {

         IdRegion.Add(newRegions, info.token, info.message, info.token.val.Length);

       }

 

@@ -368,11 +366,6 @@ namespace DafnyLanguage
       public readonly OccurrenceKind Kind;

       public readonly IVariable Variable;

 

-      static bool SurfaceSyntaxToken(Bpl.IToken tok) {

-        Contract.Requires(tok != null);

-        return !(tok is TokenWrapper);

-      }

-

       public static void Add(List<IdRegion> regions, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) {

         Contract.Requires(regions != null);

         Contract.Requires(tok != null);

@@ -383,27 +376,21 @@ namespace DafnyLanguage
         Contract.Requires(regions != null);

         Contract.Requires(tok != null);

         Contract.Requires(v != null);

-        if (SurfaceSyntaxToken(tok)) {

-          regions.Add(new IdRegion(tok, v, isDefinition, kind, context));

-        }

+        regions.Add(new IdRegion(tok, v, isDefinition, kind, context));

       }

       public static void Add(List<IdRegion> regions, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {

         Contract.Requires(regions != null);

         Contract.Requires(tok != null);

         Contract.Requires(decl != null);

         Contract.Requires(kind != null);

-        if (SurfaceSyntaxToken(tok)) {

-          regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context));

-        }

+        regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context));

       }

 

       public static void Add(List<IdRegion> regions, Bpl.IToken tok, string text, int length) {

         Contract.Requires(regions != null);

         Contract.Requires(tok != null);

         Contract.Requires(text != null);

-        if (SurfaceSyntaxToken(tok)) {

-          regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length));

-        }

+        regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length));

       }

 

       private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) {

diff --git a/Test/dafny0/one-message-per-failed-precondition.dfy b/Test/dafny0/one-message-per-failed-precondition.dfy
new file mode 100644
index 00000000..ef4f5bd6
--- /dev/null
+++ b/Test/dafny0/one-message-per-failed-precondition.dfy
@@ -0,0 +1,20 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// When a function call violates two preconditions at the same time, it causes

+// two errors to be reported for the same token

+

+method A(x: int)

+  requires x > 0

+  requires x < 0

+{}

+

+method B(x: int) {

+  A(x);

+}

+

+function fA(x: int): int

+  requires x > 0

+  requires x < 0 { 1 }

+

+function fB(x: int): int { fA(x) }

diff --git a/Test/dafny0/one-message-per-failed-precondition.dfy.expect b/Test/dafny0/one-message-per-failed-precondition.dfy.expect
new file mode 100644
index 00000000..0a76965e
--- /dev/null
+++ b/Test/dafny0/one-message-per-failed-precondition.dfy.expect
@@ -0,0 +1,20 @@
+one-message-per-failed-precondition.dfy(13,3): Error BP5002: A precondition for this call might not hold.

+one-message-per-failed-precondition.dfy(9,13): Related location: This is the precondition that might not hold.

+Execution trace:

+    (0,0): anon0

+one-message-per-failed-precondition.dfy(13,3): Error BP5002: A precondition for this call might not hold.

+one-message-per-failed-precondition.dfy(8,13): Related location: This is the precondition that might not hold.

+Execution trace:

+    (0,0): anon0

+one-message-per-failed-precondition.dfy(20,27): Error: possible violation of function precondition

+one-message-per-failed-precondition.dfy(18,13): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+one-message-per-failed-precondition.dfy(20,27): Error: possible violation of function precondition

+one-message-per-failed-precondition.dfy(17,13): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+

+Dafny program verifier finished with 4 verified, 4 errors

diff --git a/Test/triggers/function-applications-are-triggers.dfy b/Test/triggers/function-applications-are-triggers.dfy
new file mode 100644
index 00000000..67ffe4e4
--- /dev/null
+++ b/Test/triggers/function-applications-are-triggers.dfy
@@ -0,0 +1,15 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file checks that function applications yield trigger candidates

+

+method M(P: (int -> int) -> bool, g: int -> int)

+  requires P.requires(g)

+  requires P(g) {

+  assume forall f: int -> int :: P.requires(f);

+  assume forall f: int -> int :: P(f) ==> f.requires(10) && f(10) == 0;

+  assert forall f: int -> int ::

+    (forall x :: f.requires(x) && g.requires(x) ==> f(x) == g(x)) ==>

+    f.requires(10) ==>

+    f(10) == 0;

+}

diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/triggers/function-applications-are-triggers.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/triggers/large-quantifiers-dont-break-dafny.dfy b/Test/triggers/large-quantifiers-dont-break-dafny.dfy
new file mode 100644
index 00000000..8becae97
--- /dev/null
+++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy
@@ -0,0 +1,61 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This test ensures that the trigger  collector (the routine that picks trigger

+// candidates) does not  actually consider all subsets of terms;  if it did, the

+// following would take horribly long

+

+predicate P0(x: bool)

+predicate P1(x: bool)

+predicate P2(x: bool)

+predicate P3(x: bool)

+predicate P4(x: bool)

+predicate P5(x: bool)

+predicate P6(x: bool)

+predicate P7(x: bool)

+predicate P8(x: bool)

+predicate P9(x: bool)

+predicate P10(x: bool)

+predicate P11(x: bool)

+predicate P12(x: bool)

+predicate P13(x: bool)

+predicate P14(x: bool)

+predicate P15(x: bool)

+predicate P16(x: bool)

+predicate P17(x: bool)

+predicate P18(x: bool)

+predicate P19(x: bool)

+predicate P20(x: bool)

+predicate P21(x: bool)

+predicate P22(x: bool)

+predicate P23(x: bool)

+predicate P24(x: bool)

+predicate P25(x: bool)

+predicate P26(x: bool)

+predicate P27(x: bool)

+predicate P28(x: bool)

+predicate P29(x: bool)

+predicate P30(x: bool)

+predicate P31(x: bool)

+predicate P32(x: bool)

+predicate P33(x: bool)

+predicate P34(x: bool)

+predicate P35(x: bool)

+predicate P36(x: bool)

+predicate P37(x: bool)

+predicate P38(x: bool)

+predicate P39(x: bool)

+predicate P40(x: bool)

+predicate P41(x: bool)

+predicate P42(x: bool)

+predicate P43(x: bool)

+predicate P44(x: bool)

+predicate P45(x: bool)

+predicate P46(x: bool)

+predicate P47(x: bool)

+predicate P48(x: bool)

+predicate P49(x: bool)

+

+method M() {

+  assert forall x :: true || P0(x) || P1(x) || P2(x) || P3(x) || P4(x) || P5(x) || P6(x) || P7(x) || P8(x) || P9(x) || P10(x) || P11(x) || P12(x) || P13(x) || P14(x) || P15(x) || P16(x) || P17(x) || P18(x) || P19(x) || P20(x) || P21(x) || P22(x) || P23(x) || P24(x) || P25(x) || P26(x) || P27(x) || P28(x) || P29(x) || P30(x) || P31(x) || P32(x) || P33(x) || P34(x) || P35(x) || P36(x) || P37(x) || P38(x) || P39(x) || P40(x) || P41(x) || P42(x) || P43(x) || P44(x) || P45(x) || P46(x) || P47(x) || P48(x) || P49(x);

+}

diff --git a/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
new file mode 100644
index 00000000..c90560b0
--- /dev/null
+++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 52 verified, 0 errors

diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy b/Test/triggers/loop-detection-is-not-too-strict.dfy
new file mode 100644
index 00000000..c6722399
--- /dev/null
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy
@@ -0,0 +1,21 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This test shows that the loop detection engine makes compromises when looking

+// for subexpressions matching a trigger; in particular, it allows a

+// subexpression to match a trigger without reporting a loop and without being

+// equal to that trigger, as long as the only differences are variable

+

+predicate P(x: int, y: int)

+

+method Test() {

+  // P(x, y) and P(y, x) might look like they would cause a loop. Since they

+  // only differ by their variables, though, they won't raise flags.

+  assume forall x: int, y: int :: P(x, y) == P(y, x);

+

+  // This works independent of extra parentheses:

+  assume forall x: int, y: int :: P(x, y) == (P(y, x));

+

+  // Contrast with the following:

+  assume forall x: int, y: int :: P(x, y) == P(x, y+1);

+}

diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
new file mode 100644
index 00000000..29882da7
--- /dev/null
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
@@ -0,0 +1,4 @@
+loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (loops with {P(x, y + 1)})

+ (!) Suppressing loops would leave this expression without triggers.

+

+Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy b/Test/triggers/loop-detection-messages--unit-tests.dfy
new file mode 100644
index 00000000..d5439e09
--- /dev/null
+++ b/Test/triggers/loop-detection-messages--unit-tests.dfy
@@ -0,0 +1,29 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file is a series of basic tests for loop detection, focusing on the

+// warnings and information messages

+

+function f(i: int): int

+function g(i: int): int

+

+method M() {

+  assert forall i :: false ==> f(i) == f(f(i));

+  assert forall i :: false ==> f(i) == f(i+1);

+  assert forall i {:matchingloop} :: false ==> f(i) == f(i+1);

+

+  assert forall i :: false ==> f(i) == f(i+1) && f(i) == g(i);

+  assert forall i :: false ==> f(i) == f(i+1) && f(i) == f(i);

+  assert forall i {:matchingloop} :: false ==> f(i) == f(i+1) && f(i) == f(i);

+

+  assert forall i :: false ==> f(i) == 0;

+  assert forall i :: false ==> f(i+1) == 0;

+  assert forall i {:autotriggers false} :: false ==> f(i+1) == 0;

+

+  assert forall i, j: int :: false ==> f(i) == f(j);

+  assert forall i, j: int :: false ==> f(i) == f(i);

+  assert forall i, j: int :: false ==> f(i) == f(i) && g(j) == 0;

+  assert forall i, j: int :: false ==> f(i) == f(i) && g(j+1) == 0;

+  assert forall i, j: int {:autotriggers false} :: false ==> f(i) == f(i);

+  assert forall i, j: int {:trigger f(i), g(j)} :: false ==> f(i) == f(i);

+}

diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
new file mode 100644
index 00000000..1ebc0bce
--- /dev/null
+++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
@@ -0,0 +1,13 @@
+loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (loops with {f(i + 1)})

+ (!) Suppressing loops would leave this expression without triggers.

+loop-detection-messages--unit-tests.dfy(16,9): Warning: For expression {false ==> f(i) == f(i + 1)}:

+   Selected triggers: {f(i)} (loops with {f(i + 1)})

+   (!) Suppressing loops would leave this expression without triggers.

+loop-detection-messages--unit-tests.dfy(20,9): Warning: (!) No terms found to trigger on.

+loop-detection-messages--unit-tests.dfy(24,9): Warning: (!) No trigger covering all quantified variables found.

+loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> f(i) == f(i)}:

+   (!) No trigger covering all quantified variables found.

+loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> g(j + 1) == 0}:

+   (!) No trigger covering all quantified variables found.

+

+Dafny program verifier finished with 4 verified, 0 errors

diff --git a/Test/triggers/nested-quantifiers-all-get-triggers.dfy b/Test/triggers/nested-quantifiers-all-get-triggers.dfy
new file mode 100644
index 00000000..c75cfab9
--- /dev/null
+++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy
@@ -0,0 +1,9 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This checks that nested quantifiers do get triggers, and that the parent

+// quantifier does not get annotated twice

+

+method M() {

+  ghost var x := forall s: set<int>, x: int :: (x in s ==> forall y :: y == x ==> y in s);

+}

diff --git a/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy
new file mode 100644
index 00000000..7423e086
--- /dev/null
+++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy
@@ -0,0 +1,16 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file shows how Dafny detects loops even for terms that are not literal

+// AST matches. This file also checks that triggers are reported exactly as

+// picked (that is, `x in s` yields `s[x]` for a multiset s), but matches as

+// they appear in the buffer text (that is, `x+1 in s` is not translated to

+// s[x+1] when highlited as a cause for a potential matching loop.

+

+method M() {

+  // This is an obvious loop

+  ghost var b := forall s: multiset<int>, x: int :: s[x] > 0 ==> s[x+1] > 0;

+

+  // x in s loops with s[x+1] due to the way [x in s] is translated

+  ghost var a := forall s: multiset<int>, x: int :: x in s ==> s[x+1] > 0 && x+2 !in s;

+}

diff --git a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
new file mode 100644
index 00000000..83648626
--- /dev/null
+++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
@@ -0,0 +1,10 @@
+some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (loops with {s[x + 1]})

+ (!) Suppressing loops would leave this expression without triggers.

+some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> s[x + 1] > 0}:

+   Selected triggers: {s[x]} (loops with {s[x + 1]})

+   (!) Suppressing loops would leave this expression without triggers.

+some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> x + 2 !in s}:

+   Selected triggers: {s[x]} (loops with {x + 2 !in s})

+   (!) Suppressing loops would leave this expression without triggers.

+

+Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy b/Test/triggers/splitting-triggers-recovers-expressivity.dfy
new file mode 100644
index 00000000..79a0dc72
--- /dev/null
+++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy
@@ -0,0 +1,61 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+predicate P(i: int)

+predicate Q(i: int)

+

+/* This file demonstrates a case where automatic trigger splitting is useful to

+   prevent loop detection from reducing expressivity too much. */

+

+lemma exists_0()

+  requires P(0)

+  ensures exists i {:split false} :: P(i) || (Q(i) ==> P(i+1)) {

+    // Fails: P(i) is not a trigger

+}

+

+lemma forall_0(i: int)

+  requires forall j {:split false} :: j >= 0 ==> (P(j) && (Q(j) ==> P(j+1)))

+  requires i >= 0

+  ensures P(i) {

+    // Fails: P(i) is not a trigger

+}

+

+

+lemma exists_1()

+  requires P(0)

+  ensures exists i {:split false} :: P(i) || (Q(i) ==> P(i+1)) {

+    assert Q(0) || !Q(0);

+    // Works: the dummy assertion introduces a term that causes the quantifier

+    // to trigger, producing a witness.

+  }

+

+lemma forall_1(i: int)

+  requires forall j {:split false} :: j >= 0 ==> (P(j) && (Q(j) ==> P(j+1)))

+  requires i >= 0

+  ensures P(i) {

+    assert Q(i) || !Q(i);

+    // Works: the dummy assertion introduces a term that causes the quantifier

+    // to trigger, producing a witness.

+}

+

+

+lemma exists_2()

+  requires P(0)

+  ensures exists i :: P(i) || (Q(i) ==> P(i+1)) {

+    // Works: automatic trigger splitting allows P(i) to get its own triggers

+}

+

+lemma forall_2(i: int)

+  requires forall j :: j >= 0 ==> (P(j) && (Q(j) ==> P(j+1)))

+  requires i >= 0

+  ensures P(i) {

+    // Works: automatic trigger splitting allows P(i) to get its own triggers

+}

+

+

+lemma loop()

+  requires P(0)

+  requires forall i {:matchingloop} :: i >= 0 ==> Q(i) && (P(i) ==> P(i+1))

+  ensures P(100) {

+    // Works: the matching loop is explicitly allowed

+}

diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
new file mode 100644
index 00000000..8d7ff4ef
--- /dev/null
+++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
@@ -0,0 +1,10 @@
+splitting-triggers-recovers-expressivity.dfy(12,63): Error BP5003: A postcondition might not hold on this return path.

+splitting-triggers-recovers-expressivity.dfy(12,10): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+splitting-triggers-recovers-expressivity.dfy(19,15): Error BP5003: A postcondition might not hold on this return path.

+splitting-triggers-recovers-expressivity.dfy(19,10): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 14 verified, 2 errors

diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
new file mode 100644
index 00000000..f25a624e
--- /dev/null
+++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
@@ -0,0 +1,21 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This tests shows that, since quantifiers are split, it becomes possible to know more precisely what part of a precondition did not hold at the call site.

+

+method f()

+  requires forall y :: y > 0 && y < 0 {

+}

+

+method g(x: int) {

+  f();

+}

+

+function gf(): int

+  requires forall y :: y > 0 && y < 0 {

+    1

+}

+

+function gg(x: int): int {

+  gf()

+}

diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect
new file mode 100644
index 00000000..c8e1a5fa
--- /dev/null
+++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect
@@ -0,0 +1,32 @@
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression {y > 0}:

+   (!) No terms found to trigger on.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression {y < 0}:

+   (!) No terms found to trigger on.

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression {y > 0}:

+   (!) No terms found to trigger on.

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression {y < 0}:

+   (!) No terms found to trigger on.

+splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error BP5002: A precondition for this call might not hold.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: This is the precondition that might not hold.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,34): Related location

+Execution trace:

+    (0,0): anon0

+splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error BP5002: A precondition for this call might not hold.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: This is the precondition that might not hold.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,25): Related location

+Execution trace:

+    (0,0): anon0

+splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,34): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,25): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+

+Dafny program verifier finished with 4 verified, 4 errors

diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy b/Test/triggers/triggers-prevent-some-inlining.dfy
new file mode 100644
index 00000000..04b8051c
--- /dev/null
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy
@@ -0,0 +1,26 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This  file looks  at the  interactions  between inlining  and triggers.   The

+// sum_is_sum predicate gets a {sum(a,  b)} trigger, which explicitly depends on

+// one of the  variables being passed in. Since triggers  are generated prior to

+// inlining  (inlining  happens  during  translation),  inlining  the  last  two

+// instances of that call below would cause  b+1 (a trigger killer) to pop up in

+// a trigger.   This would create  an invalid trigger,  so Dafny doesn't  let it

+// happen.

+

+function sum(a: int, b: int): int {

+  a + b

+}

+

+predicate sum_is_sum(b: int, c: int) {

+  forall a: int :: sum(a, b) + c == a + b + c

+}

+

+method can_we_inline(b: int, c: int)

+  ensures sum_is_sum(0, 0)     // OK  to inline

+  ensures sum_is_sum(b, c)     // OK  to inline

+  ensures sum_is_sum(b, c+1)   // OK  to inline

+  ensures sum_is_sum(b+1, c)   // NOK to inline

+  ensures sum_is_sum(b+1, c+1) // NOK to inline

+{ }

diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy.expect b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
new file mode 100644
index 00000000..73ba063c
--- /dev/null
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 4 verified, 0 errors

diff --git a/Test/triggers/useless-triggers-are-removed.dfy b/Test/triggers/useless-triggers-are-removed.dfy
new file mode 100644
index 00000000..16458e41
--- /dev/null
+++ b/Test/triggers/useless-triggers-are-removed.dfy
@@ -0,0 +1,25 @@
+// RUN: %dafny /printTooltips /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file ensures that Dafny does get rid of redundant triggers before

+// annotating a quantifier, and that ths process does not interfere with cycle

+// detection.

+

+function f(x: int): int

+function g(x: int): int

+function h(x: int): int

+

+method M()

+  // In the following, only f(x) is kept. Note that the subset enumeration was

+  // already smart enough to not build any trigger with multiple terms (it only

+  // built 5 candidates)

+  requires forall x: int :: f(x) + g(f(x)) + h(f(x)) + g(h(f(x))) + h(g(f(x))) == 0

+

+  // Loop detection still works fine: in the following example, the trigger is

+  // f(f(x))

+  requires forall x: int :: f(x) == f(f(x))

+

+  // This works for multi-triggers, too:

+  requires forall x, y :: f(x) + g(f(y)) + g(y) + g(f(x)) == 0

+{

+}

diff --git a/Test/triggers/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect
new file mode 100644
index 00000000..6c2c0a2b
--- /dev/null
+++ b/Test/triggers/useless-triggers-are-removed.dfy.expect
@@ -0,0 +1,17 @@
+useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)}

+ Rejected triggers:

+   {h(g(f(x)))} (stronger than {g(f(x))}, {f(x)})

+   {g(h(f(x)))} (stronger than {h(f(x))}, {f(x)})

+   {h(f(x))} (stronger than {f(x)})

+   {g(f(x))} (stronger than {f(x)})

+useless-triggers-are-removed.dfy(20,11): Info: Selected triggers: {f(f(x))}

+ Rejected triggers: {f(x)} (loops with {f(f(x))})

+useless-triggers-are-removed.dfy(23,11): Info: Selected triggers:

+   {g(f(x)), g(y)}, {f(y), f(x)}

+ Rejected triggers:

+   {g(y), f(x)} (loops with {g(f(y))}, {g(f(x))})

+   {g(f(x)), g(f(y))} (stronger than {g(f(x)), f(y)}, {g(f(y)), f(x)}, {f(y), f(x)})

+   {g(f(x)), f(y)} (stronger than {f(y), f(x)})

+   {g(f(y)), f(x)} (stronger than {f(y), f(x)})

+

+Dafny program verifier finished with 5 verified, 0 errors

diff --git a/Test/wishlist/calc.dfy b/Test/wishlist/calc.dfy
new file mode 100644
index 00000000..308fbb9a
--- /dev/null
+++ b/Test/wishlist/calc.dfy
@@ -0,0 +1,17 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// There is a bug in Dafny that causes the error from `L` to be reported at

+// position 0 in this file, instead of on a curly brace.

+

+lemma L()

+  ensures false {

+    calc { true; }

+}

+

+// Empty calc statements work fine, though:

+

+lemma L'()

+  ensures false {

+    calc { }

+}

diff --git a/Test/wishlist/calc.dfy.expect b/Test/wishlist/calc.dfy.expect
new file mode 100644
index 00000000..1d5a55a6
--- /dev/null
+++ b/Test/wishlist/calc.dfy.expect
@@ -0,0 +1,11 @@
+(0,-1): Error BP5003: A postcondition might not hold on this return path.

+calc.dfy(8,10): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    calc.dfy(9,5): anon2_Else

+calc.dfy(15,16): Error BP5003: A postcondition might not hold on this return path.

+calc.dfy(15,10): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 2 verified, 2 errors

diff --git a/Test/wishlist/sequences-literals.dfy b/Test/wishlist/sequences-literals.dfy
new file mode 100644
index 00000000..382349a4
--- /dev/null
+++ b/Test/wishlist/sequences-literals.dfy
@@ -0,0 +1,58 @@
+// RUN: %dafny /compile:0 /autoTriggers:1 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// Note: in the tests below, it could be useful to experiment with the

+// following triggers for some of the library axioms:

+//

+// axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::

+//   { Seq#Contains(s0, x), Seq#Append(s0, s1) }

+//   { Seq#Contains(s1, x), Seq#Append(s0, s1) }

+//   Seq#Contains(Seq#Append(s0, s1), x)

+//      <==> Seq#Contains(s0, x) || Seq#Contains(s1, x));

+//

+// axiom (forall<T> s: Seq T, v: T, x: T ::

+//   { Seq#Contains(s, x), Seq#Build(s, v) }

+//   Seq#Contains(Seq#Build(s, v), x) <==> v == x || Seq#Contains(s, x));

+//

+// Another, not necessarily incompatible approach would be to explicitly add

+// `assume k in s` for each element k of constant lists.

+

+method SmallList() {

+  var s := [0, 1, 5, 6];

+  if * {

+    // This fails: Dafny needs a hint here, because the triggers on the library axioms are pretty strict:

+    assert exists n :: n in s; // WISH

+  } else if * {

+    // This works

+    assert 0 in s;

+    assert exists n :: n in s;

+  } else if * {

+    // This also works, thanks to the magic of triggering on `$Box`.

+    assert exists n {:autotriggers false} :: n in s;

+  }

+}

+

+method LargeList() {

+  var s := [0, 1, 2, 3, 4, 5, 6, 7, 8, /* 9, 10, 11, */ 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, /* 119, 120, 121, */ 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136];

+  if * {

+    // The hint fails here. Maybe because z3 gets into a loop trying to unwrap

+    // this large list? This is also very slow.

+    assert 0 in s; // WISH

+    assert exists n :: n in s;

+  } else if * {

+    // Strangely, the hint works here. Why?

+    assert 122 in s;

+    assert exists n :: n in s;

+  } else if * {

+    // This also fails; since z3 only goes to a depth of 100, this probably

+    // wouldn't work with relaxed triggers eithers

+    assert exists n :: n in s && n >= 120;

+  } else if * {

+    // This works: this is certainly more `triggering-on-$Box` magic, but I'm

+    // not sure exactly how it works

+    assert exists n {:autotriggers false} :: n in s && n >= 120;

+  } else if * {

+    // `$Box` only offers limited solace, though

+    assert exists n {:autotriggers false} :: n in s && n < 3;

+  }

+}

diff --git a/Test/wishlist/sequences-literals.dfy.expect b/Test/wishlist/sequences-literals.dfy.expect
new file mode 100644
index 00000000..18e3f98a
--- /dev/null
+++ b/Test/wishlist/sequences-literals.dfy.expect
@@ -0,0 +1,20 @@
+sequences-literals.dfy(24,11): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Then

+sequences-literals.dfy(40,13): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon17_Then

+sequences-literals.dfy(49,11): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon20_Then

+    (0,0): anon7

+sequences-literals.dfy(56,11): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon24_Then

+    (0,0): anon15

+

+Dafny program verifier finished with 2 verified, 4 errors

diff --git a/Test/wishlist/sequences-s0-in-s.dfy b/Test/wishlist/sequences-s0-in-s.dfy
new file mode 100644
index 00000000..20127917
--- /dev/null
+++ b/Test/wishlist/sequences-s0-in-s.dfy
@@ -0,0 +1,25 @@
+// RUN: %dafny /compile:0 /autoTriggers:1 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// The following is also due to a weakness in the axiomatization: namely, it is

+// not easy to learn, using Dafny's axioms, that s[0] in s. One can of course

+// prove it, but it doesn't come for free.

+

+method InSeqTriggers(s: seq<int>, i: nat)

+  requires forall x :: x in s ==> x > 0;

+  requires |s| > 0 {

+    if * {

+      // Fails

+      assert s[0] > 0; // WISH

+    } else if * {

+      // Works

+      assert s[0] in s;

+      assert s[0] > 0;

+    }

+}

+

+method InSeqNoAutoTriggers(s: seq<int>, i: nat)

+  requires forall x {:autotriggers false} :: x in s ==> x > 0;

+  requires |s| > 0 {

+    assert s[0] > 0; // Works

+}

diff --git a/Test/wishlist/sequences-s0-in-s.dfy.expect b/Test/wishlist/sequences-s0-in-s.dfy.expect
new file mode 100644
index 00000000..4633e5f6
--- /dev/null
+++ b/Test/wishlist/sequences-s0-in-s.dfy.expect
@@ -0,0 +1,6 @@
+sequences-s0-in-s.dfy(13,18): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+

+Dafny program verifier finished with 3 verified, 1 error

diff --git a/Test/wishlist/strings.dfy b/Test/wishlist/strings.dfy
new file mode 100644
index 00000000..372711b0
--- /dev/null
+++ b/Test/wishlist/strings.dfy
@@ -0,0 +1,6 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+method EqualityOfStrings() {

+  assert "a" != "b"; // WISH

+}

diff --git a/Test/wishlist/strings.dfy.expect b/Test/wishlist/strings.dfy.expect
new file mode 100644
index 00000000..2817a66e
--- /dev/null
+++ b/Test/wishlist/strings.dfy.expect
@@ -0,0 +1,5 @@
+strings.dfy(5,13): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 1 verified, 1 error