Major simplifications

boogie-org · Nov 15, 2023 · 4ad4d6a · 4ad4d6a
1 parent 7529785
commit 4ad4d6a
Show file tree

Hide file tree

Showing 6 changed files with 27 additions and 25 deletions.
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
@@ -270,10 +270,12 @@ public virtual void SetRlimit(uint limit)
   {
   }
 
-  public virtual void SetOtherSMTOption(string name, string value)
+  // Sets a local SMT option (cleared with ClearLocalSMTOptions)
+  public virtual void SetLocalSMTOption(string name, string value)
   {
   }
 
+  // Clear options set with SetLocalSMTOption
   public virtual void ClearLocalSMTOptions()
   {
   }

diff --git a/Source/Provers/SMTLib/ProverUtil.cs b/Source/Provers/SMTLib/ProverUtil.cs
@@ -20,8 +20,6 @@ public class ProverOptions
     public bool ForceLogStatus = false;
     public uint TimeLimit = 0;
     public uint ResourceLimit = 0;
-    // Other options suitable for (set-option :key value)
-    // TODO: put ResourceLimit in here?
     public int? RandomSeed = null;
     public int MemoryLimit = 0;
     public int Verbosity = 0;

diff --git a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs
@@ -1,7 +1,6 @@
 using System;
 using System.Collections.Concurrent;
 using System.Collections.Generic;
-using System.ComponentModel.Design;
 using System.IO;
 using System.Linq;
 using System.Diagnostics;
@@ -434,6 +433,7 @@ protected void SendVCOptions()
       if (options.Solver == SolverKind.Z3 || options.Solver == SolverKind.NoOpWithZ3Options)
       {
         SendThisVC("(set-option :" + Z3.TimeoutOption + " " + options.TimeLimit + ")");
+        SendThisVC("(set-option :" + Z3.RlimitOption + " " + options.ResourceLimit + ")");
         if (options.RandomSeed != null) {
           SendThisVC("(set-option :" + Z3.SmtRandomSeed + " " + options.RandomSeed.Value + ")");
           SendThisVC("(set-option :" + Z3.SatRandomSeed + " " + options.RandomSeed.Value + ")");
@@ -1162,27 +1162,17 @@ public override void AssertAxioms()
       FlushAxioms();
     }
 
-    // This doesn't use SetOtherSMTOption because it may be set using
-    // different mechanisms than set-option in some cases.
     public override void SetTimeout(uint ms)
     {
       options.TimeLimit = ms;
     }
 
-    // Don't use SetOtherSMTOption directly, because we want a
-    // connection to TimeLimit.
     public override void SetRlimit(uint limit)
     {
-      if (options.Solver == SolverKind.Z3) {
-        SetOtherSMTOption(Z3.RlimitOption, limit.ToString());
-        if (limit > 0) {
-          SetTimeout(0);
-        }
-      }
+      options.ResourceLimit = limit;
     }
 
-    // Note: must be re-set for every query
-    public override void SetOtherSMTOption(string name, string value)
+    public override void SetLocalSMTOption(string name, string value)
     {
       options.SmtOptions.Add(new OptionValue(name, value));
     }

diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs
@@ -143,6 +143,16 @@ public void Target(Program prog, ProverContext ctx, Split split)
       }
     }
 
+    private void SetTimeout(uint timeout)
+    {
+      TheoremProver.SetTimeout(Util.BoundedMultiply(timeout, 1000));
+    }
+
+    private void SetRlimit(uint rlimit)
+    {
+      TheoremProver.SetRlimit(rlimit);
+    }
+
     /// <summary>
     /// Set up the context.
     /// </summary>
@@ -306,7 +316,7 @@ private async Task Check(string descriptiveName, VCExpr vc, CancellationToken ca
       proverRunTime = ProverStopwatch.Elapsed;
     }
 
-    public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, CancellationToken cancellationToken)
+    public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, uint timeout, uint rlimit, CancellationToken cancellationToken)
     {
       Contract.Requires(descriptiveName != null);
       Contract.Requires(vc != null);
@@ -319,6 +329,12 @@ public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.
       this.handler = handler;
 
       await thmProver.Reset(gen);
+      if (0 < rlimit)
+      {
+        timeout = 0;
+      }
+      SetTimeout(timeout);
+      SetRlimit(rlimit);
 
       ProverStart = DateTime.UtcNow;
       ProverStopwatch.Restart();

diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs
@@ -305,10 +305,8 @@ async Task<bool> CheckUnreachable(TextWriter traceWriter, Block cur, List<Cmd> s
           Emit();
         }
       }
-
-      checker.TheoremProver.SetTimeout(Options.SmokeTimeout);
-      checker.TheoremProver.SetRlimit(Options.ResourceLimit);
-      await checker.BeginCheck(cce.NonNull(Implementation.Name + "_smoke" + id++), vc, new ErrorHandler(Options, absyIds, callback), CancellationToken.None);
+      await checker.BeginCheck(cce.NonNull(Implementation.Name + "_smoke" + id++), vc, new ErrorHandler(Options, absyIds, callback),
+        Options.SmokeTimeout, Options.ResourceLimit, CancellationToken.None);
 
       await checker.ProverTask;
 

diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs
@@ -1353,12 +1353,10 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa
           Print();
         }
 
-        checker.TheoremProver.SetTimeout(Util.BoundedMultiply(timeout, 1000));
-        checker.TheoremProver.SetRlimit(rlimit);
         foreach (var entry in Implementation.GetExtraSMTOptions()) {
-          checker.TheoremProver.SetOtherSMTOption(entry.Key, entry.Value);
+          checker.TheoremProver.SetLocalSMTOption(entry.Key, entry.Value);
         }
-        await checker.BeginCheck(Description, vc, reporter, cancellationToken);
+        await checker.BeginCheck(Description, vc, reporter, timeout, rlimit, cancellationToken);
       }
 
       public string Description