Provide /p: as the short form of /proverOpt:.

Add /p:O:<name>=<value> and /p:C:<solver-argument> prover options in SMT.
Add default Z3 options when using Z3.

7 files changed, 215 insertions, 46 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 0c47754b..4396d837 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1063,6 +1063,8 @@ namespace Microsoft.Boogie {
             }

             break;

 

+          case "-p":

+          case "/p":

           case "-proverOpt":

           case "/proverOpt":

             if (ps.ConfirmArgumentCount(1)) {

@@ -2242,7 +2244,7 @@ namespace Microsoft.Boogie {
                    SMTLib (only writes to a file)

                    ContractInference (uses Z3)

                    Z3api (Z3 using Managed .NET API)

-  /proverOpt:KEY[=VALUE] : Provide a prover-specific option.

+  /proverOpt:KEY[=VALUE] : Provide a prover-specific option (short form /p).

   /proverLog:<file> : Log input for the theorem prover.  Like filenames

                    supplied as arguments to other options, <file> can use the

                    following macros:

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index bfcbf682..f299af30 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -22,36 +22,6 @@ using System.Text;
 

 namespace Microsoft.Boogie.SMTLib

 {

-  public class SMTLibProverOptions : ProverOptions

-  {

-    public bool UseWeights = true;

-    public bool UseLabels { get { return UseZ3; } }

-    public bool UseZ3 = true;

-

-    protected override bool Parse(string opt)

-    {

-      return

-        ParseBool(opt, "USE_WEIGHTS", ref UseWeights) ||

-        ParseBool(opt, "USE_Z3", ref UseZ3) ||

-        base.Parse(opt);

-    }

-

-    public override string Help

-    {

-      get

-      {

-        return

-@"

-SMT-specific options:

-~~~~~~~~~~~~~~~~~~~~~

-USE_Z3=<bool>             Use z3.exe as the prover, and use Z3 extensions (default: true)

-USE_WEIGHTS=<bool>        Pass :weight annotations on quantified formulas (default: true)

-VERBOSITY=<int>           1 - print prover output (default: 0)

-" + base.Help;

-      }

-    }

-  }

-

   public class SMTLibProcessTheoremProver : ProverInterface

   {

     private readonly DeclFreeProverContext ctx;

@@ -105,7 +75,7 @@ VERBOSITY=<int>           1 - print prover output (default: 0)
       this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer);

 

       if (this.options.UseZ3) {

-        var psi = SMTLibProcess.ComputerProcessStartInfo(Z3.Z3ExecutablePath(), "AUTO_CONFIG=false -smt2 -in");

+        var psi = SMTLibProcess.ComputerProcessStartInfo(Z3.ExecutablePath(), "AUTO_CONFIG=false -smt2 -in");

         Process = new SMTLibProcess(psi, this.options);

         Process.ErrorHandler += this.HandleProverError;

       }

@@ -171,8 +141,15 @@ VERBOSITY=<int>           1 - print prover output (default: 0)
 

     private void PrepareCommon()

     {

-      if (common.Length == 0)

+      if (common.Length == 0) {

+        SendCommon("(set-option :print-success false)");

+        SendCommon("(set-info :smt-lib-version 2.0)");

+        foreach (var opt in options.SmtOptions) {

+          SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");

+        }

+        SendCommon("; done setting options\n");

         SendCommon(_backgroundPredicates);

+      }

 

       if (!AxiomsAreSetup) {

         var axioms = ctx.Axioms;

@@ -275,6 +252,9 @@ VERBOSITY=<int>           1 - print prover output (default: 0)
         return result;

 

       var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;

+      if (errorsLeft < 1)

+        errorsLeft = 1;

+

       var globalResult = Outcome.Undetermined;

 

       while (errorsLeft-- > 0) {

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index 536fd43e..4eb753a2 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -107,6 +107,7 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

+    <Compile Include="SMTLibProverOptions.cs" />

     <Compile Include="ProverInterface.cs" />

     <Compile Include="SExpr.cs" />

     <Compile Include="SMTLibLineariser.cs" />

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 8cc67256..b23fddbb 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -71,7 +71,7 @@ namespace Microsoft.Boogie.SMTLib
 

     public bool IsPong(SExpr sx)

     {

-      return sx.Name == ":name";

+      return sx != null && sx.Name == ":name";

     }

 

     public void PingPong()

@@ -79,6 +79,11 @@ namespace Microsoft.Boogie.SMTLib
       Ping();

       while (true) {

         var sx = GetProverResponse();

+        if (sx == null) {

+          ErrorHandler("Prover died");

+          return;

+        }

+

         if (IsPong(sx))

           return;

         else

@@ -261,21 +266,25 @@ namespace Microsoft.Boogie.SMTLib
     void prover_OutputDataReceived(object sender, DataReceivedEventArgs e)

     {

       lock (this) {

-        if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name"))) {

-          Console.WriteLine("[SMT-OUT] {0}", e.Data);

+        if (e.Data != null) {

+          if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name "))) {

+            Console.WriteLine("[SMT-OUT] {0}", e.Data);

+          }

+          proverOutput.Enqueue(e.Data);

+          Monitor.Pulse(this);

         }

-        proverOutput.Enqueue(e.Data);

-        Monitor.Pulse(this);

       }

     }

 

     void prover_ErrorDataReceived(object sender, DataReceivedEventArgs e)

     {

       lock (this) {

-        if (options.Verbosity >= 1)

-          Console.WriteLine("[SMT-ERR] {0}", e.Data);

-        proverErrors.Enqueue(e.Data);

-        Monitor.Pulse(this);

+        if (e.Data != null) {

+          if (options.Verbosity >= 1)

+            Console.WriteLine("[SMT-ERR] {0}", e.Data);

+          proverErrors.Enqueue(e.Data);

+          Monitor.Pulse(this);

+        }

       }

     }

     #endregion

diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
new file mode 100644
index 00000000..0565e677
--- /dev/null
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -0,0 +1,115 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics.Contracts;

+

+namespace Microsoft.Boogie.SMTLib

+{

+

+  public class OptionValue

+  {

+    public readonly string Option;

+    public readonly string Value;

+    [ContractInvariantMethod]

+    void ObjectInvariant()

+    {

+      Contract.Invariant(Option != null);

+      Contract.Invariant(Value != null);

+    }

+

+    public OptionValue(string option, string value)

+    {

+      Contract.Requires(option != null);

+      Contract.Requires(value != null);

+      Option = option;

+      Value = value;

+    }

+  }

+

+  public class SMTLibProverOptions : ProverOptions

+  {

+    public bool UseWeights = true;

+    public bool UseLabels { get { return UseZ3; } }

+    public List<OptionValue> SmtOptions = new List<OptionValue>();

+    public List<string> SolverArguments = new List<string>();

+

+    // Z3 specific (at the moment; some of them make sense also for other provers)

+    public bool UseZ3 = true;

+    public string Inspector = null;

+    public bool OptimizeForBv = false;

+

+    public void AddSolverArgument(string s)

+    {

+      SolverArguments.Add(s);

+    }

+

+    public void AddSmtOption(string name, string val)

+    {

+      SmtOptions.Add(new OptionValue(name, val));

+    }

+

+    public void AddWeakSmtOption(string name, string val)

+    {

+      if (!SmtOptions.Any(o => o.Option == name))

+        SmtOptions.Add(new OptionValue(name, val));

+    }

+

+    public void AddSmtOption(string opt)

+    {

+      var idx = opt.IndexOf('=');

+      if (idx <= 0 || idx == opt.Length - 1)

+        ReportError("Options to be passed to the prover should have the format: O:<name>=<value>, got '" + opt + "'");

+      AddSmtOption(opt.Substring(0, idx), opt.Substring(idx + 1));

+    }

+

+    protected override bool Parse(string opt)

+    {

+      if (opt.StartsWith("O:")) {

+        AddSmtOption(opt.Substring(2));

+        return true;

+      }

+

+      if (opt.StartsWith("C:")) {

+        AddSolverArgument(opt.Substring(2));

+        return true;

+      }

+

+      return

+        ParseBool(opt, "USE_WEIGHTS", ref UseWeights) ||

+        ParseBool(opt, "USE_Z3", ref UseZ3) ||

+        ParseString(opt, "INSPECTOR", ref Inspector) ||

+        ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||

+        base.Parse(opt);

+    }

+

+    public override void PostParse()

+    {

+      base.PostParse();

+      if (UseZ3)

+        Z3.SetupOptions(this);

+    }

+

+    public override string Help

+    {

+      get

+      {

+        return

+@"

+SMT-specific options:

+~~~~~~~~~~~~~~~~~~~~~

+USE_WEIGHTS=<bool>        Pass :weight annotations on quantified formulas (default: true)

+VERBOSITY=<int>           1 - print prover output (default: 0)

+O:<name>=<value>          Pass (set-option :<name> <value>) to the SMT solver.

+C:<string>                Pass <string> to the SMT on the command line. 

+

+Z3-specific options:

+~~~~~~~~~~~~~~~~~~~~

+INSPECTOR=<string>        Use the specified Z3Inspector binary.

+OPTIMIZE_FOR_BV=<bool>    Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.

+USE_Z3=<bool>             Use z3.exe as the prover, and use Z3 extensions (default: true)

+" + base.Help;

+      }

+    }

+  }

+}

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 3867a55b..feb8b109 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -24,14 +24,14 @@ namespace Microsoft.Boogie.SMTLib
       return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location));

     }

 

-    public static string Z3ExecutablePath()

+    public static string ExecutablePath()

     {

       if (_proverPath == null)

-        FindZ3Executable();

+        FindExecutable();

       return _proverPath;

     }

 

-    static void FindZ3Executable()

+    static void FindExecutable()

     // throws ProverException, System.IO.FileNotFoundException;

     {      

       Contract.Ensures(_proverPath != null);

@@ -99,6 +99,69 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

+    // options that work only on the command line

+    static string[] commandLineOnly = { "TRACE" };

+

+    public static void SetupOptions(SMTLibProverOptions options)

+    {

+      options.AddWeakSmtOption("MODEL_PARTIAL", "true");

+      //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");

+      options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");

+      //options.WeakAddSmtOption("MODEL_V1", "true");

+      options.AddWeakSmtOption("ASYNC_COMMANDS", "false");

+

+      if (!options.OptimizeForBv) {

+        // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.

+        // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.

+        options.AddWeakSmtOption("PHASE_SELECTION", "0");

+        options.AddWeakSmtOption("RESTART_STRATEGY", "0");

+        options.AddWeakSmtOption("RESTART_FACTOR", "|1.5|");

+

+        // Make the integer model more diverse by default, speeds up some benchmarks a lot.

+        options.AddWeakSmtOption("ARITH_RANDOM_INITIAL_VALUE", "true");

+

+        // The left-to-right structural case-splitting strategy.

+        options.AddWeakSmtOption("SORT_AND_OR", "false");

+        options.AddWeakSmtOption("CASE_SPLIT", "3");

+

+        // In addition delay adding unit conflicts.

+        options.AddWeakSmtOption("DELAY_UNITS", "true");

+        options.AddWeakSmtOption("DELAY_UNITS_THRESHOLD", "16");

+      }

+

+      // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,

+      // the foo(x0) will be activated for e-matching when x is skolemized to x0.

+      options.AddWeakSmtOption("NNF_SK_HACK", "true");

+

+      // More or less like MAM=0.

+      options.AddWeakSmtOption("QI_EAGER_THRESHOLD", "100");

+      // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.

+

+      // the following will make the :weight option more usable

+      options.AddWeakSmtOption("QI_COST", "|\"(+ weight generation)\"|");

+

+      //if (options.Inspector != null)

+      //  options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");

+

+      options.AddWeakSmtOption("TYPE_CHECK", "true");

+      options.AddWeakSmtOption("BV_REFLECT", "true");

+

+      if (CommandLineOptions.Clo.LazyInlining == 2)

+        options.AddWeakSmtOption("MACRO_EXPANSION", "true");

+

+      // legacy option handling

+      foreach (string opt in CommandLineOptions.Clo.Z3Options) {

+        Contract.Assert(opt != null);

+        int eq = opt.IndexOf("=");

+        var optName = opt.Substring(0, eq);

+        if (eq > 0 && 'A' <= opt[0] && opt[0] <= 'Z' && !commandLineOnly.Contains(optName)) {

+          options.AddSmtOption(optName, opt.Substring(eq + 1));

+        } else {

+          options.AddSolverArgument(opt);

+        }

+      }

+    }

+

 

   }

 }

diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 9fd87127..19097f8c 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -112,7 +112,6 @@ void ObjectInvariant()
       Contract.Invariant(ExeName!=null);

     }

 

-

     protected override bool Parse(string opt)

     {

       //Contract.Requires(opt!=null);