From 5d23ab3bf5bc80ee1bf5bbc6194a6de67264c61f Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 28 Dec 2015 20:28:04 -0600 Subject: Fix issue with ids for assume-statements. --- Source/Provers/SMTLib/TypeDeclCollector.cs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'Source/Provers/SMTLib/TypeDeclCollector.cs') diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 32e28560..1c23c22f 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -255,7 +255,10 @@ void ObjectInvariant() RegisterType(node.Type); string decl = "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")"; - AddDeclaration(decl); + if (!printedName.StartsWith("assume$$")) + { + AddDeclaration(decl); + } KnownVariables.Add(node); if(declHandler != null) declHandler.VarDecl(node); -- cgit v1.2.3 From 502942a53a6db2b3a900d7570807216372d49ad0 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 3 Mar 2016 17:32:31 -0600 Subject: Improve support for optimization and identifying unnecessary assumes. --- Source/Provers/SMTLib/ProverInterface.cs | 34 +++++++++------------- Source/Provers/SMTLib/SMTLibLineariser.cs | 22 ++++++++++++-- Source/Provers/SMTLib/TypeDeclCollector.cs | 12 ++++++-- Source/VCExpr/VCExprAST.cs | 2 ++ Source/VCGeneration/Check.cs | 7 ++--- Source/VCGeneration/VC.cs | 12 ++++---- Source/VCGeneration/Wlp.cs | 17 +++++++---- .../unnecessaryassumes1.bpl.expect | 2 +- 8 files changed, 64 insertions(+), 44 deletions(-) (limited to 'Source/Provers/SMTLib/TypeDeclCollector.cs') diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 7e98e8f8..432d7f3e 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -411,15 +411,6 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(push 1)"); SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")"); - if (CommandLineOptions.Clo.PrintNecessaryAssumes && NamedAssumeVars != null) - { - foreach (var v in NamedAssumeVars) - { - SendThisVC(string.Format("(declare-fun {0} () Bool)", v)); - SendThisVC(string.Format("(assert (! {0} :named {1}))", v, "aux$$" + v.Name)); - } - } - SendThisVC(vcString); SendOptimizationRequests(); @@ -1293,7 +1284,7 @@ namespace Microsoft.Boogie.SMTLib var reporter = handler as VC.VCGen.ErrorReporter; // TODO(wuestholz): Is the reporter ever null? - if (CommandLineOptions.Clo.PrintNecessaryAssumes && NamedAssumeVars != null && NamedAssumeVars.Any() && result == Outcome.Valid && reporter != null) + if (CommandLineOptions.Clo.PrintNecessaryAssumes && ContainsNamedAssumes && result == Outcome.Valid && reporter != null) { SendThisVC("(get-unsat-core)"); var resp = Process.GetProverResponse(); @@ -1993,6 +1984,8 @@ namespace Microsoft.Boogie.SMTLib readonly IList OptimizationRequests = new List(); + bool ContainsNamedAssumes; + protected string VCExpr2String(VCExpr expr, int polarity) { Contract.Requires(expr != null); @@ -2032,8 +2025,8 @@ namespace Microsoft.Boogie.SMTLib DeclCollector.Collect(sortedExpr); FeedTypeDeclsToProver(); - AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options)); - string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, OptimizationRequests); + AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options, ref ContainsNamedAssumes)); + string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, ref ContainsNamedAssumes, OptimizationRequests); Contract.Assert(res != null); if (CommandLineOptions.Clo.Trace) @@ -2141,20 +2134,19 @@ namespace Microsoft.Boogie.SMTLib throw new NotImplementedException(); } - public override void Assert(VCExpr vc, bool polarity) + public override void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1) { OptimizationRequests.Clear(); - string a = ""; - if (polarity) - { - a = "(assert " + VCExpr2String(vc, 1) + ")"; + string assert = "assert"; + if (options.Solver == SolverKind.Z3 && isSoft) { + assert += "-soft"; } - else - { - a = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))"; + var expr = polarity ? VCExpr2String(vc, 1) : "(not\n" + VCExpr2String(vc, 1) + "\n)"; + if (options.Solver == SolverKind.Z3 && isSoft) { + expr += " :weight " + weight; } AssertAxioms(); - SendThisVC(a); + SendThisVC("(" + assert + " " + expr + ")"); SendOptimizationRequests(); } diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index de8798b8..6df44c2f 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -34,7 +34,7 @@ namespace Microsoft.Boogie.SMTLib public class SMTLibExprLineariser : IVCExprVisitor { - public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, IList optReqs = null) + public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, ref bool containsNamedAssumes, IList optReqs = null) { Contract.Requires(e != null); Contract.Requires(namer != null); @@ -44,6 +44,7 @@ namespace Microsoft.Boogie.SMTLib SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, optReqs); Contract.Assert(lin != null); lin.Linearise(e, LineariserOptions.Default); + containsNamedAssumes |= lin.ContainsNamedAssumes; return cce.NonNull(sw.ToString()); } @@ -76,6 +77,12 @@ namespace Microsoft.Boogie.SMTLib readonly IList OptimizationRequests; + bool containsNamedAssumes; + public bool ContainsNamedAssumes + { + get { return containsNamedAssumes; } + } + public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList optReqs = null) { Contract.Requires(wr != null); Contract.Requires(namer != null); @@ -270,7 +277,18 @@ 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))); + OptimizationRequests.Add(string.Format("({0} {1})", optOp, ToString(node[0], Namer, ProverOptions, ref containsNamedAssumes))); + Linearise(node[1], options); + return true; + } + if (node.Op.Equals(VCExpressionGenerator.SoftOp)) + { + Linearise(node[1], options); + return true; + } + if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) + { + containsNamedAssumes = true; Linearise(node[1], options); return true; } diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 1c23c22f..72540c9c 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -210,7 +210,15 @@ void ObjectInvariant() if (node.Op is VCExprStoreOp) RegisterStore(node); else if (node.Op is VCExprSelectOp) RegisterSelect(node); - else { + else if (node.Op.Equals(VCExpressionGenerator.SoftOp)) { + var exprVar = node[0] as VCExprVar; + AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); + AddDeclaration(string.Format("(assert-soft {0} :weight 1)", exprVar.Name)); + } 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)); + } else { VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp; if (op != null && !(op.Func is DatatypeConstructor) && !(op.Func is DatatypeMembership) && !(op.Func is DatatypeSelector) && @@ -255,7 +263,7 @@ void ObjectInvariant() RegisterType(node.Type); string decl = "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")"; - if (!printedName.StartsWith("assume$$")) + if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$"))) { AddDeclaration(decl); } diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 2fbb102c..a58cfb7f 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -343,6 +343,8 @@ namespace Microsoft.Boogie { public static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool); public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool); + public static readonly VCExprOp NamedAssumeOp = new VCExprCustomOp("named_assume##dummy", 2, Type.Bool); + public static readonly VCExprOp SoftOp = new VCExprCustomOp("soft##dummy", 2, Type.Bool); public VCExprOp BoogieFunctionOp(Function func) { Contract.Requires(func != null); diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 8c1ae407..ae4d158a 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -346,7 +346,7 @@ namespace Microsoft.Boogie { } } - public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, IList namedAssumeVars = null) { + public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) { Contract.Requires(descriptiveName != null); Contract.Requires(vc != null); Contract.Requires(handler != null); @@ -360,7 +360,6 @@ namespace Microsoft.Boogie { thmProver.Reset(gen); SetTimeout(); proverStart = DateTime.UtcNow; - thmProver.NamedAssumeVars = namedAssumeVars; thmProver.BeginCheck(descriptiveName, vc, handler); // gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy @@ -388,8 +387,6 @@ namespace Microsoft.Boogie { public abstract class ProverInterface { - public IList NamedAssumeVars; - public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) { Contract.Requires(prog != null); @@ -546,7 +543,7 @@ namespace Microsoft.Boogie { } // (assert vc) - public virtual void Assert(VCExpr vc, bool polarity) + public virtual void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1) { throw new NotImplementedException(); } diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index ad067c04..6e43e917 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1386,8 +1386,7 @@ namespace VC { var exprGen = ctx.ExprGen; VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO); - var namedAssumeVars = new List(); - VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context, namedAssumeVars: namedAssumeVars); + VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context); Contract.Assert(vc != null); if (!CommandLineOptions.Clo.UseLabels) @@ -1415,7 +1414,7 @@ namespace VC { string desc = cce.NonNull(impl.Name); if (no >= 0) desc += "_split" + no; - checker.BeginCheck(desc, vc, reporter, namedAssumeVars); + checker.BeginCheck(desc, vc, reporter); } private void SoundnessCheck(HashSet/*!*/>/*!*/ cache, Block/*!*/ orig, List/*!*/ copies) { @@ -1568,8 +1567,7 @@ namespace VC { } break; case CommandLineOptions.VCVariety.DagIterative: - // TODO(wuestholz): Support named assume statements not just for this encoding. - vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount, namedAssumeVars: namedAssumeVars); + vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount); break; case CommandLineOptions.VCVariety.Doomed: vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount); @@ -3393,7 +3391,7 @@ namespace VC { Dictionary label2absy, ProverContext proverCtxt, out int assertionCount, - bool isPositiveContext = true, IList namedAssumeVars = null) + bool isPositiveContext = true) { Contract.Requires(blocks != null); Contract.Requires(proverCtxt != null); @@ -3453,7 +3451,7 @@ namespace VC { } VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext); - VCExpr vc = Wlp.Block(block, SuccCorrect, context, namedAssumeVars); + VCExpr vc = Wlp.Block(block, SuccCorrect, context); assertionCount += context.AssertionCount; VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool); diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 508a1400..07db709d 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -48,7 +48,7 @@ namespace VC { public class Wlp { - public static VCExpr Block(Block b, VCExpr N, VCContext ctxt, IList namedAssumeVars = null) + public static VCExpr Block(Block b, VCExpr N, VCContext ctxt) //modifies ctxt.*; { Contract.Requires(b != null); @@ -63,7 +63,7 @@ namespace VC { for (int i = b.Cmds.Count; --i >= 0; ) { - res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt, namedAssumeVars); + res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt); } int id = b.UniqueId; @@ -87,7 +87,7 @@ namespace VC { /// /// Computes the wlp for an assert or assume command "cmd". /// - internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt, IList namedAssumeVars = null) { + internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) { Contract.Requires(cmd != null); Contract.Requires(N != null); Contract.Requires(ctxt != null); @@ -193,11 +193,16 @@ namespace VC { var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id"); - if (CommandLineOptions.Clo.PrintNecessaryAssumes && aid != null && namedAssumeVars != null) + if (CommandLineOptions.Clo.PrintNecessaryAssumes && aid != null) { var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool); - namedAssumeVars.Add(v); - expr = gen.ImpliesSimp(v, expr); + expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr)); + } + var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft"); + if (soft && aid != null) + { + var v = gen.Variable("soft$$" + aid, Microsoft.Boogie.Type.Bool); + expr = gen.Function(VCExpressionGenerator.SoftOp, v, gen.ImpliesSimp(v, expr)); } return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(expr, N)); } else { diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect index dd04bb46..0d3aeca2 100644 --- a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect @@ -1,3 +1,3 @@ -Necessary assume command(s): s0, s3, s2 +Necessary assume command(s): s0, s2, s3 Boogie program verifier finished with 3 verified, 0 errors -- cgit v1.2.3 From 63c4b7642cd4566a39906b2d73c47b4ebe9f7c1c Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 7 Mar 2016 18:25:13 -0600 Subject: Add support for weights on soft assumes. --- Source/Provers/SMTLib/SMTLibLineariser.cs | 2 +- Source/Provers/SMTLib/TypeDeclCollector.cs | 4 ++-- Source/VCExpr/VCExprAST.cs | 11 ++++++++++- Source/VCGeneration/Wlp.cs | 5 +++-- 4 files changed, 16 insertions(+), 6 deletions(-) (limited to 'Source/Provers/SMTLib/TypeDeclCollector.cs') diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 6df44c2f..06554fcb 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -281,7 +281,7 @@ namespace Microsoft.Boogie.SMTLib Linearise(node[1], options); return true; } - if (node.Op.Equals(VCExpressionGenerator.SoftOp)) + if (node.Op is VCExprSoftOp) { Linearise(node[1], options); return true; diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 72540c9c..d911ce58 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -210,10 +210,10 @@ void ObjectInvariant() if (node.Op is VCExprStoreOp) RegisterStore(node); else if (node.Op is VCExprSelectOp) RegisterSelect(node); - else if (node.Op.Equals(VCExpressionGenerator.SoftOp)) { + else if (node.Op is VCExprSoftOp) { var exprVar = node[0] as VCExprVar; AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); - AddDeclaration(string.Format("(assert-soft {0} :weight 1)", exprVar.Name)); + AddDeclaration(string.Format("(assert-soft {0} :weight {1})", exprVar.Name, ((VCExprSoftOp)node.Op).Weight)); } else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) { var exprVar = node[0] as VCExprVar; AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name)); diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index a58cfb7f..2c77a252 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -344,7 +344,6 @@ namespace Microsoft.Boogie { public static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool); public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool); public static readonly VCExprOp NamedAssumeOp = new VCExprCustomOp("named_assume##dummy", 2, Type.Bool); - public static readonly VCExprOp SoftOp = new VCExprCustomOp("soft##dummy", 2, Type.Bool); public VCExprOp BoogieFunctionOp(Function func) { Contract.Requires(func != null); @@ -1570,6 +1569,16 @@ namespace Microsoft.Boogie.VCExprAST { } } + public class VCExprSoftOp : VCExprCustomOp + { + public readonly int Weight; + + public VCExprSoftOp(int weight) : base("soft##dummy", 2, Microsoft.Boogie.Type.Bool) + { + Weight = weight; + } + } + public class VCExprCustomOp : VCExprOp { public readonly string/*!*/ Name; int arity; diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 07db709d..d18c544a 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -199,10 +199,11 @@ namespace VC { expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr)); } var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft"); - if (soft && aid != null) + var softWeight = QKeyValue.FindIntAttribute(ac.Attributes, "soft", 0); + if ((soft || 0 < softWeight) && aid != null) { var v = gen.Variable("soft$$" + aid, Microsoft.Boogie.Type.Bool); - expr = gen.Function(VCExpressionGenerator.SoftOp, v, gen.ImpliesSimp(v, expr)); + expr = gen.Function(new VCExprSoftOp(Math.Max(softWeight, 1)), v, gen.ImpliesSimp(v, expr)); } return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(expr, N)); } else { -- cgit v1.2.3 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(-) (limited to 'Source/Provers/SMTLib/TypeDeclCollector.cs') 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