summaryrefslogtreecommitdiff
path: root/tex/thesis/implementation
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis/implementation')
-rw-r--r--tex/thesis/implementation/experiments/counter.c4
-rw-r--r--tex/thesis/implementation/experiments/example-output90
-rw-r--r--tex/thesis/implementation/experiments/example.c4
-rw-r--r--tex/thesis/implementation/experiments/fib-output302
-rw-r--r--tex/thesis/implementation/experiments/nested-output260
-rw-r--r--tex/thesis/implementation/implementation.tex355
6 files changed, 474 insertions, 541 deletions
diff --git a/tex/thesis/implementation/experiments/counter.c b/tex/thesis/implementation/experiments/counter.c
index ae935e6..ebd6ff0 100644
--- a/tex/thesis/implementation/experiments/counter.c
+++ b/tex/thesis/implementation/experiments/counter.c
@@ -1,8 +1,10 @@
int counter() {
+ /* A */
int i = 0;
- while (i < 100) {
+ while (/* B */i < 100) {
i = i + 1;
}
+ /* C */
return i;
}
diff --git a/tex/thesis/implementation/experiments/example-output b/tex/thesis/implementation/experiments/example-output
index 5194e12..38ce67a 100644
--- a/tex/thesis/implementation/experiments/example-output
+++ b/tex/thesis/implementation/experiments/example-output
@@ -39,8 +39,8 @@
Succs (1): B3
[B5]
- 1: 1
- 2: int x1 = 1;
+ 1: 0
+ 2: int x1 = 0;
3: 1
4: int x2 = 1;
Preds (1): B6
@@ -52,104 +52,56 @@
0-6-pre = max(-inf, inf)
1-6-pre = max(-inf, inf)
2-6-pre = max(-inf, inf)
-3-6-pre = max(-inf, inf)
-4-6-pre = max(-inf, inf)
-5-6-pre = max(-inf, inf)
0-5-pre = max(-inf, 0-6-pre)
1-5-pre = max(-inf, 1-6-pre)
2-5-pre = max(-inf, 2-6-pre)
-3-5-pre = max(-inf, 3-6-pre)
-4-5-pre = max(-inf, 4-6-pre)
-5-5-pre = max(-inf, 5-6-pre)
-0-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)))
-1-5-0 = max(-inf, add(-1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)))
-2-5-0 = max(-inf, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))
-3-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)))
-4-5-0 = max(-inf, add(-1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)))
-5-5-0 = max(-inf, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))
+0-5-0 = max(-inf, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre))
+1-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre)))
+2-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre)))
0-2-pre = max(-inf, 0-5-0, 0-3-pre)
1-2-pre = max(-inf, 1-5-0, 1-3-pre)
2-2-pre = max(-inf, 2-5-0, 2-3-pre)
-3-2-pre = max(-inf, 3-5-0, 3-3-pre)
-4-2-pre = max(-inf, 4-5-0, 4-3-pre)
-5-2-pre = max(-inf, 5-5-0, 5-3-pre)
0-4-pre = max(-inf, min(8, 0-2-pre))
1-4-pre = max(-inf, 1-2-pre)
2-4-pre = max(-inf, 2-2-pre)
-3-4-pre = max(-inf, 3-2-pre)
-4-4-pre = max(-inf, 4-2-pre)
-5-4-pre = max(-inf, 5-2-pre)
0-1-pre = max(-inf, 0-2-pre)
-1-1-pre = max(-inf, min(-9, 1-2-pre))
+1-1-pre = max(-inf, 1-2-pre)
2-1-pre = max(-inf, 2-2-pre)
-3-1-pre = max(-inf, 3-2-pre)
-4-1-pre = max(-inf, 4-2-pre)
-5-1-pre = max(-inf, 5-2-pre)
-0-4-0 = max(-inf, add(2, MCF<[-1,1,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)))
-1-4-0 = max(-inf, add(-2, MCF<[1,-1,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)))
-2-4-0 = max(-inf, MCF<[0,1,-1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))
-3-4-0 = max(-inf, add(2, MCF<[-1,0,1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)))
-4-4-0 = max(-inf, add(-2, MCF<[1,0,-1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)))
-5-4-0 = max(-inf, MCF<[0,-1,1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))
+0-4-0 = max(-inf, add(2, MCF<[-1,1,0],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre)))
+1-4-0 = max(-inf, add(2, MCF<[-1,0,1],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre)))
+2-4-0 = max(-inf, MCF<[0,-1,1],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre))
0-3-pre = max(-inf, 0-4-0)
1-3-pre = max(-inf, 1-4-0)
2-3-pre = max(-inf, 2-4-0)
-3-3-pre = max(-inf, 3-4-0)
-4-3-pre = max(-inf, 4-4-0)
-5-3-pre = max(-inf, 5-4-0)
0-0-pre = max(-inf, 0-1-pre)
1-0-pre = max(-inf, 1-1-pre)
2-0-pre = max(-inf, 2-1-pre)
-3-0-pre = max(-inf, 3-1-pre)
-4-0-pre = max(-inf, 4-1-pre)
-5-0-pre = max(-inf, 5-1-pre)
Block 0:
x1 <= 10
- -x1 <= -9
- x1 - x2 <= 0
- x2 <= 10
- -x2 <= -1
- x2 - x1 <= 0
+ x2 <= 11
+ x2-x1 <= 1
Block 1:
x1 <= 10
- -x1 <= -9
- x1 - x2 <= 0
- x2 <= 10
- -x2 <= -1
- x2 - x1 <= 0
+ x2 <= 11
+ x2-x1 <= 1
Block 2:
x1 <= 10
- -x1 <= -1
- x1 - x2 <= 0
- x2 <= 10
- -x2 <= -1
- x2 - x1 <= 0
+ x2 <= 11
+ x2-x1 <= 1
Block 3:
x1 <= 10
- -x1 <= -3
- x1 - x2 <= 0
- x2 <= 10
- -x2 <= -3
- x2 - x1 <= 0
+ x2 <= 11
+ x2-x1 <= 1
Block 4:
x1 <= 8
- -x1 <= -1
- x1 - x2 <= 0
- x2 <= 10
- -x2 <= -1
- x2 - x1 <= 0
+ x2 <= 11
+ x2-x1 <= 1
Block 5:
x1 <= inf
- -x1 <= inf
- x1 - x2 <= inf
x2 <= inf
- -x2 <= inf
- x2 - x1 <= inf
+ x2-x1 <= inf
Block 6:
x1 <= inf
- -x1 <= inf
- x1 - x2 <= inf
x2 <= inf
- -x2 <= inf
- x2 - x1 <= inf
+ x2-x1 <= inf
diff --git a/tex/thesis/implementation/experiments/example.c b/tex/thesis/implementation/experiments/example.c
index 39b65f2..0010804 100644
--- a/tex/thesis/implementation/experiments/example.c
+++ b/tex/thesis/implementation/experiments/example.c
@@ -1,11 +1,13 @@
int example() {
+ /* A */
int x1 = 1;
int x2 = 1;
- while (x1 <= 8) {
+ while (/* B */ x1 <= 8) {
x1 = x1 + 2;
x2 = x2 + 2;
}
+ /* C */
return x2;
}
diff --git a/tex/thesis/implementation/experiments/fib-output b/tex/thesis/implementation/experiments/fib-output
index 900f636..ec86733 100644
--- a/tex/thesis/implementation/experiments/fib-output
+++ b/tex/thesis/implementation/experiments/fib-output
@@ -65,345 +65,107 @@
3-6-pre = max(-inf, inf)
4-6-pre = max(-inf, inf)
5-6-pre = max(-inf, inf)
-6-6-pre = max(-inf, inf)
-7-6-pre = max(-inf, inf)
-8-6-pre = max(-inf, inf)
-9-6-pre = max(-inf, inf)
-10-6-pre = max(-inf, inf)
-11-6-pre = max(-inf, inf)
-12-6-pre = max(-inf, inf)
-13-6-pre = max(-inf, inf)
-14-6-pre = max(-inf, inf)
-15-6-pre = max(-inf, inf)
-16-6-pre = max(-inf, inf)
-17-6-pre = max(-inf, inf)
-18-6-pre = max(-inf, inf)
-19-6-pre = max(-inf, inf)
0-5-pre = max(-inf, 0-6-pre)
1-5-pre = max(-inf, 1-6-pre)
2-5-pre = max(-inf, 2-6-pre)
3-5-pre = max(-inf, 3-6-pre)
4-5-pre = max(-inf, 4-6-pre)
5-5-pre = max(-inf, 5-6-pre)
-6-5-pre = max(-inf, 6-6-pre)
-7-5-pre = max(-inf, 7-6-pre)
-8-5-pre = max(-inf, 8-6-pre)
-9-5-pre = max(-inf, 9-6-pre)
-10-5-pre = max(-inf, 10-6-pre)
-11-5-pre = max(-inf, 11-6-pre)
-12-5-pre = max(-inf, 12-6-pre)
-13-5-pre = max(-inf, 13-6-pre)
-14-5-pre = max(-inf, 14-6-pre)
-15-5-pre = max(-inf, 15-6-pre)
-16-5-pre = max(-inf, 16-6-pre)
-17-5-pre = max(-inf, 17-6-pre)
-18-5-pre = max(-inf, 18-6-pre)
-19-5-pre = max(-inf, 19-6-pre)
-0-5-0 = max(-inf, add(1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)))
-1-5-0 = max(-inf, add(-1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)))
-2-5-0 = max(-inf, add(1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)))
-3-5-0 = max(-inf, add(1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)))
-4-5-0 = max(-inf, add(1, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)))
-5-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))
-6-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))
-7-5-0 = max(-inf, add(-1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)))
-8-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))
-9-5-0 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))
-10-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))
-11-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))
-12-5-0 = max(-inf, add(-1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)))
-13-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))
-14-5-0 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))
-15-5-0 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))
-16-5-0 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))
-17-5-0 = max(-inf, add(-1, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)))
-18-5-0 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))
-19-5-0 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))
+0-5-0 = max(-inf, add(1, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)))
+1-5-0 = max(-inf, add(-1, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)))
+2-5-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))
+3-5-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))
+4-5-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))
+5-5-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))
0-2-pre = max(-inf, 0-5-0, 0-3-pre)
1-2-pre = max(-inf, 1-5-0, 1-3-pre)
2-2-pre = max(-inf, 2-5-0, 2-3-pre)
3-2-pre = max(-inf, 3-5-0, 3-3-pre)
4-2-pre = max(-inf, 4-5-0, 4-3-pre)
5-2-pre = max(-inf, 5-5-0, 5-3-pre)
-6-2-pre = max(-inf, 6-5-0, 6-3-pre)
-7-2-pre = max(-inf, 7-5-0, 7-3-pre)
-8-2-pre = max(-inf, 8-5-0, 8-3-pre)
-9-2-pre = max(-inf, 9-5-0, 9-3-pre)
-10-2-pre = max(-inf, 10-5-0, 10-3-pre)
-11-2-pre = max(-inf, 11-5-0, 11-3-pre)
-12-2-pre = max(-inf, 12-5-0, 12-3-pre)
-13-2-pre = max(-inf, 13-5-0, 13-3-pre)
-14-2-pre = max(-inf, 14-5-0, 14-3-pre)
-15-2-pre = max(-inf, 15-5-0, 15-3-pre)
-16-2-pre = max(-inf, 16-5-0, 16-3-pre)
-17-2-pre = max(-inf, 17-5-0, 17-3-pre)
-18-2-pre = max(-inf, 18-5-0, 18-3-pre)
-19-2-pre = max(-inf, 19-5-0, 19-3-pre)
0-4-pre = max(-inf, 0-2-pre)
1-4-pre = max(-inf, 1-2-pre)
2-4-pre = max(-inf, 2-2-pre)
3-4-pre = max(-inf, 3-2-pre)
-4-4-pre = max(-inf, 4-2-pre)
+4-4-pre = max(-inf, min(19, 4-2-pre))
5-4-pre = max(-inf, 5-2-pre)
-6-4-pre = max(-inf, 6-2-pre)
-7-4-pre = max(-inf, 7-2-pre)
-8-4-pre = max(-inf, 8-2-pre)
-9-4-pre = max(-inf, 9-2-pre)
-10-4-pre = max(-inf, min(19, 10-2-pre))
-11-4-pre = max(-inf, 11-2-pre)
-12-4-pre = max(-inf, 12-2-pre)
-13-4-pre = max(-inf, 13-2-pre)
-14-4-pre = max(-inf, 14-2-pre)
-15-4-pre = max(-inf, 15-2-pre)
-16-4-pre = max(-inf, 16-2-pre)
-17-4-pre = max(-inf, 17-2-pre)
-18-4-pre = max(-inf, 18-2-pre)
-19-4-pre = max(-inf, 19-2-pre)
0-1-pre = max(-inf, 0-2-pre)
1-1-pre = max(-inf, 1-2-pre)
2-1-pre = max(-inf, 2-2-pre)
3-1-pre = max(-inf, 3-2-pre)
4-1-pre = max(-inf, 4-2-pre)
-5-1-pre = max(-inf, 5-2-pre)
-6-1-pre = max(-inf, 6-2-pre)
-7-1-pre = max(-inf, 7-2-pre)
-8-1-pre = max(-inf, 8-2-pre)
-9-1-pre = max(-inf, 9-2-pre)
-10-1-pre = max(-inf, 10-2-pre)
-11-1-pre = max(-inf, min(-20, 11-2-pre))
-12-1-pre = max(-inf, 12-2-pre)
-13-1-pre = max(-inf, 13-2-pre)
-14-1-pre = max(-inf, 14-2-pre)
-15-1-pre = max(-inf, 15-2-pre)
-16-1-pre = max(-inf, 16-2-pre)
-17-1-pre = max(-inf, 17-2-pre)
-18-1-pre = max(-inf, 18-2-pre)
-19-1-pre = max(-inf, 19-2-pre)
-0-4-0 = max(-inf, MCF<[-2,1,1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-1-4-0 = max(-inf, MCF<[2,-1,-1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-2-4-0 = max(-inf, MCF<[-1,1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-3-4-0 = max(-inf, MCF<[-1,1,1,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-4-4-0 = max(-inf, MCF<[-1,0,1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-5-4-0 = max(-inf, MCF<[-1,0,1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-6-4-0 = max(-inf, MCF<[1,0,-1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-7-4-0 = max(-inf, MCF<[1,-1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-8-4-0 = max(-inf, MCF<[0,0,1,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-9-4-0 = max(-inf, MCF<[0,-1,1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-10-4-0 = max(-inf, MCF<[-1,0,0,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-11-4-0 = max(-inf, MCF<[1,0,0,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-12-4-0 = max(-inf, MCF<[1,-1,-1,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-13-4-0 = max(-inf, MCF<[0,0,-1,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-14-4-0 = max(-inf, MCF<[0,-1,0,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-15-4-0 = max(-inf, MCF<[-1,1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-16-4-0 = max(-inf, MCF<[1,-1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-17-4-0 = max(-inf, MCF<[1,0,-1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-18-4-0 = max(-inf, MCF<[0,1,-1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-19-4-0 = max(-inf, MCF<[0,1,0,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre))
-0-4-1 = max(-inf, MCF<[-1,1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))
-1-4-1 = max(-inf, MCF<[1,-1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))
-2-4-1 = max(-inf, MCF<[0,1,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))
-3-4-1 = max(-inf, add(-1, MCF<[0,1,0,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)))
-4-4-1 = max(-inf, MCF<[0,1,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))
-5-4-1 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))
-6-4-1 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))
-7-4-1 = max(-inf, MCF<[0,-1,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))
-8-4-1 = max(-inf, add(-1, MCF<[0,0,0,-1,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)))
-9-4-1 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))
-10-4-1 = max(-inf, add(1, MCF<[-1,0,0,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)))
-11-4-1 = max(-inf, add(-1, MCF<[1,0,0,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)))
-12-4-1 = max(-inf, add(1, MCF<[0,-1,0,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)))
-13-4-1 = max(-inf, add(1, MCF<[0,0,0,1,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)))
-14-4-1 = max(-inf, add(1, MCF<[0,0,0,1,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)))
-15-4-1 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))
-16-4-1 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))
-17-4-1 = max(-inf, MCF<[0,-1,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))
-18-4-1 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))
-19-4-1 = max(-inf, add(-1, MCF<[0,0,0,-1,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)))
+5-1-pre = max(-inf, min(-20, 5-2-pre))
+0-4-0 = max(-inf, MCF<[-2,1,1,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))
+1-4-0 = max(-inf, MCF<[2,-1,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))
+2-4-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))
+3-4-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))
+4-4-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))
+5-4-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))
+0-4-1 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0))
+1-4-1 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0))
+2-4-1 = max(-inf, MCF<[-1,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0))
+3-4-1 = max(-inf, MCF<[1,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0))
+4-4-1 = max(-inf, add(1, MCF<[-1,0,0,1],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0)))
+5-4-1 = max(-inf, add(-1, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0)))
0-3-pre = max(-inf, 0-4-1)
1-3-pre = max(-inf, 1-4-1)
2-3-pre = max(-inf, 2-4-1)
3-3-pre = max(-inf, 3-4-1)
4-3-pre = max(-inf, 4-4-1)
5-3-pre = max(-inf, 5-4-1)
-6-3-pre = max(-inf, 6-4-1)
-7-3-pre = max(-inf, 7-4-1)
-8-3-pre = max(-inf, 8-4-1)
-9-3-pre = max(-inf, 9-4-1)
-10-3-pre = max(-inf, 10-4-1)
-11-3-pre = max(-inf, 11-4-1)
-12-3-pre = max(-inf, 12-4-1)
-13-3-pre = max(-inf, 13-4-1)
-14-3-pre = max(-inf, 14-4-1)
-15-3-pre = max(-inf, 15-4-1)
-16-3-pre = max(-inf, 16-4-1)
-17-3-pre = max(-inf, 17-4-1)
-18-3-pre = max(-inf, 18-4-1)
-19-3-pre = max(-inf, 19-4-1)
0-0-pre = max(-inf, 0-1-pre)
1-0-pre = max(-inf, 1-1-pre)
2-0-pre = max(-inf, 2-1-pre)
3-0-pre = max(-inf, 3-1-pre)
4-0-pre = max(-inf, 4-1-pre)
5-0-pre = max(-inf, 5-1-pre)
-6-0-pre = max(-inf, 6-1-pre)
-7-0-pre = max(-inf, 7-1-pre)
-8-0-pre = max(-inf, 8-1-pre)
-9-0-pre = max(-inf, 9-1-pre)
-10-0-pre = max(-inf, 10-1-pre)
-11-0-pre = max(-inf, 11-1-pre)
-12-0-pre = max(-inf, 12-1-pre)
-13-0-pre = max(-inf, 13-1-pre)
-14-0-pre = max(-inf, 14-1-pre)
-15-0-pre = max(-inf, 15-1-pre)
-16-0-pre = max(-inf, 16-1-pre)
-17-0-pre = max(-inf, 17-1-pre)
-18-0-pre = max(-inf, 18-1-pre)
-19-0-pre = max(-inf, 19-1-pre)
Block 0:
fib <= 1
-fib <= -1
- fib - fib_last <= 1
- fib - i <= 1
- fib - temp_fib <= inf
- fib_last <= 1
- -fib_last <= 0
- fib_last - fib <= 0
- fib_last - i <= 0
- fib_last - temp_fib <= inf
+ fib_last <= inf
+ -fib_last <= inf
i <= 20
-i <= -20
- i - fib <= 19
- i - fib_last <= 19
- i - temp_fib <= inf
- temp_fib <= inf
- -temp_fib <= inf
- temp_fib - fib <= inf
- temp_fib - fib_last <= inf
- temp_fib - i <= inf
Block 1:
fib <= 1
-fib <= -1
- fib - fib_last <= 1
- fib - i <= 1
- fib - temp_fib <= inf
- fib_last <= 1
- -fib_last <= 0
- fib_last - fib <= 0
- fib_last - i <= 0
- fib_last - temp_fib <= inf
+ fib_last <= inf
+ -fib_last <= inf
i <= 20
-i <= -20
- i - fib <= 19
- i - fib_last <= 19
- i - temp_fib <= inf
- temp_fib <= inf
- -temp_fib <= inf
- temp_fib - fib <= inf
- temp_fib - fib_last <= inf
- temp_fib - i <= inf
Block 2:
- fib <= 39
- -fib <= -1
- fib - fib_last <= 19
- fib - i <= 37
- fib - temp_fib <= inf
- fib_last <= 38
- -fib_last <= 0
- fib_last - fib <= 0
- fib_last - i <= inf
- fib_last - temp_fib <= inf
+ fib <= inf
+ -fib <= inf
+ fib_last <= inf
+ -fib_last <= inf
i <= 20
-i <= 0
- i - fib <= 19
- i - fib_last <= 19
- i - temp_fib <= inf
- temp_fib <= inf
- -temp_fib <= inf
- temp_fib - fib <= inf
- temp_fib - fib_last <= inf
- temp_fib - i <= inf
Block 3:
fib <= inf
- -fib <= -1
- fib - fib_last <= inf
- fib - i <= inf
- fib - temp_fib <= inf
+ -fib <= inf
fib_last <= inf
- -fib_last <= -1
- fib_last - fib <= 0
- fib_last - i <= inf
- fib_last - temp_fib <= 0
+ -fib_last <= inf
i <= 20
-i <= -1
- i - fib <= 19
- i - fib_last <= 19
- i - temp_fib <= 19
- temp_fib <= inf
- -temp_fib <= -1
- temp_fib - fib <= 0
- temp_fib - fib_last <= 0
- temp_fib - i <= inf
Block 4:
fib <= inf
- -fib <= -1
- fib - fib_last <= inf
- fib - i <= inf
- fib - temp_fib <= inf
+ -fib <= inf
fib_last <= inf
- -fib_last <= 0
- fib_last - fib <= 0
- fib_last - i <= inf
- fib_last - temp_fib <= inf
+ -fib_last <= inf
i <= 19
-i <= 0
- i - fib <= 19
- i - fib_last <= 19
- i - temp_fib <= inf
- temp_fib <= inf
- -temp_fib <= inf
- temp_fib - fib <= inf
- temp_fib - fib_last <= inf
- temp_fib - i <= inf
Block 5:
fib <= inf
-fib <= inf
- fib - fib_last <= inf
- fib - i <= inf
- fib - temp_fib <= inf
fib_last <= inf
-fib_last <= inf
- fib_last - fib <= inf
- fib_last - i <= inf
- fib_last - temp_fib <= inf
i <= inf
-i <= inf
- i - fib <= inf
- i - fib_last <= inf
- i - temp_fib <= inf
- temp_fib <= inf
- -temp_fib <= inf
- temp_fib - fib <= inf
- temp_fib - fib_last <= inf
- temp_fib - i <= inf
Block 6:
fib <= inf
-fib <= inf
- fib - fib_last <= inf
- fib - i <= inf
- fib - temp_fib <= inf
fib_last <= inf
-fib_last <= inf
- fib_last - fib <= inf
- fib_last - i <= inf
- fib_last - temp_fib <= inf
i <= inf
-i <= inf
- i - fib <= inf
- i - fib_last <= inf
- i - temp_fib <= inf
- temp_fib <= inf
- -temp_fib <= inf
- temp_fib - fib <= inf
- temp_fib - fib_last <= inf
- temp_fib - i <= inf
diff --git a/tex/thesis/implementation/experiments/nested-output b/tex/thesis/implementation/experiments/nested-output
index d6b55be..15e95c2 100644
--- a/tex/thesis/implementation/experiments/nested-output
+++ b/tex/thesis/implementation/experiments/nested-output
@@ -82,10 +82,6 @@
5-9-pre = max(-inf, inf)
6-9-pre = max(-inf, inf)
7-9-pre = max(-inf, inf)
-8-9-pre = max(-inf, inf)
-9-9-pre = max(-inf, inf)
-10-9-pre = max(-inf, inf)
-11-9-pre = max(-inf, inf)
0-8-pre = max(-inf, 0-9-pre)
1-8-pre = max(-inf, 1-9-pre)
2-8-pre = max(-inf, 2-9-pre)
@@ -94,22 +90,14 @@
5-8-pre = max(-inf, 5-9-pre)
6-8-pre = max(-inf, 6-9-pre)
7-8-pre = max(-inf, 7-9-pre)
-8-8-pre = max(-inf, 8-9-pre)
-9-8-pre = max(-inf, 9-9-pre)
-10-8-pre = max(-inf, 10-9-pre)
-11-8-pre = max(-inf, 11-9-pre)
-0-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-1-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-2-8-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-3-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-4-8-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-5-8-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-6-8-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-7-8-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-8-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-9-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-10-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
-11-8-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre, 8-8-pre, 9-8-pre, 10-8-pre, 11-8-pre))
+0-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre))
+1-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre))
+2-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre))
+3-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre))
+4-8-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre))
+5-8-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre))
+6-8-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre))
+7-8-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-8-pre, 1-8-pre, 2-8-pre, 3-8-pre, 4-8-pre, 5-8-pre, 6-8-pre, 7-8-pre))
0-2-pre = max(-inf, 0-8-0, 0-3-0)
1-2-pre = max(-inf, 1-8-0, 1-3-0)
2-2-pre = max(-inf, 2-8-0, 2-3-0)
@@ -118,46 +106,30 @@
5-2-pre = max(-inf, 5-8-0, 5-3-0)
6-2-pre = max(-inf, 6-8-0, 6-3-0)
7-2-pre = max(-inf, 7-8-0, 7-3-0)
-8-2-pre = max(-inf, 8-8-0, 8-3-0)
-9-2-pre = max(-inf, 9-8-0, 9-3-0)
-10-2-pre = max(-inf, 10-8-0, 10-3-0)
-11-2-pre = max(-inf, 11-8-0, 11-3-0)
-0-7-pre = max(-inf, min(9, 0-2-pre))
+0-7-pre = max(-inf, 0-2-pre)
1-7-pre = max(-inf, 1-2-pre)
-2-7-pre = max(-inf, 2-2-pre)
+2-7-pre = max(-inf, min(9, 2-2-pre))
3-7-pre = max(-inf, 3-2-pre)
4-7-pre = max(-inf, 4-2-pre)
5-7-pre = max(-inf, 5-2-pre)
6-7-pre = max(-inf, 6-2-pre)
7-7-pre = max(-inf, 7-2-pre)
-8-7-pre = max(-inf, 8-2-pre)
-9-7-pre = max(-inf, 9-2-pre)
-10-7-pre = max(-inf, 10-2-pre)
-11-7-pre = max(-inf, 11-2-pre)
0-1-pre = max(-inf, 0-2-pre)
-1-1-pre = max(-inf, min(-10, 1-2-pre))
+1-1-pre = max(-inf, 1-2-pre)
2-1-pre = max(-inf, 2-2-pre)
-3-1-pre = max(-inf, 3-2-pre)
+3-1-pre = max(-inf, min(-10, 3-2-pre))
4-1-pre = max(-inf, 4-2-pre)
5-1-pre = max(-inf, 5-2-pre)
6-1-pre = max(-inf, 6-2-pre)
7-1-pre = max(-inf, 7-2-pre)
-8-1-pre = max(-inf, 8-2-pre)
-9-1-pre = max(-inf, 9-2-pre)
-10-1-pre = max(-inf, 10-2-pre)
-11-1-pre = max(-inf, 11-2-pre)
-0-7-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-1-7-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-2-7-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-3-7-0 = max(-inf, MCF<[0,1,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-4-7-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-5-7-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-6-7-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-7-7-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-8-7-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-9-7-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-10-7-0 = max(-inf, MCF<[0,-1,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
-11-7-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre, 8-7-pre, 9-7-pre, 10-7-pre, 11-7-pre))
+0-7-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre))
+1-7-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre))
+2-7-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre))
+3-7-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre))
+4-7-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre))
+5-7-0 = max(-inf, MCF<[0,0,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre))
+6-7-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre))
+7-7-0 = max(-inf, MCF<[0,1,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-7-pre, 1-7-pre, 2-7-pre, 3-7-pre, 4-7-pre, 5-7-pre, 6-7-pre, 7-7-pre))
0-4-pre = max(-inf, 0-7-0, 0-5-0)
1-4-pre = max(-inf, 1-7-0, 1-5-0)
2-4-pre = max(-inf, 2-7-0, 2-5-0)
@@ -166,10 +138,6 @@
5-4-pre = max(-inf, 5-7-0, 5-5-0)
6-4-pre = max(-inf, 6-7-0, 6-5-0)
7-4-pre = max(-inf, 7-7-0, 7-5-0)
-8-4-pre = max(-inf, 8-7-0, 8-5-0)
-9-4-pre = max(-inf, 9-7-0, 9-5-0)
-10-4-pre = max(-inf, 10-7-0, 10-5-0)
-11-4-pre = max(-inf, 11-7-0, 11-5-0)
0-0-pre = max(-inf, 0-1-pre)
1-0-pre = max(-inf, 1-1-pre)
2-0-pre = max(-inf, 2-1-pre)
@@ -178,10 +146,6 @@
5-0-pre = max(-inf, 5-1-pre)
6-0-pre = max(-inf, 6-1-pre)
7-0-pre = max(-inf, 7-1-pre)
-8-0-pre = max(-inf, 8-1-pre)
-9-0-pre = max(-inf, 9-1-pre)
-10-0-pre = max(-inf, 10-1-pre)
-11-0-pre = max(-inf, 11-1-pre)
0-6-pre = max(-inf, 0-4-pre)
1-6-pre = max(-inf, 1-4-pre)
2-6-pre = max(-inf, 2-4-pre)
@@ -190,10 +154,6 @@
5-6-pre = max(-inf, 5-4-pre)
6-6-pre = max(-inf, 6-4-pre)
7-6-pre = max(-inf, 7-4-pre)
-8-6-pre = max(-inf, 8-4-pre)
-9-6-pre = max(-inf, 9-4-pre)
-10-6-pre = max(-inf, 10-4-pre)
-11-6-pre = max(-inf, 11-4-pre)
0-3-pre = max(-inf, 0-4-pre)
1-3-pre = max(-inf, 1-4-pre)
2-3-pre = max(-inf, 2-4-pre)
@@ -202,22 +162,14 @@
5-3-pre = max(-inf, min(-10, 5-4-pre))
6-3-pre = max(-inf, 6-4-pre)
7-3-pre = max(-inf, 7-4-pre)
-8-3-pre = max(-inf, 8-4-pre)
-9-3-pre = max(-inf, 9-4-pre)
-10-3-pre = max(-inf, 10-4-pre)
-11-3-pre = max(-inf, 11-4-pre)
-0-6-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre))
-1-6-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre))
-2-6-0 = max(-inf, MCF<[0,1,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre))
-3-6-0 = max(-inf, add(-1, MCF<[0,1,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre)))
-4-6-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre))
-5-6-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre))
-6-6-0 = max(-inf, MCF<[0,-1,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre))
-7-6-0 = max(-inf, add(-1, MCF<[0,0,1,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre)))
-8-6-0 = max(-inf, add(1, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre)))
-9-6-0 = max(-inf, add(-1, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre)))
-10-6-0 = max(-inf, add(1, MCF<[0,-1,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre)))
-11-6-0 = max(-inf, add(1, MCF<[0,0,-1,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre, 8-6-pre, 9-6-pre, 10-6-pre, 11-6-pre)))
+0-6-0 = max(-inf, add(1, MCF<[-1,1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre)))
+1-6-0 = max(-inf, add(-1, MCF<[1,-1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre)))
+2-6-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre))
+3-6-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre))
+4-6-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre))
+5-6-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre))
+6-6-0 = max(-inf, add(1, MCF<[0,1,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre)))
+7-6-0 = max(-inf, add(1, MCF<[0,1,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-6-pre, 1-6-pre, 2-6-pre, 3-6-pre, 4-6-pre, 5-6-pre, 6-6-pre, 7-6-pre)))
0-5-pre = max(-inf, 0-6-0)
1-5-pre = max(-inf, 1-6-0)
2-5-pre = max(-inf, 2-6-0)
@@ -226,162 +178,110 @@
5-5-pre = max(-inf, 5-6-0)
6-5-pre = max(-inf, 6-6-0)
7-5-pre = max(-inf, 7-6-0)
-8-5-pre = max(-inf, 8-6-0)
-9-5-pre = max(-inf, 9-6-0)
-10-5-pre = max(-inf, 10-6-0)
-11-5-pre = max(-inf, 11-6-0)
-0-3-0 = max(-inf, add(1, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre)))
-1-3-0 = max(-inf, add(-1, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre)))
-2-3-0 = max(-inf, add(1, MCF<[0,1,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre)))
-3-3-0 = max(-inf, add(1, MCF<[0,1,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre)))
-4-3-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre))
-5-3-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre))
-6-3-0 = max(-inf, add(-1, MCF<[0,-1,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre)))
-7-3-0 = max(-inf, MCF<[0,0,1,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre))
-8-3-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre))
-9-3-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre))
-10-3-0 = max(-inf, add(-1, MCF<[0,-1,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre)))
-11-3-0 = max(-inf, MCF<[0,0,-1,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre, 8-3-pre, 9-3-pre, 10-3-pre, 11-3-pre))
-0-5-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre))
-1-5-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre))
-2-5-0 = max(-inf, add(-1, MCF<[0,1,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre)))
-3-5-0 = max(-inf, MCF<[0,1,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre))
-4-5-0 = max(-inf, add(1, MCF<[-1,0,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre)))
-5-5-0 = max(-inf, add(-1, MCF<[1,0,-1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre)))
-6-5-0 = max(-inf, add(1, MCF<[0,-1,1,0],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre)))
-7-5-0 = max(-inf, add(1, MCF<[0,0,1,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre)))
-8-5-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre))
-9-5-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre))
-10-5-0 = max(-inf, MCF<[0,-1,0,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre))
-11-5-0 = max(-inf, add(-1, MCF<[0,0,-1,1],[2:1,1:2,2:3,2:4,3:1,1:3,3:2,3:4,4:1,1:4,4:2,4:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre)))
+0-3-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre))
+1-3-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre))
+2-3-0 = max(-inf, add(1, MCF<[-1,0,1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre)))
+3-3-0 = max(-inf, add(-1, MCF<[1,0,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre)))
+4-3-0 = max(-inf, MCF<[-1,0,0,1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre))
+5-3-0 = max(-inf, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre))
+6-3-0 = max(-inf, MCF<[0,1,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre))
+7-3-0 = max(-inf, add(-1, MCF<[0,1,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-3-pre, 1-3-pre, 2-3-pre, 3-3-pre, 4-3-pre, 5-3-pre, 6-3-pre, 7-3-pre)))
+0-5-0 = max(-inf, MCF<[-1,1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre))
+1-5-0 = max(-inf, MCF<[1,-1,0,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre))
+2-5-0 = max(-inf, MCF<[-1,0,1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre))
+3-5-0 = max(-inf, MCF<[1,0,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre))
+4-5-0 = max(-inf, add(1, MCF<[-1,0,0,1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre)))
+5-5-0 = max(-inf, add(-1, MCF<[1,0,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre)))
+6-5-0 = max(-inf, add(-1, MCF<[0,1,0,-1],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre)))
+7-5-0 = max(-inf, MCF<[0,1,-1,0],[2:1,1:2,3:1,1:3,4:1,1:4,2:4,2:3]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre))
Block 0:
+ result <= 0
+ -result <= 0
i <= 0
-i <= -10
- i - j <= inf
- i - result <= 0
j <= inf
-j <= inf
- j - i <= inf
- j - result <= inf
+ result-j <= inf
+ result-i <= 0
+Block 1:
result <= 0
-result <= 0
- result - i <= 0
- result - j <= inf
-Block 1:
i <= 0
-i <= -10
- i - j <= inf
- i - result <= 0
j <= inf
-j <= inf
- j - i <= inf
- j - result <= inf
+ result-j <= inf
+ result-i <= 0
+Block 2:
result <= 0
-result <= 0
- result - i <= 0
- result - j <= inf
-Block 2:
i <= 0
-i <= 0
- i - j <= inf
- i - result <= 0
j <= inf
-j <= inf
- j - i <= inf
- j - result <= inf
- result <= 0
- -result <= 0
- result - i <= 0
- result - j <= inf
+ result-j <= inf
+ result-i <= 0
Block 3:
+ result <= 10
+ -result <= 0
i <= 0
-i <= 0
- i - j <= 0
- i - result <= 0
j <= 10
-j <= -10
- j - i <= 10
- j - result <= 0
+ result-j <= 0
+ result-i <= 10
+Block 4:
result <= 10
-result <= 0
- result - i <= 10
- result - j <= 0
-Block 4:
i <= 0
-i <= 0
- i - j <= 0
- i - result <= 0
j <= 10
-j <= 0
- j - i <= 10
- j - result <= 0
- result <= 10
- -result <= 0
- result - i <= 10
- result - j <= 0
+ result-j <= 0
+ result-i <= 10
Block 5:
+ result <= 10
+ -result <= -1
i <= 0
-i <= 0
- i - j <= 0
- i - result <= -1
j <= 9
-j <= 0
- j - i <= 9
- j - result <= -1
- result <= 10
- -result <= -1
- result - i <= 10
- result - j <= 1
+ result-j <= 1
+ result-i <= 10
Block 6:
+ result <= 10
+ -result <= 0
i <= 0
-i <= 0
- i - j <= 0
- i - result <= 0
j <= 9
-j <= 0
- j - i <= 10
- j - result <= 0
- result <= 10
- -result <= 0
- result - i <= 10
- result - j <= 0
+ result-j <= 0
+ result-i <= 10
Block 7:
+ result <= 0
+ -result <= 0
i <= 0
-i <= 0
- i - j <= inf
- i - result <= 0
j <= inf
-j <= inf
- j - i <= inf
- j - result <= inf
- result <= 0
- -result <= 0
- result - i <= 0
- result - j <= inf
+ result-j <= inf
+ result-i <= 0
Block 8:
+ result <= inf
+ -result <= inf
i <= inf
-i <= inf
- i - j <= inf
- i - result <= inf
j <= inf
-j <= inf
- j - i <= inf
- j - result <= inf
+ result-j <= inf
+ result-i <= inf
+Block 9:
result <= inf
-result <= inf
- result - i <= inf
- result - j <= inf
-Block 9:
i <= inf
-i <= inf
- i - j <= inf
- i - result <= inf
j <= inf
-j <= inf
- j - i <= inf
- j - result <= inf
- result <= inf
- -result <= inf
- result - i <= inf
- result - j <= inf
+ result-j <= inf
+ result-i <= inf
diff --git a/tex/thesis/implementation/implementation.tex b/tex/thesis/implementation/implementation.tex
index 02f2180..287cf8d 100644
--- a/tex/thesis/implementation/implementation.tex
+++ b/tex/thesis/implementation/implementation.tex
@@ -21,22 +21,198 @@ presented in Chapter \ref{chap:contribution}. The primary difference
is the use of objects instead of higher-order functions, as C++'s
support for higher-order functions was insufficient for our purposes.
-The solver was developed using only the STL for the core of the
-solver. A front-end was developed using the ANTLR parser generator
-\cite{antlr} to test the solver separately to the LLVM/Clang
-integration.
+The solver was developed using only the Standard Template
+Library~\cite{stl} for the core of the solver. A front-end was
+developed using the ANTLR parser generator \cite{antlr} to test the
+solver without the equation system generation of the clang framework.
+A high level overview of the implementation is presented in Figure
+\ref{fig:solver-arch}. The strategy iteration and fixpoint iteration
+loops provide feedback to each other about which values have changed
+at each iteration, continuing until the strategy stabilises.
+
+\begin{figure}
+ \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+ distance=4cm,main node/.style={rectangle,draw,minimum
+ height=2cm,minimum width=3cm}]
+
+ \node[main node] (maximiser) {Strategy iteration};
+ \node[main node] (minimiser) [below of=maximiser] {Fixpoint iteration};
+ \node (input) [node distance=5cm,left of=maximiser] {\emph{input}};
+ \node (output) [node distance=5cm,right of=minimiser] {\emph{output}};
+
+ \path []
+ (input) edge node {Equation system} (maximiser)
+ (maximiser) edge [bend left] node {Improved strategy} (minimiser)
+ (minimiser) edge [bend left] node [align=center]{Greatest fixpoint \\ of strategy} (maximiser)
+ (minimiser) edge node [align=center] {Least fixpoint \\ of system} (output)
+ ;
+
+ \end{tikzpicture}
+ \caption{A very high level overview of the solver implementation.}
+ \label{fig:solver-arch}
+\end{figure}
+
+In the following subsections we provide some timings for two general
+classes of equation systems. Each of the equation systems consists
+solely of inexpensive operations, either a variable lookup or a
+constant term, so we are comparing only the effect of the algorithms
+without consideration of the expense of calculating subexpressions.
+
+All these measurements were performed on a Core 2 Duo E8400 with 4GB
+of memory running Debian sid. Binaries were compiled with GCC 4.7.2
+with the -O3 flag. The source code for the solver is available
+online~\cite{bitbucket-repo}.
\subsection{Chain}
+Our first class of example equation systems is a chain. These equation
+systems have the following form:
+\begin{align*}
+ x_0 &= \max(-inf, 0) \\
+ x_1 &= \max(-inf, x_0) \\
+ ... &~ ... \\
+ x_n &= \max(-inf, x_{n-1})
+\end{align*}
+
+This particular class of equation system is the simplest of the class
+of equations with acyclic dependency graphs. In this particular case
+our solver significantly outperforms the naive algorithm for most
+problem sizes. For equation systems of less than four variables the
+naive approach is slightly faster, but this is of no real practical
+concern as in both cases it takes less than a millisecond to provide a
+result.
+
+\begin{figure}
+ \begin{tikzpicture}
+ \begin{loglogaxis}[%
+ scale only axis,
+ width=0.7\textwidth,
+ height=10cm,
+ xmin=1, xmax=65536,
+ xlabel=size of equation system,
+ ymin=0, ymax=250,
+ ylabel=time (in seconds),
+ axis on top,
+ legend entries={DSI, Naive}]
+ \addplot coordinates{
+ (1,0.000018267)
+ (2,0.000042359)
+ (4,0.000077031)
+ (8,0.000155439)
+ (16,0.000308687)
+ (32,0.000570927)
+ (64,0.001190886)
+ (128,0.002441834)
+ (256,0.004609652)
+ (512,0.009588408)
+ (1024,0.018226228)
+ (2048,0.036292838)
+ (4096,0.076125736)
+ (8192,0.152150204)
+ (16384,0.307867610)
+ (32768,0.654639048)
+ (65536,1.190741627)
+ };
+
+ \addplot coordinates{
+ (1,0.000012504 )
+ (2,0.000021558 )
+ (4,0.000060316 )
+ (8,0.000276887 )
+ (16,0.001414449 )
+ (32,0.009278044 )
+ (64,0.067620090 )
+ (128,0.508776074 )
+ (256,3.939142736 )
+ (512,31.373059038 )
+ (1024,246.603110160 )
+ };
+
+ \end{loglogaxis}
+ \end{tikzpicture}
+ \caption{Chart comparing the performance of our DSI algorithm
+ compared to a naive approach on simple chain examples. Note that
+ both axes are logarithmic.}
+ \label{fig:solver-chain}
+\end{figure}
\subsection{Cycle}
+The next class of equation system we will consider will be long
+\emph{cycles}. These will
+\begin{align*}
+ x_0 &= \max(-inf, 0, x_n) \\
+ x_1 &= \max(-inf, x_0) \\
+ ... &~ ... \\
+ x_n &= \max(-inf, x_{n-1})
+\end{align*}
+Our dependency graph is no longer acyclic, so finding the value of any
+one variable requires the evaluation, and potential strategy
+improvement, of all other values. The chart in Figure
+\ref{fig:solver-cycle} shows the running time of the DSI algorithm
+again, showing that the addition of an acyclic dependency does not
+have a significant effect.
+
+
+\begin{figure}
+ \begin{tikzpicture}
+ \begin{loglogaxis}[%
+ scale only axis,
+ width=0.7\textwidth,
+ height=10cm,
+ xmin=1, xmax=65536,
+ xlabel=size of equation system,
+ ymin=0, ymax=250,
+ ylabel=time (in seconds),
+ axis on top,
+ legend entries={DSI, Naive}]
+
+ \addplot coordinates{
+ (1,0.000016665)
+ (2,0.000044187)
+ (4,0.000081627)
+ (8,0.000159545)
+ (16,0.000309742)
+ (32,0.000627197)
+ (64,0.001236493)
+ (128,0.002338711)
+ (256,0.004967883)
+ (512,0.009164379)
+ (1024,0.018700068)
+ (2048,0.041385796)
+ (4096,0.073920841)
+ (8192,0.150712424)
+ (16384,0.302473783)
+ (32768,0.665616132)
+ (65536,1.220667681)
+ };
+
+ \addplot coordinates{
+ (1,0.000012877 )
+ (2,0.000021507 )
+ (4,0.000059573 )
+ (8,0.000252723 )
+ (16,0.001419862 )
+ (32,0.009221822 )
+ (64,0.067315559 )
+ (128,0.500673679 )
+ (256,3.912675638 )
+ (512,31.750177791 )
+ (1024,249.912189424 )
+ };
+
+ \end{loglogaxis}
+ \end{tikzpicture}
+ \caption{Chart comparing the performance of our DSI algorithm
+ compared to a naive approach on simple cyclical examples. Note
+ that both axes are logarithmic.}
+ \label{fig:solver-cycle}
+\end{figure}
-\subsection{Dense}
@@ -66,11 +242,13 @@ different points in the program.
\node[main node,fill=red!60] (eqns) [below of=clang-analysis]
{Zone analysis};
\node[main node] (dsi) [below of=eqns] {DSI};
- \node (reality) [node distance=5cm,right of=eqns] {};
+ \node (input) [node distance=7cm,left of=clang-analysis] {\emph{input}};
+ \node (reality) [node distance=5cm,right of=eqns] {\emph{output}};
\path []
%(clang) edge[bend right] node[anchor=east] {CFG} (clang-analysis)
- (clang-analysis) edge[bend right] node[anchor=east] {CFG} (eqns)
+ (input) edge node {Source code} (clang-analysis)
+ (clang-analysis) edge node[anchor=east] {CFG} (eqns)
(eqns) edge[bend right] node[anchor=east] {Equation System} (dsi)
(dsi) edge[bend right] node[anchor=west] {Solution} (eqns)
(eqns) edge node[anchor=north] {Variable bounds} (reality)
@@ -84,28 +262,165 @@ different points in the program.
\end{figure}
-\pagebreak
-\subsection{Chain}
-\lstinputlisting{implementation/experiments/chain.c}
+In the sections which follow we present the results of evaluating our
+analysis pass on several small programs. The full output from our tool
+is provided in Appendix~\ref{appendix:tool-output}, but a condensed
+form of the equation systems and variable bounds is presented here. In
+the following equation systems we use $MCF\{G\}$ to denote the minimum
+cost flow through the flow network $G$.
\pagebreak
\subsection{Counter}
\lstinputlisting{implementation/experiments/counter.c}
-\lstinputlisting{implementation/experiments/backwards_counter.c}
+This program is extremely simple, consisting only of incrementing a
+variable repeatedly in a loop. It is possible to gain a precise result
+from a widening and narrowing on this function, so we also achieve a
+precise result with this approach.
-\pagebreak
-\subsection{Nested Loops}
-\lstinputlisting{implementation/experiments/nested.c}
+Since we only have a single variable, we only wish to determine the
+bounds on $i$ and $-i$. Thus, we have the following equation system:
+\begin{align*}
+ ub(i)_A &= \infty \\
+ -lb(i)_A &= \infty \\
+ ub(i)_B &= \max(-\infty, 0,
+ MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+ distance=2cm]
+ \node (i)[draw,circle] {$1$};
+ \node (dummy)[draw,circle,right of=i] {$-1$};
+ \path [use as bounding box] (0,0) rectangle (0.5,1);
+ \path
+ (i) edge[->,bend left] node {$\min(ub(i)_B, 99)$} (dummy)
+ (dummy) edge[->,bend left] node {$-lb(i)_B$} (i);
+ \end{tikzpicture}\right\} + 1) \\
+%
+ -lb(i)_B &= \max(-\infty, 0,
+ MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+ distance=2cm]
+ \node (i)[draw,circle] {$-1$};
+ \node (dummy)[draw,circle,right of=i] {$1$};
+ \path [use as bounding box] (0,0) rectangle (0.5,1);
+ \path
+ (i) edge[->,bend left] node {$\min(ub(i)_B, 99)$} (dummy)
+ (dummy) edge[->,bend left] node {$-lb(i)_B$} (i);
+ \end{tikzpicture}\right\} - 1) \\
+%
+%
+ ub(i)_C &= \max(-\infty,
+ MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+ distance=2.5cm]
+ \node (i)[draw,circle] {$1$};
+ \node (dummy)[draw,circle,right of=i] {$-1$};
+ \path [use as bounding box] (0,0) rectangle (0.75,1.25);
+ \path
+ (i) edge[->,bend left] node {$ub(i)_B$} (dummy)
+ (dummy) edge[->,bend left] node {$\min(-lb(i)_B, -100)$} (i);
+ \end{tikzpicture}\right\}) \\
+%
+ -lb(i)_C &= \max(-\infty,
+ MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+ distance=2.5cm]
+ \node (i)[draw,circle] {$-1$};
+ \node (dummy)[draw,circle,right of=i] {$1$};
+ \path [use as bounding box] (0,0) rectangle (0.75,1.25);
+ \path
+ (i) edge[->,bend left] node {$ub(i)_B$} (dummy)
+ (dummy) edge[->,bend left] node {$\min(-lb(i)_B, -100)$} (i);
+ \end{tikzpicture}\right\})
+\end{align*}
+
+Solving this system of equations gives us the following bounds on $i$:
+\\
+\begin{center}
+ \begin{tabular}{c|cc}
+ Block & ub(i) & lb(i) \\
+ \hline
+ A & $\infty$ & $-\infty$ \\
+ B & $100$ & $0$ \\
+ C & $100$ & $-100$
+ \end{tabular}
+\end{center}
+
+This is a precise analysis of the values of $i$, performed without
+widening/narrowing. It captures the possible values of $i$ precisely
+and identifies the value of $i$ at the exit of the loop.
\pagebreak
\subsection{Double counting}
\lstinputlisting{implementation/experiments/example.c}
-\pagebreak
-\subsection{Fibonacci}
-\lstinputlisting{implementation/experiments/fib.c}
+In this example we are incrementing two different program variables at
+the same time, based on a condition of one of the variables. In
+standard interval analysis it is impossible to capture the
+relationship between these variables, but by performing abstract
+interpretation over zones we can perform a more precise analysis.
-\pagebreak
-\subsection{Unreachable}
-\lstinputlisting{implementation/experiments/irreducible.c}
+This example is a translation to C of the example presented by
+Gawlitza et al.~\cite{EasyChair:117}. In our abstract analysis we will
+consider the values $x1$, $x2$ and $x2 - x1$.
+
+\begin{align*}
+ ub(x1)_A &= \infty \\
+ ub(x2)_A &= \infty \\
+ ub(x2 - x1)_A &= \infty \\
+%
+ ub(x1)_B &= \max(-\infty, 0,
+ MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+ distance=2.5cm]
+ \node (x1)[draw,circle] {$1$};
+ \node (x2)[draw,circle,below of=x1] {$0$};
+ \node (dummy)[draw,circle,below right of=x1] {$-1$};
+ \path
+ (x1) edge[->,bend left] node {$\min(8, ub(x1)_B)$} (dummy)
+ (x2) edge[->,bend left] node {$ub(x2)_B$} (x1)
+ (x2) edge[->,bend left] node {$ub(x2 - x1)_B$} (dummy);
+ \end{tikzpicture}\right\} + 2) \\
+ ub(x2)_B &= \max(-\infty, 1,
+ MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+ distance=2.5cm]
+ \node (x1)[draw,circle] {$0$};
+ \node (x2)[draw,circle,below of=x1] {$1$};
+ \node (dummy)[draw,circle,below right of=x1] {$-1$};
+ \path
+ (x1) edge[->,bend left] node {$\min(8, ub(x1)_B)$} (dummy)
+ (x2) edge[->,bend left] node {$ub(x2)_B$} (x1)
+ (x2) edge[->,bend left] node {$ub(x2 - x1)_B$} (dummy);
+ \end{tikzpicture}\right\} + 2) \\
+ ub(x2 - x1)_B &= \max(-\infty, 1,
+ MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+ distance=2.5cm]
+ \node (x1)[draw,circle] {$-1$};
+ \node (x2)[draw,circle,below of=x1] {$1$};
+ \node (dummy)[draw,circle,below right of=x1] {$0$};
+ \path
+ (x1) edge[->,bend left] node {$\min(8, ub(x1)_B)$} (dummy)
+ (x2) edge[->,bend left] node {$ub(x2)_B$} (x1)
+ (x2) edge[->,bend left] node {$ub(x2 - x1)_B$} (dummy);
+ \end{tikzpicture}\right\}) \\
+%
+%
+ ub(x1)_C &= \max(-\infty, ub(x1)_B) \\
+ ub(x2)_C &= \max(-\infty, ub(x2)_B) \\
+ ub(x2 - x1)_C &= \max(-\infty, ub(x2 - x1)_B)
+\end{align*}
+
+
+Solving this system of equations gives us the following bounds on
+$x1,x2$ and $x2-x1$:
+\\
+\begin{center}
+ \begin{tabular}{c|ccc}
+ Block & ub(x1) & ub(x2) & ub(x2 - x1) \\
+ \hline
+ A & $\infty$ & $\infty$ & $\infty$ \\
+ B & $10$ & $11$ & $1$ \\
+ C & $10$ & $11$ & $1$
+ \end{tabular}
+\end{center}
+
+This result is more precise than any that could have been obtained by
+interval analysis. We accurately capture the relationship between $x1$
+and $x2$ by bounding $x2 - x1 \le 1$, and this allows us to correctly
+determine the upper bound of $x2$ at the exit of the loop. The output
+of our automatic analysis for this function can be seen in Section
+\ref{sec:example-function-output}.
generated by cgit v1.2.3 (git 2.46.2) at 2024-12-25 06:32:03 +0000