Turned on options in Z3 to try producing models for timeouts.

1 files changed, 137 insertions, 132 deletions

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index d2e06168..14b8ebb2 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -202,171 +202,176 @@ namespace Microsoft.Boogie.SMTLib
 

         public static void SetupOptions(SMTLibProverOptions options)

         {

-            FindExecutable();

-            int major, minor;

-            GetVersion(out major, out minor);

-            if (major > 4 || major == 4 && minor >= 3)

-            {

+          FindExecutable();

+          int major, minor;

+          GetVersion(out major, out minor);

+          if (major > 4 || major == 4 && minor >= 3)

+          {

 

-                // don't bother with auto-config - it would disable explicit settings for eager threshold and so on

-                options.AddWeakSmtOption("AUTO_CONFIG", "false");

+            // don't bother with auto-config - it would disable explicit settings for eager threshold and so on

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

 

-                //options.AddWeakSmtOption("MODEL_PARTIAL", "true");

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

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

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

 

-                // options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false"); TODO: what does this do?

+            // options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false"); TODO: what does this do?

 

-                options.AddWeakSmtOption("MODEL.V2", "true");

-                //options.AddWeakSmtOption("ASYNC_COMMANDS", "false"); TODO: is this needed?

+            options.AddWeakSmtOption("MODEL.V2", "true");

+            //options.AddWeakSmtOption("ASYNC_COMMANDS", "false"); TODO: is this needed?

 

-                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("smt.PHASE_SELECTION", "0");

-                    options.AddWeakSmtOption("smt.RESTART_STRATEGY", "0");

-                    options.AddWeakSmtOption("smt.RESTART_FACTOR", "|1.5|");

-

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

-                    options.AddWeakSmtOption("smt.ARITH.RANDOM_INITIAL_VALUE", "true");

-

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

-                    //options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now

-                    options.AddWeakSmtOption("smt.CASE_SPLIT", "3");

-

-                    // In addition delay adding unit conflicts.

-                    options.AddWeakSmtOption("smt.DELAY_UNITS", "true");

-                    //options.AddWeakSmtOption("DELAY_UNITS_THRESHOLD", "16"); TODO: what?

-                }

+            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("smt.PHASE_SELECTION", "0");

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

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

+

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

+              options.AddWeakSmtOption("smt.ARITH.RANDOM_INITIAL_VALUE", "true");

+

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

+              //options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now

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

+

+              // In addition delay adding unit conflicts.

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

+              //options.AddWeakSmtOption("DELAY_UNITS_THRESHOLD", "16"); TODO: what?

+            }

 

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

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

 

-                // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems

-                options.AddWeakSmtOption("smt.MBQI", "false");

+            // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems

+            options.AddWeakSmtOption("smt.MBQI", "false");

 

-                // More or less like MAM=0.

-                options.AddWeakSmtOption("smt.QI.EAGER_THRESHOLD", "100");

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

+            // More or less like MAM=0.

+            options.AddWeakSmtOption("smt.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("smt.QI.COST", "|\"(+ weight generation)\"|"); // TODO: this doesn't seem to work

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

+            options.AddWeakSmtOption("smt.QI.COST", "|\"(+ weight generation)\"|"); // TODO: this doesn't seem to work

 

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

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

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

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

 

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

-                options.AddWeakSmtOption("smt.BV.REFLECT", "true");

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

+            options.AddWeakSmtOption("smt.BV.REFLECT", "true");

 

-                if (options.TimeLimit > 0)

-                {

-                    options.AddWeakSmtOption("TIMEOUT", options.TimeLimit.ToString());

-                    // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.

-                    // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);

-                }

+            if (options.TimeLimit > 0)

+            {

+              options.AddWeakSmtOption("TIMEOUT", options.TimeLimit.ToString());

+              // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.

+              // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);

+            }

 

-                if (options.Inspector != null)

-                    options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");

+            if (options.Inspector != null)

+              options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");

 

-                if (CommandLineOptions.Clo.WeakArrayTheory)

-                {

-                    options.AddWeakSmtOption("smt.array.weak", "true");

-                    options.AddWeakSmtOption("smt.array.extensional", "false");

-                } 

+            if (CommandLineOptions.Clo.WeakArrayTheory)

+            {

+              options.AddWeakSmtOption("smt.array.weak", "true");

+              options.AddWeakSmtOption("smt.array.extensional", "false");

+            }

+          }

+          else

+          {

+            // don't bother with auto-config - it would disable explicit settings for eager threshold and so on

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

+

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

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

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

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

+

+            if (CommandLineOptions.Clo.UseSmtOutputFormat)

+            {

+              options.AddWeakSmtOption("pp-bv-literals", "false"); ;

             }

             else

             {

-                // don't bother with auto-config - it would disable explicit settings for eager threshold and so on

-                options.AddWeakSmtOption("AUTO_CONFIG", "false");

-

-                //options.AddWeakSmtOption("MODEL_PARTIAL", "true");

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

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

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

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

+            }

 

-				if (CommandLineOptions.Clo.UseSmtOutputFormat) {

-					options.AddWeakSmtOption("pp-bv-literals", "false");;

-				} else {

-					options.AddWeakSmtOption("MODEL_V2", "true");

-				}

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

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

+

+              // In addition delay adding unit conflicts.

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

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

+            }

 

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

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

 

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

+            // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems

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

 

-                // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems

-                options.AddWeakSmtOption("MBQI", "false");

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

 

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

 

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

 

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

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

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

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

 

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

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

+            if (options.TimeLimit > 0)

+            {

+              options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());

+              // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.

+              // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);

+            }

 

-                if (options.TimeLimit > 0)

-                {

-                    options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());

-                    // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.

-                    // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);

-                }

+            if (options.Inspector != null)

+              options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");

 

-                if (options.Inspector != null)

-                    options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");

-                

-                if (CommandLineOptions.Clo.WeakArrayTheory)

-                {

-                    options.AddWeakSmtOption("ARRAY_WEAK", "true");

-                    options.AddWeakSmtOption("ARRAY_EXTENSIONAL", "false");

-                }

-                

+            if (CommandLineOptions.Clo.WeakArrayTheory)

+            {

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

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

             }

+          }

+

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

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

 

-            // legacy option handling

-            if (!CommandLineOptions.Clo.z3AtFlag)

-                options.MultiTraces = true;

+          // legacy option handling

+          if (!CommandLineOptions.Clo.z3AtFlag)

+            options.MultiTraces = true;

 

 

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

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

+          {

+            Contract.Assert(opt != null);

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

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

             {

-                Contract.Assert(opt != null);

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

-                if (eq > 0 && 'A' <= opt[0] && opt[0] <= 'Z' && !commandLineOnly.Contains(opt.Substring(0, eq)))

-                {

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

-                }

-                else

-                {

-                    options.AddSolverArgument(opt);

-                }

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

+            }

+            else

+            {

+              options.AddSolverArgument(opt);

             }

+          }

         }