Add the ability to specify how much "fuel" a function should have,

i.e., how many times Z3 is permitted to unfold it's definition.  The
new {:fuel} annotation can be added to the function itself, it which
case it will apply to all uses of that function, or it can overridden
within the scope of a module, function, method, iterator, calc, forall,
while, assert, or assume.  The general format is:

{:fuel functionName,lowFuel,highFuel}

When applied as an annotation to the function itself, omit functionName.
If highFuel is omitted, it defaults to lowFuel + 1.

The default fuel setting for recursive functions is 1,2.  Setting the fuel higher,
say, to 3,4, will give more unfoldings, which may make some proofs go through
with less programmer assistance (e.g., with fewer assert statements), but it may
also increase verification time, so use it with care.  Setting the fuel to 0,0 is
similar to making the definition opaque, except when used with all literal arguments.

1 files changed, 3 insertions, 1 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 6cc0af5a..5d4a4321 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1965,6 +1965,7 @@ ModifyStmt<out Statement s>
 CalcStmt<out Statement s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);

      Token x;

+     Attributes attrs = null;

      CalcStmt.CalcOp op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;

      var lines = new List<Expression>();

      var hints = new List<BlockStmt>();

@@ -1976,6 +1977,7 @@ CalcStmt<out Statement s>
      IToken danglingOperator = null;

   .)

   "calc"                                                  (. x = t; .)

+  { IF(IsAttribute()) Attribute<ref attrs> }

   [ CalcOp<out opTok, out calcOp>                         (. maybeOp = calcOp.ResultOp(calcOp); // guard against non-transitive calcOp (like !=)

                                                              if (maybeOp == null) {

                                                                SemErr(opTok, "the main operator of a calculation must be transitive");

@@ -2024,7 +2026,7 @@ CalcStmt<out Statement s>
       // Repeat the last line to create a dummy line for the dangling hint

       lines.Add(lines[lines.Count - 1]);

     }

-    s = new CalcStmt(x, t, calcOp, lines, hints, stepOps, resOp);

+    s = new CalcStmt(x, t, calcOp, lines, hints, stepOps, resOp, attrs);

   .)

   .

 CalcOp<out IToken x, out CalcStmt.CalcOp/*!*/ op>