diff options
| -rw-r--r-- | tex/thesis/appendices/tool-output.tex | 18 | ||||
| -rw-r--r-- | tex/thesis/conclusion/conclusion.tex | 32 | ||||
| -rw-r--r-- | tex/thesis/contribution/contribution.tex | 3 | ||||
| -rw-r--r-- | tex/thesis/implementation/experiments/counter.c | 4 | ||||
| -rw-r--r-- | tex/thesis/implementation/experiments/example-output | 90 | ||||
| -rw-r--r-- | tex/thesis/implementation/experiments/example.c | 4 | ||||
| -rw-r--r-- | tex/thesis/implementation/experiments/fib-output | 302 | ||||
| -rw-r--r-- | tex/thesis/implementation/experiments/nested-output | 260 | ||||
| -rw-r--r-- | tex/thesis/implementation/implementation.tex | 355 | ||||
| -rw-r--r-- | tex/thesis/litreview/litreview.tex | 125 | ||||
| -rw-r--r-- | tex/thesis/references.bib | 10 | ||||
| -rw-r--r-- | tex/thesis/thanks/thanks.tex | 18 | ||||
| -rw-r--r-- | tex/thesis/thesis.tex | 2 |
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}} |