Add experimental support for optimization (requires Z3 build after changeset 9cba63c31f6f1466dd4ef442bb840d1ab84539c7).

3 files changed, 33 insertions, 7 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index cb8442e5..ca530da2 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -401,6 +401,8 @@ namespace Microsoft.Boogie.SMTLib
 
       PrepareCommon();
 
+      OptimizationRequests.Clear();
+
       string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
       FlushAxioms();
 
@@ -418,6 +420,15 @@ namespace Microsoft.Boogie.SMTLib
       }
 
       SendThisVC(vcString);
+
+      if (options.Solver == SolverKind.Z3 && 0 < OptimizationRequests.Count)
+      {
+        foreach (var r in OptimizationRequests)
+        {
+          SendThisVC(r);
+        }
+      }
+
       FlushLogFile();
 
       if (Process != null) {
@@ -1838,6 +1849,7 @@ namespace Microsoft.Boogie.SMTLib
     private Model GetErrorModel() {
       if (!options.ExpectingModel())
         return null;
+
       SendThisVC("(get-model)");
       Process.Ping();
       Model theModel = null;
@@ -1932,6 +1944,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;
@@ -1970,6 +1985,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);
@@ -2009,10 +2026,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)
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)