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

8 files changed, 87 insertions, 12 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index c33f0743..2e33e1dd 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -3218,8 +3218,14 @@ namespace Microsoft.Boogie {
       this.Expr.Emit(stream);
       stream.WriteLine(";");
     }
+    public override void Resolve(ResolutionContext rc) {
+      //Contract.Requires(rc != null);
+      ResolveAttributes(Attributes, rc);
+      base.Resolve(rc);
+    }
     public override void Typecheck(TypecheckingContext tc) {
       //Contract.Requires(tc != null);
+      TypecheckAttributes(Attributes, tc);
       Expr.Typecheck(tc);
       Contract.Assert(Expr.Type != null);  // follows from Expr.Typecheck postcondition
       if (!Expr.Type.Unify(Type.Bool)) {
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 9f94490b..39f18657 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -338,6 +338,12 @@ namespace Microsoft.Boogie {
 
     public override void Resolve(ResolutionContext rc) {
       //Contract.Requires(rc != null);
+
+      if ((Key == "minimize" || Key == "maximize") && Params.Count != 1)
+      {
+        rc.Error(this, "attributes :minimize and :maximize accept only one argument");
+      }
+
       foreach (object p in Params) {
         if (p is Expr) {
           ((Expr)p).Resolve(rc);
@@ -348,8 +354,15 @@ namespace Microsoft.Boogie {
     public override void Typecheck(TypecheckingContext tc) {
       //Contract.Requires(tc != null);
       foreach (object p in Params) {
-        if (p is Expr) {
-          ((Expr)p).Typecheck(tc);
+        var expr = p as Expr;
+        if (expr != null) {
+          expr.Typecheck(tc);
+        }
+        if ((Key == "minimize" || Key == "maximize")
+            && (expr == null || !(expr.Type.IsInt || expr.Type.IsReal || expr.Type.IsBv)))
+        {
+          tc.Error(this, "attributes :minimize and :maximize accept only one argument of type int, real or bv");
+          break;
         }
       }
     }
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)
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 0a9ba6b3..2a06447e 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -341,6 +341,9 @@ namespace Microsoft.Boogie {
 
     public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool);
 
+    public static readonly VCExprOp MinimizeOp = new VCExprNAryOp(2, Type.Bool);
+    public static readonly VCExprOp MaximizeOp = new VCExprNAryOp(2, Type.Bool);
+
     public VCExprOp BoogieFunctionOp(Function func) {
       Contract.Requires(func != null);
       Contract.Ensures(Contract.Result<VCExprOp>() != null);
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index ae0a1147..5971d6f8 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1539,6 +1539,18 @@ namespace VC {
         PredicateCmd pc = (PredicateCmd)c.Clone();
         Contract.Assert(pc != null);
 
+        QKeyValue current = pc.Attributes;
+        while (current != null)
+        {
+          if (current.Key == "minimize" || current.Key == "maximize") {
+            Contract.Assume(current.Params.Count == 1);
+            var param = current.Params[0] as Expr;
+            Contract.Assume(param != null && (param.Type.IsInt || param.Type.IsReal || param.Type.IsBv));
+            current.ClearParams();
+            current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
+          }
+          current = current.Next;
+        }
         Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
         if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) {
           string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 74b77188..741ed723 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -186,7 +186,7 @@ namespace VC {
             if (naryExpr.Fun is FunctionCall) {
               int id = ac.UniqueId;
               ctxt.Label2absy[id] = ac;
-              return gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);
+              return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N));
             }
           }
         }
@@ -199,13 +199,28 @@ namespace VC {
           namedAssumeVars.Add(v);
           expr = gen.ImpliesSimp(v, expr);
         }
-        return gen.ImpliesSimp(expr, N);
+        return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(expr, N));
       } else {
         Console.WriteLine(cmd.ToString());
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected command
       }
     }
-    
+
+    private static VCExpr MaybeWrapWithOptimization(VCContext ctxt, VCExpressionGenerator gen, QKeyValue attrs, VCExpr expr)
+    {
+      var min = QKeyValue.FindExprAttribute(attrs, "minimize");
+      if (min != null)
+      {
+        expr = gen.Function(VCExpressionGenerator.MinimizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(min), expr);
+      }
+      var max = QKeyValue.FindExprAttribute(attrs, "maximize");
+      if (max != null)
+      {
+        expr = gen.Function(VCExpressionGenerator.MaximizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(max), expr);
+      }
+      return expr;
+    }
+
     public static CommandLineOptions.SubsumptionOption Subsumption(AssertCmd ac) {
       Contract.Requires(ac != null);
       int n = QKeyValue.FindIntAttribute(ac.Attributes, "subsumption", -1);