summaryrefslogtreecommitdiff
path: root/Source/Provers
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs133
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs31
-rw-r--r--Source/Provers/SMTLib/SMTLibNamer.cs2
-rw-r--r--Source/Provers/SMTLib/TypeDeclCollector.cs18
4 files changed, 143 insertions, 41 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index e93ecee9..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)
@@ -246,9 +261,9 @@ namespace Microsoft.Boogie.SMTLib
// Set produce-unsat-cores last. It seems there's a bug in Z3 where if we set it earlier its value
// gets reset by other set-option commands ( https://z3.codeplex.com/workitem/188 )
- if (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini))
+ if (CommandLineOptions.Clo.PrintNecessaryAssumes || (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini)))
{
- SendThisVC("(set-option :produce-unsat-cores true)");
+ SendCommon("(set-option :produce-unsat-cores true)");
this.usingUnsatCore = true;
}
@@ -401,6 +416,8 @@ namespace Microsoft.Boogie.SMTLib
PrepareCommon();
+ OptimizationRequests.Clear();
+
string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
FlushAxioms();
@@ -408,7 +425,11 @@ namespace Microsoft.Boogie.SMTLib
SendThisVC("(push 1)");
SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
+
SendThisVC(vcString);
+
+ SendOptimizationRequests();
+
FlushLogFile();
if (Process != null) {
@@ -418,10 +439,21 @@ namespace Microsoft.Boogie.SMTLib
Process.Inspector.NewProblem(descriptiveName, vc, handler);
}
- SendThisVC("(check-sat)");
+ SendCheckSat();
FlushLogFile();
}
+ private void SendOptimizationRequests()
+ {
+ if (options.Solver == SolverKind.Z3 && 0 < OptimizationRequests.Count)
+ {
+ foreach (var r in OptimizationRequests)
+ {
+ SendThisVC(r);
+ }
+ }
+ }
+
public override void Reset(VCExpressionGenerator gen)
{
if (options.Solver == SolverKind.Z3)
@@ -446,6 +478,7 @@ namespace Microsoft.Boogie.SMTLib
if (options.Solver == SolverKind.Z3)
{
this.gen = gen;
+ SendThisVC("(reset)");
Namer.Reset();
common.Clear();
SetupAxiomBuilder(gen);
@@ -456,6 +489,8 @@ namespace Microsoft.Boogie.SMTLib
ctx.KnownDatatypeConstructors.Clear();
ctx.parent = this;
DeclCollector.Reset();
+ NamedAssumes.Clear();
+ UsedNamedAssumes = null;
SendThisVC("; did a full reset");
}
}
@@ -1264,6 +1299,38 @@ namespace Microsoft.Boogie.SMTLib
result = GetResponse();
+ var reporter = handler as VC.VCGen.ErrorReporter;
+ // TODO(wuestholz): Is the reporter ever null?
+ if (usingUnsatCore && result == Outcome.Valid && reporter != null && 0 < NamedAssumes.Count)
+ {
+ if (usingUnsatCore)
+ {
+ 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));
+ }
+ }
+ }
+ else
+ {
+ UsedNamedAssumes = null;
+ }
+ }
+
if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut)
{
#region Run timeout diagnostics
@@ -1423,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();
}
}
@@ -1474,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();
}
@@ -1812,6 +1879,7 @@ namespace Microsoft.Boogie.SMTLib
private Model GetErrorModel() {
if (!options.ExpectingModel())
return null;
+
SendThisVC("(get-model)");
Process.Ping();
Model theModel = null;
@@ -1906,6 +1974,9 @@ namespace Microsoft.Boogie.SMTLib
result = Outcome.Invalid;
wasUnknown = true;
break;
+ case "objectives":
+ // We ignore this.
+ break;
default:
HandleProverError("Unexpected prover response: " + resp.ToString());
break;
@@ -1944,6 +2015,8 @@ namespace Microsoft.Boogie.SMTLib
return result;
}
+ readonly IList<string> OptimizationRequests = new List<string>();
+
protected string VCExpr2String(VCExpr expr, int polarity)
{
Contract.Requires(expr != null);
@@ -1983,10 +2056,8 @@ namespace Microsoft.Boogie.SMTLib
DeclCollector.Collect(sortedExpr);
FeedTypeDeclsToProver();
-
-
- AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options));
- string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options);
+ 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)
@@ -2094,19 +2165,20 @@ 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)
{
- string a = "";
- if (polarity)
- {
- a = "(assert " + VCExpr2String(vc, 1) + ")";
+ OptimizationRequests.Clear();
+ 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();
}
public override void DefineMacro(Macro f, VCExpr vc) {
@@ -2126,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)
{
@@ -2325,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 dcf95bd2..06aa5bbe 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -34,14 +34,14 @@ namespace Microsoft.Boogie.SMTLib
public class SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/>
{
- public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts)
+ 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);
+ SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, namedAssumes, optReqs);
Contract.Assert(lin != null);
lin.Linearise(e, LineariserOptions.Default);
return cce.NonNull(sw.ToString());
@@ -74,12 +74,17 @@ namespace Microsoft.Boogie.SMTLib
internal int UnderQuantifier = 0;
internal readonly SMTLibProverOptions ProverOptions;
- public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts)
+ readonly IList<string> OptimizationRequests;
+ readonly ISet<VCExprVar> NamedAssumes;
+
+ 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)
@@ -263,6 +268,26 @@ namespace Microsoft.Boogie.SMTLib
}
return true;
}
+ if (OptimizationRequests != null
+ && (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, NamedAssumes)));
+ Linearise(node[1], options);
+ return true;
+ }
+ if (node.Op is VCExprSoftOp)
+ {
+ Linearise(node[1], options);
+ return true;
+ }
+ if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp))
+ {
+ var exprVar = node[0] as VCExprVar;
+ NamedAssumes.Add(exprVar);
+ Linearise(node[1], options);
+ return true;
+ }
return node.Accept<bool, LineariserOptions/*!*/>(OpLineariser, options);
}
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 900bdbcc..f1179159 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Boogie.SMTLib
"flet", "implies", "!=", "if_then_else",
// Z3 extensions
"lblneg", "lblpos", "lbl-lit",
- "if", "&&", "||", "equals", "equiv", "bool",
+ "if", "&&", "||", "equals", "equiv", "bool", "minimize", "maximize",
// Boogie-defined
"real_pow", "UOrdering2", "UOrdering3",
// Floating point (final draft SMTLIB-v2.5)
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 32e28560..eaed83e9 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -210,7 +210,18 @@ void ObjectInvariant()
if (node.Op is VCExprStoreOp) RegisterStore(node);
else if (node.Op is VCExprSelectOp) RegisterSelect(node);
- else {
+ 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, ((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));
+ 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 &&
!(op.Func is DatatypeConstructor) && !(op.Func is DatatypeMembership) && !(op.Func is DatatypeSelector) &&
@@ -255,7 +266,10 @@ void ObjectInvariant()
RegisterType(node.Type);
string decl =
"(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
- AddDeclaration(decl);
+ if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") || printedName.StartsWith("try$$")))
+ {
+ AddDeclaration(decl);
+ }
KnownVariables.Add(node);
if(declHandler != null)
declHandler.VarDecl(node);
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 06:37:56 +0000