From a51f4e6cba57b6711e36ef482f4e320c9cf0542f Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Wed, 18 Nov 2015 15:46:24 -0600
Subject: Add experimental support for optimization (requires Z3 build after
 changeset 9cba63c31f6f1466dd4ef442bb840d1ab84539c7).

---
 Test/optimization/Optimization0.bpl | 86 +++++++++++++++++++++++++++++++++++++
 1 file changed, 86 insertions(+)
 create mode 100644 Test/optimization/Optimization0.bpl

(limited to 'Test/optimization/Optimization0.bpl')

diff --git a/Test/optimization/Optimization0.bpl b/Test/optimization/Optimization0.bpl
new file mode 100644
index 00000000..c704c855
--- /dev/null
+++ b/Test/optimization/Optimization0.bpl
@@ -0,0 +1,86 @@
+// RUN: %boogie /doNotUseLabels /printModel:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function may_fail(f: int) : bool;
+
+procedure test0()
+{
+    var x: int;
+
+    havoc x;
+    assume 42 < x;
+    assume {:minimize x} true;
+    assert may_fail(x);
+}
+
+procedure test1()
+{
+    var x: int;
+
+    x := 24;
+    if (*) {
+        x := 42;
+    }
+    assume {:minimize x} true;
+    assert may_fail(x);
+}
+
+procedure test2()
+{
+    var x: int;
+
+    x := 1;
+    while (*) {
+        x := x + 1;
+    }
+    assume {:minimize x} true;
+    assert x < 10;
+}
+
+procedure test3()
+{
+    var x: int;
+
+    havoc x;
+    assume x < 42;
+    assume {:maximize x} true;
+    assert may_fail(x);
+}
+
+procedure test4()
+{
+    var x: int;
+
+    x := 24;
+    if (*) {
+        x := 42;
+    }
+    assume {:maximize x} true;
+    assert may_fail(x);
+}
+
+procedure test5()
+{
+    var x: int;
+
+    x := 1;
+    while (*) {
+        x := x - 1;
+    }
+    assume {:maximize x} true;
+    assert x < 1;
+}
+
+procedure test6()
+{
+    var x: int;
+
+    x := 1;
+    if (*) {
+        x := 2;
+    }
+    assume {:maximize x} true;
+    assert may_fail(x);
+}
+
+// TODO(wuestholz): Make this work without the /doNotUseLabels flag.
-- 
cgit v1.2.3


From c8d15354d033713295a6c55802c6dfe55a95f2b5 Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Wed, 18 Nov 2015 22:21:47 -0600
Subject: Improve experimental support for optimization (requires Z3 changeset
 5948013b1b04d8529bce366c0c7b87e1d88a1827 or later).

---
 Test/optimization/Optimization0.bpl        |  2 +-
 Test/optimization/Optimization0.bpl.expect | 71 +++++-------------------------
 2 files changed, 13 insertions(+), 60 deletions(-)

(limited to 'Test/optimization/Optimization0.bpl')

diff --git a/Test/optimization/Optimization0.bpl b/Test/optimization/Optimization0.bpl
index c704c855..d000fd79 100644
--- a/Test/optimization/Optimization0.bpl
+++ b/Test/optimization/Optimization0.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie /doNotUseLabels /printModel:4 "%s" > "%t"
+// RUN: %boogie /printModel:4 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function may_fail(f: int) : bool;
diff --git a/Test/optimization/Optimization0.bpl.expect b/Test/optimization/Optimization0.bpl.expect
index d2f9b606..f5a51848 100644
--- a/Test/optimization/Optimization0.bpl.expect
+++ b/Test/optimization/Optimization0.bpl.expect
@@ -3,12 +3,6 @@
 %lbl%+260 -> true
 %lbl%+39 -> true
 x@0 -> 43
