summaryrefslogtreecommitdiff
path: root/tex/thesis
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis')
-rw-r--r--tex/thesis/appendices/tool-output.tex18
-rw-r--r--tex/thesis/conclusion/conclusion.tex32
-rw-r--r--tex/thesis/contribution/contribution.tex3
-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
-rw-r--r--tex/thesis/litreview/litreview.tex125
-rw-r--r--tex/thesis/references.bib10
-rw-r--r--tex/thesis/thanks/thanks.tex18
-rw-r--r--tex/thesis/thesis.tex2
13 files changed, 619 insertions, 604 deletions
diff --git a/tex/thesis/appendices/tool-output.tex b/tex/thesis/appendices/tool-output.tex
index 229ed94..e62aa2a 100644
--- a/tex/thesis/appendices/tool-output.tex
+++ b/tex/thesis/appendices/tool-output.tex
@@ -1,5 +1,5 @@
\appendix
-\chapter{Analysis tool results}
+\chapter{Analysis tool results} \label{appendix:tool-output}
In the following output a min-cost flow operator is presented as
{\tt MCF<supplies,edges>(costs)}. This represents the solution to a
@@ -39,33 +39,29 @@ each block is printed.
\lstset{basicstyle=\ttfamily\scriptsize,breaklines=true,breakatwhitespace=true,frame=lrtb}
-\pagebreak
-\section{Chain construction}
-\lstinputlisting{implementation/experiments/chain-output}
-
-In this example we show
\pagebreak
\section{Counter}
+\lstinputlisting{implementation/experiments/counter.c}
\lstinputlisting{implementation/experiments/counter-output}
-\lstinputlisting{implementation/experiments/backwards_counter-output}
-
\pagebreak
\section{Nested Loops}
+\lstinputlisting{implementation/experiments/nested.c}
\lstinputlisting{implementation/experiments/nested-output}
\pagebreak
-\section{Double counting}
+\section{Double counting} \label{sec:example-function-output}
+\lstinputlisting{implementation/experiments/example.c}
\lstinputlisting{implementation/experiments/example-output}
-In this example
-
\pagebreak
\section{Fibonacci}
+\lstinputlisting{implementation/experiments/fib.c}
\lstinputlisting{implementation/experiments/fib-output}
\pagebreak
\section{Unreachable}
+\lstinputlisting{implementation/experiments/irreducible.c}
\lstinputlisting{implementation/experiments/irreducible-output}
diff --git a/tex/thesis/conclusion/conclusion.tex b/tex/thesis/conclusion/conclusion.tex
index d28a84b..1f6c803 100644
--- a/tex/thesis/conclusion/conclusion.tex
+++ b/tex/thesis/conclusion/conclusion.tex
@@ -1,4 +1,34 @@
\chapter{Conclusion} \label{chap:conclusion}
-The conclusion goes here.
+In this thesis we have presented an enhancement on a game-theoretic
+algorithm for efficiently solving systems of monotonic, expansive
+equations for their least fixpoints. We implemented this algorithm in
+C++ and evaluated its performance relative to the existing approach,
+finding it to be significantly faster for practical instances of
+equation systems.
+We further have integrated our solver into the LLVM/Clang static
+analysis framework to perform static analysis of C programs. We
+implemented a translation from C programs into monotonic, expansive
+equation systems to analyse C programs with abstract interpretation,
+in the domain of zones. We have evaluated the results of this analysis
+on a number of test cases to evaluate its precision.
+
+\section{Further work}
+
+There are still several areas in which the work of this thesis could
+be improved upon:
+
+\begin{itemize}
+\item
+ {\bf Refine variable dependencies} The enhanced DSI algorithm still
+ over approximates dependencies between variables to a slight
+ degree. Reducing this over approximation could result in a slight
+ improvement in the running time of the algorithm.
+\item
+ {\bf Complete the implementation} The provided LLVM/Clang
+ integration is currently only at a proof-of-concept stage. Only a
+ subset of the C semantics are currently considered in the analysis
+ pass. There is significant work to be done to ensure that analysis
+ can be performed for all, or at least most, C code.
+\end{itemize}
diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index c4a0700..5b3acb9 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -1171,6 +1171,3 @@ the $\max$-strategy. If the variable has stabilised to the same value
as it had previously then it has not changed and thus has no effect on
the $\max$-strategy.
-
-
-\subsection{Implementation} \label{sec:ldsi:implementation}
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}.
diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex
index 983bb44..d223f36 100644
--- a/tex/thesis/litreview/litreview.tex
+++ b/tex/thesis/litreview/litreview.tex
@@ -276,14 +276,11 @@ interpretation over zones.
\end{figure}
We now attempt to derive a system of inequalities from this for the
- \emph{least upper bound} of $x$ at each program point.
- \begin{align*}
- ub: {} & ~\Vars \to \CZ \\
- ub(x) &= \min\{v \in \CZ ~|~ x \le v\}.
- \end{align*}
- We wish to find a value for $ub(x)$ at each program point in our
- original program. We denote these values by $ub_A(x)$, $ub_B(x)$ and
- $ub_C(x)$.
+ \emph{least upper bound} of a variable $x$ at each program
+ point. That is, we want to find a value $ub(x)$ such that, for all
+ possible executions of the program $x \le ub(x)$. We wish to find a
+ value for $ub(x)$ at each program point in our original program. We
+ denote these values by $ub_A(x)$, $ub_B(x)$ and $ub_C(x)$.
For $A$ the value of $x$ is entirely unknown, so no useful bound can
be given. The possible values of $x$ are bounded only by the top
@@ -370,10 +367,14 @@ equation system can be constructed to aid us in locating the
For every partial-ordering on a set there exists an equivalent
lattice, defined in terms of a meet operator ($\vee$) and a join
-operator ($\land$), which are defined by the following relationships:
+operator ($\land$), which are defined by:
\begin{align*}
- x \le y ~&\iff~ x \vee y = y \\
- x \le y ~&\iff~ x \land y = x
+ x \vee y = z \iff z \ge x, z \ge y, (w \ge x, w \ge y \implies w \ge
+ z, \forall w) \\
+ x \land y = z \iff z \le x, z \le y, (w \le x, w \le y \implies w \le
+ z, \forall w)
+ %x \le y ~&\iff~ x \vee y = y \\
+ %x \le y ~&\iff~ x \land y = x
\end{align*}
In the case of Example \ref{example:partial-ordered-construction},
@@ -595,47 +596,77 @@ constraint system.
\section{Min-cost flow}
-This matrix fomulation sufficient to calculate bounds on individual
+The matrix formulation is sufficient to calculate bounds on individual
program variables, as in the interval domain, but in doing so there is
a significant loss of precision. In order to reclaim some of this
-precision we can use a relational domain.
-
-
-
-
-
-\endinput
-
-\subsection{Example solve}
-\label{sec-1-3-5}
-
+precision we use a relational domain, such as zones.
-Reconsidering our earlier equation system, we now attempt to find
-the minimal fixpoint by means of \emph{policy iteration} and
-\emph{fixpoint iteration}.
+We use a ``template constraint matrix'' to specify interesting values
+for our analysis. A template constraint matrix is an $m \times n$
+matrix, where $n$ is the number of program variables and $m$ is the
+number of interesting abstract values.
-\begin{eqnarray*}
-x &=& \max(1, \min(x, 99) + 1) \\
-\end{eqnarray*}
-
-At the beginning and end of each player's turn we will have a variable
-assignment $\{ x \to ? \}$, which will start with the value
-$\{ x \to -\infty \}$.
+\begin{example}
+ If we have two program variables $x_1$ and $x_2$ then we can analyse
+ for values $x_1$, $-x_1$, $x_2$, $-x_2$, $(x_1 - x_2)$ and $(x_2 -
+ x_1)$. If we are only interested in the values of $x_1$, $x_2$ and
+ $(x_2 - x_1)$ then we set our template constraint matrix to be
+ \begin{align*}
+ T &= \left[\begin{array}{cc}
+ 1 & 0 \\
+ 0 & 1 \\
+ -1 & 1
+ \end{array}\right]
+ \end{align*}
+\end{example}
-The $\max$ player then gets a chance to play. They choose to improve
-the strategy by choosing for $x$ to take the value $1$. The $\min$
-player then has no choice but to find a variable assignment $\{ x
-\to 1 \}$, as the $\max$ player has left them no choice.
+This template constraint matrix also specifies the topology of a
+graph. By considering each row as an edge, and each column as a node,
+we can produce a directed graph $G$, such that for each row an edge
+exists between the column containing a $1$ and the column containing a
+$-1$ in that row. In order to guarantee that all rows exist in $G$ it
+is also necessary to add an extra ``dummy node'' such that any
+unspecified edges are adjacent to the dummy node.
-Play then returns to the $\max$ player who chooses, again, to improve
-their strategy to instead map $x$ to $\min(x, 99) + 1$. This time the
-$\min$ player must make a decision. It solves $x = \min(x, 99) + 1$
-for it's maximal fixpoint, deciding to use the $99$ value (as the $x$
-value will grow without bound with the $+ 1$, thereby making $99$ the
-minimum of the two options) and returning $\{ x \to 100 \}$ as
-the new assignment.
+\begin{example}
+ For the template constraint matrix
+ \begin{align*}
+ T &= \left[\begin{array}{cc}
+ 1 & 0 \\
+ 0 & 1 \\
+ -1 & 1
+ \end{array}\right]
+ \end{align*}
-The $\max$ player has no further way to improve their strategy, as $1
-< 100$, so the game is over. The minimal fixpoint of the original
-system has been found as $x = 100$.
+ \noindent we construct a directed graph
+
+ \begin{center}
+ \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+ distance=2.5cm]
+ \node (x1)[draw,circle] {$x1$};
+ \node (x2)[draw,circle,below of=x1] {$x2$};
+ \node (dummy)[draw,circle,below right of=x1] {dummy};
+
+ \path
+ (x1) edge[->,bend left] node {} (dummy)
+ (x2) edge[->,bend left] node {} (x1)
+ (x2) edge[->,bend left] node {} (dummy);
+ \end{tikzpicture}.
+ \end{center}
+\end{example}
+Once we have determined the topology of this graph, we then perform
+abstract interpretation by assigning the nodes ``supplies'' and the
+edges ``costs''. The supplies correspond to a statement's semantics,
+capturing the combination of variables which are the result of a given
+assignment, while the costs consider the incoming values of variables
+into the statement.
+
+We use the min-cost flow problem on this graph as an operator in our
+equation systems. We fix the topology and the costs in the graph and
+then consider it as a function of its edge costs, which are the
+abstract values entering this node. The validity of this approach is
+considered by Gawlitza et al.~\cite{EasyChair:117}, where it is shown
+that the min-cost flow problem, when considered as a function of its
+edge weights is monotonic and quasi-expansive, thereby making it a
+valid operator in our equation systems.
diff --git a/tex/thesis/references.bib b/tex/thesis/references.bib
index 2d68228..5154bd3 100644
--- a/tex/thesis/references.bib
+++ b/tex/thesis/references.bib
@@ -308,4 +308,14 @@ url={http://clang.llvm.org/}
@misc{clang-analysis,
title={Clang Static Analyser},
url={http://clang-analyzer.llvm.org/}
+}
+@TECHREPORT{stl,
+ author = {Alexander Stepanov and Meng Lee},
+ title = {The standard template library},
+ institution = {WG21/N0482, ISO Programming Language C++ Project},
+ year = {1994}
+}
+@misc{bitbucket-repo,
+title={Source code repository},
+url={https://bitbucket.org/czan/honours}
} \ No newline at end of file
diff --git a/tex/thesis/thanks/thanks.tex b/tex/thesis/thanks/thanks.tex
index 3e066eb..37e59a5 100644
--- a/tex/thesis/thanks/thanks.tex
+++ b/tex/thesis/thanks/thanks.tex
@@ -1,4 +1,20 @@
\chapter*{Acknowledgements}
-The thanks go in here.
+Bernhard Scholz, for his tireless efforts and boundless patience with
+me as I've worked on this thesis. His guidance was much appreciated
+throughout the whole process of writing and working, and without his
+assistance this thesis would be in much worse shape. His experience
+was invaluable to me, especially in the presentation of
+Thomas Gawlitza, for his technical guidance and helpful
+attitude. Despite significant difficulties he was always willing to
+help when asked and provide helpful advice for presenting complicated
+concepts more clearly.
+
+My family, for their constant desire to help me, despite a lack of
+knowledge of the domain. For the many cups of tea that they have made
+for me and the grace with which they have treated me, even when I have
+not been the easiest person to deal with.
+
+Finally I would like to thank the Lord Jesus Christ, without whom I
+would not be who I am today.
diff --git a/tex/thesis/thesis.tex b/tex/thesis/thesis.tex
index c69f78c..6fc8868 100644
--- a/tex/thesis/thesis.tex
+++ b/tex/thesis/thesis.tex
@@ -27,6 +27,7 @@
\usepackage{subfigure}
\usepackage{pdflscape}
\usepackage{pgf}
+\usepackage{pgfplots}
\usepackage{pifont}
\usepackage{qtree}
\usepackage[english,rounding]{rccol}
@@ -47,6 +48,7 @@
\lstset{language={Python}, literate={<=}{$\le$}{1}}%, frame=tlrb}
\usetikzlibrary{arrows}
+\pgfplotsset{compat=1.4}
\newcommand\D{\mathbb{D}}
\newcommand\R{\mathbb{R}}