Boogie: added /z3bv option that overrides the current setting of Z3 options for better performance on VCs that are heavy on bitvector arithmetic

6 files changed, 58 insertions, 22 deletions

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 828540ca..c0ba6eaa 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -206,6 +206,7 @@ namespace Microsoft.Boogie
     public int Z3mam = 0;

     [Peer] public List<string!>! Z3Options = new List<string!>();

     public bool Z3types = false;

+    public bool Z3OptimizeForBitvectors = false;

     public int Z3lets = 3;  // 0 - none, 1 - only LET TERM, 2 - only LET FORMULA, 3 - (default) any

     invariant 0 <= Z3lets && Z3lets < 4;

 

@@ -1236,6 +1237,7 @@ namespace Microsoft.Boogie
               ps.CheckBooleanFlag("causalImplies", ref CausalImplies) ||

               ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) ||

               ps.CheckBooleanFlag("z3types", ref Z3types) ||

+              ps.CheckBooleanFlag("z3bv", ref Z3OptimizeForBitvectors) ||

               ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||

               ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||

               ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||

@@ -2102,6 +2104,7 @@ namespace Microsoft.Boogie
   /z3types       : generate multi-sorted VC that make use of Z3 types

   /z3lets:<n>    : 0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA,

                    3 - (default) any

+  /z3bv          : use Z3 settings optimized for bitvector reasoning

 ");

     }

   }

diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index 923a62ef..abe644ec 100644
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ b/Source/Provers/Simplify/ProverInterface.cs
@@ -519,7 +519,7 @@ namespace Microsoft.Boogie.Simplify {
     [NoDefaultContract]

     private void FireUpNewProver()

     {

-            Contract.Requires( cce.IsExposed(this));

+      Contract.Requires( cce.IsExposed(this));

       Contract.Requires( thmProver == null);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

 

diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 3fcafba8..36c5c82d 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -113,33 +113,36 @@ namespace Microsoft.Boogie.Z3
       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|");

+      if (!CommandLineOptions.Clo.Z3OptimizeForBitvectors) {

 

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

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

 

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

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

 

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

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

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

 

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

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

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

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

 

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

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

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

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

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

 

-      // In addition delay adding unit conflicts.

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

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

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

diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer
index 1bcc3a2b..aa060ee4 100644
--- a/Test/bitvectors/Answer
+++ b/Test/bitvectors/Answer
@@ -49,3 +49,7 @@ Boogie program verifier finished with 0 verified, 1 error
 -------------------- bv8.bpl --------------------

 

 Boogie program verifier finished with 2 verified, 0 errors

+-------------------- bv9.bpl /bv:z /z3bv --------------------

+Boogie program verifier version 2, Copyright (c) 2003-2010, Microsoft.

+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/bitvectors/bv9.bpl b/Test/bitvectors/bv9.bpl
new file mode 100644
index 00000000..9637c87f
--- /dev/null
+++ b/Test/bitvectors/bv9.bpl
@@ -0,0 +1,23 @@
+procedure foo();

+

+implementation foo()

+{

+    assert (forall Q#a$1^15.32#tc1: bv64, Q#b$1^15.32#tc1: bv64, Q#c$1^15.32#tc1: bv64 :: true && true && true ==> ($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) == Q#c$1^15.32#tc1 || $bv_bvadd64($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), 1bv64) == Q#c$1^15.32#tc1) && (if Q#c$1^15.32#tc1 == $bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) then $bv_bvugt64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1)) else $bv_bvuge64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1))) ==> $bv_bvlshr64($bv_bvxor64($bv_bvor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), $bv_bvand64($bv_bvxor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), Q#c$1^15.32#tc1)), 0bv32 ++ 63bv32) == 1bv64);

+}

+

+function {:bvbuiltin "bvlshr"} $bv_bvlshr64(p1: bv64, p2: bv64) : bv64;

+

+function {:bvbuiltin "bvand"} $bv_bvand64(p1: bv64, p2: bv64) : bv64;

+

+function {:bvbuiltin "bvor"} $bv_bvor64(p1: bv64, p2: bv64) : bv64;

+

+function {:bvbuiltin "bvxor"} $bv_bvxor64(p1: bv64, p2: bv64) : bv64;

+

+function {:bvbuiltin "bvuge"} $bv_bvuge64(p1: bv64, p2: bv64) : bool;

+

+function {:bvbuiltin "bvugt"} $bv_bvugt64(p1: bv64, p2: bv64) : bool;

+

+function {:bvbuiltin "bvsub"} $bv_bvsub64(p1: bv64, p2: bv64) : bv64;

+

+function {:bvbuiltin "bvadd"} $bv_bvadd64(p1: bv64, p2: bv64) : bv64;

+

diff --git a/Test/bitvectors/runtest.bat b/Test/bitvectors/runtest.bat
index cbafa065..2ec881fd 100644
--- a/Test/bitvectors/runtest.bat
+++ b/Test/bitvectors/runtest.bat
@@ -15,3 +15,6 @@ for %%f in (bv5.bpl bv6.bpl bv8.bpl) do (
   echo -------------------- %%f --------------------

   %BGEXE% %* %%f

 )

+

+echo -------------------- bv9.bpl /bv:z /z3bv --------------------

+%BGEXE% /bv:z /z3bv bv9.bpl
\ No newline at end of file