From 408127c0fb6f2d38ce41d5e838777b7df36df438 Mon Sep 17 00:00:00 2001 From: MichalMoskal Date: Wed, 23 Feb 2011 22:22:03 +0000 Subject: Add MULTI_TRACES prover option (equivalent of /z3multipleErrors) --- Source/Provers/SMTLib/ProverInterface.cs | 35 ++++++++++++++++++---------- Source/Provers/SMTLib/SMTLibLineariser.cs | 5 ++-- Source/Provers/SMTLib/SMTLibNamer.cs | 4 ++-- Source/Provers/SMTLib/SMTLibProverOptions.cs | 3 +++ Source/Provers/SMTLib/TypeDeclCollector.cs | 8 +++---- Source/Provers/SMTLib/Z3.cs | 3 +++ 6 files changed, 37 insertions(+), 21 deletions(-) (limited to 'Source/Provers') diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index b0269d2e..b46ba916 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -322,20 +322,33 @@ namespace Microsoft.Boogie.SMTLib var globalResult = Outcome.Undetermined; while (errorsLeft-- > 0) { - string negLabel = null; + string[] labels = null; result = GetResponse(); if (globalResult == Outcome.Undetermined) globalResult = result; if (result == Outcome.Invalid && options.UseZ3) { - negLabel = GetLabelsInfo(handler); + labels = GetLabelsInfo(handler); } - if (negLabel == null) break; + if (labels == null) break; - SendThisVC("(assert " + SMTLibNamer.QuoteId(SMTLibNamer.BlockedLabel(negLabel)) + ")"); - SendThisVC("(check-sat)"); + var negLabels = labels.Where(l => l.StartsWith("@")).ToArray(); + var posLabels = labels.Where(l => !l.StartsWith("@")); + Func lbl = (s) => SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(s)); + if (negLabels.Length != 1) { + HandleProverError("Wrong number of negative labels: " + negLabels.Length); + break; + } else { + if (!options.MultiTraces) + posLabels = Enumerable.Empty(); + var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat1(lbl(negLabels[0])).ToArray(); + var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")"); + SendThisVC("(assert " + expr + ")"); + SendThisVC("(check-sat)"); + } + } SendThisVC("(pop 1)"); @@ -348,16 +361,16 @@ namespace Microsoft.Boogie.SMTLib } } - private string GetLabelsInfo(ErrorHandler handler) + private string[] GetLabelsInfo(ErrorHandler handler) { SendThisVC("(get-info :labels)"); if (options.ExpectingModel()) SendThisVC("(get-info :model)"); Process.Ping(); - string negLabel = null; List labelNums = null; Model theModel = null; + string[] res = null; while (true) { var resp = Process.GetProverResponse(); @@ -365,11 +378,9 @@ namespace Microsoft.Boogie.SMTLib break; if (resp.Name == ":labels" && resp.ArgCount >= 1) { var labels = resp[0].Arguments.Select(a => a.Name.Replace("|", "")).ToArray(); - negLabel = labels.FirstOrDefault(l => l.StartsWith("@")); + res = labels; if (labelNums != null) HandleProverError("Got multiple :labels responses"); - labelNums = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList(); - if (negLabel == null) - HandleProverError("No negative label in: " + labels.Concat(" ")); + labelNums = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList(); } else if (resp.Name == ":model" && resp.ArgCount >= 1) { var modelStr = resp[0].Name; List models = null; @@ -397,7 +408,7 @@ namespace Microsoft.Boogie.SMTLib handler.OnModel(labelNums, m); } - return negLabel; + return res; } private Outcome GetResponse() diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 4884b44f..35c4d5f0 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -511,12 +511,11 @@ namespace Microsoft.Boogie.SMTLib wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label)); } - if (!op.pos) - wr.Write("(or {0} ", SMTLibNamer.QuoteId(SMTLibNamer.BlockedLabel(op.label))); + wr.Write("({0} {1} ", op.pos ? "and" : "or", SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(op.label))); ExprLineariser.Linearise(node[0], options); - if (!op.pos) wr.Write(")"); + wr.Write(")"); if (ExprLineariser.ProverOptions.UseLabels) wr.Write(")"); diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index 600d6e51..e669e407 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -95,9 +95,9 @@ namespace Microsoft.Boogie.SMTLib return s; } - public static string BlockedLabel(string s) + public static string LabelVar(string s) { - return "%block%" + s; + return "%lbl%" + s; } public static string QuoteId(string s) diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs index 76bce71c..44f91cc2 100644 --- a/Source/Provers/SMTLib/SMTLibProverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -33,6 +33,7 @@ namespace Microsoft.Boogie.SMTLib public bool UseLabels { get { return UseZ3; } } public List SmtOptions = new List(); public List SolverArguments = new List(); + public bool MultiTraces = false; // Z3 specific (at the moment; some of them make sense also for other provers) public bool UseZ3 = true; @@ -86,6 +87,7 @@ namespace Microsoft.Boogie.SMTLib } return + ParseBool(opt, "MULTI_TRACES", ref MultiTraces) || ParseBool(opt, "USE_WEIGHTS", ref UseWeights) || ParseBool(opt, "USE_Z3", ref UseZ3) || ParseString(opt, "INSPECTOR", ref Inspector) || @@ -115,6 +117,7 @@ C: Pass to the SMT on the command line. Z3-specific options: ~~~~~~~~~~~~~~~~~~~~ +MULTI_TRACES= Report errors with multiple paths leading to the same assertion. 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) diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 60527ae8..96f16366 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -55,7 +55,7 @@ void ObjectInvariant() private readonly Dictionary/*!*/ KnownTypes = new Dictionary(); private readonly Dictionary/*!*/ KnownStoreFunctions = new Dictionary(); private readonly Dictionary/*!*/ KnownSelectFunctions = new Dictionary(); - private readonly HashSet KnownLBLNEG = new HashSet(); + private readonly HashSet KnownLBL = new HashSet(); public List!*/> AllDeclarations { get { @@ -124,9 +124,9 @@ void ObjectInvariant() KnownFunctions.Add(f, true); } else { var lab = node.Op as VCExprLabelOp; - if (lab != null && !lab.pos && !KnownLBLNEG.Contains(lab.label)) { - KnownLBLNEG.Add(lab.label); - var name = SMTLibNamer.QuoteId(SMTLibNamer.BlockedLabel(lab.label)); + if (lab != null && !KnownLBL.Contains(lab.label)) { + KnownLBL.Add(lab.label); + var name = SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(lab.label)); AddDeclaration("(declare-fun " + name + " () Bool)"); } } diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 74af2b84..27d86915 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -161,6 +161,9 @@ namespace Microsoft.Boogie.SMTLib options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString()); // 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("="); -- cgit v1.2.3