summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs84
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs20
-rw-r--r--Source/Provers/SMTLib/TypeDeclCollector.cs7
-rw-r--r--Source/VCGeneration/Check.cs4
-rw-r--r--Source/VCGeneration/Wlp.cs5
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<string>();
+ 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<string> OptimizationRequests = new List<string>();
- 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<bool, LineariserOptions/*!*/>
{
- public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, ref bool containsNamedAssumes, IList<string> optReqs = null)
+ public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, ISet<VCExprVar> namedAssumes = null, IList<string> optReqs = null, ISet<VCExprVar> tryAssumes = null)
{
Contract.Requires(e != null);
Contract.Requires(namer != null);
Contract.Ensures(Contract.Result<string>() != 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<string> OptimizationRequests;
+ readonly ISet<VCExprVar> NamedAssumes;
- bool containsNamedAssumes;
- public bool ContainsNamedAssumes
- {
- get { return containsNamedAssumes; }
- }
-
- public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList<string> optReqs = null)
+ public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, ISet<VCExprVar> namedAssumes = null, IList<string> 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<VCExprVar> NamedAssumes = new HashSet<VCExprVar>();
+ public ISet<string> 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");
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 08:29:47 +0000