Remove support for Z3 V1 and clean up parameter processing code for Z3

svn-ignoring some build artifacts

4 files changed, 84 insertions, 113 deletions

diff --git a/Binaries/Makefile b/Binaries/Makefile
index 3a2a7e20..6a792393 100644
--- a/Binaries/Makefile
+++ b/Binaries/Makefile
@@ -6,8 +6,8 @@ SPECSHARPROOT = d:\SpecSharpCodePlex\SpecSharp
 # Use the first one if you want to build Boogie using the LKG build of Spec#.

 # Use the second one if you want to build Boogie using a freshly built version of Spec#.

 #

-#SPECSHARPBINDIR = Microsoft.SpecSharp\LastKnownGood9

-SPECSHARPBINDIR = Microsoft.SpecSharp\Registration

+SPECSHARPBINDIR = Microsoft.SpecSharp\LastKnownGood9

+#SPECSHARPBINDIR = Microsoft.SpecSharp\Registration

 

 all: 

 	copy /y "$(SPECSHARPROOT)\$(SPECSHARPBINDIR)\ITaskManager.dll"

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 9fb05d24..828540ca 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -2053,7 +2053,6 @@ namespace Microsoft.Boogie
                    ContractInference (uses Z3)

                    Z3api (Z3 using Managed .NET API)

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

-                   V1 - enables Z3 version 1.3 (with /prover:z3).

   /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/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index c431b5af..3fcafba8 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -26,11 +26,8 @@ namespace Microsoft.Boogie.Z3
     private readonly Inspector/*?*/ inspector;

     private readonly bool expectingModel = false;

 

-    private string cmdLineArgs = "";

-

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(cmdLineArgs != null);

       Contract.Invariant(opts != null);

       Contract.Invariant(cce.NonNullElements(parameterSettings));

     }

@@ -69,96 +66,93 @@ namespace Microsoft.Boogie.Z3
       cmdLineBldr.Append(' ').Append(OptionChar()).Append(name);

     }

 

-    static List<OptionValue/*!*/>/*!*/ CreateParameterListForOptions(Z3InstanceOptions opts, Inspector inspector, out string cmdLineArgs, out bool expectingModel)

+    static bool ExpectingModel()

+    {

+      return CommandLineOptions.Clo.PrintErrorModel >= 1 ||

+             CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||

+             CommandLineOptions.Clo.ContractInfer ||

+             CommandLineOptions.Clo.LazyInlining > 0 ||

+             CommandLineOptions.Clo.StratifiedInlining > 0;

+    }

+

