Allow disable-non-linear-arithmetic per module

Source/DafnyCore/DafnyCore.csproj

@@ -32,7 +32,7 @@
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.5" />
+      <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.6" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 

Source/DafnyCore/DafnyOptions.cs

@@ -1158,7 +1158,7 @@ public void SetZ3Options(Version z3Version) {
       // (or verified at all) using a different solver.
       SetZ3Option("smt.arith.solver", "2");
 
-      if (DisableNLarith || 3 <= ArithMode) {
+      if (3 <= ArithMode) {
         SetZ3Option("smt.arith.nl", "false");
       }
     }

Source/DafnyCore/Options/BoogieOptionBag.cs

@@ -120,7 +120,7 @@ static BoogieOptionBag() {
         o.TheProverFactory = ProverFactory.Load(o.ProverDllName);
       }
     });
-    DafnyOptions.RegisterLegacyBinding(SolverResourceLimit, (o, v) => o.ResourceLimit = v);
+    DafnyOptions.RegisterLegacyBinding(SolverResourceLimit, (o, v) => o.ResourceLimit = Boogie.Util.BoundedMultiply(v, 1000));
     DafnyOptions.RegisterLegacyBinding(SolverLog, (o, v) => o.ProverLogFilePath = v);
     DafnyOptions.RegisterLegacyBinding(SolverOption, (o, v) => {
       if (v is not null) {

Source/DafnyCore/Rewriters/TriggerGeneratingRewriter.cs

@@ -16,7 +16,7 @@ internal override void PostCyclicityResolve(ModuleDefinition definition, ErrorRe
       finder.Visit(decl, null);
     }
 
-    var triggersCollector = new Triggers.TriggersCollector(finder.exprsInOldContext, Reporter.Options);
+    var triggersCollector = new Triggers.TriggersCollector(finder.exprsInOldContext, Reporter.Options, definition);
     foreach (var quantifierCollection in finder.quantifierCollections) {
       quantifierCollection.ComputeTriggers(triggersCollector);
       quantifierCollection.CommitTriggers(Reporter.Options, systemModuleManager);

Source/DafnyCore/Triggers/QuantifierSplitter.cs

@@ -147,8 +147,8 @@ internal void Commit() {
   }
 
   class MatchingLoopRewriter {
-    public MatchingLoopRewriter(DafnyOptions options) {
-      triggersCollector = new TriggersCollector(new Dictionary<Expression, HashSet<OldExpr>>(), options);
+    public MatchingLoopRewriter(DafnyOptions options, ModuleDefinition forModule) {
+      triggersCollector = new TriggersCollector(new Dictionary<Expression, HashSet<OldExpr>>(), options, forModule);
     }
 
     TriggersCollector triggersCollector;

Source/DafnyCore/Triggers/QuantifiersCollection.cs

@@ -49,7 +49,7 @@ internal void ComputeTriggers(TriggersCollector triggersCollector) {
       CollectAndShareTriggers(triggersCollector);
       TrimInvalidTriggers();
       BuildDependenciesGraph();
-      if (SuppressMatchingLoops() && RewriteMatchingLoop()) {
+      if (SuppressMatchingLoops() && RewriteMatchingLoop(triggersCollector)) {
         CollectWithoutShareTriggers(triggersCollector);
         TrimInvalidTriggers();
         SuppressMatchingLoops();
@@ -169,15 +169,15 @@ bool SuppressMatchingLoops() {
       return foundloop;
     }
 
-    bool RewriteMatchingLoop() {
+    bool RewriteMatchingLoop(TriggersCollector triggersCollector) {
       if (expr is QuantifierExpr) {
         QuantifierExpr quantifier = (QuantifierExpr)expr;
         var l = new List<QuantifierWithTriggers>();
         List<Expression> splits = new List<Expression>();
         bool rewritten = false;
         foreach (var q in quantifiers) {
           if (TriggerUtils.NeedsAutoTriggers(q.quantifier) && TriggerUtils.WantsMatchingLoopRewrite(q.quantifier)) {
-            var matchingLoopRewriter = new MatchingLoopRewriter(reporter.Options);
+            var matchingLoopRewriter = new MatchingLoopRewriter(reporter.Options, triggersCollector.ForModule);
             var qq = matchingLoopRewriter.RewriteMatchingLoops(q);
             splits.Add(qq);
             l.Add(new QuantifierWithTriggers(qq));

Source/DafnyCore/Triggers/TriggersCollector.cs

@@ -158,11 +158,13 @@ public TriggerAnnotationsCache(Dictionary<Expression, HashSet<OldExpr>> exprsInO
   }
 
   internal class TriggersCollector {
+    public ModuleDefinition ForModule { get; }
     private DafnyOptions options;
     TriggerAnnotationsCache cache;
 
-    internal TriggersCollector(Dictionary<Expression, HashSet<OldExpr>> exprsInOldContext, DafnyOptions options) {
+    internal TriggersCollector(Dictionary<Expression, HashSet<OldExpr>> exprsInOldContext, DafnyOptions options, ModuleDefinition forModule) {
       this.options = options;
+      this.ForModule = forModule;
       this.cache = new TriggerAnnotationsCache(exprsInOldContext);
     }
 
@@ -281,22 +283,23 @@ public bool TranslateToFunctionCall(Expression expr) {
       }
       BinaryExpr e = (BinaryExpr)expr;
       bool isReal = e.E0.Type.IsNumericBased(Type.NumericPersuasion.Real);
+      var disableNonLinearArithmetic = BoogieGenerator.DetermineDisableNonLinearArithmetic(ForModule, options);
       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:
-          if (!isReal && !e.E0.Type.IsBitVectorType && !e.E0.Type.IsBigOrdinalType && options.DisableNLarith) {
+          if (!isReal && !e.E0.Type.IsBitVectorType && !e.E0.Type.IsBigOrdinalType && disableNonLinearArithmetic) {
             return true;
           }
           break;
         case BinaryExpr.ResolvedOpcode.Mul:
         case BinaryExpr.ResolvedOpcode.Div:
         case BinaryExpr.ResolvedOpcode.Mod:
           if (!isReal && !e.E0.Type.IsBitVectorType && !e.E0.Type.IsBigOrdinalType) {
-            if (options.DisableNLarith || (options.ArithMode != 0 && options.ArithMode != 3)) {
+            if (disableNonLinearArithmetic || (options.ArithMode != 0 && options.ArithMode != 3)) {
               return true;
             }
           }

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -3,13 +3,15 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using System.Numerics;
+using Microsoft.BaseTypes;
 using Microsoft.Boogie;
 using static Microsoft.Dafny.Util;
 
 namespace Microsoft.Dafny {
   public partial class BoogieGenerator {
     public class ExpressionTranslator {
       private DafnyOptions options;
+
       // HeapExpr == null ==> translation of pure (no-heap) expression
       readonly Boogie.Expr _the_heap_expr;
       public Boogie.Expr HeapExpr {
@@ -923,7 +925,7 @@ public Boogie.Expr TrExpr(Expression expr) {
                     return TrToFunctionCall(GetToken(binaryExpr), "lt_bv" + bvWidth, Boogie.Type.Bool, e0, e1, liftLit);
                   } else if (e.E0.Type.IsBigOrdinalType) {
                     return FunctionCall(GetToken(binaryExpr), "ORD#Less", Boogie.Type.Bool, e0, e1);
-                  } else if (isReal || !options.DisableNLarith) {
+                  } else if (isReal || !BoogieGenerator.DisableNonLinearArithmetic) {
                     typ = Boogie.Type.Bool;
                     bOpcode = BinaryOperator.Opcode.Lt;
                     break;
@@ -940,7 +942,7 @@ public Boogie.Expr TrExpr(Expression expr) {
                     var less = FunctionCall(GetToken(binaryExpr), "ORD#Less", Boogie.Type.Bool, e0, e1);
                     var eq = Boogie.Expr.Eq(e0, e1);
                     return BplOr(eq, less);
-                  } else if (isReal || !options.DisableNLarith) {
+                  } else if (isReal || !BoogieGenerator.DisableNonLinearArithmetic) {
                     typ = Boogie.Type.Bool;
                     bOpcode = BinaryOperator.Opcode.Le;
                     break;
@@ -955,7 +957,7 @@ public Boogie.Expr TrExpr(Expression expr) {
                     var less = FunctionCall(GetToken(binaryExpr), "ORD#Less", Boogie.Type.Bool, e1, e0);
                     var eq = Boogie.Expr.Eq(e1, e0);
                     return BplOr(eq, less);
-                  } else if (isReal || !options.DisableNLarith) {
+                  } else if (isReal || !BoogieGenerator.DisableNonLinearArithmetic) {
                     typ = Boogie.Type.Bool;
                     bOpcode = BinaryOperator.Opcode.Ge;
                     break;
@@ -967,7 +969,7 @@ public Boogie.Expr TrExpr(Expression expr) {
                     return TrToFunctionCall(GetToken(binaryExpr), "gt_bv" + bvWidth, Boogie.Type.Bool, e0, e1, liftLit);
                   } else if (e.E0.Type.IsBigOrdinalType) {
                     return FunctionCall(GetToken(binaryExpr), "ORD#Less", Boogie.Type.Bool, e1, e0);
-                  } else if (isReal || !options.DisableNLarith) {
+                  } else if (isReal || !BoogieGenerator.DisableNonLinearArithmetic) {
                     typ = Boogie.Type.Bool;
                     bOpcode = BinaryOperator.Opcode.Gt;
                     break;
@@ -982,7 +984,7 @@ public Boogie.Expr TrExpr(Expression expr) {
                     return TrToFunctionCall(GetToken(binaryExpr), "ORD#Plus", predef.BigOrdinalType, e0, e1, liftLit);
                   } else if (e.E0.Type.IsCharType) {
                     return TrToFunctionCall(GetToken(binaryExpr), "char#Plus", predef.CharType, e0, e1, liftLit);
-                  } else if (!isReal && options.DisableNLarith) {
+                  } else if (!isReal && BoogieGenerator.DisableNonLinearArithmetic) {
                     return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_add_boogie", Boogie.Type.Int, e0, e1, liftLit);
                   } else if (!isReal && (options.ArithMode == 2 || 5 <= options.ArithMode)) {
                     return TrToFunctionCall(GetToken(binaryExpr), "Add", Boogie.Type.Int, oe0, oe1, liftLit);
@@ -998,7 +1000,7 @@ public Boogie.Expr TrExpr(Expression expr) {
                     return TrToFunctionCall(GetToken(binaryExpr), "ORD#Minus", predef.BigOrdinalType, e0, e1, liftLit);
                   } else if (e.E0.Type.IsCharType) {
                     return TrToFunctionCall(GetToken(binaryExpr), "char#Minus", predef.CharType, e0, e1, liftLit);
-                  } else if (!isReal && options.DisableNLarith) {
+                  } else if (!isReal && BoogieGenerator.DisableNonLinearArithmetic) {
                     return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_sub_boogie", Boogie.Type.Int, e0, e1, liftLit);
                   } else if (!isReal && (options.ArithMode == 2 || 5 <= options.ArithMode)) {
                     return TrToFunctionCall(GetToken(binaryExpr), "Sub", Boogie.Type.Int, oe0, oe1, liftLit);
@@ -1010,7 +1012,7 @@ public Boogie.Expr TrExpr(Expression expr) {
                 case BinaryExpr.ResolvedOpcode.Mul:
                   if (0 <= bvWidth) {
                     return TrToFunctionCall(GetToken(binaryExpr), "mul_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit);
-                  } else if (!isReal && options.DisableNLarith) {
+                  } else if (!isReal && BoogieGenerator.DisableNonLinearArithmetic) {
                     return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_mul_boogie", Boogie.Type.Int, e0, e1, liftLit);
                   } else if (!isReal && options.ArithMode != 0 && options.ArithMode != 3) {
                     return TrToFunctionCall(GetToken(binaryExpr), "Mul", Boogie.Type.Int, oe0, oe1, liftLit);
@@ -1022,7 +1024,7 @@ public Boogie.Expr TrExpr(Expression expr) {
                 case BinaryExpr.ResolvedOpcode.Div:
                   if (0 <= bvWidth) {
                     return TrToFunctionCall(GetToken(binaryExpr), "div_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit);
-                  } else if (!isReal && options.DisableNLarith && !isReal) {
+                  } else if (!isReal && BoogieGenerator.DisableNonLinearArithmetic && !isReal) {
                     return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_div_boogie", Boogie.Type.Int, e0, e1, liftLit);
                   } else if (!isReal && options.ArithMode != 0 && options.ArithMode != 3) {
                     return TrToFunctionCall(GetToken(binaryExpr), "Div", Boogie.Type.Int, e0, oe1, liftLit);
@@ -1038,7 +1040,7 @@ public Boogie.Expr TrExpr(Expression expr) {
                 case BinaryExpr.ResolvedOpcode.Mod:
                   if (0 <= bvWidth) {
                     return TrToFunctionCall(GetToken(binaryExpr), "mod_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit);
-                  } else if (options.DisableNLarith && !isReal) {
+                  } else if (BoogieGenerator.DisableNonLinearArithmetic && !isReal) {
                     return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_mod_boogie", Boogie.Type.Int, e0, e1, liftLit);
                   } else if (!isReal && options.ArithMode != 0 && options.ArithMode != 3) {
                     return TrToFunctionCall(GetToken(binaryExpr), "Mod", Boogie.Type.Int, e0, oe1, liftLit);
@@ -1943,6 +1945,15 @@ public Boogie.QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute)
           } else if (name == "synthesize") {
             name = "extern";
           }
+
+          // Values for _rlimit are already in terms of Boogie units (1000 x user-provided value) because they're
+          // derived from command-line rlimit settings.
+          if (!hasNewRLimit && name == "rlimit" && parms.Count > 0 && parms[0] is Boogie.LiteralExpr litExpr && litExpr.isBigNum) {
+            parms[0] = new Boogie.LiteralExpr(
+              litExpr.tok,
+              BigNum.FromUInt(Boogie.Util.BoundedMultiply((uint)litExpr.asBigNum.ToIntSafe, 1000)),
+              litExpr.Immutable);
+          }
           kv = new Boogie.QKeyValue(Token.NoToken, name, parms, kv);
         }
         return kv;
@@ -2094,7 +2105,7 @@ public Expr CanCallAssumption(Expression expr) {
               }
             case BinaryExpr.ResolvedOpcode.Mul:
               if (7 <= BoogieGenerator.options.ArithMode) {
-                if (e.E0.Type.IsNumericBased(Type.NumericPersuasion.Int) && !BoogieGenerator.options.DisableNLarith) {
+                if (e.E0.Type.IsNumericBased(Type.NumericPersuasion.Int) && !BoogieGenerator.DisableNonLinearArithmetic) {
                   // Produce a useful fact about the associativity of multiplication. It is a bit dicey to do as an axiom.
                   // Change (k*A)*B or (A*k)*B into (A*B)*k, where k is a numeric literal
                   var left = e.E0.Resolved as BinaryExpr;

Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs

@@ -194,7 +194,7 @@ void AddWellformednessCheck(ConstantField decl) {
       var proc = new Bpl.Procedure(decl.tok, name, new List<Bpl.TypeVariable>(),
         inParams, new List<Variable>(),
         false, req, varlist, new List<Bpl.Ensures>(), etran.TrAttributes(decl.Attributes, null));
-      AddVerboseName(proc, decl.FullDafnyName, MethodTranslationKind.SpecWellformedness);
+      AddVerboseNameAttribute(proc, decl.FullDafnyName, MethodTranslationKind.SpecWellformedness);
       sink.AddTopLevelDeclaration(proc);
 
       var implInParams = Bpl.Formal.StripWhereClauses(inParams);
@@ -216,7 +216,7 @@ void AddWellformednessCheck(ConstantField decl) {
         QKeyValue kv = etran.TrAttributes(decl.Attributes, null);
         var implBody = builder.Collect(decl.tok);
 
-        AddImplementationWithVerboseName(GetToken(decl), proc, implInParams,
+        AddImplementationWithAttributes(GetToken(decl), proc, implInParams,
           new List<Variable>(), locals, implBody, kv);
       }
 

Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs

@@ -100,7 +100,7 @@ void AddWellformednessCheck(Function f) {
     var proc = new Bpl.Procedure(f.tok, "CheckWellformed" + NameSeparator + f.FullSanitizedName, new List<Bpl.TypeVariable>(),
       Concat(Concat(typeInParams, inParams_Heap), inParams), outParams,
       false, req, mod, ens, etran.TrAttributes(f.Attributes, null));
-    AddVerboseName(proc, f.FullDafnyName, MethodTranslationKind.SpecWellformedness);
+    AddVerboseNameAttribute(proc, f.FullDafnyName, MethodTranslationKind.SpecWellformedness);
     sink.AddTopLevelDeclaration(proc);
 
     if (InsertChecksums) {
@@ -283,7 +283,7 @@ void AddWellformednessCheck(Function f) {
     if (EmitImplementation(f.Attributes)) {
       // emit the impl only when there are proof obligations.
       QKeyValue kv = etran.TrAttributes(f.Attributes, null);
-      var impl = AddImplementationWithVerboseName(GetToken(f), proc,
+      var impl = AddImplementationWithAttributes(GetToken(f), proc,
         Concat(Concat(Bpl.Formal.StripWhereClauses(typeInParams), inParams_Heap), implInParams),
         implOutParams,
         locals, implBody, kv);

Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs

@@ -123,7 +123,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) {
 
       var name = MethodName(iter, kind);
       var proc = new Bpl.Procedure(iter.tok, name, new List<Bpl.TypeVariable>(), inParams, outParams, false, req, mod, ens, etran.TrAttributes(iter.Attributes, null));
-      AddVerboseName(proc, iter.FullDafnyName, kind);
+      AddVerboseNameAttribute(proc, iter.FullDafnyName, kind);
 
       currentModule = null;
       codeContext = null;
@@ -255,7 +255,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) {
 
       if (EmitImplementation(iter.Attributes)) {
         QKeyValue kv = etran.TrAttributes(iter.Attributes, null);
-        AddImplementationWithVerboseName(GetToken(iter), proc, inParams, new List<Variable>(),
+        AddImplementationWithAttributes(GetToken(iter), proc, inParams, new List<Variable>(),
           localVariables, stmts, kv);
       }
 
@@ -323,7 +323,7 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) {
         // emit the impl only when there are proof obligations.
         QKeyValue kv = etran.TrAttributes(iter.Attributes, null);
 
-        AddImplementationWithVerboseName(GetToken(iter), proc, inParams,
+        AddImplementationWithAttributes(GetToken(iter), proc, inParams,
           new List<Variable>(), localVariables, stmts, kv);
       }