From 6b85a0f0d4f88b6ad57812175354acf3a2947a0e Mon Sep 17 00:00:00 2001 From: MichalMoskal Date: Thu, 17 Feb 2011 19:00:30 +0000 Subject: Provide /p: as the short form of /proverOpt:. Add /p:O:= and /p:C: prover options in SMT. Add default Z3 options when using Z3. --- Source/Provers/SMTLib/ProverInterface.cs | 44 +++------- Source/Provers/SMTLib/SMTLib.csproj | 1 + Source/Provers/SMTLib/SMTLibProcess.cs | 27 ++++--- Source/Provers/SMTLib/SMTLibProverOptions.cs | 115 +++++++++++++++++++++++++++ Source/Provers/SMTLib/Z3.cs | 69 +++++++++++++++- 5 files changed, 212 insertions(+), 44 deletions(-) create mode 100644 Source/Provers/SMTLib/SMTLibProverOptions.cs (limited to 'Source/Provers/SMTLib') diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index bfcbf682..f299af30 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -22,36 +22,6 @@ using System.Text; namespace Microsoft.Boogie.SMTLib { - public class SMTLibProverOptions : ProverOptions - { - public bool UseWeights = true; - public bool UseLabels { get { return UseZ3; } } - public bool UseZ3 = true; - - protected override bool Parse(string opt) - { - return - ParseBool(opt, "USE_WEIGHTS", ref UseWeights) || - ParseBool(opt, "USE_Z3", ref UseZ3) || - base.Parse(opt); - } - - public override string Help - { - get - { - return -@" -SMT-specific options: -~~~~~~~~~~~~~~~~~~~~~ -USE_Z3= Use z3.exe as the prover, and use Z3 extensions (default: true) -USE_WEIGHTS= Pass :weight annotations on quantified formulas (default: true) -VERBOSITY= 1 - print prover output (default: 0) -" + base.Help; - } - } - } - public class SMTLibProcessTheoremProver : ProverInterface { private readonly DeclFreeProverContext ctx; @@ -105,7 +75,7 @@ VERBOSITY= 1 - print prover output (default: 0) this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer); if (this.options.UseZ3) { - var psi = SMTLibProcess.ComputerProcessStartInfo(Z3.Z3ExecutablePath(), "AUTO_CONFIG=false -smt2 -in"); + var psi = SMTLibProcess.ComputerProcessStartInfo(Z3.ExecutablePath(), "AUTO_CONFIG=false -smt2 -in"); Process = new SMTLibProcess(psi, this.options); Process.ErrorHandler += this.HandleProverError; } @@ -171,8 +141,15 @@ VERBOSITY= 1 - print prover output (default: 0) private void PrepareCommon() { - if (common.Length == 0) + if (common.Length == 0) { + SendCommon("(set-option :print-success false)"); + SendCommon("(set-info :smt-lib-version 2.0)"); + foreach (var opt in options.SmtOptions) { + SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")"); + } + SendCommon("; done setting options\n"); SendCommon(_backgroundPredicates); + } if (!AxiomsAreSetup) { var axioms = ctx.Axioms; @@ -275,6 +252,9 @@ VERBOSITY= 1 - print prover output (default: 0) return result; var errorsLeft = CommandLineOptions.Clo.ProverCCLimit; + if (errorsLeft < 1) + errorsLeft = 1; + var globalResult = Outcome.Undetermined; while (errorsLeft-- > 0) { diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj index 536fd43e..4eb753a2 100644 --- a/Source/Provers/SMTLib/SMTLib.csproj +++ b/Source/Provers/SMTLib/SMTLib.csproj @@ -107,6 +107,7 @@ + diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 8cc67256..b23fddbb 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -71,7 +71,7 @@ namespace Microsoft.Boogie.SMTLib public bool IsPong(SExpr sx) { - return sx.Name == ":name"; + return sx != null && sx.Name == ":name"; } public void PingPong() @@ -79,6 +79,11 @@ namespace Microsoft.Boogie.SMTLib Ping(); while (true) { var sx = GetProverResponse(); + if (sx == null) { + ErrorHandler("Prover died"); + return; + } + if (IsPong(sx)) return; else @@ -261,21 +266,25 @@ namespace Microsoft.Boogie.SMTLib void prover_OutputDataReceived(object sender, DataReceivedEventArgs e) { lock (this) { - if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name"))) { - Console.WriteLine("[SMT-OUT] {0}", e.Data); + if (e.Data != null) { + if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name "))) { + Console.WriteLine("[SMT-OUT] {0}", e.Data); + } + proverOutput.Enqueue(e.Data); + Monitor.Pulse(this); } - proverOutput.Enqueue(e.Data); - Monitor.Pulse(this); } } void prover_ErrorDataReceived(object sender, DataReceivedEventArgs e) { lock (this) { - if (options.Verbosity >= 1) - Console.WriteLine("[SMT-ERR] {0}", e.Data); - proverErrors.Enqueue(e.Data); - Monitor.Pulse(this); + if (e.Data != null) { + if (options.Verbosity >= 1) + Console.WriteLine("[SMT-ERR] {0}", e.Data); + proverErrors.Enqueue(e.Data); + Monitor.Pulse(this); + } } } #endregion diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs new file mode 100644 index 00000000..0565e677 --- /dev/null +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -0,0 +1,115 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Diagnostics.Contracts; + +namespace Microsoft.Boogie.SMTLib +{ + + public class OptionValue + { + public readonly string Option; + public readonly string Value; + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(Option != null); + Contract.Invariant(Value != null); + } + + public OptionValue(string option, string value) + { + Contract.Requires(option != null); + Contract.Requires(value != null); + Option = option; + Value = value; + } + } + + public class SMTLibProverOptions : ProverOptions + { + public bool UseWeights = true; + public bool UseLabels { get { return UseZ3; } } + public List SmtOptions = new List(); + public List SolverArguments = new List(); + + // Z3 specific (at the moment; some of them make sense also for other provers) + public bool UseZ3 = true; + public string Inspector = null; + public bool OptimizeForBv = false; + + public void AddSolverArgument(string s) + { + SolverArguments.Add(s); + } + + public void AddSmtOption(string name, string val) + { + SmtOptions.Add(new OptionValue(name, val)); + } + + public void AddWeakSmtOption(string name, string val) + { + if (!SmtOptions.Any(o => o.Option == name)) + SmtOptions.Add(new OptionValue(name, val)); + } + + public void AddSmtOption(string opt) + { + var idx = opt.IndexOf('='); + if (idx <= 0 || idx == opt.Length - 1) + ReportError("Options to be passed to the prover should have the format: O:=, got '" + opt + "'"); + AddSmtOption(opt.Substring(0, idx), opt.Substring(idx + 1)); + } + + protected override bool Parse(string opt) + { + if (opt.StartsWith("O:")) { + AddSmtOption(opt.Substring(2)); + return true; + } + + if (opt.StartsWith("C:")) { + AddSolverArgument(opt.Substring(2)); + return true; + } + + return + ParseBool(opt, "USE_WEIGHTS", ref UseWeights) || + ParseBool(opt, "USE_Z3", ref UseZ3) || + ParseString(opt, "INSPECTOR", ref Inspector) || + ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) || + base.Parse(opt); + } + + public override void PostParse() + { + base.PostParse(); + if (UseZ3) + Z3.SetupOptions(this); + } + + public override string Help + { + get + { + return +@" +SMT-specific options: +~~~~~~~~~~~~~~~~~~~~~ +USE_WEIGHTS= Pass :weight annotations on quantified formulas (default: true) +VERBOSITY= 1 - print prover output (default: 0) +O:= Pass (set-option : ) to the SMT solver. +C: Pass to the SMT on the command line. + +Z3-specific options: +~~~~~~~~~~~~~~~~~~~~ +INSPECTOR= Use the specified Z3Inspector binary. +OPTIMIZE_FOR_BV= Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false. +USE_Z3= Use z3.exe as the prover, and use Z3 extensions (default: true) +" + base.Help; + } + } + } +} diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 3867a55b..feb8b109 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -24,14 +24,14 @@ namespace Microsoft.Boogie.SMTLib return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)); } - public static string Z3ExecutablePath() + public static string ExecutablePath() { if (_proverPath == null) - FindZ3Executable(); + FindExecutable(); return _proverPath; } - static void FindZ3Executable() + static void FindExecutable() // throws ProverException, System.IO.FileNotFoundException; { Contract.Ensures(_proverPath != null); @@ -99,6 +99,69 @@ namespace Microsoft.Boogie.SMTLib } } + // options that work only on the command line + static string[] commandLineOnly = { "TRACE" }; + + public static void SetupOptions(SMTLibProverOptions options) + { + options.AddWeakSmtOption("MODEL_PARTIAL", "true"); + //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false"); + options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false"); + //options.WeakAddSmtOption("MODEL_V1", "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"); + 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"); + + // 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 (CommandLineOptions.Clo.LazyInlining == 2) + options.AddWeakSmtOption("MACRO_EXPANSION", "true"); + + // legacy option handling + foreach (string opt in CommandLineOptions.Clo.Z3Options) { + Contract.Assert(opt != null); + int eq = opt.IndexOf("="); + var optName = opt.Substring(0, eq); + if (eq > 0 && 'A' <= opt[0] && opt[0] <= 'Z' && !commandLineOnly.Contains(optName)) { + options.AddSmtOption(optName, opt.Substring(eq + 1)); + } else { + options.AddSolverArgument(opt); + } + } + } + } } -- cgit v1.2.3