diff options
Diffstat (limited to 'Source/Provers/SMTLib/Z3.cs')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 479 |
1 files changed, 310 insertions, 169 deletions
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index addfa3de..8081603e 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -14,195 +14,336 @@ using System.Text.RegularExpressions; namespace Microsoft.Boogie.SMTLib
{
- class Z3
- {
- static string _proverPath;
-
- static string CodebaseString()
+ class Z3
{
- Contract.Ensures(Contract.Result<string>() != null);
- return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location));
- }
+ static string _proverPath;
- public static string ExecutablePath()
- {
- if (_proverPath == null)
- FindExecutable();
- return _proverPath;
- }
+ static string CodebaseString()
+ {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location));
+ }
- static void FindExecutable()
- // throws ProverException, System.IO.FileNotFoundException;
- {
- Contract.Ensures(_proverPath != null);
+ public static string ExecutablePath()
+ {
+ if (_proverPath == null)
+ FindExecutable();
+ return _proverPath;
+ }
- // Command line option 'z3exe' always has priority if set
- if (CommandLineOptions.Clo.Z3ExecutablePath != null) {
- _proverPath = CommandLineOptions.Clo.Z3ExecutablePath;
- if (!File.Exists(_proverPath)) {
- throw new ProverException("Cannot find prover specified with z3exe: " + _proverPath);
+ static void FindExecutable()
+ // throws ProverException, System.IO.FileNotFoundException;
+ {
+ Contract.Ensures(_proverPath != null);
+
+ // Command line option 'z3exe' always has priority if set
+ if (CommandLineOptions.Clo.Z3ExecutablePath != null)
+ {
+ _proverPath = CommandLineOptions.Clo.Z3ExecutablePath;
+ if (!File.Exists(_proverPath))
+ {
+ throw new ProverException("Cannot find prover specified with z3exe: " + _proverPath);
+ }
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("[TRACE] Using prover: " + _proverPath);
+ }
+ return;
+ }
+
+ var proverExe = "z3.exe";
+
+ if (_proverPath == null)
+ {
+ // Initialize '_proverPath'
+ _proverPath = Path.Combine(CodebaseString(), proverExe);
+ string firstTry = _proverPath;
+
+ if (File.Exists(firstTry))
+ {
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("[TRACE] Using prover: " + _proverPath);
+ }
+ return;
+ }
+
+ List<string> z3Dirs = new List<string>();
+
+ string programFiles = Environment.GetEnvironmentVariable("ProgramFiles");
+ if (programFiles != null)
+ {
+ string programFilesX86 = Environment.GetEnvironmentVariable("ProgramFiles(x86)");
+ if (programFiles.Equals(programFilesX86))
+ {
+ // If both %ProgramFiles% and %ProgramFiles(x86)% point to "ProgramFiles (x86)", use %ProgramW6432% instead.
+ programFiles = Environment.GetEnvironmentVariable("ProgramW6432");
+ }
+
+
+ if (Directory.Exists(programFiles + @"\Microsoft Research\"))
+ {
+ string msrDir = programFiles + @"\Microsoft Research\";
+ z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*"));
+ }
+ if (Directory.Exists(programFilesX86 + @"\Microsoft Research\"))
+ {
+ string msrDir = programFilesX86 + @"\Microsoft Research\";
+ z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*"));
+ }
+ }
+
+ int minMajor = 3, minMinor = 2;
+
+ // Look for the most recent version of Z3.
+ int minor = 0, major = 0;
+ string winner = null;
+ Regex r = new Regex(@"^Z3-(\d+)\.(\d+)$");
+ foreach (string d in z3Dirs)
+ {
+ string name = new DirectoryInfo(d).Name;
+ foreach (Match m in r.Matches(name))
+ {
+ int ma, mi;
+ ma = int.Parse(m.Groups[1].ToString());
+ mi = int.Parse(m.Groups[2].ToString());
+ if (major < ma || (major == ma && minor < mi))
+ {
+ major = ma;
+ minor = mi;
+ winner = d;
+ }
+ }
+ }
+
+ if (major == 0 && minor == 0)
+ {
+ throw new ProverException("Cannot find executable: " + firstTry);
+ }
+
+ Contract.Assert(winner != null);
+
+ _proverPath = Path.Combine(Path.Combine(winner, "bin"), proverExe);
+ if (!File.Exists(_proverPath))
+ {
+ throw new ProverException("Cannot find prover: " + _proverPath);
+ }
+
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("[TRACE] Using prover: " + _proverPath);
+ }
+
+ if (major < minMajor || (major == minMajor && minor < minMinor))
+ {
+ throw new ProverException(string.Format("Found version {0}.{1} of Z3. Please install version {2}.{3} or later. " +
+ "(More conservative users might opt to supply -prover:Z3 option instead to get the historic Simplify back-end)",
+ major, minor, minMajor, minMinor));
+ }
+ }
}
- if (CommandLineOptions.Clo.Trace) {
- Console.WriteLine("[TRACE] Using prover: " + _proverPath);
+
+
+ static int Z3MajorVersion = 0;
+ static int Z3MinorVersion = 0;
+ static bool Z3VersionObtained = false;
+
+ public static void GetVersion(out int major, out int minor)
+ {
+ if (!Z3VersionObtained)
+ {
+ var proc = new System.Diagnostics.Process();
+ proc.StartInfo.FileName = _proverPath;
+ proc.StartInfo.Arguments = "--version";
+ proc.StartInfo.RedirectStandardOutput = true;
+ proc.StartInfo.RedirectStandardError = true;
+ proc.StartInfo.UseShellExecute = false;
+ proc.StartInfo.CreateNoWindow = true;
+ proc.Start();
+ proc.WaitForExit();
+ if (proc.ExitCode == 0)
+ {
+ string answer = proc.StandardOutput.ReadToEnd();
+ var firstdot = answer.IndexOf('.');
+ if (firstdot >= 0)
+ {
+ var seconddot = answer.IndexOf('.', firstdot + 1);
+ if (seconddot >= firstdot + 1)
+ {
+ var spacebeforefirstdot = answer.LastIndexOf(' ', firstdot);
+ if (spacebeforefirstdot >= 0)
+ {
+ var majorstr = answer.Substring(spacebeforefirstdot, firstdot - spacebeforefirstdot);
+ var minorstr = answer.Substring(firstdot + 1, seconddot - firstdot - 1);
+ Z3MajorVersion = Convert.ToInt32(majorstr);
+ Z3MinorVersion = Convert.ToInt32(minorstr);
+ }
+ }
+ }
+ }
+ Z3VersionObtained = true;
+ }
+ major = Z3MajorVersion;
+ minor = Z3MinorVersion;
}
- return;
- }
- var proverExe = "z3.exe";
+ // options that work only on the command line
+ static string[] commandLineOnly = { "TRACE", "PROOF_MODE" };
- if (_proverPath == null) {
- // Initialize '_proverPath'
- _proverPath = Path.Combine(CodebaseString(), proverExe);
- string firstTry = _proverPath;
+ public static void SetupOptions(SMTLibProverOptions options)
+ {
+ FindExecutable();
+ int major, minor;
+ GetVersion(out major, out minor);
+ if (major > 4 || major == 4 && minor >= 3)
+ {
- if (File.Exists(firstTry)) {
- if (CommandLineOptions.Clo.Trace) {
- Console.WriteLine("[TRACE] Using prover: " + _proverPath);
- }
- return;
- }
+ // don't bother with auto-config - it would disable explicit settings for eager threshold and so on
+ options.AddWeakSmtOption("AUTO_CONFIG", "false");
- List<string> z3Dirs = new List<string>();
-
- string programFiles = Environment.GetEnvironmentVariable("ProgramFiles");
- if (programFiles != null) {
- string programFilesX86 = Environment.GetEnvironmentVariable("ProgramFiles(x86)");
- if (programFiles.Equals(programFilesX86)) {
- // If both %ProgramFiles% and %ProgramFiles(x86)% point to "ProgramFiles (x86)", use %ProgramW6432% instead.
- programFiles = Environment.GetEnvironmentVariable("ProgramW6432");
- }
-
-
- if (Directory.Exists(programFiles + @"\Microsoft Research\")) {
- string msrDir = programFiles + @"\Microsoft Research\";
- z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*"));
- }
- if (Directory.Exists(programFilesX86 + @"\Microsoft Research\")) {
- string msrDir = programFilesX86 + @"\Microsoft Research\";
- z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*"));
- }
- }
+ //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.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?
+ }
+
+ // 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");
+
+ // 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
+
+ //if (options.Inspector != null)
+ // options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");
+
+ options.AddWeakSmtOption("TYPE_CHECK", "true");
+ options.AddWeakSmtOption("smt.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.Inspector != null)
+ options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");
- int minMajor = 3, minMinor = 2;
-
- // Look for the most recent version of Z3.
- int minor = 0, major = 0;
- string winner = null;
- Regex r = new Regex(@"^Z3-(\d+)\.(\d+)$");
- foreach (string d in z3Dirs) {
- string name = new DirectoryInfo(d).Name;
- foreach (Match m in r.Matches(name)) {
- int ma, mi;
- ma = int.Parse(m.Groups[1].ToString());
- mi = int.Parse(m.Groups[2].ToString());
- if (major < ma || (major == ma && minor < mi)) {
- major = ma;
- minor = mi;
- winner = d;
}
- }
- }
+ else
+ {
+ // don't bother with auto-config - it would disable explicit settings for eager threshold and so on
+ options.AddWeakSmtOption("AUTO_CONFIG", "false");
- if (major == 0 && minor == 0) {
- throw new ProverException("Cannot find executable: " + firstTry);
- }
+ //options.AddWeakSmtOption("MODEL_PARTIAL", "true");
+ //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
+ options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");
+ options.AddWeakSmtOption("MODEL_V2", "true");
+ options.AddWeakSmtOption("ASYNC_COMMANDS", "false");
- Contract.Assert(winner != null);
+ 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|");
- _proverPath = Path.Combine(Path.Combine(winner, "bin"), proverExe);
- if (!File.Exists(_proverPath)) {
- throw new ProverException("Cannot find prover: " + _proverPath);
- }
+ // Make the integer model more diverse by default, speeds up some benchmarks a lot.
+ options.AddWeakSmtOption("ARITH_RANDOM_INITIAL_VALUE", "true");
- if (CommandLineOptions.Clo.Trace) {
- Console.WriteLine("[TRACE] Using prover: " + _proverPath);
- }
+ // The left-to-right structural case-splitting strategy.
+ //options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now
+ options.AddWeakSmtOption("CASE_SPLIT", "3");
- if (major < minMajor || (major == minMajor && minor < minMinor)) {
- throw new ProverException(string.Format("Found version {0}.{1} of Z3. Please install version {2}.{3} or later. " +
- "(More conservative users might opt to supply -prover:Z3 option instead to get the historic Simplify back-end)",
- major, minor, minMajor, minMinor));
- }
- }
- }
+ // In addition delay adding unit conflicts.
+ options.AddWeakSmtOption("DELAY_UNITS", "true");
+ options.AddWeakSmtOption("DELAY_UNITS_THRESHOLD", "16");
+ }
- // options that work only on the command line
- static string[] commandLineOnly = { "TRACE", "PROOF_MODE" };
+ // 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");
- public static void SetupOptions(SMTLibProverOptions options)
- {
- // 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("MODEL_V2", "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"); // 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");
-
- // 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.
-
- // 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 (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");
-
- // legacy option handling
- if (!CommandLineOptions.Clo.z3AtFlag)
- options.MultiTraces = true;
-
- 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))) {
- options.AddSmtOption(opt.Substring(0, eq), opt.Substring(eq + 1));
- } else {
- options.AddSolverArgument(opt);
+ // 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.
+
+ // 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 (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");
+
+
+ }
+
+ // legacy option handling
+ if (!CommandLineOptions.Clo.z3AtFlag)
+ options.MultiTraces = true;
+
+
+ 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)))
+ {
+ options.AddSmtOption(opt.Substring(0, eq), opt.Substring(eq + 1));
+ }
+ else
+ {
+ options.AddSolverArgument(opt);
+ }
+ }
}
- }
- }
- }
+ }
}
|