From 7dfa02c3da9f68b10b20e6afcd81767d3c6ebf02 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Thu, 19 Nov 2015 15:39:01 -0600
Subject: Add code that uses Z3's optimization features (currently disabled by
 default).

---
 Source/Dafny/Translator.cs | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'Source/Dafny')

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3417d4c3..8e8c3c19 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -94,6 +94,8 @@ namespace Microsoft.Dafny {
 
   public class Translator {
     ErrorReporter reporter;
+    // TODO(wuestholz): Enable this once Dafny's recommended Z3 version includes changeset 0592e765744497a089c42021990740f303901e67.
+    public bool UseOptimizationInZ3 { get; set; }
 
     [NotDelayed]
     public Translator(ErrorReporter reporter) {
@@ -2756,6 +2758,18 @@ namespace Microsoft.Dafny {
       List<Variable> localVariables = new List<Variable>();
       GenerateImplPrelude(m, wellformednessProc, inParams, outParams, builder, localVariables);
 
+      if (UseOptimizationInZ3 && m.Ins != null)
+      {
+        // We ask Z3 to minimize all parameters of type 'nat'.
+        foreach (var f in m.Ins)
+        {
+          if (f.Type is NatType)
+          {
+            builder.Add(optimizeExpr(true, new IdentifierExpr(f), f.Tok, etran));
+          }
+        }
+      }
+
       Bpl.StmtList stmts;
       if (!wellformednessProc) {
         var inductionVars = ApplyInduction(m.Ins, m.Attributes);
@@ -2920,6 +2934,17 @@ namespace Microsoft.Dafny {
       Reset();
     }
 
+    internal static AssumeCmd optimizeExpr(bool minimize, Expression expr, IToken tok, ExpressionTranslator etran)
+    {
+      Contract.Requires(expr != null);
+      Contract.Requires(expr.Type.IsIntegerType || expr.Type.IsRealType);
+      Contract.Requires(tok != null && etran != null);
+
+      var assumeCmd = new AssumeCmd(tok, Expr.True);
+      assumeCmd.Attributes = new QKeyValue(expr.tok, (minimize ? "minimize" : "maximize"), new List<object> { etran.TrExpr(expr) }, null);
+      return assumeCmd;
+    }
+
     private void AddFunctionOverrideCheckImpl(Function f)
     {
         Contract.Requires(f != null);
-- 
cgit v1.2.3