+    static string/*!*/ CreateCommandLineArgsForOptions(Z3InstanceOptions opts)

     {

-      List<OptionValue/*!*/>/*!*/ result = new List<OptionValue/*!*/>();

       StringBuilder cmdLineArgsBldr = new StringBuilder();

       AppendCmdLineOption(cmdLineArgsBldr, "si");

-      expectingModel = false;

 

-      if (opts.V1) {

-        AddOption(result, "PARTIAL_MODELS", "true");

-        AddOption(result, "MODEL_VALUE_COMPLETION", "false");

-        AddOption(result, "HIDE_UNUSED_PARTITIONS", "false");

-        AppendCmdLineOption(cmdLineArgsBldr, "mam", CommandLineOptions.Clo.Z3mam);

-      } else {

-        AddOption(result, "MODEL_PARTIAL", "true");

-        AddOption(result, "MODEL_VALUE_COMPLETION", "false");

-        AddOption(result, "MODEL_HIDE_UNUSED_PARTITIONS", "false");

-        AddOption(result, "MODEL_V1", "true");

-        AddOption(result, "ASYNC_COMMANDS", "false");

-

-        // 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.

-        AddOption(result, "PHASE_SELECTION", "0");

-        AddOption(result, "RESTART_STRATEGY", "0");

-        AddOption(result, "RESTART_FACTOR", "|1.5|");

-

-        // 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.

-        AddOption(result, "NNF_SK_HACK", "true");

-

-        // More or less like MAM=0.

-        AddOption(result, "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

-        AddOption(result, "QI_COST", "|\"(+ weight generation)\"|");

-

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

-        AddOption(result, "ARITH_RANDOM_INITIAL_VALUE", "true");

-

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

-        AddOption(result, "SORT_AND_OR", "false");

-        AddOption(result, "CASE_SPLIT", "3");

-

-        // In addition delay adding unit conflicts.

-        AddOption(result, "DELAY_UNITS", "true");

-        AddOption(result, "DELAY_UNITS_THRESHOLD", "16");

-

-        if (opts.Inspector != null) {

-          AddOption(result, "PROGRESS_SAMPLING_FREQ", "100");

-        }

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

+        AppendCmdLineOption(cmdLineArgsBldr, "nw");

+

+      if (CommandLineOptions.Clo.z3AtFlag)

+        AppendCmdLineOption(cmdLineArgsBldr, "@");

+

+      if (0 <= CommandLineOptions.Clo.ProverCCLimit)

+        AppendCmdLineOption(cmdLineArgsBldr, "cex", CommandLineOptions.Clo.ProverCCLimit);

+

+      if (0 <= opts.Timeout)

+        AppendCmdLineOption(cmdLineArgsBldr, "t", opts.Timeout);

+

+      if (ExpectingModel())

+        AppendCmdLineOption(cmdLineArgsBldr, "m");

+

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

+        Contract.Assert(opt != null);

+        cmdLineArgsBldr.Append(" \"").Append(opt).Append('\"');

       }

 

+      return cmdLineArgsBldr.ToString();

+    }

+

+    static List<OptionValue/*!*/>/*!*/ CreateParameterListForOptions(Z3InstanceOptions opts, Inspector inspector)

+    {

+      List<OptionValue/*!*/>/*!*/ result = new List<OptionValue/*!*/>();

+

+      AddOption(result, "MODEL_PARTIAL", "true");

+      AddOption(result, "MODEL_VALUE_COMPLETION", "false");

+      AddOption(result, "MODEL_HIDE_UNUSED_PARTITIONS", "false");

+      AddOption(result, "MODEL_V1", "true");

+      AddOption(result, "ASYNC_COMMANDS", "false");

+

+      // 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.

+      AddOption(result, "PHASE_SELECTION", "0");

+      AddOption(result, "RESTART_STRATEGY", "0");

+      AddOption(result, "RESTART_FACTOR", "|1.5|");

+

+      // 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.

+      AddOption(result, "NNF_SK_HACK", "true");

+

+      // More or less like MAM=0.

+      AddOption(result, "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

+      AddOption(result, "QI_COST", "|\"(+ weight generation)\"|");

+

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

+      AddOption(result, "ARITH_RANDOM_INITIAL_VALUE", "true");

+

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

+      AddOption(result, "SORT_AND_OR", "false");

+      AddOption(result, "CASE_SPLIT", "3");

+

+      // In addition delay adding unit conflicts.

+      AddOption(result, "DELAY_UNITS", "true");

+      AddOption(result, "DELAY_UNITS_THRESHOLD", "16");

+

+      if (opts.Inspector != null)

+        AddOption(result, "PROGRESS_SAMPLING_FREQ", "100");

+

       if (opts.Typed) {

         AddOption(result, "TYPE_CHECK", "true");

         if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native)

-          if (opts.V2)

             AddOption(result, "BV_REFLECT", "true");

-          else

-            AddOption(result, "REFLECT_BV_OPS", "true");

       }

 

-      if (CommandLineOptions.Clo.LazyInlining == 2) {

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

         AddOption(result, "MACRO_EXPANSION", "true");

-        AppendCmdLineOption(cmdLineArgsBldr, "nw");

-      }

-

-      if (CommandLineOptions.Clo.z3AtFlag) 

-        AppendCmdLineOption(cmdLineArgsBldr, "@ "); 

       

-      if (0 <= CommandLineOptions.Clo.ProverCCLimit)

-         AppendCmdLineOption(cmdLineArgsBldr, "cex", CommandLineOptions.Clo.ProverCCLimit);

-      

-      if (0 <= opts.Timeout) {

-        AppendCmdLineOption(cmdLineArgsBldr, "t", opts.Timeout);

-      }

-      if (CommandLineOptions.Clo.PrintErrorModel >= 1 ||

-          CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||

-          CommandLineOptions.Clo.ContractInfer ||

-          CommandLineOptions.Clo.LazyInlining > 0 ||

-          CommandLineOptions.Clo.StratifiedInlining > 0) {

-        AppendCmdLineOption(cmdLineArgsBldr, "m");

-        expectingModel = true;

-      }

-      

-      // Z3 version 1.3 does not support SETPARAMETER in the input, so we tack on the OPTION=value pairs to z3args

-      if (opts.V1) {

-        foreach (OptionValue opt in result) 

-          cmdLineArgsBldr.Append(" \"").Append(opt.Option).Append('=').Append(opt.Value).Append('\"');

-      }

-

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

         Contract.Assert(opt != null);

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

@@ -169,10 +163,8 @@ namespace Microsoft.Boogie.Z3
         if (eq > 0 && opt.IndexOf(" ") < 0 && 'A' <= opt[0] && opt[0] <= 'Z') {

           AddOption(result, opt.Substring(0, eq), opt.Substring(eq + 1));

         }

-        cmdLineArgsBldr.Append(" \"").Append(opt).Append('\"');

       }

 

-      cmdLineArgs = cmdLineArgsBldr.ToString();

       return result;

     }

 

