Fix issue 124. Consider math operators that later turned into function calls

as candidates for triggers.

3 files changed, 42 insertions, 0 deletions

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index f96d3e4c..4204cc29 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -198,6 +198,7 @@ namespace Microsoft.Dafny.Triggers {
           expr is OldExpr || 

           expr is ApplyExpr || 

           expr is DisplayExpression ||

+          TranslateToFunctionCall(expr) ||

           (expr is UnaryOpExpr && (((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Cardinality)) || // FIXME || ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh doesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944

           (expr is BinaryExpr && (((BinaryExpr)expr).Op == BinaryExpr.Opcode.NotIn || ((BinaryExpr)expr).Op == BinaryExpr.Opcode.In))) {

         annotation = AnnotatePotentialCandidate(expr);

@@ -227,6 +228,31 @@ namespace Microsoft.Dafny.Triggers {
       return annotation;

     }

 

+    // math operations can be turned into a Boogie-level function as in the 

+    // case with /noNLarith.

+    public bool TranslateToFunctionCall(Expression expr) {

+      if (!(expr is BinaryExpr)) {

+        return false;

+      }

+      BinaryExpr e = (BinaryExpr) expr;

+      bool isReal = e.E0.Type.IsNumericBased(Type.NumericPersuation.Real);

+      switch (e.ResolvedOp) {

+        case BinaryExpr.ResolvedOpcode.Lt:

+        case BinaryExpr.ResolvedOpcode.Le:

+        case BinaryExpr.ResolvedOpcode.Ge:

+        case BinaryExpr.ResolvedOpcode.Gt:

+        case BinaryExpr.ResolvedOpcode.Add:

+        case BinaryExpr.ResolvedOpcode.Sub:

+        case BinaryExpr.ResolvedOpcode.Mul:

+        case BinaryExpr.ResolvedOpcode.Div:

+        case BinaryExpr.ResolvedOpcode.Mod:

+          if (!isReal && DafnyOptions.O.DisableNLarith) {

+            return true;

+          }

+          break;

+      }

+      return false;

+    }

     private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) {

       bool expr_is_killer = false;

       var new_expr = TriggerUtils.MaybeWrapInOld(TriggerUtils.PrepareExprForInclusionInTrigger(expr, out expr_is_killer), cache.exprsInOldContext.Contains(expr));

diff --git a/Test/dafny4/Bug124.dfy b/Test/dafny4/Bug124.dfy
new file mode 100644
index 00000000..60f26a00
--- /dev/null
+++ b/Test/dafny4/Bug124.dfy
@@ -0,0 +1,14 @@
+// RUN: %dafny /compile:0 /autoTriggers:1 /noNLarith  "%s" > "%t"

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

+

+function power(n:nat, e:nat) : int

+

+lemma lemma_power()

+    ensures forall n:nat, e:nat :: 0 <= n * e && power(n, e) == 5;

+{

+    forall n:nat, e:nat 

+        ensures 0 <= n * e && power(n, e) == 5;

+    {

+        assume false;

+    }

+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug124.dfy.expect b/Test/dafny4/Bug124.dfy.expect
new file mode 100644
index 00000000..52595bf9
--- /dev/null
+++ b/Test/dafny4/Bug124.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 3 verified, 0 errors