From 9a9991f2131de8e78035581ea2569ba187318ff0 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 7 May 2013 17:40:40 -0700 Subject: Adding fixedpoint engine backend --- Source/Boogie.sln | 2 +- Source/BoogieDriver/BoogieDriver.cs | 16 +- Source/Core/CommandLineOptions.cs | 45 +++ Source/Provers/SMTLib/ProverInterface.cs | 189 ++++++++++++ Source/Provers/SMTLib/SMTLibLineariser.cs | 24 +- Source/Provers/SMTLib/TypeDeclCollector.cs | 14 +- Source/Provers/SMTLib/Z3.cs | 479 +++++++++++++++++++---------- Source/VCGeneration/Check.cs | 5 + Source/VCGeneration/VC.cs | 2 +- Source/VCGeneration/VCGeneration.csproj | 3 + 10 files changed, 594 insertions(+), 185 deletions(-) diff --git a/Source/Boogie.sln b/Source/Boogie.sln index f3f068d7..7d27c011 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -1,5 +1,5 @@  -Microsoft Visual Studio Solution File, Format Version 12.00 +Microsoft Visual Studio Solution File, Format Version 11.00 # Visual Studio 2012 Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758C1E3-824A-439F-AA2F-0BA1143E8C8D}" EndProject diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index c12ba47d..1ee9bab6 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -743,10 +743,18 @@ namespace Microsoft.Boogie { try { if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); - } else if (CommandLineOptions.Clo.StratifiedInlining > 0) { - vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); - } else { - vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); + } + else if (CommandLineOptions.Clo.FixedPointEngine != null) + { + vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); + } + else if (CommandLineOptions.Clo.StratifiedInlining > 0) + { + vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); + } + else + { + vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); } } catch (ProverException e) { ErrorWriteLine("Fatal Error: ProverException: {0}", e); diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index e94367ad..3e923ee9 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -574,6 +574,7 @@ namespace Microsoft.Boogie { public bool ExtractLoops = false; public bool DeterministicExtractLoops = false; public int StratifiedInlining = 0; + public string FixedPointEngine = null; public int StratifiedInliningOption = 0; public bool StratifiedInliningWithoutModels = false; // disable model generation for SI public int StratifiedInliningVerbose = 0; // verbosity level @@ -583,6 +584,16 @@ namespace Microsoft.Boogie { public string CoverageReporterPath = null; public Process coverageReporter = null; // used internally for debugging + // Inference mode for fixed point engine + public enum FixedPointInferenceMode { + Corral, + OldCorral, + Flat, + Procedure, + Call + }; + public FixedPointInferenceMode FixedPointMode = FixedPointInferenceMode.Procedure; + public enum TypeEncoding { None, Predicates, @@ -1002,6 +1013,38 @@ namespace Microsoft.Boogie { } } return true; + case "fixedPointEngine": + if (ps.ConfirmArgumentCount(1)) + { + FixedPointEngine = args[ps.i]; + } + return true; + case "fixedPointInfer": + if (ps.ConfirmArgumentCount(1)) + { + switch (args[ps.i]) + { + case "corral": + FixedPointMode = FixedPointInferenceMode.Corral; + break; + case "oldCorral": + FixedPointMode = FixedPointInferenceMode.OldCorral; + break; + case "flat": + FixedPointMode = FixedPointInferenceMode.Flat; + break; + case "procedure": + FixedPointMode = FixedPointInferenceMode.Procedure; + break; + case "call": + FixedPointMode = FixedPointInferenceMode.Call; + break; + default: + ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s); + break; + } + } + return true; case "siVerbose": if (ps.ConfirmArgumentCount(1)) { StratifiedInliningVerbose = Int32.Parse(cce.NonNull(args[ps.i])); @@ -1574,6 +1617,8 @@ namespace Microsoft.Boogie { Use the lazy inlining algorithm /stratifiedInline:1 Use the stratified inlining algorithm + /fixedPointEngine: + Use the specified fixed point engine for inference /recursionBound: Set the recursion bound for stratified inlining to be n (default 500) diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 3df1bd32..3004fafa 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -19,6 +19,8 @@ using Microsoft.Boogie.Clustering; using Microsoft.Boogie.TypeErasure; using System.Text; +using RPFP = Microsoft.Boogie.RPFP; + namespace Microsoft.Boogie.SMTLib { public class SMTLibProcessTheoremProver : ProverInterface @@ -27,6 +29,7 @@ namespace Microsoft.Boogie.SMTLib private readonly VCExpressionGenerator gen; private readonly SMTLibProverOptions options; private bool usingUnsatCore; + private RPFP rpfp = null; [ContractInvariantMethod] void ObjectInvariant() @@ -361,6 +364,7 @@ namespace Microsoft.Boogie.SMTLib //Contract.Requires(descriptiveName != null); //Contract.Requires(vc != null); //Contract.Requires(handler != null); + rpfp = null; if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen @@ -391,6 +395,191 @@ namespace Microsoft.Boogie.SMTLib FlushLogFile(); } + private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler) + { + Dictionary nmap = new Dictionary(); + Dictionary pmap = new Dictionary(); + + foreach(var node in rpfp.nodes) + pmap.Add((node.Name as VCExprBoogieFunctionOp).Func.Name,node); + + RPFP.Node topnode = null; + var lines = resp.Arguments; + + // last line of derivation is from query, skip it + for (int i = 0; i < lines.Length-1; i++) + { + var line = lines[i]; + if (line.ArgCount != 5) + { + HandleProverError("bad derivation line from prover: " + line.ToString()); + return null; + } + var name = line[0]; + var conseq = line[1]; + var subst = line[2]; + var labs = line[3]; + var refs = line[4]; + var predName = conseq.Name; + RPFP.Node node = null; + if (!pmap.TryGetValue(predName, out node)) + { + HandleProverError("unknown predicate from prover: " + predName.ToString()); + return null; + } + RPFP.Node cexnode = rpfp.CloneNode(node); + cexnode.map = node; + nmap.Add(name.Name, cexnode); + List Chs = new List(); + + if (refs.Name != "ref") + { + HandleProverError("bad references from prover: " + refs.ToString()); + return null; + } + foreach (var c in refs.Arguments) + { + if (c.Name == "true") + Chs.Add(null); + else + { + RPFP.Node ch = null; + if (!nmap.TryGetValue(c.Name, out ch)) + { + HandleProverError("unknown reference from prover: " + c.ToString()); + return null; + } + Chs.Add(ch); + } + } + RPFP.Edge e = rpfp.CreateEdge(cexnode, node.Outgoing.F, Chs.ToArray()); + topnode = cexnode; + + if (labs.Name != "labels") + { + HandleProverError("bad labels from prover: " + refs.ToString()); + return null; + } + e.labels = new HashSet(); + foreach (var l in labs.Arguments) + e.labels.Add(l.Name); + + } + if (topnode == null) + { + HandleProverError("empty derivation from prover: " + resp.ToString()); + } + return topnode; + } + + public override Outcome CheckRPFP(string descriptiveName, RPFP _rpfp, ErrorHandler handler, out RPFP.Node cex) + { + //Contract.Requires(descriptiveName != null); + //Contract.Requires(vc != null); + //Contract.Requires(handler != null); + rpfp = _rpfp; + cex = null; + + if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen + + if (options.LogFilename != null && currentLogFile == null) + { + currentLogFile = OpenOutputFile(descriptiveName); + currentLogFile.Write(common.ToString()); + } + + foreach (var node in rpfp.nodes) + { + DeclCollector.RegisterRelation((node.Name as VCExprBoogieFunctionOp).Func); + } + + PrepareCommon(); + + LineariserOptions.Default.LabelsBelowQuantifiers = true; + List ruleStrings = new List(); + foreach (var edge in rpfp.edges) + { + string ruleString = "(rule " + VCExpr2String(rpfp.GetRule(edge), 1) + "\n)"; + ruleStrings.Add(ruleString); + } + string queryString = "(query " + VCExpr2String(rpfp.GetQuery(), 1) + "\n :engine duality\n :print-certificate true\n)"; + LineariserOptions.Default.LabelsBelowQuantifiers = false; + FlushAxioms(); + + PossiblyRestart(); + + SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")"); + foreach(var rs in ruleStrings) + SendThisVC(rs); + FlushLogFile(); + + if (Process != null) + { + Process.PingPong(); // flush any errors + +#if false + // TODO: this is not going to work + if (Process.Inspector != null) + Process.Inspector.NewProblem(descriptiveName, vc, handler); +#endif + } + + SendThisVC(queryString); + FlushLogFile(); + + var result = Outcome.Undetermined; + + if (Process != null) + { + + var resp = Process.GetProverResponse(); + + switch (resp.Name) + { + case "unsat": + result = Outcome.Valid; + break; + case "sat": + result = Outcome.Invalid; + break; + case "unknown": + result = Outcome.Invalid; + break; + default: + HandleProverError("Unexpected prover response: " + resp.ToString()); + break; + } + + switch (result) + { + case Outcome.Invalid: + { + resp = Process.GetProverResponse(); + if (resp.Name == "derivation") + { + cex = SExprToCex(resp, handler); + } + else + HandleProverError("Unexpected prover response: " + resp.ToString()); + break; + } + default: + break; + } + +#if false + while (true) + { + resp = Process.GetProverResponse(); + if (resp == null || Process.IsPong(resp)) + break; + HandleProverError("Unexpected prover response: " + resp.ToString()); + } +#endif + } + return result; + } + private static HashSet usedLogNames = new HashSet(); private TextWriter OpenOutputFile(string descriptiveName) diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index da73dea1..1f4b6a7f 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -23,7 +23,8 @@ namespace Microsoft.Boogie.SMTLib // Options for the linearisation public class LineariserOptions { - public static readonly LineariserOptions Default = new LineariserOptions(); + public static LineariserOptions Default = new LineariserOptions(); + public bool LabelsBelowQuantifiers = false; } @@ -518,23 +519,28 @@ namespace Microsoft.Boogie.SMTLib public bool VisitLabelOp(VCExprNAry node, LineariserOptions options) { - if (ExprLineariser.UnderQuantifier > 0) { + if (ExprLineariser.UnderQuantifier > 0 && !options.LabelsBelowQuantifiers) { ExprLineariser.Linearise(node[0], options); return true; } var op = (VCExprLabelOp)node.Op; - if (CommandLineOptions.Clo.UseLabels) { - // Z3 extension - //wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label)); - wr.Write("(! "); + + if (CommandLineOptions.Clo.UseLabels) + { + // Z3 extension + //wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label)); + wr.Write("(! "); } - wr.Write("({0} {1} ", op.pos ? "and" : "or", SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(op.label))); - + if(!options.LabelsBelowQuantifiers) + wr.Write("({0} {1} ", op.pos ? "and" : "or", SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(op.label))); + ExprLineariser.Linearise(node[0], options); - wr.Write(")"); + + if (!options.LabelsBelowQuantifiers) + wr.Write(")"); if (CommandLineOptions.Clo.UseLabels) wr.Write(" :{0} {1})", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label)); diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index bff949ea..9d908138 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -20,6 +20,7 @@ namespace Microsoft.Boogie.SMTLib private readonly UniqueNamer Namer; private readonly SMTLibProverOptions Options; + private HashSet/*!*/ RegisteredRelations = new HashSet(); [ContractInvariantMethod] void ObjectInvariant() @@ -170,6 +171,13 @@ void ObjectInvariant() KnownFunctions.Add(func); } + public void RegisterRelation(Function func) + { + if (RegisteredRelations.Contains(func)) + return; + RegisteredRelations.Add(func); + } + public override bool Visit(VCExprNAry node, bool arg) { Contract.Requires(node != null); @@ -190,7 +198,11 @@ void ObjectInvariant() Contract.Assert(f.OutParams.Length == 1); var argTypes = f.InParams.Cast().MapConcat(p => TypeToStringReg(p.TypedIdent.Type), " "); - string decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")"; + string decl; + if(RegisteredRelations.Contains(op.Func)) + decl = "(declare-rel " + printedName + " (" + argTypes + ") " + ")"; + else + decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")"; AddDeclaration(decl); } KnownFunctions.Add(f); 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() != 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() != 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 z3Dirs = new List(); + + 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 z3Dirs = new List(); - - 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); + } + } } - } - } - } + } } diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index fe4b4b99..607476e7 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -405,6 +405,11 @@ namespace Microsoft.Boogie { } } public abstract void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler); + + public virtual Outcome CheckRPFP(string descriptiveName, RPFP vc, ErrorHandler handler, out RPFP.Node cex) + { + throw new System.NotImplementedException(); + } [NoDefaultContract] public abstract Outcome CheckOutcome(ErrorHandler handler); public virtual string[] CalculatePath(int controlFlowConstant) { diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index bcf0b0e5..3748d7f7 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1356,7 +1356,7 @@ namespace VC { vc = NestedBlockVC(impl, label2absy, true, proverContext, out assertionCount); break; case CommandLineOptions.VCVariety.Dag: - if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags) { + if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags || CommandLineOptions.Clo.FixedPointEngine != null) { vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, new Hashtable/**/(), proverContext, out assertionCount); } else { vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, proverContext, out assertionCount); diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj index 0c98a891..f724307b 100644 --- a/Source/VCGeneration/VCGeneration.csproj +++ b/Source/VCGeneration/VCGeneration.csproj @@ -147,7 +147,10 @@ + + + -- cgit v1.2.3