summaryrefslogtreecommitdiff
path: root/Source/Provers
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs59
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs17
-rw-r--r--Source/Provers/SMTLib/SMTLibNamer.cs2
-rw-r--r--Source/Provers/SMTLib/TypeDeclCollector.cs5
4 files changed, 73 insertions, 10 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index e93ecee9..7e98e8f8 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -246,9 +246,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 +401,8 @@ namespace Microsoft.Boogie.SMTLib
PrepareCommon();
+ OptimizationRequests.Clear();
+
string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
FlushAxioms();
@@ -408,7 +410,20 @@ 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();
+
FlushLogFile();
if (Process != null) {
@@ -422,6 +437,17 @@ namespace Microsoft.Boogie.SMTLib
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 +472,7 @@ namespace Microsoft.Boogie.SMTLib
if (options.Solver == SolverKind.Z3)
{
this.gen = gen;
+ SendThisVC("(reset)");
Namer.Reset();
common.Clear();
SetupAxiomBuilder(gen);
@@ -1264,6 +1291,22 @@ namespace Microsoft.Boogie.SMTLib
result = GetResponse();
+ 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)
+ {
+ SendThisVC("(get-unsat-core)");
+ var resp = Process.GetProverResponse();
+ if (resp.Name != "")
+ {
+ reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length));
+ }
+ foreach (var arg in resp.Arguments)
+ {
+ reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length));
+ }
+ }
+
if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut)
{
#region Run timeout diagnostics
@@ -1812,6 +1855,7 @@ namespace Microsoft.Boogie.SMTLib
private Model GetErrorModel() {
if (!options.ExpectingModel())
return null;
+
SendThisVC("(get-model)");
Process.Ping();
Model theModel = null;
@@ -1906,6 +1950,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 +1991,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 +2032,8 @@ namespace Microsoft.Boogie.SMTLib
DeclCollector.Collect(sortedExpr);
FeedTypeDeclsToProver();
-
-
AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options));
- string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options);
+ string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, OptimizationRequests);
Contract.Assert(res != null);
if (CommandLineOptions.Clo.Trace)
@@ -2096,6 +2143,7 @@ namespace Microsoft.Boogie.SMTLib
public override void Assert(VCExpr vc, bool polarity)
{
+ OptimizationRequests.Clear();
string a = "";
if (polarity)
{
@@ -2107,6 +2155,7 @@ namespace Microsoft.Boogie.SMTLib
}
AssertAxioms();
SendThisVC(a);
+ SendOptimizationRequests();
}
public override void DefineMacro(Macro f, VCExpr vc) {
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index dcf95bd2..de8798b8 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, IList<string> optReqs = 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, optReqs);
Contract.Assert(lin != null);
lin.Linearise(e, LineariserOptions.Default);
return cce.NonNull(sw.ToString());
@@ -74,12 +74,15 @@ namespace Microsoft.Boogie.SMTLib
internal int UnderQuantifier = 0;
internal readonly SMTLibProverOptions ProverOptions;
- public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts)
+ readonly IList<string> OptimizationRequests;
+
+ public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList<string> optReqs = null)
{
Contract.Requires(wr != null); Contract.Requires(namer != null);
this.wr = wr;
this.Namer = namer;
this.ProverOptions = opts;
+ this.OptimizationRequests = optReqs;
}
public void Linearise(VCExpr expr, LineariserOptions options)
@@ -263,6 +266,14 @@ 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)));
+ 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..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);
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 16:05:14 +0000