-ControlFlow -> {
-  0 0 -> 260
-  0 260 -> 39
-  0 39 -> (- 280)
-  else -> 260
-}
 tickleBool -> {
   true -> true
   false -> true
@@ -23,18 +17,11 @@ Optimization0.bpl(13,5): Error BP5001: This assertion might not hold.
 Execution trace:
     Optimization0.bpl(10,5): anon0
 *** MODEL
-%lbl%@328 -> false
-%lbl%+306 -> true
+%lbl%@321 -> false
+%lbl%+299 -> true
 %lbl%+66 -> true
 %lbl%+68 -> true
 x@0@@0 -> 24
-ControlFlow -> {
-  0 0 -> 306
-  0 306 -> 66
-  0 68 -> (- 328)
-  0 66 -> 68
-  else -> 306
-}
 tickleBool -> {
   true -> true
   false -> true
@@ -51,18 +38,11 @@ Execution trace:
     Optimization0.bpl(21,5): anon3_Else
     Optimization0.bpl(24,5): anon2
 *** MODEL
-%lbl%@360 -> false
-%lbl%+342 -> true
+%lbl%@353 -> false
+%lbl%+335 -> true
 %lbl%+95 -> true
 %lbl%+99 -> true
 x@0@@1 -> 10
-ControlFlow -> {
-  0 0 -> 342
-  0 342 -> 95
-  0 95 -> 99
-  0 99 -> (- 360)
-  else -> 342
-}
 tickleBool -> {
   true -> true
   false -> true
@@ -75,16 +55,10 @@ Execution trace:
     Optimization0.bpl(33,5): anon3_LoopHead
     Optimization0.bpl(33,5): anon3_LoopDone
 *** MODEL
-%lbl%@393 -> false
+%lbl%@386 -> false
 %lbl%+122 -> true
-%lbl%+382 -> true
+%lbl%+375 -> true
 x@0@@2 -> 41
-ControlFlow -> {
-  0 0 -> 382
-  0 382 -> 122
-  0 122 -> (- 393)
-  else -> 382
-}
 tickleBool -> {
   true -> true
   false -> true
@@ -99,18 +73,11 @@ Optimization0.bpl(47,5): Error BP5001: This assertion might not hold.
 Execution trace:
     Optimization0.bpl(44,5): anon0
 *** MODEL
-%lbl%@421 -> false
+%lbl%@414 -> false
 %lbl%+147 -> true
 %lbl%+151 -> true
-%lbl%+399 -> true
+%lbl%+392 -> true
 x@0@@3 -> 42
-ControlFlow -> {
-  0 0 -> 399
-  0 399 -> 147
-  0 147 -> 151
-  0 151 -> (- 421)
-  else -> 399
-}
 tickleBool -> {
   true -> true
   false -> true
@@ -127,18 +94,11 @@ Execution trace:
     Optimization0.bpl(56,11): anon3_Then
     Optimization0.bpl(58,5): anon2
 *** MODEL
-%lbl%@453 -> false
+%lbl%@446 -> false
 %lbl%+178 -> true
 %lbl%+182 -> true
-%lbl%+435 -> true
+%lbl%+428 -> true
 x@0@@4 -> 1
-ControlFlow -> {
-  0 0 -> 435
-  0 435 -> 178
-  0 178 -> 182
-  0 182 -> (- 453)
-  else -> 435
-}
 tickleBool -> {
   true -> true
   false -> true
@@ -151,18 +111,11 @@ Execution trace:
     Optimization0.bpl(67,5): anon3_LoopHead
     Optimization0.bpl(67,5): anon3_LoopDone
 *** MODEL
-%lbl%@497 -> false
+%lbl%@490 -> false
 %lbl%+209 -> true
 %lbl%+213 -> true
-%lbl%+475 -> true
+%lbl%+468 -> true
 x@0@@5 -> 2
-ControlFlow -> {
-  0 0 -> 475
-  0 475 -> 209
-  0 209 -> 213
-  0 213 -> (- 497)
-  else -> 475
-}
 tickleBool -> {
   true -> true
   false -> true
-- 
cgit v1.2.3


From 51d0b71fa4fd0795c56f1cddbd85b49625c6c91e Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Thu, 19 Nov 2015 11:09:58 -0600
Subject: Minor changes

---
 Source/VCExpr/VCExprAST.cs          | 4 ++--
 Test/optimization/Optimization0.bpl | 2 --
 Test/optimization/lit.local.cfg     | 2 +-
 3 files changed, 3 insertions(+), 5 deletions(-)

(limited to 'Test/optimization/Optimization0.bpl')

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 2a06447e..2fbb102c 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -341,8 +341,8 @@ 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 static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool);
+    public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool);
 
     public VCExprOp BoogieFunctionOp(Function func) {
       Contract.Requires(func != null);
diff --git a/Test/optimization/Optimization0.bpl b/Test/optimization/Optimization0.bpl
index d000fd79..24424e53 100644
--- a/Test/optimization/Optimization0.bpl
+++ b/Test/optimization/Optimization0.bpl
@@ -82,5 +82,3 @@ procedure test6()
     assume {:maximize x} true;
     assert may_fail(x);
 }
-
-// TODO(wuestholz): Make this work without the /doNotUseLabels flag.
diff --git a/Test/optimization/lit.local.cfg b/Test/optimization/lit.local.cfg
index 158a1e4d..35c7e558 100644
--- a/Test/optimization/lit.local.cfg
+++ b/Test/optimization/lit.local.cfg
@@ -1,3 +1,3 @@
 # Do not run tests in this directory and below
 config.unsupported = True
-# TODO(wuestholz): Enable these tests once we can rely on Z3 4.4.2 or higher.
+# TODO(wuestholz): Enable these tests once we can rely on a version of Z3 that includes changeset 5948013b1b04d8529bce366c0c7b87e1d88a1827.
-- 
cgit v1.2.3