1 files changed, 35 insertions, 4 deletions
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index b4ee4c09..cad5914b 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -87,7 +87,7 @@ namespace VC {
     /// <summary>
     /// Computes the wlp for an assert or assume command "cmd".
     /// </summary>
-    public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) {
+    internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) {
       Contract.Requires(cmd != null);
       Contract.Requires(N != null);
       Contract.Requires(ctxt != null);
@@ -186,17 +186,48 @@ 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));
             }
           }
         }
-        return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
+        var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
+        
+        var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id");
+        if (aid != null)
+        {
+          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");
+        var softWeight = QKeyValue.FindIntAttribute(ac.Attributes, "soft", 0);
+        if ((soft || 0 < softWeight) && aid != null)
+        {
+          var v = gen.Variable("soft$$" + aid, Microsoft.Boogie.Type.Bool);
+          expr = gen.Function(new VCExprSoftOp(Math.Max(softWeight, 1)), v, gen.ImpliesSimp(v, expr));
+        }
+        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);