From 8ed5dab22d8377924ee6282b83c1b1f8aa8f3573 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Wed, 9 Mar 2016 19:18:15 -0600 Subject: Improve support for identifying unnecessary assumes. --- Source/Provers/SMTLib/ProverInterface.cs | 84 +++++++++++++++++++----------- Source/Provers/SMTLib/SMTLibLineariser.cs | 20 +++---- Source/Provers/SMTLib/TypeDeclCollector.cs | 7 ++- Source/VCGeneration/Check.cs | 4 ++ Source/VCGeneration/Wlp.cs | 5 +- 5 files changed, 73 insertions(+), 47 deletions(-) diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 432d7f3e..300fbc10 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -86,6 +86,21 @@ namespace Microsoft.Boogie.SMTLib } } + public override void AssertNamed(VCExpr vc, bool polarity, string name) + { + string vcString; + if (polarity) + { + vcString = VCExpr2String(vc, 1); + } + else + { + vcString = "(not " + VCExpr2String(vc, 1) + ")"; + } + AssertAxioms(); + SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name)); + } + private void SetupAxiomBuilder(VCExpressionGenerator gen) { switch (CommandLineOptions.Clo.TypeEncodingMethod) @@ -424,7 +439,7 @@ namespace Microsoft.Boogie.SMTLib Process.Inspector.NewProblem(descriptiveName, vc, handler); } - SendThisVC("(check-sat)"); + SendCheckSat(); FlushLogFile(); } @@ -474,6 +489,8 @@ namespace Microsoft.Boogie.SMTLib ctx.KnownDatatypeConstructors.Clear(); ctx.parent = this; DeclCollector.Reset(); + NamedAssumes.Clear(); + UsedNamedAssumes = null; SendThisVC("; did a full reset"); } } @@ -1284,17 +1301,33 @@ namespace Microsoft.Boogie.SMTLib var reporter = handler as VC.VCGen.ErrorReporter; // TODO(wuestholz): Is the reporter ever null? - if (CommandLineOptions.Clo.PrintNecessaryAssumes && ContainsNamedAssumes && result == Outcome.Valid && reporter != null) + if (usingUnsatCore && result == Outcome.Valid && reporter != null && 0 < NamedAssumes.Count) { - SendThisVC("(get-unsat-core)"); - var resp = Process.GetProverResponse(); - if (resp.Name != "") + if (usingUnsatCore) { - reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length)); + UsedNamedAssumes = new HashSet(); + SendThisVC("(get-unsat-core)"); + var resp = Process.GetProverResponse(); + if (resp.Name != "") + { + UsedNamedAssumes.Add(resp.Name); + if (CommandLineOptions.Clo.PrintNecessaryAssumes) + { + reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length)); + } + } + foreach (var arg in resp.Arguments) + { + UsedNamedAssumes.Add(arg.Name); + if (CommandLineOptions.Clo.PrintNecessaryAssumes) + { + reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length)); + } + } } - foreach (var arg in resp.Arguments) + else { - reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length)); + UsedNamedAssumes = null; } } @@ -1457,13 +1490,13 @@ namespace Microsoft.Boogie.SMTLib expr = "false"; } SendThisVC("(assert " + expr + ")"); - SendThisVC("(check-sat)"); + SendCheckSat(); } else { string source = labels[labels.Length - 2]; string target = labels[labels.Length - 1]; SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") (- " + target + "))))"); - SendThisVC("(check-sat)"); + SendCheckSat(); } } @@ -1508,7 +1541,7 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(apply (then (using-params propagate-values :max_rounds 1) simplify) :print false)"); } FlushLogFile(); - SendThisVC("(check-sat)"); + SendCheckSat(); queries++; return GetResponse(); } @@ -1984,8 +2017,6 @@ namespace Microsoft.Boogie.SMTLib readonly IList OptimizationRequests = new List(); - bool ContainsNamedAssumes; - protected string VCExpr2String(VCExpr expr, int polarity) { Contract.Requires(expr != null); @@ -2025,8 +2056,8 @@ namespace Microsoft.Boogie.SMTLib DeclCollector.Collect(sortedExpr); FeedTypeDeclsToProver(); - AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options, ref ContainsNamedAssumes)); - string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, ref ContainsNamedAssumes, OptimizationRequests); + AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options, namedAssumes: NamedAssumes)); + string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, NamedAssumes, OptimizationRequests); Contract.Assert(res != null); if (CommandLineOptions.Clo.Trace) @@ -2167,9 +2198,15 @@ namespace Microsoft.Boogie.SMTLib public override void Check() { PrepareCommon(); - SendThisVC("(check-sat)"); + SendCheckSat(); FlushLogFile(); } + + public void SendCheckSat() + { + UsedNamedAssumes = null; + SendThisVC("(check-sat)"); + } public override void SetTimeOut(int ms) { @@ -2366,21 +2403,6 @@ namespace Microsoft.Boogie.SMTLib return opts; } - public override void AssertNamed(VCExpr vc, bool polarity, string name) - { - string vcString; - if (polarity) - { - vcString = VCExpr2String(vc, 1); - } - else - { - vcString = "(not " + VCExpr2String(vc, 1) + ")"; - } - AssertAxioms(); - SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name)); - } - public override VCExpr ComputeInterpolant(VCExpr A, VCExpr B) { string A_str = VCExpr2String(A, 1); diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 06554fcb..06aa5bbe 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -34,17 +34,16 @@ namespace Microsoft.Boogie.SMTLib public class SMTLibExprLineariser : IVCExprVisitor { - public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, ref bool containsNamedAssumes, IList optReqs = null) + public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, ISet namedAssumes = null, IList optReqs = null, ISet tryAssumes = null) { Contract.Requires(e != null); Contract.Requires(namer != null); Contract.Ensures(Contract.Result() != null); StringWriter sw = new StringWriter(); - SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, optReqs); + SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, namedAssumes, optReqs); Contract.Assert(lin != null); lin.Linearise(e, LineariserOptions.Default); - containsNamedAssumes |= lin.ContainsNamedAssumes; return cce.NonNull(sw.ToString()); } @@ -76,20 +75,16 @@ namespace Microsoft.Boogie.SMTLib internal readonly SMTLibProverOptions ProverOptions; readonly IList OptimizationRequests; + readonly ISet NamedAssumes; - bool containsNamedAssumes; - public bool ContainsNamedAssumes - { - get { return containsNamedAssumes; } - } - - public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList optReqs = null) + public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, ISet namedAssumes = null, IList optReqs = null) { Contract.Requires(wr != null); Contract.Requires(namer != null); this.wr = wr; this.Namer = namer; this.ProverOptions = opts; this.OptimizationRequests = optReqs; + this.NamedAssumes = namedAssumes; } public void Linearise(VCExpr expr, LineariserOptions options) @@ -277,7 +272,7 @@ namespace Microsoft.Boogie.SMTLib && (node.Op.Equals(VCExpressionGenerator.MinimizeOp) || node.Op.Equals(VCExpressionGenerator.MaximizeOp))) { string optOp = node.Op.Equals(VCExpressionGenerator.MinimizeOp) ? "minimize" : "maximize"; - OptimizationRequests.Add(string.Format("({0} {1})", optOp, ToString(node[0], Namer, ProverOptions, ref containsNamedAssumes))); + OptimizationRequests.Add(string.Format("({0} {1})", optOp, ToString(node[0], Namer, ProverOptions, NamedAssumes))); Linearise(node[1], options); return true; } @@ -288,7 +283,8 @@ namespace Microsoft.Boogie.SMTLib } if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) { - containsNamedAssumes = true; + var exprVar = node[0] as VCExprVar; + NamedAssumes.Add(exprVar); Linearise(node[1], options); return true; } diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index d911ce58..eaed83e9 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -217,7 +217,10 @@ void ObjectInvariant() } else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) { var exprVar = node[0] as VCExprVar; AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); - AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name)); + if (CommandLineOptions.Clo.PrintNecessaryAssumes) + { + AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name)); + } } else { VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp; if (op != null && @@ -263,7 +266,7 @@ void ObjectInvariant() RegisterType(node.Type); string decl = "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")"; - if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$"))) + if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") || printedName.StartsWith("try$$"))) { AddDeclaration(decl); } diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index ae4d158a..7bda0022 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -453,6 +453,10 @@ namespace Microsoft.Boogie { Undetermined, Bounded } + + public readonly ISet NamedAssumes = new HashSet(); + public ISet UsedNamedAssumes { get; protected set; } + public class ErrorHandler { // Used in CheckOutcomeCore public virtual int StartingProcId() diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index d18c544a..cad5914b 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -193,9 +193,10 @@ namespace VC { var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id"); - if (CommandLineOptions.Clo.PrintNecessaryAssumes && aid != null) + if (aid != null) { - var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool); + var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try"); + var v = gen.Variable((isTry ? "try$$" : "assume$$") + aid, Microsoft.Boogie.Type.Bool); expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr)); } var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft"); -- cgit v1.2.3