@@ -182,18 +174,16 @@ namespace Microsoft.Boogie.Z3
       : base(ComputeProcessStartInfo(opts), opts.ExeName) { // throws ProverException

       Contract.Requires(opts != null);

       Contract.Requires(inspector == null || cce.Owner.Same(opts, inspector));

-      this.parameterSettings = CreateParameterListForOptions(opts, inspector, out this.cmdLineArgs, out expectingModel);

+      this.parameterSettings = CreateParameterListForOptions(opts, inspector);

       cce.Owner.AssignSame(this, opts);

       this.opts = opts;

       this.inspector = inspector;

+      this.expectingModel = ExpectingModel();

     }

 

     private static ProcessStartInfo ComputeProcessStartInfo(Z3InstanceOptions opts)

     {

-      string cmdLineArgs;

-      bool dummy;

-      CreateParameterListForOptions(opts, null, out cmdLineArgs, out dummy);

-      return new ProcessStartInfo(opts.ExeName, cmdLineArgs)

+      return new ProcessStartInfo(opts.ExeName, CreateCommandLineArgsForOptions(opts))

                {

                  CreateNoWindow = true,

                  UseShellExecute = false,

@@ -208,7 +198,7 @@ namespace Microsoft.Boogie.Z3
 

       StringBuilder sb = new StringBuilder();

       sb.AppendFormat("Z3 command line: {0} {1}\nUser supplied Z3 options:",

-                      opts.ExeName, cmdLineArgs);

+                      opts.ExeName, this.simplify.StartInfo.Arguments);

       Contract.Assume(cce.IsPeerConsistent(CommandLineOptions.Clo));

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

         Contract.Assert(opt != null);

@@ -222,11 +212,8 @@ namespace Microsoft.Boogie.Z3
     public override IEnumerable<string/*!>!*/> ParameterSettings {

       get {

         Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string>>()));

-

-        if (opts.V2) {

-          foreach (OptionValue opt in parameterSettings) {

-            yield return "(SETPARAMETER " + opt.Option + " " + opt.Value + ")";

-          }

+        foreach (OptionValue opt in parameterSettings) {

+          yield return "(SETPARAMETER " + opt.Option + " " + opt.Value + ")";

         }

       }

     }

diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 689f1024..f1ba1369 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -100,8 +100,6 @@ void ObjectInvariant()
         return CommandLineOptions.Clo.Z3lets;

       }

     }

-    public bool V1 = false;

-    public bool V2 = false; // default set in PostParse

     public bool DistZ3 = false;

     public string ExeName = "z3.exe";

     public bool InverseImplies = false;

@@ -116,9 +114,7 @@ void ObjectInvariant()
     protected override bool Parse(string opt)

     {

       Contract.Requires(opt!=null);

-      return ParseBool(opt, "V1", ref V1) ||

-             ParseBool(opt, "V2", ref V2) ||

-             ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||

+      return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||

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

              ParseBool(opt, "DIST", ref DistZ3) ||

              base.Parse(opt);

@@ -128,21 +124,10 @@ void ObjectInvariant()
     {

       base.PostParse();

 

-      if (!V1 && !V2) {

-        V2 = true; // default

-      } else if (V1 && V2) {

-        ReportError("V1 and V2 requested at the same time");

-      } else if (V1 && DistZ3) {

-        ReportError("V1 and DistZ3 requested at the same time");

-      }

-      if (V1) {

-        ExeName = "z3-v1.3.exe";

-      }

       if (DistZ3) {

         ExeName = "z3-dist.exe";

         CommandLineOptions.Clo.RestartProverPerVC = true;

-      }

-      

+      }     

     }

   }

 

@@ -169,7 +154,7 @@ void ObjectInvariant()
     }

 

     public override bool UseWeights { get {

-      return opts.V2;

+      return true;

     } }

 

     public override bool UseTypes { get {