Remove -z3DebugTraces and -z3Mam options (no longer working). Rename the -z3bv option to Z3-specific -proverOpt:OPTIMIZE_FOR_BV=true. Start with the prover-specific help (still needs changes in the yet-unconverted part).

3 files changed, 57 insertions, 34 deletions

diff --git a/Source/Provers/Z3/Inspector.cs b/Source/Provers/Z3/Inspector.cs
index 425de1ff..3675f6a7 100644
--- a/Source/Provers/Z3/Inspector.cs
+++ b/Source/Provers/Z3/Inspector.cs
@@ -53,12 +53,12 @@ void ObjectInvariant()
     [Rep] readonly TextReader fromInspector;

     [Rep] readonly TextWriter toInspector;

     [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(inspector!=null);

+    void ObjectInvariant() 

+    {

+      Contract.Invariant(inspector!=null);

       Contract.Invariant(fromInspector!=null);

       Contract.Invariant(toInspector != null);

-}

+    }

 

 

     public Inspector(Z3InstanceOptions opts)

diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 36c5c82d..2bb02e64 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -113,25 +113,13 @@ namespace Microsoft.Boogie.Z3
       AddOption(result, "MODEL_V1", "true");

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

 

-      if (!CommandLineOptions.Clo.Z3OptimizeForBitvectors) {

-

+      if (!opts.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.

         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");

 

@@ -144,6 +132,17 @@ namespace Microsoft.Boogie.Z3
         AddOption(result, "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.

+      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)\"|");

+

       if (opts.Inspector != null)

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

 

diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 172fbf60..bcf55c4c 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -104,11 +104,13 @@ void ObjectInvariant()
     public string ExeName = "z3.exe";

     public bool InverseImplies = false;

     public string Inspector = null;

+    public bool OptimizeForBv = false;

+

     [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(ExeName!=null);

-}

+    void ObjectInvariant() 

+    {

+      Contract.Invariant(ExeName!=null);

+    }

 

 

     protected override bool Parse(string opt)

@@ -117,6 +119,7 @@ void ObjectInvariant()
       return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||

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

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

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

              base.Parse(opt);

     }

 

@@ -129,16 +132,37 @@ void ObjectInvariant()
         CommandLineOptions.Clo.RestartProverPerVC = true;

       }     

     }

+

+    public string Help

+    {

+      get

+      {

+          return

+              // base.Help +

+@"

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

+

+Obscure options:

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

+DIST=<bool>               Use z3-dist.exe binary.

+REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.

+";

+          // DIST requires non-public binaries

+      }

+    }

   }

 

   internal class Z3LineariserOptions : LineariserOptions {

     private readonly Z3InstanceOptions opts;

 

     [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(opts!=null);

-}

+    void ObjectInvariant() 

+    {

+        Contract.Invariant(opts!=null);

+    }

 

 

     public override CommandLineOptions.BvHandling Bitvectors { get {

@@ -250,15 +274,15 @@ void ObjectInvariant()
       return new Z3VCExprTranslator(this);

     }

 

-[ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(Opts!=null);

-    Contract.Invariant(Gen != null);

-  Contract.Invariant(AxBuilder != null);

-  Contract.Invariant(Namer != null);

-  Contract.Invariant(DeclCollector != null);

-}

+    [ContractInvariantMethod]

+    void ObjectInvariant() 

+    {

+      Contract.Invariant(Opts!=null);

+      Contract.Invariant(Gen != null);

+      Contract.Invariant(AxBuilder != null);

+      Contract.Invariant(Namer != null);

+      Contract.Invariant(DeclCollector != null);

+    }

 

     private readonly Z3InstanceOptions Opts;

     private readonly VCExpressionGenerator Gen;