Add smt_option attribute (#808)

This adds support for an attribute of the form `{:smt_option name,
value}` to set SMT-Lib options using the `(set-option :name value)`
command. It's available on a per-procedure level.

Source/Core/AST/Absy.cs

@@ -3673,6 +3673,22 @@ public int Priority
       }
     }
 
+    public Dictionary<string, string> GetExtraSMTOptions()
+    {
+      Dictionary<string, string> extraSMTOpts = new();
+      for (var a = Attributes; a != null; a = a.Next) {
+        var n = a.Params.Count;
+        var k = a.Key;
+        if (k.Equals("smt_option")) {
+          if (n == 2 && a.Params[0] is string s) {
+            extraSMTOpts.Add(s, a.Params[1].ToString());
+          }
+        }
+      }
+
+      return extraSMTOpts;
+    }
+
     public IDictionary<byte[], object> ErrorChecksumToCachedError { get; private set; }
 
     public bool IsErrorChecksumInCachedSnapshot(byte[] checksum)

Source/Directory.Build.props

@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.0.5</Version>
+    <Version>3.0.6</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

Source/ExecutionEngine/CommandLineOptions.cs

@@ -1523,6 +1523,11 @@ used by the `/trackVerificationCoverage` option.
        Set the random seed for verifying a given implementation.
        Has the same effect as setting /randomSeed but only for a single implementation.
 
+     {:smt_option name, value}
+       Set the SMT option 'name' to 'value', using the SMT-Lib command
+       '(set-option :name value)', just for the verification of this
+       procedure.
+
      {:verboseName <string>}
        Set the name to use when printing messages about verification
        status in `/trace` and selecting procedures to verify with

Source/Provers/SMTLib/ProverInterface.cs

@@ -270,6 +270,16 @@ public virtual void SetRlimit(uint limit)
   {
   }
 
+  // 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()
+  {
+  }
+
   public virtual Task<int> GetRCount()
   {
     throw new NotImplementedException();

Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs

@@ -439,6 +439,10 @@ protected void SendVCOptions()
           SendThisVC("(set-option :" + Z3.SatRandomSeed + " " + options.RandomSeed.Value + ")");
         }
       }
+
+      foreach (var entry in options.SmtOptions) {
+        SendThisVC("(set-option :" + entry.Option + " " + entry.Value + ")");
+      }
     }
 
     protected void SendVCId(string descriptiveName)
@@ -1168,6 +1172,18 @@ public override void SetRlimit(uint limit)
       options.ResourceLimit = limit;
     }
 
+    public override void SetLocalSMTOption(string name, string value)
+    {
+      options.SmtOptions.Add(new OptionValue(name, value));
+    }
+
+    public override void ClearLocalSMTOptions()
+    {
+      // Go back to global options
+      options.SmtOptions.Clear();
+      options.Parse(libOptions.ProverOptions);
+    }
+
     protected Outcome ParseOutcome(SExpr resp, out bool wasUnknown)
     {
       var result = Outcome.Undetermined;

Source/VCGeneration/Split.cs

@@ -1353,6 +1353,9 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa
           Print();
         }
 
+        foreach (var entry in Implementation.GetExtraSMTOptions()) {
+          checker.TheoremProver.SetLocalSMTOption(entry.Key, entry.Value);
+        }
         await checker.BeginCheck(Description, vc, reporter, timeout, rlimit, cancellationToken);
       }
 

Source/VCGeneration/SplitAndVerifyWorker.cs

@@ -193,6 +193,8 @@ private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Ch
         batchCompletions.OnNext((split, result));
         await checker.GoBackToIdle();
       }
+
+      checker.TheoremProver.ClearLocalSMTOptions();
     }
 
     private static bool IsProverFailed(ProverInterface.Outcome outcome)

Test/prover/smt-options.bpl

@@ -0,0 +1,10 @@
+// RUN: %boogie /proverLog:"%t.smt2" "%s"
+// RUN: %OutputCheck --file-to-check "%t.smt2" "%s"
+// CHECK: (set-option :smt.arith.solver 2)
+// CHECK: (set-option :smt.case_split 2)
+procedure
+{:smt_option "smt.arith.solver", 2}
+{:smt_option "smt.case_split", 2}
+P1(a: int, b: int) {
+  assert (a + b) - (a * b) == (b + a) - (a * b);
+}