From 08b8ab611e95ff12bef42f9863a76b75b3ecab51 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Sat, 2 Jan 2016 19:51:38 +0100 Subject: [PATCH] big update, better formalization for pegsol --- a2/1.tex | 101 ++-- a2/3.tex | 1 + a2/4.model | 0 a2/4.tex | 191 ++++---- a2/ar.tex | 4 + a2/board.jpg | Bin 0 -> 12470 bytes a2/pre.tex | 2 + a2/src/1.bak | 126 +++++ a2/src/1.bash | 50 -- a2/src/1a.bash | 166 +++++++ a2/src/1b.bash | 127 +++++ a2/src/4/4.model | 1059 ------------------------------------------ a2/src/4/4.model.bak | 1059 ++++++++++++++++++++++++++++++++++++++++++ a2/src/4/a4.py | 15 +- 14 files changed, 1652 insertions(+), 1249 deletions(-) create mode 100644 a2/4.model create mode 100644 a2/board.jpg create mode 100644 a2/src/1.bak delete mode 100755 a2/src/1.bash create mode 100755 a2/src/1a.bash create mode 100755 a2/src/1b.bash create mode 100644 a2/src/4/4.model.bak diff --git a/a2/1.tex b/a2/1.tex index 67a214c..11692f6 100644 --- a/a2/1.tex +++ b/a2/1.tex @@ -17,51 +17,90 @@ for $i\in I$ where $I=\{0\ldots\}$. For every iteration $i$ we make variables $a_i, b_i, c_i, t_i, l_i, d_i$ respectively for the capacity of city $A$, city $B$, city $C$, the truck, the trucks location and a help variable to record how much food is dumped in the city. The distance between two cities is -described with the function $dist(x, y)$. For all cities except $S$ a variable -is defined that states the maximum capacity. -$$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200$$ +described with the function $dist(x, y)$. For all cities except $S$ and the +truck a variable is defined that states the maximum capacity. We express all +the constant values in the formula called $const$. +$$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200\wedge t_{\max}=300$$ + Iteration $0$ depicts the initial state and can be described with a simple -conjuction: +conjunction called $initial$. $$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$ -After that all iterations can be formalized as -$$\begin{array}{lrl} - \bigwedge_{i\in I} \Bigg( - % Bent in S - & \Bigg[ & l_i=S\wedge d_i=0\wedge t_i=300\wedge\\ - & & \bigvee_{k\in\{A,B\}} - \bigg(l_{i-1}=k\wedge - \bigwedge_{s\in\{A,B,C\}} - s_i=s_{i-1}-dist(S, k)\bigg)\Bigg]\vee\\ - % Bent in A,B,C - & \bigvee_{k\in\{a,b,c\}}\Bigg[ & l_i=k\wedge\\ - & & d_i>0\wedge d_i0\wedge +d_i\leq t_{\max}\wedge +t_i\geq\wedge +t_i\leq t_{\max}\wedge +\bigwedge_{k\in\{A,B,C\}}k_i>0$$ -\begin{enumerate} - \item This part of the formula describes what happens if the truck is in - $S$. This is a special case of the generalized case dsecribed in $2$ - and $3$. The truck always gets a refill in $S$ and no food is dumped. - The truck could either have come from $A$ or $B$ and thus the food - stocks of $A,B$ and $C$ will drop accordingly. - \item -\end{enumerate} +We reason about the new iteration $i$ from the things we know about iteration +$i-1$. The crucial part is the location we were in iteration $i-1$ and we make +a disjunction over all possible cities and describe the result in the following +formula called $trans$. We introduce a function $conn(s)$ that returns the set +of all cities connected to city $s$. $(2)$ deals with the fact that the truck +can not dump any food in city $S$ and constraints the amount of food dumped in +the city. $(3)$ deals with the fact that the dumped food is added to the +current stock of the city. Subformula $(4)$ deals with the fact that if the +truck is in $S$ it is replenished and otherwise the dumped load is subtracted +from the trucks load. Finally $(5)$ deals with the other cities which will have +their stock decremented with the distance traveled. + +\begin{align} + \bigvee_{k\in\{S\}\cup V} + l_{i-1}=k\wedge + \bigvee_{k'\in conn(k)} & l_i=k'\wedge\\ + & (k'=S\wedge d_i=0)\vee(d_i\leq dist(k,k')+k'_{\max}-k'_{i-1}\wedge\\ + & (k'\neq S\rightarrow k_i=k_i-dist(k,k')+d_i))\wedge\\ + & (k'=S\wedge t_i=t_{\max})\vee t_i=t_{i-1}-d_i\wedge\\ + & \bigwedge_{k''\in V\setminus\{k\}} + k''_i=k''_{i-1}-dist(k,k') +\end{align} + +We tie all this together in one big formula that is as follows: +$$const\wedge initial\wedge +\bigwedge_{i\in I}\left(constraints\wedge trans\right)$$ \begin{enumerate}[a.] \item \emph{Show that it is impossible to deliver food packages in such a way that each of the villages consumes one food package per time unit forever.} + \item \emph{Show that this is possible if the capacity of the truck is increased to 320 food packages. (Note that a finite graph contains an infinite path starting in a node $v$ if and only if there is a path from $v$ to a node $w$ for which there is a non-empty path from $w$ to itself.)} + To show this we need to prove that there is a state in the statespace + that is exactly the same as some previous state. To do this we add the + following formula to the conjunction. + $$\bigvee_{i\in I}\bigvee_{j\in \{0\ldots i-1\}}\left( + t_i=t_j\wedge l_i=l_j\wedge\bigwedge_{k\in V}k_i=k_j\right) + $$ + + When we incrementally increase the number of iterations we see that + when we have more then $8$ iterations we encounter a cycle. This is + shown in the following table where iteration $2$ and iteration $9$ are + equal. + \begin{table}[H] + \centering + \begin{tabular}{ccccccc} + \toprule + $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\ + \midrule + $0$ & $40$ & $30$ & $145$ & $320$ & $0$ & $0$\\ + $1$ & $19$ & $22$ & $124$ & $307$ & $2$ & $9$\\ + $2$ & $96$ & $5$ & $107$ & $213$ & $1$ & $98$\\ + $3$ & $79$ & $119$ & $90$ & $82$ & $2$ & $133$\\ + $4$ & $58$ & $98$ & $69$ & $320$ & $0$ & $0$\\ + $5$ & $108$ & $69$ & $40$ & $241$ & $1$ & $79$\\ + $6$ & $76$ & $37$ & $194$ & $55$ & $3$ & $186$\\ + $7$ & $39$ & $55$ & $157$ & $0$ & $2$ & $53$\\ + $8$ & $18$ & $34$ & $136$ & $320$ & $0$ & $0$\\ + $9$ & $96$ & $5$ & $107$ & $213$ & $1$ & $107$\\ + \bottomrule + \end{tabular} + \end{table} \item \emph{Figure out whether it is possible if the capacity of the truck is set to $318$.} \end{enumerate} diff --git a/a2/3.tex b/a2/3.tex index e69de29..a6e47e9 100644 --- a/a2/3.tex +++ b/a2/3.tex @@ -0,0 +1 @@ +\section{Problem 3} diff --git a/a2/4.model b/a2/4.model new file mode 100644 index 0000000..e69de29 diff --git a/a2/4.tex b/a2/4.tex index 9eb06c0..cfec0ab 100644 --- a/a2/4.tex +++ b/a2/4.tex @@ -1,112 +1,109 @@ \section{Solving solitaire} \subsection{Problem description} -Standard \emph{Peg solitaire} is a game played with marbles or pegs on a board -with $33$ holes as displayed in Figure~\ref{lst:pegs}. In the Figure dots -represent a peg and o's represent a empty hole. The goal is to end up with the -last peg in the middle hole and all other pegs removed from the board. -To achieve this you have make moves that capture another peg. You can capture -another peg by finding a peg bordering it in a certain direction and on the -other side there needs to be an empty spot. The four possible moves are -displayed in Figure~\ref{lst:moves}. - -Since there is no such thing as an empty move we know the game is always -finished in $31$ steps. This is because in the start position there are $32$ -pegs on the playing field, every move we remove one peg, thus requiring $31$ -moves to end up with only one peg. +Standard \emph{English Peg solitaire} is a single player game played on a board +with $33$ holes and is played with $32$ pegs. In the initial position all holes +are occupied except for the middle hole. A traditional board is shown in +Figure~\ref{fig:sol}. The goal of the game is to remove all but one peg on the +middle position. The player can remove a peg by jumping over the peg +orthogonally to a position two holes away. The middle peg is then removed from +the board. To visualize board configurations we use the symbol $\circ$ for a +position occupied by a peg and the symbol $\times$ by a position not occupied. +The initial board configuration and possible moves are shown in +Figure~\ref{fig:init}. Variations on the game exists with different board shapes such as triangles, rotated squares or bigger crosses. There is also an alternative that makes the -end condition more flexible. Instead of requiring the last peg to be in the -middle of the board, the last peg can be anywhere on the board. - -\begin{lstlisting}[caption={Standard English peg solitaire starting -position},label={lst:pegs}] - ... - ... -....... -...o... -....... - ... - ... -\end{lstlisting} +end condition more flexible by allowing the last peg anywhere on the board. +\begin{figure}[H] + \centering + \includegraphics[width=.2\linewidth]{board.jpg} + \caption{Peg solitaire board}\label{fig:sol} +\end{figure} -\begin{lstlisting}[caption={Moves in all possible directions}, -label={lst:moves}] -right left down up - . . o . -..o->oo. o..->.oo . -> o . -> o - o o . o -\end{lstlisting} +\begin{figure}[H] + $$\xymatrix@1@=1pt@M=1pt{ + & 0 & 1 & 2 & 3 & 4 & 5 & 6\\ + 0 & & & \circ & \circ & \circ & & & & & & + \circ\ar@/^/[rr] & \circ & \times & \rightarrow & + \times & \times & \circ\\ + 1 & & & \circ & \circ & \circ\\ + 2 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & & + \times & \circ & \circ\ar@/_/[ll]& \rightarrow & + \circ & \times & \times\\ + 3 & \circ & \circ & \circ & \times & \circ & \circ & \circ\\ + 4 & \circ & \circ & \circ & \circ & \circ & \circ & \circ & & & & + \circ\ar@/_/[dd] & & \times & & \times & & \circ\\ + 5 & & & \circ & \circ & \circ & & & & & & + \circ & \rightarrow & \times & & \circ & \rightarrow& \times\\ + 6 & & & \circ & \circ & \circ & & & & & & + \times & & \circ & & \circ\ar@/^/[uu] & & \times\\ + }$$ + \caption{Initial board state and possible moves}\label{fig:init} +\end{figure} \subsection{Formalization} -Basically there are two possible formalization techniques we can use. -Formalization per position and formalization per peg. +Because in every move a peg is captured the game ends in exactly $31$ moves +since there are $32$ pegs and one is left with a sole peg. A position $p$ means +the $x$ and the $y$ coordinate as shown in Figure~\ref{fig:init}. Stating for a +point $p$, $p_x$ or $p_y$ it means the respective $x$ and $y$ component of the +position.\\ -Formalization per position means that we keep track of all the board positions -and model what the position would be in the next state considering all possible -moves. Every move there are only three positions on the board that are updated. -On the entire board there are only $76$ possible combinations of three -positions that can result in a move. This means that the formalization results -in a big disjunction of the $76$ different moves. +Set $\mathcal{P}$ is the set of all legal board positions and can be defined +as: +$$\mathcal{P}=\left\{p\in \{0\ldots7\}^2|\text{where }\neg( + (p_x<2\wedge p_y<2)\vee + (p_x>4\wedge p_y>4)\vee + (p_x>4\wedge p_y<2)\vee + (p_x<2\wedge p_y>4)\right\}$$ -The second method would be to formalize the game in means of the pegs. For -every peg we keep track of the location and when the peg is removed we put them -in the bin. In this way when we end up with only one peg with a valid winning -location and the rest in the bin the game is over. Expected is that this method -has a much higher branching factor. Moves always consist of two pegs. So for -every move we have to check every combination of pegs and every direction. This -means that when there are $32$ pegs in the game there are -$32\cdot31\cdot4=3968$ possible moves we should check. Ofcourse we can prune a -lot of combinations very quickly because one of the pegs might already in the -bin or the position of the pegs was not correct but it is still a very large -branching factor. Because of the high branching factor we first attempt to -solve the problem using the position based approach. +Set $\mathcal{M}$ is the set of position triples that form a legal move. $s$ +denotes the start position, $m$ denotes the middle position and $e$ the final +position. +$$\begin{array}{l} + \mathcal{M}=\{(s,m,e)\in \{0\ldots7\}^3|\text{where }\\ + \qquad\qquad(s_x=m_x\wedge m_x=e_x\wedge + (m_y=s_y+1\wedge e_y=m_y+1\vee m_y=s_y-1\wedge e_y=m_y-1)\vee\\ + \qquad\qquad(s_y=m_y\wedge m_y=e_y\wedge + (m_x=s_x+1\wedge e_x=m_x+1\vee m_x=s_x-1\wedge e_x=m_x-1)\\ +\end{array}$$ -\begin{lstlisting}[caption={Coordinate system},label={lst:coord}] - 0123456 -0 ooo -1 ooo -2ooooooo -3ooooooo -4ooooooo -5 ooo -6 ooo -\end{lstlisting} +For every iteration $i\in\{0\ldots32\}$ and for every position $p\in \mathcal{P}$ +we create a variable representing the state of occupation. We also define +$g=\langle3,3\rangle$ as being the middle position. With these definitions we +can describe the initial state $\mathcal{INIT}$ as follows: +$$\neg i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}} +i_0x_{p_x}y_{p_y}$$ -To represent each position, as in Listing~\ref{lst:coord}, we assign per -iteration $i$ for $i\in I$ where $I=\{0..32\}$ a variable $i_ix_xy_y$ per -position where $(x,y)\in P$ where $P=\{(x,y) | (x,y)\text{ position on the -board}\}$. So for example for the topmost row we have for $i=0$ the variables -$\{i_0x_2y_0, i_0x_2y_1, i_0x_3y_0, i_0x_3y_1, i_0x_4y_0, i_0x_4y_1\}$. +Every iteration with $i>0$ we define with a function called $\mathcal{ITER}(i)$ +which for every move describes the updates for the positions. Only the +positions involved in the move are updated when the rest stay the same. Part +$(1)$ of the formula describes the preconditions for a move to be valid. $(2)$ +describes the result of the move and $(3)$ expresses the invariability of the +other positions. +$$\begin{array}{llr} + \bigvee_{(s,m,e)\in M} \Biggl[& + i_{i-1}x_{s_x}y_{s_y}\wedge + i_{i-1}x_{m_x}y_{m_y}\wedge + \neg i_{i-1}x_{e_x}y_{e_y}\wedge & (1)\\ + & \neg i_{i}x_{s_x}y_{s_y}\wedge + \neg i_{i}x_{m_x}y_{m_y}\wedge + i_{i}x_{e_x}y_{e_y}\wedge & (2)\\ + & \bigwedge_{o\in \mathcal{P}\setminus\{s,m,e\}} + i_ix_{o_x}y_{o_y}=i_{i-1}x_{o_x}y_{o_y}\quad\Biggr] & (3) +\end{array} +$$ -To iterate over all moves we have to distinguish start and end positions from -the middle position. All positions from $P$ are legal start or end positions -but some are excluded from being a legal middle position of a move. Basically -all positions in $P$ except for the corners are legal middle positions and -therefore we define $P'$ that only contains legal middle positions and -therefore $P'=P\setminus\{(2,0), (4,0), (0,2), (0,4), (6,2), (6,4), (2,6), -(4,6)\}$ +The final state should be an inversion of the initial state. All holes should +be empty except the middle hole $g$. $\mathcal{POST}$ is defined as follows: +$$i_0x_{g_x}y_{g_y}\wedge\bigwedge_{p\in \mathcal{P}\setminus\{g\}} +\neg i_0x_{p_x}y_{p_y}$$ -\begin{align} - \neg i_0x_3y_3\wedge\bigwedge_{(x,y)\in -P\setminus\{(3,3)\}}\left(i_0x_xy_y\right)\wedge\\ - \bigwedge^{I}_{i=1} - \bigvee_{(sx, sy)\in P}\bigvee_{(mx, my)\in P'} - \bigvee_{(ex, ey)\in P}\Bigl( - & \bigl((sy=my\wedge my=ey\wedge sx=mx+1\wedge mx=ex+1)\vee\\ - & \quad(sy=my\wedge my=ey\wedge sx=mx-1\wedge mx=ex-1)\vee\\ - & \quad(sx=mx\wedge mx=ex\wedge sy=my+1\wedge my=ey+1)\vee\\ - & \quad(sx=mx\wedge mx=ex\wedge sy=my-1\wedge my=ey-1)\bigr)\wedge\\ - & i_{i-1}x_{sx}y_{sy}\wedge - i_{i-1}x_{mx}y_{my}\wedge - \neg i_{i-1}x_{ex}y_{ey}\wedge\\ - & \neg i_{i}x_{sx}y_{sy}\wedge - \neg i_{i}x_{mx}y_{my}\wedge - i_{i}x_{ex}y_{ey}\wedge\\ - & \bigwedge_{(ox,oy)\in P\setminus\{(ex,ey),(mx,my),(sx,sy)\}}\left( - i_ix_{ox}y_{oy}=i_{i-1}x_{ox}y_{oy}\right)\Bigr)\wedge\\ - i_{31}x_3y_3\wedge\bigwedge_{(x,y)\in P\setminus\{(3,3)\}}\neg i_{31}x_xy_y -\end{align} +All of this together in the following formula is satisfiable if +and only if there is a solution to English \textit{Peg solitaire}. The model +that satisfies the formula is the sequence of moves to be performed to win a +game. +$$\mathcal{INIT}\wedge\left(\bigwedge_{i=1}^{31}\mathcal{ITER}(i)\right) +\wedge\mathcal{POST}$$ -\lstinputlisting[caption={Solution for peg solitaire},label={lst:sol}] - {./src/4/a4.tex} +\subsection{Solution} +The conversion to SMT-Lib is trivial diff --git a/a2/ar.tex b/a2/ar.tex index 5dabd82..73a4629 100644 --- a/a2/ar.tex +++ b/a2/ar.tex @@ -3,12 +3,16 @@ \maketitle \tableofcontents +\newpage \input{1.tex} +\newpage \input{2.tex} +\newpage \input{3.tex} +\newpage \input{4.tex} \end{document} diff --git a/a2/board.jpg b/a2/board.jpg new file mode 100644 index 0000000000000000000000000000000000000000..ed7505df8bc0bc1c364322e3a1d0d395769f98cc GIT binary patch literal 12470 zcmbW7cTf|+_uxbCB1q^+uMwmL=}qYb2%S)rPC!6<7Zhoc7CNDK0tBRlCMdo4-jUu> zkRk|ret&m!cXNN;-R|tp+j(zx_cPmP-`|D5-vAFaRW(!rI5;?fSN|g5?*>3x#UJhf z0BC3k0Ehtq03P5W6bFFwPr~{8_b(L`|G(r%WB>s5|0e%a1O6@po&$&p35f^^h>3`Z zNJxlD$!RFa$;ikVs2@?%urRVdW?^JzX5$j#W#f3l$;{06jQ@$Sh`6{oE3cHCq^PWr zn7HVFD#0NkAt5Itr>CHx7iDK=7yW+@e>(tF#5lA#ig-9209+~@JSv>OJpk5!2n7E~ z{{#C!0uC-7J^>*SF$pQzKLhMT04@$59xgr}0RcY#KkJZxdH_BZ0X4gb65%7LH4%pg zjp#dM0Wqg?Z6{EF@&}igjput3Qd&BC21afkUOs*Saj?WQNh#^)FH}_3)HO5>42_IU zOwC}ncJ>aAPH<;0Zy#Sj|A4^o4-t`3(J_dmf*if0F$l zTvY$KaPjf+@QMDzg@fz&FX2()6R?XAQY%4;tUVrah`uAHQAQTjc9L+4>Hh%Qcutbi za*1znpZy2zzsUaYz~29Vk^N7w|HZWgAjiY`H+Xnd00qE>CLfK78ONlCnlk{#&zDb7 z%!?a4rH7+tm7>Q7$e)_>P{%I}*GS|KYrryTew+;}&%MQG9^k|61!`c;t?z8I?lG?S zhrTwgPoajYm9KTz(R6xE?l(^SX7T%VaQ=_7kjef%eO$`tD1a-?79<~^2L)e+^Wl^x zWy2eY;l&);aQ?6r{VfEaI3R_TuNZeX3q?{~iaVvRzx$3ja8iYae5x=hMW0@ON)G~{ z(RV-qV4D0g6S%v{;*Z`LR%7V}->r1yX)0O>#$Uo*_SqR6fn%#jo)M%DjbK;L>HLOAW>dH?1TA&BV{ut%t#SQw0y{sGz+N}67>o4+_63Dxv}&wj^w27bCY{?_UI zeY`3t*K{c%fKlL~CEc|$2y(jjwT z=yswvZU(PHPo;9t@MqRK%eWV_#a6|v7*mL)?wanv9Pg5zPwXF>Gg-kq(_6%xh)<>%f6puBo|D`Mr`O@RW|n za4#p4kSvf=H%q{s84sk?B_CrWxK2QB4qUS#y~}u9sHuie%(BhnC5|Rkq+0qL8YAz? z%y{=sYtR_tlcET(gr3Vv4O&Gb=HEum-rejJB3r);+X8>Jri$cGoyyzl7H(cuHr?uV-|n54Ax+qnGj{mAIj*c z&=uHz0#8$j7x3Xj-hHE%Mu}6X)uVa23|-?Fs+Qy2mY%WO2*%$ND1YIes&6#0Q&4uk z{}{v(QfQ9i&hiz}J_o&$XC(>DZfZX3(5lbNX>debEK%z*iYcDRz8 zK2@;QH%<f-89VHFIaelp?1yWmq^4Tckuem1VK7-vk#Rkhuh z1R|gO1;7)FiAPq)0u9X~BPuZ#1>9Lbs)ANwPVsg_??s6MKU1WqXsI)-&s?x-cAjy$ zVfNnpZn0{%T2vcbbC*nvpPbjZ`55PU`kmm13HXEwp@c?< z+-)ObS+fp9{!Ki8vD7(uR?`x8K=DO}O^A!!Whpdg=jFV(nyXjPs}Cxi^3oB!;0PaA z*+;3F3_5|ref(VyVFYHQhu%x>F;9!K13c@|hm;(jnOttba-tfq@IT=Tv&6kwf^0v8 zdv;%$E;+t>(JvF$uPAL|`)y#2MS3H{gDVs7N0kT^ks!L#Dr7E}I^zyoi11W;J?GOP zw!T8V#p&feSe@0I`xxc-Ok%kCf#!pC&20?KCBV0?F84#O2yC*vgsISxZq&i&Eii3! z-c&;6yh=Fer{!VyxKOCTRa$gc`Ni3+9dj+HNL5)GYR6l(jFeZws8I)1BjDiN=k!G7TB5k1jO54uy*p3(n^ zrRe*!61ZZX<3~G6i0M5F@6qi)=t}s zL)}D(X8Ux7(2H`%<|O*e#WBDjnqg16Dg1kqs*4lM^!F=I0YTo*+t~Aj2IVtVO736x zp#1hT;M}G$1R+gY!W!$g6|6;F7kJuPqbZ6RwDZ(3*!?U6GRJd&omkMt*1=G<`ch@O zI{jYsh3fHQC;DPkp8_^o+QjR5zb&WY$yl;gIs7D(>+$8VPImU?WY&>Z%IHS|g%`MOnU{b)?il&hru?IMiKb88Vvq2v=qQ%uQzy+SpE0fN z8Xi_I9AaH{WE_Qio-25&Y3>!Du`ZSjMoMJ_;Ux5xo^esS`aJm%E4%`VirdN6Yac9A zPT^)+FmmKN&O8XzMLemoqtYeo+AAAHT1scU5yl{XX1OXHOPegegiH1FqK@yL`3g0d z7H7tPQ$JX$?SVoqCKsl%mnTnM+!Fo-B>$S+EkAg82ay^15K4x6DJ?(w$fC3;cq{MH znLl{<5U94H^E1jxg)ikQ4u03Yt=2s7HrR2-Ln&6OGnr^&dZf-5dIN1K-iTDcD$Tj3 z?ekfUbuP(#cLmfLyVVM4OLw3W>H2NF{G2%~uH)Hnqx2wmX6F&%(PbJ___`Ow_|0=d zcPnfQ{EdAy5xvL!TJycY#;$w4X21WAP9S2XDPEoH0fo19rL_LJC`LCYAgduVlPOBE zD;Kl|0ec6Gnk!LoOJ`{-X)L8Bq41OwQT!z3wv5LBu6cr*mrRv?fV;|$>Uy)!w2cos zz9HXP1w4sZNX||+YlJ;l6xuN1$|dlAXhy$j*e`d)3rX=YwL_-%lxxRT>>4;+1 z*;iE=Et(tq9*PPF&c@WR`z!b>g8Id4rQ2jIHu^PtXIVIjya2Q0$fT_*);a2o2VUsSF;24CebQOogJbhqiU&h4e~ihM&`VGUFw zK}TKbCb(Qif@zZD*g&;tS&r7EOdETR`&+Pw%eN3qAz{})7MDLCQtnw{7$-gEpCd}1 zjTRJbP!CpXf2uu)i9V2KdR&`x3;|R+w!Q)vR(?4ur`e1@ z0zJwG*fZbx)-O{# z+}4g(V?`Y8?xPkVoxf0nZS$_K76mvNKFdojPGfq$@uio7+~~bDM&rr~=_0kKX_N&^ z^4Nn`-@GdszI>hN<^!`Ize>AQm!|RMzvb<~CakK?z9a1IFJY~h+=5(HF=b4zO&`9p zk0+W-1BYdk(Bvt)pw4(op13e;aT3U8d!ROiu!Ao~Y6k|2nq^V^*0UvrcesU)HSNB`Cxs39x?c!v-q{zeYPkL`BFMeJ;T%FM?Qja4m)|QC|ZOnn@ke1(q^NZ^rl27klIF_YB zCU&k>8iY0BW|}v06izRGCz@2guk=5ckK*=s8G&eM@_Sgt?+FiSdeBTO(jCP5mpy_G zEaVy4TmwNJ#gD7BKgE zCy=6culGmC^Krs}x(8xMD&SF$?5g-W9Et|2uIM-6K)wuL&2KfbS{^vVI)0DCjGTf! zeB)(%&Bd;DAMtiO4W3CO=S zWLbugqn~erhum|K!RQ4IQ z)*!hk#T(C6^(k8}(y0hOoo7x)4x9g${hb*+NVJn9gWHWzN9oQ*%d9nNs-sne+@G+m z+3Y6pwO^#q+UR+{f^dJ}cO>^ro0OZ~c*bP-IL6T`7LMhvHFTCL%^Z5^tb_UUDP7Jq zH&vg)?Un&2^4vjc-<hYOxw)J*~`jw7CRNr0e2m`{_u1 zvIALYQ_y8IyK|Sj9?V*U`vl(76enxxRZ8w}nC$vp3QjDFaf8fD?2OmS;z2Dx=2HDa z--4N@bk>yIc3UgX&t)={zSw&87`p_OwM6Km@>8#C_*x>a(>jj^u4_DL5vveu=P%@S zUlNCDO4khL$r3|Jx4UQFOdh)$@xKme$94o!)^S&4YS|5sc^p`k6(9TsoN2?Bv?b5a z#$hETzeMNy6n|Dgh*IAs!Ju7if!t>PjrS2AXoKO8HdtTzl;$-Typh;=N)1|PSTrTrzQX> zeb&aQRU`Vc9Em($tR1;Y)0Wg}IvO7I{nM-1o?STZ`{ej;nS* zl1E;9TwofK$>l2cXSPvxW6vOr2>2x_^JW?Fv^SfASVedyGQ)XL5NrH7B<=iJA*yaR ztMY4lnRe)6bwIso(YVlh@M#D{LCbRf)vb}nOCc9srGydW!Ub-N$Abxni?q_6Hv5&w zU08bH^q8EO5nG4s0}&Hs6f(j2?6^_-)Qj#XgK6@$3C5a9HBT#TM@ew^(J#`)xnhz> z5dfb9jWRw<9&Wi#g&fH*D&8_)kBu<(*iN==Qnz$q3Q~LCt4_KasyMcFV42pkk${!a za#n6REGwuYQy_O%-m=DSDflB17Y8TSSG$pGT)d!v58xg?87e%?G2d-<#S#KDAKAXaKdc4p=LS%5!{Bi7J)McK%7PB$@8*MTcvlY$SwuRfyLr+UjO~Wd{2ertydU{?$=4I#W zm}atf-s`($H;0NSv{?S+wD6WARvG;?#z{bjYN30kO@^@454gzoM;IhZiBmE1SPR+k z7?C~ymcyU}NFI+6MW*9@@i6NvD#duN1g!Nk$w@P*)6&nAerb0G{jQW@!w(m{pES;& zVM_{Sk4k^~N|)%sA}WT<|B``3)|Mkjyi8CdT~wui?!vTW-2+aYe5Zl~t}Q!4*`HA@ zTkr(26X+gU$$__qJ&*f&WgW4W?|2`6OyyRTrLwGffSTAdvK)74$vd7Ke|l{K?l`n! z&(TQTanl{j-)w4-Q-zo-;##LO#KnBKpo|eLYs~KH_~tEN*s^a1={XSW@j0H(KN@r8&+LYjat1Ru+PjsyhFiz*R8ZTYM1O7akR)`2(T5(hCE?}tP`*Df{ zuWpJts1ohTDN}k`q26o1BF8x~wdKlAjpI`(K^JljnA}kq%naB`oeBiKQD3^l>ou8S zPkyD%s`TAd;>OJ>sU^I4bo=m0X4fFnl2Idyc^)JzaU1uE#V=v5RhRqPx7=?sz2Nif z-$jHNjN{^?oo|97;7s~cqIS#1`?(mJlWS!=W8dN`PRHQuURdNy1;u!( z8MUS}49C1s{`ZNlw%Hw~oRX!YPZhpv0$<|wI3G5Ip2X%&)q&G}ETcG+k%kRUX`8o_ z#fcoXI|)iw+5AfVwsAuib1etAj?o2e9^~kq5jEx?>zY0DK6F8Yz!=hO978ZZVqL#U zOX@}BGkTxzqZVhta@{UOshPJ&xvs@E*99<+1^#?Tdtk7N^~mj6)9)-*-M5JF<#tf4_t%9tJYgy}6$r zCcmhWpApJlcOC4SFL07J{PgQBQ-EGhM-pX0wY$}ixD`)qZ!4WuGmFZbNi_XvZw{Da z#Xwc1igig$jUiR9wr^JwxAi6As+Mh~?klc!68vrNfoh$lxdTV4jBIL;STC!njU1Ay z!e@^PG??F1N#U(eHP(pdPYRpBa||DFledgH&kn{t>CnTe(Cgo6eEw6)+`5jYcAD9;?M-7W>Yn+%!4y0DI!?7yUzWv37t+H6W9{G^lFMd=RYtH;LKIKnvQ6kY)#i|Rf_ocZI^o z%>BvZU)4H4InE64H@jJLd^Ih~2k-g81&~9_+Slki3OIY!vPBeIZdU_!`^eKDlY4W& zGKHMQP#)slbFF4Eu9aeDkXyU%d(^ZuIxyG1>f<4W*T@`i@^~jl!v)-ki!HYPDKIZE zf*0vAfyz^nw?BqwKL};q=>bhUs_?>DjN1A`B_GeicSLxIRyhjd!N$y_#!qfybH%J= z7LE?Rmg0|MBz{keyRY@j1^_s(!JZca8XO$CL_D?LF)$XRt;4zpd(9PyHkj?(=h$(I z{=ky0RNM543vho;6jrj@_oE{lYg>MzOZ&`so4VhB0b;qzx5i3mPK~c9K84!L&Rdcg zL9dM_$DzvCL22T0xP~p}AA6P_ouXxvEwxlg^hs;BOkwVbDtCJ-`XvTR$X@ubS&Zim z<_Srxb;g!d)uGprFH)n@l3^(?O5A0hJLAP3`uRQI)SY07=>WIl&rh=MvXouTC(jN2 z$0quN{Khpgu2nBPI=cOY<+H{V1PR~AR)lC`46Eact>v~J;CYF`IdVw!yT+2D^HE|VBP(On*i+?{q9fxI$bIkP`C9B!P zH`_Jo2-UQre-0($-1Yj~C*U+|aFg*o3C z-#O`6FTR_ZZ99in_@Lw}Jp>FA!%VsJO#6VG$b{n^7WQ>RVeOk3srhG4o+6R`&Lt(C zLN(RBAY6TkwZ6}2%mzwAq%dr$(E5DWp8wyuEZ(k%Cs$z!L?#_hy=UYI;nX}Re2 zmd<;pAE4c+FW{JyF#WS+T9!&&l&~2E)(co1td58dHxV&hvOgh%_)QceERKd9j?+W6L{`d-*`$h^wkOctrU5Am8htgF>d^`M~IQBQ(71Lh1wOu2hO(x`96D%F1<2)c=;dw;|0KqZGgG?A5#w_$aue;TA^*PR_dZEnUCS+$&Ots>H-_@NvCp8I_IsC@ zr<@}JvZxD5YfD|7Ab#SNJn!pXPdZfatxu;$f$U=@W-7~HfiXgAEu%2T^@0+|!U2@V zjKikz8xpyrw+mnDH<0JMFSziI5ZmlYyH_erpIjBR)fpoHn1vlfbOekM zA(~~CbqnY1IucsD)VLyjassDu@>y;p^G+7;I>tavb8TS4@@IbmmFd4bd~WB(zYw)Q zvJI9IyZ*?!gP6+Yp^mQ}8S*a9MeKYfAF6lRHMJq5?Hiw}@~?RTpDb%s_8R7^4p*7X zpUMX@5v6|lNtH0v;6@I8F$D=LLRUMd)|j9OClfvobM{if)?U$5g|D@ez4$!4#-!e9 zoi|{j78H;_v^{KxN!Vl~#g-m1QnL!pZbl?Div5~5tkj&}5s9UpmnfR<@zrpN8z`r3 z#<+Ki$|eZLkWVp zowr5W|2{Wf8e3Z>6dz2$8aAl_O>6e z)6z<8$Yw=3zFE#i7R)pI-R5wtzXA?5TTV?nqLbb2frHLoiN$#DR}2C_(;^k33VxQLeD{l-su6rC5+NX7jR=hQwiS+h##}K| zwCtX&Ub=V{uXnZck`MV4T&#Ag-0 zzCcRNa;-FtWNshZAuL(x&ldqh@eSs5Ew7Mj$tT9(QJ&4Aoe#)tU&(JXjPeEYIWifB zbUvVgF)^ziu57n>T2yL$eK#!jtCMtam1bQ|%drdRON5q0&I7Mp%5qE|8T?$M{3DtU z2WRkFt}@hovT){`fa?75>QST*rw(?mUl)|}+W*3{@dpV8Ew~v!BxS5PcHb_b^%p>V z=sU%d$Y3H%!+>F->`Je1#csROXnOtp5sG7(yM{^tj~VHhVB=(5q-tbE@ZEGS@k`%g zyVg{=+oz-SiywP}7HzOE;`I2IiU6d;v$9f-X!4;fruy>EYEsEu4VmMy)|8e)Ov~P_ zG1}eTT~y0`SG$||<~MfUpLg5^UHtl(WKh2N%*f^kN54n2Rb1u?t3oDtZedZ)`Ze1- z-||CU{Sb)jODdA*X*}Ks8Zvc16LrK!A*2Kr$ia$31|2n+uVum-M>B1dmdQk2w;z4S zbs2!Ra;Nq>PK(izC<$KX31b#DXQ_aW4Cig^=HU~<0j!7f=*!|SC_c}J05yFXRPpV* ztO_mGC%Q@l)s{A{&-K+ixEuwKL7IQ|pFHJ!l{{6oZwzsFcH^Q?a|<|@G2$)hwmDp` z?b>oWFh1V6zgpiQ5-%4nzTOu&sWP`6lb%<7kS>1eXzUv!S*CA`fL)Etg_RT{Y{ZF2 zg%L@pK*I)c<&HV|rc%uP#{yPi2H28YDqbvN4+Z`x>ueVU>TZ68?gUQk&&yl97hUH( z$A^89eyunLVP-8tqF2u_o<-+_3}Cdj^ag)HXOC*^+)Ok00cZS*M!G1kyZr}ru^ z`;Ceqc085y+nJR)L`JN}$NOc{_!vGlPF2t-*UvGRf|%G^cMH2P|B{xEo_nk?btYl) z-{ljSwyiSKzQ!%}&jNES_oZ`dMTc^5LHF%OcAgd6erkM2i#d(>gX>1b=#7P1ecg)S2MbosR5?FAV8Ba@;A(k@C)8)ytk2_r*DYD6Es6NE{ zmOYzl`>k{qF=J3gSI1Bwi@U0}WjU==XMTgsj-~1}m z8o%=nNwW691qHQ7b3Yy(!KjDQ&W0X(?)jexI7D#X3XQDP+X3_setuSdV`xnp<0xH9k1dtZFP+^-)*<-_GZhy}< zhofbh-7+fLSCJA=x>>V?q1S3R;F2&xA|)uSdq*YtIu2sBMw`y{bY%l0Q!ApemWDVK zCgm&4V3aKGl}<)H=d>@+bnc|-65v8;m&kIM4t*MsQwbQ4zR(c=9qvIaZze^5VwK&6 zUW2Lmkg0G)8q@E#I6iW!9}#r7lS~tfvZ6QMNiIJ4%qh7YG$&tQJYHm#X{$exd}~lu zX2jtX)Ax0fyq2pE%|E7p$BxOYi^@A2f_mL%DA1iTy66L4@~LGA17 zF!!Z*`6Ku1L^0DQ2^A6n$x}I(Kv3#yT==!7RY6$d(j!q91JE z?jhbIoiqSpBBcW;0>hZ5-b%A#Tt>H9^I#Y}zU*4Kij0EJA6ay*X}SN#^l`L3l&mpj zDv^YuZ1%58UxH6I*5`dYQHCBuB0J6-`ngToJ9oU+!oFWK8J-I*bU!ecgSf9B#FTf~ zqzQIh$fs7vFuQax8`w2(k+y*2G=2_erW4rP1(X(jb6HsTX^k<=1+Y=w%$|^SCiRLA zzcmK4b~jUp3Y_%NiJhzVUZXd#Mv~B7g&J#^tliCP-Px_64|>lT@tSs+aZFB5tb%DR zk)eKbrH%EbXI#hhw}FODbhR&<^$9__{KKBhpAL%6o!;bWcC|G-;Mcoa{V7fQsc%6m zi0ZNRsL;YbSco!~1DSIe^$m+R)rX)a9>4t=NV@!~AzU|nSX(TwZ4V8mXwX~i-RY7# z{pZ;ug2#T;E94ektv~f;vN@r|tS;B!{)TBjRtl&2Xc=grBDDX+yLM~EY`}2`h~zDX>R_!c!8~H{ph#sMDBxZdFxMt{rd*OGGDZ?PYltGN2e4fuC-frBsv>e+{5?=nvbm6uJKi=t)7 zS%}Tjp>+y($JHu~>XWgF>HxUo+rek1RSiZCLl0~pWkGrI2fP*vaA{1`2)v+U#}s*> zR={xsl2@{LHdQg`WXn~vV?ynpTGtc)T{plc*gC=}UGJ-{q+*pS;oMajFjryoiQM5Z z+aG2|r2Hv8BP?Q4+wE=hcmWNQqx%MZr7L4D0*+(1Up&(=r2DByO{F82^!aDmY5{AX zcYn&KAAjHLPro(%e9ic2{Hg58_*{wl4^fGl4JdZzg9q!j0AX(M{RC0FknvFKQ(^7k z5%VRKJLiWt0QvXzcFn;o=X@0qZ-&O+FUA*8!~DTr)rO_4Ph0N}A$BV-ciy8#rS=Il z9_RRY`sr-aTrgvumSM{<%2l;^>v`lPHhn4I{5vs7+tQ|Aai{{-lwi-3 zlRHYqdv-XsX8!`Za;iz{DwgrN#N0dYOPtU**_$yPw;15UfyA2(NmKDMT zej7is*De}G(6A-;ijUOzN@4tzn)-058Y8Y$WY20(Ap&L>&F@s0K|ljlj3d>AX{r!# z3v%N=oF*-C=#jDoK~0oR~e3Rah_ z-_4brqbwG04XIa`FN&0aZxTJO18Hhb#2WkQe;P{tNIGm2V4` z)~&VDxZW{(+*gxwX?rsj;Nc_6I`$C<;$3pYF3RdLM> z*jMO_jEo`oBv?5HhK!25RPf9H!>Nl{GLPK1=~Hl#i=X6OskrD;NM~`_8;h)r zBN*Jwoe4QxPD8t}n1+ie3Lb_ir3Itn7jeFYVRGd>?V6J6-6oY%yk_kYyi*wv!lcjS zOwKM?%D_ zWD-+LQ_<0-RC?d^kyMI-vjMNIGlI|1cLJvbJpbNHqBA3A-je1SgRnB87}5JF`nRgB z7WyZ^lurjJfhe}6kP*jIFb}T|v9)D@Vvs()Uc4b=?*^4KdhjOc+E(4p>rU-wb=6Ww zVBgnN;YIVy^Yrub+bqT^&)<2!M{lOzCC{J^B67aooxdC^rk#jKvfc5S(ki%lv2)vY z@cuv-eQHkr#dHRo!Z+G4OvA?G_^{856izY!1ysFKfPJOS!T0BKlfQI+?@~(d?6Gez zQ1_}p&sq_0={;Ob9pcSx3wkG>VuP@u4p*Te{^xP|iiVLdUm2>Up-A|z1o)~{h)^Nm zaVmUAtSkOcgBw0dV}Qe7?4?2zrp#XqRl&m*<|i&hC<34ez7p$5LZ?E+6I^IKU*Sh` z7+)bunN*W6UkUXu!%af)N6Y93O{xHBpeg|RA{rol1y*YJmRbzvlif{x=CU BtegM< literal 0 HcmV?d00001 diff --git a/a2/pre.tex b/a2/pre.tex index 7970698..b9325ec 100644 --- a/a2/pre.tex +++ b/a2/pre.tex @@ -7,6 +7,8 @@ \usepackage{amsmath} % For nice tables \usepackage{listings} % For nice tables \usepackage{float} % For nice tables +\usepackage{graphicx} +\usepackage{xypic} \everymath{\displaystyle} diff --git a/a2/src/1.bak b/a2/src/1.bak new file mode 100644 index 0000000..2966704 --- /dev/null +++ b/a2/src/1.bak @@ -0,0 +1,126 @@ +#!/bin/bash +YICES=~/projects/yices-2.4.2/bin/yices-smt +AI=40 +BI=30 +CI=145 +AMAX=120 +BMAX=120 +CMAX=200 + +function generate { + ITERATIONS=$1 + TMAX=$2 + cat< a$i 0) + (> b$i 0) + (> c$i 0) + (or ;-- ITERATION $i + (and ;-- SPECIAL CASE FOR STATE S(0) + (= l$i 0) + (= d$i 0) + (= t$i $TMAX) + (= a$i (- a$((i-1)) p$i)) + (= b$i (- b$((i-1)) p$i)) + (= c$i (- c$((i-1)) p$i)) + (or + (and ;-- CAME FROM A + (= l$((i-1)) 1) + (= p$i 29) + ) + (and ;-- CAME FROM B + (= l$((i-1)) 2) + (= p$i 21) + ) + ) + ) + (and ;-- CASE FOR STATE A(1) + (= l$i 1) + (>= d$i 0) (<= d$i t$((i-1))) + (<= d$i (+ p$i (- $AMAX a$((i-1))))) + (= t$i (- t$((i-1)) d$i)) + (= a$i (- (+ a$((i-1)) d$i) p$i)) + + (= b$i (- b$((i-1)) p$i)) + (= c$i (- c$((i-1)) p$i)) + (or + (and ;-- CAME FROM S(0) + (= l$((i-1)) 0) + (= p$i 29) + ) (and ;-- CAME FROM B(2) + (= p$i 17) + (= l$((i-1)) 2) + ) (and ;-- CAME FROM C(3) + (= p$i 32) + (= l$((i-1)) 3) + ) + ) + ) + (and ;-- CASE FOR STATE B(2) + (= l$i 3) + (>= d$i 0) (<= d$i t$((i-1))) + (<= d$i (+ p$i (- $BMAX b$((i-1))))) + (= t$i (- t$((i-1)) d$i)) + (= b$i (- (+ b$((i-1)) d$i) p$i)) + + (= a$i (- a$((i-1)) p$i)) + (= c$i (- c$((i-1)) p$i)) + + (or + (and ;-- CAME FROM S(0) + (= l$((i-1)) 0) + (= p$i 21) + ) (and ;-- CAME FROM A(1) + (= l$((i-1)) 1) + (= p$i 17) + ) (and ;-- CAME FROM C(3) + (= l$((i-1)) 3) + (= p$i 37) + ) + ) + ) + (and ;-- CASE FOR STATE C(3) + (= l$i 3) + (>= d$i 0) (<= d$i t$((i-1))) + (<= d$i (+ p$i (- $CMAX c$((i-1))))) + (= t$i (- t$((i-1)) d$i)) + (= c$i (- (+ c$((i-1)) d$i) p$i)) + (= a$i (- a$((i-1)) p$i)) + (= b$i (- b$((i-1)) p$i)) + (or + (and ;-- CAME FROM A(1) + (= l$((i-1)) 1) + (= p$i 32) + ) (and ;-- CAME FROM B(2) + (= l$((i-1)) 2) + (= p$i 37) + ) + ) + ) + ) +GEN + done + cat< $1 -generate diff --git a/a2/src/1a.bash b/a2/src/1a.bash new file mode 100755 index 0000000..1724514 --- /dev/null +++ b/a2/src/1a.bash @@ -0,0 +1,166 @@ +#!/bin/bash +YICES=~/projects/yices-2.4.2/bin/yices-smt +AI=40 +BI=30 +CI=145 +AMAX=120 +BMAX=120 +CMAX=200 + +function generate { + ITERATIONS=$1 + TMAX=$2 + cat< a$i 0) + (> b$i 0) + (> c$i 0) + (>= d$i 0) + (<= d$i $TMAX) + (>= t$i 0) + (<= t$i $TMAX) + (or ;-- ITERATION $i + (and ;-- WAS IN S + (= l$((i-1)) 0) + (or + (and ; now in A + (= l$i 1) + (<= d$i (+ 29 (- $AMAX a$((i-1))))) + (= a$i (+ (- a$((i-1)) 29) d$i)) + + (= b$i (- b$((i-1)) 29)) + (= c$i (- c$((i-1)) 29)) + + (= t$i (- t$((i-1)) d$i)) + ) (and ; now in B + (= l$i 2) + (<= d$i (+ 21 (- $BMAX b$((i-1))))) + (= b$i (+ (- b$((i-1)) 21) d$i)) + + (= a$i (- a$((i-1)) 21)) + (= c$i (- c$((i-1)) 21)) + + (= t$i (- t$((i-1)) d$i)) + ) + ) + ) + (and ;-- WAS IN A + (= l$((i-1)) 1) + (or + (and ; now in S + (= l$i 0) + (= d$i 0) + + (= a$i (- a$((i-1)) 29)) + (= b$i (- b$((i-1)) 29)) + (= c$i (- c$((i-1)) 29)) + + (= t$i $TMAX) + ) (and ; now in B + (= l$i 2) + (<= d$i (+ 17 (- $BMAX b$((i-1))))) + (= b$i (+ (- b$((i-1)) 17) d$i)) + + (= a$i (- a$((i-1)) 17)) + (= c$i (- c$((i-1)) 17)) + + (= t$i (- t$((i-1)) d$i)) + ) (and ; now in C + (= l$i 3) + + (<= d$i (+ 32 (- $CMAX c$((i-1))))) + (= c$i (+ (- c$((i-1)) 32) d$i)) + + (= a$i (- a$((i-1)) 32)) + (= b$i (- b$((i-1)) 32)) + + (= t$i (- t$((i-1)) d$i)) + ) + ) + ) + (and ;-- WAS IN B + (= l$((i-1)) 2) + (or + (and ; now in S + (= l$i 0) + (= d$i 0) + + (= a$i (- a$((i-1)) 21)) + (= b$i (- b$((i-1)) 21)) + (= c$i (- c$((i-1)) 21)) + + (= t$i $TMAX) + ) (and ; now in A + (= l$i 1) + (<= d$i (+ 17 (- $AMAX a$((i-1))))) + (= a$i (+ (- a$((i-1)) 17) d$i)) + + (= b$i (- b$((i-1)) 17)) + (= c$i (- c$((i-1)) 17)) + + (= t$i (- t$((i-1)) d$i)) + ) (and ; now in C + (= l$i 3) + (<= d$i (+ 37 (- $CMAX c$((i-1))))) + (= c$i (+ (- c$((i-1)) 37) d$i)) + + (= a$i (- a$((i-1)) 37)) + (= b$i (- b$((i-1)) 37)) + + (= t$i (- t$((i-1)) d$i)) + ) + ) + ) + (and ;-- WAS IN C + (= l$((i-1)) 3) + (or + (and ; now in A + (= l$i 1) + (<= d$i (+ 32 (- $AMAX a$((i-1))))) + (= a$i (+ (- a$((i-1)) 32) d$i)) + + (= b$i (- b$((i-1)) 32)) + (= c$i (- c$((i-1)) 32)) + + (= t$i (- t$((i-1)) d$i)) + ) (and ; now in B + (= l$i 2) + (<= d$i (+ 37 (- $BMAX b$((i-1))))) + (= b$i (+ (- b$((i-1)) 37) d$i)) + + (= a$i (- a$((i-1)) 37)) + (= c$i (- c$((i-1)) 37)) + + (= t$i (- t$((i-1)) d$i)) + ) + ) + ) + ) +GEN + done + echo "(or" + for i in $(seq 0 $ITERATIONS); do + for j in $(seq $((i+1)) $ITERATIONS); do + echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))" + done + done + echo ")))" +} +it=1 +while generate $it 318 | $YICES -m | pee sort "grep -q unsat" +do + echo $((it++)) +done diff --git a/a2/src/1b.bash b/a2/src/1b.bash new file mode 100755 index 0000000..17a3e78 --- /dev/null +++ b/a2/src/1b.bash @@ -0,0 +1,127 @@ +#!/bin/bash +YICES=~/projects/yices-2.4.2/bin/yices-smt +AI=40 +BI=30 +CI=145 +AMAX=120 +BMAX=120 +CMAX=200 + +function generate { + ITERATIONS=$1 + TMAX=$2 + cat< a$i 0) + (> b$i 0) + (> c$i 0) + (or ;-- ITERATION $i + (and ;-- SPECIAL CASE FOR STATE S(0) + (= l$i 0) + (= d$i 0) + (= t$i $TMAX) + (or + (and ;-- CAME FROM A + (= l$((i-1)) 1) + (= a$i (- a$((i-1)) 29)) + (= b$i (- b$((i-1)) 29)) + (= c$i (- c$((i-1)) 29)) + ) + (and ;-- CAME FROM B + (= l$((i-1)) 2) + (= a$i (- a$((i-1)) 21)) + (= b$i (- b$((i-1)) 21)) + (= c$i (- c$((i-1)) 21)) + ) + ) + ) + (and ;-- CASE FOR STATE A(1) + (= l$i 1) + (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $AMAX a$((i-1)))) + (= t$i (- t$((i-1)) d$i)) (= a$i (+ a$((i-1)) d$i)) + + (or + (and ;-- CAME FROM S(0) + (= l$((i-1)) 0) + (= b$i (- b$((i-1)) 29)) + (= c$i (- c$((i-1)) 29)) + ) (and ;-- CAME FROM B(2) + (= l$((i-1)) 2) + (= b$i (- b$((i-1)) 17)) + (= c$i (- c$((i-1)) 17)) + ) (and ;-- CAME FROM C(3) + (= l$((i-1)) 3) + (= b$i (- b$((i-1)) 32)) + (= c$i (- c$((i-1)) 32)) + ) + ) + ) + (and ;-- CASE FOR STATE B(2) + (= l$i 2) + (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $BMAX b$((i-1)))) + (= t$i (- t$((i-1)) d$i)) (= b$i (+ b$((i-1)) d$i)) + + (or + (and ;-- CAME FROM S(0) + (= l$((i-1)) 0) + (= a$i (- a$((i-1)) 21)) + (= c$i (- c$((i-1)) 21)) + ) (and ;-- CAME FROM A(1) + (= l$((i-1)) 1) + (= a$i (- a$((i-1)) 17)) + (= c$i (- c$((i-1)) 17)) + ) (and ;-- CAME FROM C(3) + (= l$((i-1)) 3) + (= a$i (- a$((i-1)) 37)) + (= c$i (- c$((i-1)) 37)) + ) + ) + ) + (and ;-- CASE FOR STATE C(3) + (= l$i 3) + (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $CMAX c$((i-1)))) + (= t$i (- t$((i-1)) d$i)) (= c$i (+ c$((i-1)) d$i)) + + (or + (and ;-- CAME FROM A(1) + (= l$((i-1)) 1) + (= a$i (- a$((i-1)) 32)) + (= b$i (- b$((i-1)) 32)) + ) (and ;-- CAME FROM B(2) + (= l$((i-1)) 2) + (= a$i (- a$((i-1)) 37)) + (= b$i (- b$((i-1)) 37)) + ) + ) + ) + ) +GEN + done + echo "(or" + for i in $(seq 0 $ITERATIONS); do + for j in $(seq $((i+1)) $ITERATIONS); do + echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))" + done + done + echo ")))" +} + +it=1 +while generate $it 320 | $YICES -m | pee sort "grep unsat" +do + it=$((it+1)) +done +echo $it diff --git a/a2/src/4/4.model b/a2/src/4/4.model index 3b52ae7..e69de29 100644 --- a/a2/src/4/4.model +++ b/a2/src/4/4.model @@ -1,1059 +0,0 @@ -sat - -(= i1x2y0 true) -(= i4x2y1 false) -(= i1x2y3 true) -(= i11x2y5 false) -(= i31x6y2 false) -(= i26x0y3 true) -(= i10x3y6 true) -(= i13x3y5 true) -(= i20x0y4 false) -(= i30x2y2 false) -(= i6x2y3 true) -(= i6x5y3 true) -(= i0x4y0 true) -(= i17x2y0 false) -(= i20x3y1 false) -(= i24x5y4 false) -(= i16x4y6 false) -(= i26x0y4 false) -(= i26x2y5 false) -(= i14x2y6 false) -(= i29x1y4 true) -(= i1x0y4 true) -(= i21x3y3 false) -(= i31x4y2 false) -(= i18x6y3 false) -(= i3x1y2 true) -(= i4x3y6 true) -(= i9x1y3 true) -(= i16x6y4 false) -(= i18x6y4 false) -(= i19x1y4 true) -(= i14x3y0 false) -(= i9x3y3 false) -(= i3x5y4 true) -(= i21x4y5 false) -(= i14x4y5 false) -(= i30x5y2 false) -(= i22x4y6 false) -(= i6x0y3 true) -(= i18x2y5 false) -(= i27x1y2 false) -(= i26x2y1 false) -(= i24x4y6 false) -(= i31x4y4 false) -(= i19x5y3 false) -(= i15x1y4 false) -(= i9x3y6 true) -(= i0x3y1 true) -(= i14x6y2 false) -(= i28x0y3 false) -(= i0x6y2 true) -(= i9x5y3 true) -(= i13x0y4 true) -(= i11x1y3 true) -(= i7x3y3 false) -(= i21x2y4 false) -(= i15x5y4 false) -(= i27x4y2 false) -(= i6x0y2 true) -(= i14x3y4 false) -(= i9x0y4 true) -(= i20x6y4 false) -(= i7x1y4 true) -(= i21x1y2 true) -(= i24x4y5 false) -(= i30x4y5 false) -(= i31x1y4 false) -(= i8x4y1 false) -(= i1x3y5 true) -(= i3x2y6 true) -(= i13x1y4 true) -(= i2x6y2 true) -(= i9x4y1 false) -(= i29x0y2 false) -(= i15x0y4 false) -(= i28x5y2 false) -(= i24x3y6 false) -(= i18x3y1 false) -(= i19x4y6 false) -(= i22x3y1 false) -(= i19x4y1 false) -(= i13x2y0 false) -(= i27x3y3 false) -(= i12x3y5 true) -(= i16x2y0 false) -(= i10x4y0 false) -(= i27x2y0 false) -(= i11x3y4 true) -(= i9x3y0 true) -(= i2x3y6 true) -(= i12x6y2 true) -(= i18x2y6 true) -(= i23x3y4 false) -(= i13x0y2 true) -(= i31x2y4 false) -(= i13x3y6 true) -(= i2x0y4 true) -(= i8x4y6 true) -(= i17x5y4 true) -(= i18x3y2 true) -(= i6x1y2 true) -(= i16x1y3 true) -(= i18x3y3 false) -(= i27x0y4 false) -(= i6x2y5 true) -(= i24x3y0 false) -(= i9x3y1 false) -(= i11x5y4 true) -(= i3x2y3 true) -(= i15x0y2 true) -(= i27x3y2 false) -(= i12x6y3 true) -(= i5x0y2 true) -(= i29x0y3 false) -(= i30x4y6 false) -(= i13x3y3 false) -(= i28x4y5 false) -(= i31x4y3 false) -(= i2x4y5 true) -(= i8x6y4 false) -(= i13x3y1 false) -(= i10x4y1 false) -(= i17x2y1 false) -(= i26x3y2 false) -(= i30x4y0 false) -(= i19x6y3 false) -(= i24x2y1 false) -(= i12x1y4 true) -(= i29x3y6 false) -(= i23x0y3 true) -(= i6x4y3 true) -(= i15x3y5 true) -(= i23x0y4 false) -(= i29x6y2 false) -(= i21x4y4 false) -(= i14x4y3 true) -(= i29x3y0 false) -(= i24x6y3 false) -(= i25x3y3 false) -(= i5x2y2 true) -(= i30x5y4 false) -(= i16x0y4 false) -(= i2x5y3 false) -(= i3x1y3 true) -(= i12x2y0 false) -(= i16x2y5 false) -(= i25x2y6 true) -(= i7x0y3 true) -(= i10x3y2 true) -(= i12x3y1 false) -(= i26x6y3 false) -(= i27x6y3 false) -(= i6x1y4 true) -(= i20x3y3 false) -(= i27x6y4 false) -(= i29x2y6 false) -(= i3x6y3 true) -(= i24x6y2 false) -(= i1x5y4 true) -(= i27x5y4 false) -(= i10x2y4 true) -(= i30x3y6 false) -(= i26x2y3 false) -(= i14x2y3 true) -(= i28x3y5 true) -(= i5x0y4 true) -(= i24x1y2 true) -(= i2x1y3 true) -(= i4x1y3 true) -(= i7x3y0 true) -(= i15x3y4 false) -(= i25x2y5 false) -(= i12x3y2 true) -(= i22x6y4 false) -(= i14x4y6 true) -(= i14x2y1 false) -(= i22x4y1 false) -(= i24x0y4 false) -(= i26x3y5 true) -(= i4x1y4 true) -(= i23x5y2 false) -(= i30x2y6 false) -(= i16x4y4 true) -(= i25x2y2 true) -(= i0x4y3 true) -(= i6x4y5 false) -(= i20x3y2 true) -(= i30x6y3 false) -(= i20x2y0 false) -(= i29x3y5 true) -(= i12x4y3 true) -(= i22x2y5 false) -(= i12x5y3 true) -(= i28x3y3 false) -(= i23x4y1 false) -(= i24x5y3 false) -(= i20x3y5 true) -(= i8x2y0 true) -(= i17x3y0 false) -(= i9x6y4 false) -(= i2x4y6 true) -(= i29x0y4 false) -(= i13x0y3 true) -(= i8x2y2 true) -(= i14x2y5 false) -(= i17x2y3 true) -(= i11x3y0 false) -(= i24x4y1 false) -(= i14x4y0 true) -(= i27x4y4 false) -(= i4x5y4 true) -(= i23x3y3 false) -(= i9x1y2 true) -(= i3x6y2 true) -(= i30x0y2 false) -(= i3x2y1 false) -(= i11x4y4 false) -(= i6x2y2 true) -(= i15x2y4 true) -(= i23x4y4 false) -(= i26x1y3 true) -(= i4x0y3 true) -(= i28x0y4 false) -(= i29x6y3 false) -(= i2x4y0 true) -(= i0x3y0 true) -(= i14x3y3 false) -(= i30x4y1 false) -(= i11x6y4 false) -(= i0x3y6 true) -(= i12x1y3 true) -(= i8x1y3 true) -(= i28x2y2 false) -(= i4x2y5 true) -(= i26x1y4 true) -(= i6x4y6 true) -(= i21x0y3 true) -(= i21x4y3 false) -(= i26x4y0 false) -(= i24x3y3 false) -(= i18x4y1 false) -(= i21x3y0 false) -(= i25x2y1 false) -(= i26x3y6 false) -(= i27x1y4 true) -(= i27x4y5 false) -(= i28x2y6 true) -(= i27x3y6 false) -(= i19x2y6 true) -(= i1x2y1 true) -(= i0x0y3 true) -(= i25x4y6 false) -(= i4x1y2 true) -(= i0x2y0 true) -(= i17x6y3 false) -(= i11x5y2 true) -(= i7x6y3 true) -(= i12x3y3 false) -(= i9x0y2 true) -(= i21x2y2 false) -(= i4x2y3 true) -(= i16x3y1 false) -(= i21x3y1 false) -(= i24x4y2 false) -(= i4x0y4 true) -(= i7x3y5 true) -(= i11x4y3 true) -(= i9x2y3 true) -(= i20x2y6 true) -(= i18x4y5 false) -(= i2x0y2 true) -(= i13x4y0 true) -(= i25x3y6 false) -(= i27x3y5 true) -(= i4x3y3 true) -(= i31x4y5 false) -(= i10x0y2 true) -(= i20x2y5 false) -(= i9x4y6 true) -(= i1x3y1 true) -(= i28x1y2 false) -(= i28x6y2 false) -(= i20x6y2 false) -(= i5x2y5 true) -(= i1x0y2 true) -(= i1x4y5 true) -(= i1x1y3 true) -(= i6x0y4 true) -(= i14x5y2 true) -(= i9x6y2 true) -(= i19x0y3 true) -(= i21x3y2 true) -(= i26x4y2 false) -(= i24x1y3 true) -(= i20x4y1 false) -(= i5x3y6 true) -(= i23x1y4 true) -(= i1x6y2 true) -(= i23x5y3 false) -(= i12x2y1 false) -(= i2x0y3 true) -(= i18x4y6 false) -(= i7x4y0 false) -(= i1x1y2 true) -(= i0x2y1 true) -(= i1x5y3 false) -(= i1x3y0 true) -(= i8x4y0 false) -(= i10x5y4 true) -(= i4x0y2 true) -(= i26x3y3 false) -(= i0x4y6 true) -(= i7x6y2 true) -(= i17x1y3 true) -(= i13x4y4 false) -(= i3x4y1 true) -(= i5x3y4 true) -(= i21x3y5 true) -(= i28x4y0 false) -(= i22x3y5 true) -(= i14x3y6 true) -(= i2x3y5 true) -(= i29x4y6 false) -(= i12x2y2 true) -(= i30x3y3 false) -(= i17x5y2 false) -(= i4x3y5 true) -(= i11x3y3 false) -(= i30x3y5 true) -(= i14x5y4 true) -(= i8x5y2 true) -(= i25x4y0 false) -(= i9x4y4 false) -(= i4x3y0 true) -(= i3x4y3 true) -(= i11x2y6 false) -(= i18x3y5 true) -(= i12x4y0 true) -(= i11x3y5 true) -(= i28x4y3 false) -(= i14x3y2 true) -(= i16x5y3 true) -(= i6x5y4 true) -(= i2x3y4 true) -(= i19x5y4 false) -(= i1x6y4 true) -(= i15x5y2 true) -(= i1x3y4 true) -(= i3x2y5 true) -(= i20x5y4 false) -(= i23x0y2 true) -(= i23x2y5 false) -(= i3x4y6 true) -(= i6x4y4 false) -(= i7x2y1 false) -(= i26x4y5 false) -(= i25x4y1 false) -(= i10x2y2 true) -(= i23x2y1 true) -(= i9x6y3 true) -(= i8x3y1 false) -(= i13x1y3 true) -(= i14x2y0 false) -(= i7x4y5 false) -(= i15x1y2 true) -(= i21x2y1 true) -(= i1x2y6 true) -(= i17x2y6 true) -(= i12x1y2 true) -(= i22x1y2 true) -(= i12x5y4 true) -(= i1x6y3 true) -(= i25x2y4 false) -(= i25x4y5 false) -(= i7x3y4 true) -(= i10x3y1 false) -(= i25x4y2 false) -(= i18x0y4 false) -(= i26x5y3 false) -(= i11x2y4 true) -(= i10x2y1 false) -(= i18x2y3 true) -(= i24x2y4 false) -(= i29x2y5 false) -(= i28x2y5 true) -(= i11x4y2 true) -(= i7x3y2 true) -(= i16x4y5 false) -(= i27x0y3 false) -(= i16x6y3 false) -(= i19x3y2 true) -(= i20x5y2 false) -(= i12x3y6 true) -(= i22x3y6 false) -(= i27x2y1 false) -(= i13x3y4 false) -(= i24x3y1 false) -(= i10x6y2 true) -(= i0x3y5 true) -(= i21x5y4 false) -(= i17x0y4 false) -(= i7x0y4 true) -(= i8x6y2 true) -(= i10x1y3 true) -(= i11x3y2 true) -(= i24x4y3 false) -(= i13x4y5 false) -(= i13x6y2 false) -(= i25x5y3 false) -(= i13x5y2 true) -(= i13x6y4 true) -(= i15x2y2 true) -(= i31x2y6 false) -(= i25x1y2 false) -(= i18x0y3 true) -(= i29x2y4 true) -(= i0x2y5 true) -(= i15x4y5 false) -(= i16x2y1 false) -(= i29x4y2 false) -(= i30x3y1 false) -(= i28x5y3 false) -(= i13x4y1 false) -(= i13x4y3 true) -(= i22x5y2 false) -(= i14x0y3 true) -(= i20x6y3 false) -(= i7x2y2 true) -(= i22x2y6 true) -(= i18x4y2 true) -(= i10x4y3 true) -(= i24x3y2 false) -(= i16x4y2 true) -(= i20x4y5 false) -(= i24x2y6 true) -(= i17x0y3 true) -(= i26x2y2 false) -(= i31x3y2 false) -(= i23x2y4 false) -(= i18x0y2 true) -(= i24x2y0 false) -(= i5x2y6 true) -(= i25x1y4 true) -(= i29x3y3 false) -(= i13x5y3 true) -(= i17x1y2 true) -(= i27x2y5 false) -(= i22x5y4 false) -(= i8x2y6 true) -(= i30x2y5 false) -(= i6x6y2 true) -(= i28x4y6 false) -(= i3x6y4 true) -(= i29x2y2 false) -(= i22x5y3 false) -(= i26x3y4 false) -(= i11x0y2 true) -(= i6x3y2 true) -(= i11x2y2 true) -(= i0x3y3 false) -(= i1x4y1 true) -(= i11x4y0 true) -(= i12x0y4 true) -(= i10x2y6 false) -(= i28x6y4 false) -(= i17x3y3 false) -(= i20x2y4 false) -(= i4x4y5 true) -(= i5x1y3 true) -(= i0x2y4 true) -(= i15x2y1 false) -(= i26x5y2 false) -(= i25x3y4 false) -(= i3x1y4 true) -(= i26x3y1 false) -(= i8x6y3 true) -(= i19x0y2 true) -(= i11x4y1 false) -(= i19x3y4 false) -(= i28x4y2 false) -(= i2x5y4 true) -(= i23x6y3 false) -(= i21x4y6 false) -(= i10x4y2 true) -(= i26x3y0 false) -(= i6x3y4 true) -(= i25x3y5 true) -(= i17x4y0 true) -(= i27x2y3 true) -(= i29x5y2 false) -(= i12x2y4 false) -(= i0x2y3 true) -(= i24x4y0 false) -(= i13x4y6 true) -(= i31x2y5 false) -(= i30x2y3 false) -(= i4x4y3 true) -(= i14x5y3 true) -(= i7x3y1 false) -(= i17x4y2 true) -(= i22x2y1 true) -(= i0x0y2 true) -(= i11x4y6 true) -(= i7x0y2 true) -(= i4x2y6 true) -(= i22x3y0 false) -(= i9x4y0 false) -(= i23x6y2 false) -(= i9x2y0 true) -(= i16x6y2 false) -(= i15x2y0 false) -(= i29x2y0 false) -(= i2x3y1 true) -(= i5x4y3 false) -(= i3x3y5 true) -(= i9x2y5 true) -(= i27x6y2 false) -(= i22x6y3 false) -(= i1x1y4 true) -(= i23x1y3 true) -(= i5x5y3 true) -(= i17x4y5 false) -(= i17x0y2 true) -(= i18x3y0 false) -(= i6x4y2 true) -(= i24x0y2 true) -(= i0x2y2 true) -(= i7x3y6 true) -(= i20x2y3 false) -(= i31x5y2 false) -(= i22x3y4 false) -(= i1x2y4 true) -(= i16x4y0 true) -(= i19x6y4 false) -(= i8x4y4 false) -(= i19x3y0 false) -(= i30x6y4 false) -(= i22x0y3 true) -(= i4x4y1 false) -(= i29x3y2 false) -(= i8x5y4 true) -(= i5x1y4 true) -(= i29x1y3 false) -(= i7x2y5 true) -(= i10x0y4 true) -(= i5x2y1 false) -(= i8x1y4 true) -(= i13x2y6 false) -(= i14x2y4 true) -(= i22x3y2 true) -(= i22x4y3 false) -(= i8x4y5 false) -(= i24x2y3 true) -(= i7x4y3 true) -(= i7x4y4 true) -(= i5x3y3 false) -(= i28x4y4 false) -(= i3x5y2 true) -(= i30x0y3 false) -(= i10x1y2 true) -(= i8x5y3 true) -(= i0x4y4 true) -(= i3x4y0 true) -(= i31x2y3 false) -(= i18x4y4 false) -(= i6x2y6 true) -(= i28x3y4 false) -(= i16x3y5 true) -(= i19x3y1 false) -(= i22x3y3 false) -(= i24x2y2 false) -(= i24x3y5 true) -(= i5x4y0 false) -(= i12x4y1 false) -(= i17x2y2 true) -(= i28x2y1 false) -(= i16x2y4 true) -(= i24x4y4 false) -(= i6x6y3 true) -(= i8x2y3 true) -(= i3x3y4 true) -(= i22x4y4 false) -(= i1x2y2 true) -(= i5x0y3 true) -(= i8x4y3 true) -(= i20x1y3 true) -(= i21x6y3 false) -(= i5x4y1 false) -(= i8x0y2 true) -(= i19x2y1 false) -(= i21x4y0 true) -(= i23x5y4 false) -(= i15x0y3 true) -(= i10x1y4 false) -(= i29x6y4 false) -(= i5x3y0 true) -(= i13x4y2 true) -(= i27x0y2 false) -(= i17x4y3 true) -(= i26x4y6 false) -(= i10x5y3 true) -(= i29x5y4 false) -(= i18x4y3 true) -(= i4x2y4 true) -(= i1x4y0 true) -(= i10x2y5 false) -(= i25x0y4 false) -(= i5x4y2 true) -(= i30x4y3 false) -(= i2x2y4 true) -(= i25x3y1 false) -(= i3x3y1 false) -(= i12x3y4 false) -(= i15x3y1 false) -(= i2x1y2 true) -(= i22x4y5 false) -(= i17x4y4 true) -(= i6x4y0 false) -(= i17x6y2 false) -(= i18x6y2 false) -(= i5x3y2 true) -(= i7x2y6 true) -(= i21x6y4 false) -(= i25x6y2 false) -(= i2x4y2 false) -(= i31x5y4 false) -(= i3x3y3 true) -(= i14x4y2 true) -(= i19x6y2 false) -(= i25x5y4 false) -(= i19x3y5 true) -(= i5x3y5 true) -(= i7x2y4 true) -(= i15x1y3 true) -(= i16x4y1 false) -(= i3x0y4 true) -(= i8x2y5 true) -(= i13x3y2 true) -(= i25x0y3 true) -(= i5x5y4 true) -(= i13x2y3 true) -(= i20x4y0 true) -(= i4x6y2 true) -(= i21x3y6 false) -(= i22x1y3 true) -(= i1x0y3 true) -(= i1x4y3 false) -(= i8x3y5 true) -(= i25x2y0 false) -(= i13x2y5 false) -(= i4x6y4 true) -(= i4x4y4 true) -(= i20x2y2 false) -(= i21x4y2 false) -(= i4x2y2 true) -(= i31x5y3 false) -(= i15x4y2 true) -(= i28x1y3 false) -(= i25x5y2 false) -(= i7x1y3 true) -(= i13x3y0 false) -(= i16x3y4 false) -(= i23x3y5 true) -(= i0x3y2 true) -(= i15x3y3 false) -(= i1x4y6 true) -(= i2x3y3 true) -(= i19x4y5 false) -(= i7x5y3 true) -(= i6x3y6 true) -(= i19x4y0 true) -(= i4x3y1 false) -(= i16x1y4 false) -(= i27x3y0 false) -(= i13x6y3 false) -(= i17x3y5 true) -(= i6x6y4 true) -(= i0x1y4 true) -(= i23x4y6 false) -(= i23x4y2 false) -(= i16x0y3 true) -(= i17x6y4 false) -(= i29x4y0 false) -(= i31x3y1 false) -(= i13x2y2 true) -(= i15x4y3 true) -(= i18x1y3 true) -(= i12x0y3 true) -(= i15x4y4 true) -(= i31x3y0 false) -(= i11x2y3 true) -(= i3x3y2 true) -(= i15x2y3 true) -(= i27x4y3 false) -(= i27x5y3 false) -(= i22x1y4 true) -(= i19x2y2 true) -(= i31x2y1 false) -(= i21x0y4 false) -(= i18x1y4 false) -(= i10x3y0 true) -(= i18x4y0 true) -(= i3x2y2 true) -(= i5x2y0 true) -(= i10x0y3 true) -(= i9x5y2 true) -(= i0x5y3 true) -(= i15x3y6 true) -(= i18x1y2 true) -(= i31x3y4 false) -(= i19x3y3 false) -(= i30x3y0 false) -(= i27x4y1 false) -(= i9x5y4 true) -(= i4x2y0 true) -(= i26x2y0 false) -(= i3x2y4 true) -(= i30x2y1 false) -(= i22x0y4 false) -(= i3x0y2 true) -(= i15x4y1 false) -(= i9x1y4 false) -(= i26x4y3 false) -(= i6x3y3 false) -(= i8x2y1 false) -(= i17x2y4 true) -(= i19x2y3 true) -(= i22x2y4 false) -(= i31x3y6 false) -(= i7x2y3 true) -(= i29x4y4 false) -(= i0x5y4 true) -(= i21x2y3 false) -(= i30x4y2 false) -(= i4x5y2 true) -(= i11x1y2 true) -(= i22x2y3 false) -(= i3x3y0 true) -(= i17x3y1 false) -(= i6x3y5 true) -(= i26x4y1 false) -(= i3x4y4 true) -(= i29x3y4 false) -(= i25x4y4 false) -(= i4x4y0 false) -(= i14x4y1 false) -(= i19x3y6 false) -(= i8x0y4 true) -(= i23x4y3 false) -(= i21x0y2 true) -(= i6x5y2 true) -(= i25x3y2 false) -(= i16x2y6 true) -(= i6x4y1 false) -(= i14x1y3 true) -(= i29x3y1 false) -(= i0x1y3 true) -(= i13x2y4 false) -(= i18x3y4 true) -(= i0x2y6 true) -(= i2x3y2 true) -(= i28x4y1 false) -(= i2x1y4 true) -(= i0x4y2 true) -(= i28x3y6 false) -(= i6x1y3 true) -(= i18x2y2 true) -(= i29x4y3 false) -(= i30x0y4 false) -(= i2x2y3 true) -(= i15x2y5 false) -(= i8x3y6 true) -(= i19x2y4 false) -(= i20x4y4 false) -(= i3x2y0 true) -(= i28x1y4 true) -(= i22x2y2 false) -(= i6x2y4 true) -(= i31x3y5 false) -(= i5x2y3 true) -(= i13x2y1 false) -(= i16x1y2 true) -(= i1x4y4 true) -(= i15x3y0 false) -(= i20x4y3 true) -(= i21x2y5 false) -(= i25x4y3 false) -(= i7x1y2 true) -(= i24x6y4 false) -(= i9x3y4 true) -(= i19x4y3 true) -(= i9x4y2 true) -(= i5x5y2 true) -(= i23x2y2 true) -(= i26x4y4 false) -(= i4x4y6 true) -(= i28x3y0 false) -(= i14x2y2 true) -(= i5x4y6 true) -(= i21x5y3 false) -(= i5x4y4 true) -(= i5x1y2 true) -(= i5x6y3 true) -(= i5x4y5 true) -(= i19x2y0 false) -(= i15x4y0 true) -(= i16x3y3 false) -(= i11x2y0 false) -(= i9x4y5 false) -(= i2x4y1 false) -(= i8x2y4 true) -(= i9x3y2 true) -(= i16x3y0 false) -(= i19x2y5 false) -(= i30x1y2 false) -(= i18x2y4 true) -(= i30x2y0 false) -(= i1x3y6 true) -(= i10x6y4 false) -(= i17x2y5 false) -(= i28x5y4 false) -(= i12x4y2 true) -(= i14x1y4 false) -(= i29x4y5 false) -(= i1x2y5 true) -(= i2x4y3 true) -(= i7x4y1 false) -(= i1x4y2 true) -(= i24x0y3 true) -(= i10x4y4 false) -(= i6x2y1 false) -(= i7x5y2 true) -(= i8x1y2 true) -(= i8x4y2 true) -(= i10x6y3 true) -(= i14x6y4 true) -(= i10x2y0 true) -(= i23x4y0 false) -(= i28x3y1 false) -(= i10x4y5 false) -(= i31x6y4 false) -(= i19x1y2 true) -(= i7x4y2 true) -(= i16x5y2 true) -(= i24x2y5 false) -(= i24x3y4 false) -(= i2x2y1 true) -(= i15x2y6 false) -(= i2x5y2 true) -(= i23x2y6 true) -(= i30x5y3 false) -(= i3x4y5 true) -(= i10x3y5 true) -(= i27x1y3 false) -(= i26x2y6 true) -(= i20x4y2 true) -(= i2x2y2 true) -(= i22x0y2 true) -(= i19x0y4 false) -(= i9x3y5 true) -(= i24x1y4 true) -(= i21x5y2 false) -(= i5x3y1 false) -(= i20x4y6 false) -(= i30x6y2 false) -(= i18x2y0 false) -(= i31x4y6 false) -(= i17x4y6 false) -(= i27x2y4 true) -(= i2x6y4 true) -(= i26x0y2 false) -(= i30x1y3 false) -(= i14x3y5 true) -(= i28x2y3 false) -(= i31x0y2 false) -(= i28x2y4 false) -(= i12x2y6 false) -(= i4x3y4 true) -(= i31x2y2 false) -(= i7x6y4 false) -(= i8x3y2 true) -(= i11x6y2 true) -(= i17x4y1 false) -(= i29x1y2 false) -(= i12x4y5 false) -(= i27x4y6 false) -(= i22x4y0 false) -(= i2x2y0 true) -(= i9x2y4 false) -(= i3x3y6 true) -(= i11x3y6 true) -(= i11x6y3 true) -(= i9x2y1 false) -(= i12x2y5 false) -(= i23x4y5 false) -(= i27x5y2 false) -(= i23x3y6 false) -(= i31x4y0 false) -(= i8x0y3 true) -(= i23x2y0 false) -(= i28x0y2 false) -(= i20x1y4 true) -(= i0x4y5 true) -(= i6x3y1 false) -(= i12x5y2 true) -(= i12x4y6 true) -(= i18x3y6 false) -(= i3x4y2 false) -(= i2x6y3 true) -(= i5x6y4 true) -(= i21x6y2 false) -(= i1x3y3 true) -(= i16x0y2 true) -(= i11x4y5 false) -(= i26x6y4 false) -(= i31x0y4 false) -(= i20x5y3 false) -(= i25x0y2 false) -(= i31x0y3 false) -(= i10x3y3 false) -(= i10x2y3 true) -(= i27x2y6 true) -(= i11x5y3 true) -(= i2x4y4 true) -(= i16x3y2 true) -(= i19x5y2 false) -(= i1x3y2 true) -(= i21x3y4 false) -(= i10x3y4 true) -(= i21x2y6 true) -(= i30x2y4 false) -(= i28x6y3 false) -(= i27x3y1 false) -(= i12x4y4 false) -(= i22x2y0 false) -(= i15x6y2 false) -(= i29x2y1 false) -(= i6x3y0 true) -(= i11x2y1 false) -(= i23x2y3 false) -(= i10x4y6 true) -(= i18x2y1 false) -(= i10x5y2 true) -(= i16x2y2 true) -(= i2x2y5 true) -(= i7x4y6 true) -(= i25x3y0 false) -(= i17x3y2 true) -(= i31x1y2 false) -(= i22x4y2 true) -(= i26x5y4 false) -(= i24x5y2 false) -(= i0x6y4 true) -(= i17x3y4 false) -(= i29x2y3 false) -(= i21x1y3 true) -(= i23x1y2 true) -(= i21x1y4 true) -(= i5x2y4 true) -(= i25x6y3 false) -(= i11x1y4 false) -(= i20x0y3 true) -(= i16x5y4 false) -(= i28x2y0 false) -(= i5x6y2 true) -(= i15x5y3 true) -(= i31x6y3 false) -(= i1x5y2 true) -(= i17x3y6 false) -(= i18x5y4 false) -(= i13x5y4 true) -(= i16x4y3 true) -(= i6x2y0 true) -(= i25x2y3 true) -(= i19x4y4 false) -(= i3x0y3 true) -(= i30x3y4 true) -(= i4x4y2 true) -(= i18x5y2 false) -(= i21x2y0 false) -(= i29x5y3 false) -(= i11x0y4 true) -(= i31x3y3 true) -(= i7x2y0 true) -(= i20x2y1 true) -(= i0x5y2 true) -(= i14x0y2 true) -(= i19x1y3 true) -(= i11x0y3 true) -(= i20x1y2 true) -(= i25x1y3 true) -(= i30x3y2 false) -(= i16x3y6 false) -(= i4x6y3 true) -(= i8x3y4 false) -(= i31x2y0 false) -(= i20x3y0 false) -(= i29x4y1 false) -(= i0x4y1 true) -(= i14x4y4 false) -(= i0x1y2 true) -(= i2x2y6 true) -(= i26x2y4 true) -(= i23x3y0 false) -(= i14x6y3 false) -(= i16x2y3 true) -(= i19x4y2 true) -(= i31x4y1 false) -(= i20x3y4 false) -(= i31x1y3 false) -(= i22x6y2 false) -(= i25x6y4 false) -(= i17x1y4 false) -(= i30x4y4 false) -(= i9x0y3 true) -(= i0x3y4 true) -(= i20x0y2 true) -(= i23x3y1 false) -(= i3x5y3 false) -(= i26x1y2 false) -(= i11x3y1 false) -(= i9x2y6 true) -(= i14x0y4 false) -(= i14x1y2 true) -(= i20x3y6 false) -(= i14x3y1 false) -(= i9x4y3 true) -(= i27x3y4 false) -(= i27x2y2 false) -(= i15x6y4 false) -(= i12x3y0 false) -(= i12x6y4 false) -(= i26x6y2 false) -(= i17x5y3 false) -(= i23x3y2 false) -(= i12x0y2 true) -(= i18x5y3 false) -(= i8x3y3 false) -(= i2x3y0 true) -(= i15x6y3 false) -(= i0x0y4 true) -(= i23x6y4 false) -(= i4x3y2 true) -(= i4x5y3 false) -(= i9x2y2 true) -(= i30x1y4 false) -(= i28x3y2 false) -(= i0x6y3 true) -(= i7x5y4 false) -(= i21x4y1 true) -(= i8x3y0 true) -(= i15x3y2 true) -(= i27x4y0 false) -(= i15x4y6 true) -(= i13x1y2 true) -(= i12x2y3 true) - diff --git a/a2/src/4/4.model.bak b/a2/src/4/4.model.bak new file mode 100644 index 0000000..3b52ae7 --- /dev/null +++ b/a2/src/4/4.model.bak @@ -0,0 +1,1059 @@ +sat + +(= i1x2y0 true) +(= i4x2y1 false) +(= i1x2y3 true) +(= i11x2y5 false) +(= i31x6y2 false) +(= i26x0y3 true) +(= i10x3y6 true) +(= i13x3y5 true) +(= i20x0y4 false) +(= i30x2y2 false) +(= i6x2y3 true) +(= i6x5y3 true) +(= i0x4y0 true) +(= i17x2y0 false) +(= i20x3y1 false) +(= i24x5y4 false) +(= i16x4y6 false) +(= i26x0y4 false) +(= i26x2y5 false) +(= i14x2y6 false) +(= i29x1y4 true) +(= i1x0y4 true) +(= i21x3y3 false) +(= i31x4y2 false) +(= i18x6y3 false) +(= i3x1y2 true) +(= i4x3y6 true) +(= i9x1y3 true) +(= i16x6y4 false) +(= i18x6y4 false) +(= i19x1y4 true) +(= i14x3y0 false) +(= i9x3y3 false) +(= i3x5y4 true) +(= i21x4y5 false) +(= i14x4y5 false) +(= i30x5y2 false) +(= i22x4y6 false) +(= i6x0y3 true) +(= i18x2y5 false) +(= i27x1y2 false) +(= i26x2y1 false) +(= i24x4y6 false) +(= i31x4y4 false) +(= i19x5y3 false) +(= i15x1y4 false) +(= i9x3y6 true) +(= i0x3y1 true) +(= i14x6y2 false) +(= i28x0y3 false) +(= i0x6y2 true) +(= i9x5y3 true) +(= i13x0y4 true) +(= i11x1y3 true) +(= i7x3y3 false) +(= i21x2y4 false) +(= i15x5y4 false) +(= i27x4y2 false) +(= i6x0y2 true) +(= i14x3y4 false) +(= i9x0y4 true) +(= i20x6y4 false) +(= i7x1y4 true) +(= i21x1y2 true) +(= i24x4y5 false) +(= i30x4y5 false) +(= i31x1y4 false) +(= i8x4y1 false) +(= i1x3y5 true) +(= i3x2y6 true) +(= i13x1y4 true) +(= i2x6y2 true) +(= i9x4y1 false) +(= i29x0y2 false) +(= i15x0y4 false) +(= i28x5y2 false) +(= i24x3y6 false) +(= i18x3y1 false) +(= i19x4y6 false) +(= i22x3y1 false) +(= i19x4y1 false) +(= i13x2y0 false) +(= i27x3y3 false) +(= i12x3y5 true) +(= i16x2y0 false) +(= i10x4y0 false) +(= i27x2y0 false) +(= i11x3y4 true) +(= i9x3y0 true) +(= i2x3y6 true) +(= i12x6y2 true) +(= i18x2y6 true) +(= i23x3y4 false) +(= i13x0y2 true) +(= i31x2y4 false) +(= i13x3y6 true) +(= i2x0y4 true) +(= i8x4y6 true) +(= i17x5y4 true) +(= i18x3y2 true) +(= i6x1y2 true) +(= i16x1y3 true) +(= i18x3y3 false) +(= i27x0y4 false) +(= i6x2y5 true) +(= i24x3y0 false) +(= i9x3y1 false) +(= i11x5y4 true) +(= i3x2y3 true) +(= i15x0y2 true) +(= i27x3y2 false) +(= i12x6y3 true) +(= i5x0y2 true) +(= i29x0y3 false) +(= i30x4y6 false) +(= i13x3y3 false) +(= i28x4y5 false) +(= i31x4y3 false) +(= i2x4y5 true) +(= i8x6y4 false) +(= i13x3y1 false) +(= i10x4y1 false) +(= i17x2y1 false) +(= i26x3y2 false) +(= i30x4y0 false) +(= i19x6y3 false) +(= i24x2y1 false) +(= i12x1y4 true) +(= i29x3y6 false) +(= i23x0y3 true) +(= i6x4y3 true) +(= i15x3y5 true) +(= i23x0y4 false) +(= i29x6y2 false) +(= i21x4y4 false) +(= i14x4y3 true) +(= i29x3y0 false) +(= i24x6y3 false) +(= i25x3y3 false) +(= i5x2y2 true) +(= i30x5y4 false) +(= i16x0y4 false) +(= i2x5y3 false) +(= i3x1y3 true) +(= i12x2y0 false) +(= i16x2y5 false) +(= i25x2y6 true) +(= i7x0y3 true) +(= i10x3y2 true) +(= i12x3y1 false) +(= i26x6y3 false) +(= i27x6y3 false) +(= i6x1y4 true) +(= i20x3y3 false) +(= i27x6y4 false) +(= i29x2y6 false) +(= i3x6y3 true) +(= i24x6y2 false) +(= i1x5y4 true) +(= i27x5y4 false) +(= i10x2y4 true) +(= i30x3y6 false) +(= i26x2y3 false) +(= i14x2y3 true) +(= i28x3y5 true) +(= i5x0y4 true) +(= i24x1y2 true) +(= i2x1y3 true) +(= i4x1y3 true) +(= i7x3y0 true) +(= i15x3y4 false) +(= i25x2y5 false) +(= i12x3y2 true) +(= i22x6y4 false) +(= i14x4y6 true) +(= i14x2y1 false) +(= i22x4y1 false) +(= i24x0y4 false) +(= i26x3y5 true) +(= i4x1y4 true) +(= i23x5y2 false) +(= i30x2y6 false) +(= i16x4y4 true) +(= i25x2y2 true) +(= i0x4y3 true) +(= i6x4y5 false) +(= i20x3y2 true) +(= i30x6y3 false) +(= i20x2y0 false) +(= i29x3y5 true) +(= i12x4y3 true) +(= i22x2y5 false) +(= i12x5y3 true) +(= i28x3y3 false) +(= i23x4y1 false) +(= i24x5y3 false) +(= i20x3y5 true) +(= i8x2y0 true) +(= i17x3y0 false) +(= i9x6y4 false) +(= i2x4y6 true) +(= i29x0y4 false) +(= i13x0y3 true) +(= i8x2y2 true) +(= i14x2y5 false) +(= i17x2y3 true) +(= i11x3y0 false) +(= i24x4y1 false) +(= i14x4y0 true) +(= i27x4y4 false) +(= i4x5y4 true) +(= i23x3y3 false) +(= i9x1y2 true) +(= i3x6y2 true) +(= i30x0y2 false) +(= i3x2y1 false) +(= i11x4y4 false) +(= i6x2y2 true) +(= i15x2y4 true) +(= i23x4y4 false) +(= i26x1y3 true) +(= i4x0y3 true) +(= i28x0y4 false) +(= i29x6y3 false) +(= i2x4y0 true) +(= i0x3y0 true) +(= i14x3y3 false) +(= i30x4y1 false) +(= i11x6y4 false) +(= i0x3y6 true) +(= i12x1y3 true) +(= i8x1y3 true) +(= i28x2y2 false) +(= i4x2y5 true) +(= i26x1y4 true) +(= i6x4y6 true) +(= i21x0y3 true) +(= i21x4y3 false) +(= i26x4y0 false) +(= i24x3y3 false) +(= i18x4y1 false) +(= i21x3y0 false) +(= i25x2y1 false) +(= i26x3y6 false) +(= i27x1y4 true) +(= i27x4y5 false) +(= i28x2y6 true) +(= i27x3y6 false) +(= i19x2y6 true) +(= i1x2y1 true) +(= i0x0y3 true) +(= i25x4y6 false) +(= i4x1y2 true) +(= i0x2y0 true) +(= i17x6y3 false) +(= i11x5y2 true) +(= i7x6y3 true) +(= i12x3y3 false) +(= i9x0y2 true) +(= i21x2y2 false) +(= i4x2y3 true) +(= i16x3y1 false) +(= i21x3y1 false) +(= i24x4y2 false) +(= i4x0y4 true) +(= i7x3y5 true) +(= i11x4y3 true) +(= i9x2y3 true) +(= i20x2y6 true) +(= i18x4y5 false) +(= i2x0y2 true) +(= i13x4y0 true) +(= i25x3y6 false) +(= i27x3y5 true) +(= i4x3y3 true) +(= i31x4y5 false) +(= i10x0y2 true) +(= i20x2y5 false) +(= i9x4y6 true) +(= i1x3y1 true) +(= i28x1y2 false) +(= i28x6y2 false) +(= i20x6y2 false) +(= i5x2y5 true) +(= i1x0y2 true) +(= i1x4y5 true) +(= i1x1y3 true) +(= i6x0y4 true) +(= i14x5y2 true) +(= i9x6y2 true) +(= i19x0y3 true) +(= i21x3y2 true) +(= i26x4y2 false) +(= i24x1y3 true) +(= i20x4y1 false) +(= i5x3y6 true) +(= i23x1y4 true) +(= i1x6y2 true) +(= i23x5y3 false) +(= i12x2y1 false) +(= i2x0y3 true) +(= i18x4y6 false) +(= i7x4y0 false) +(= i1x1y2 true) +(= i0x2y1 true) +(= i1x5y3 false) +(= i1x3y0 true) +(= i8x4y0 false) +(= i10x5y4 true) +(= i4x0y2 true) +(= i26x3y3 false) +(= i0x4y6 true) +(= i7x6y2 true) +(= i17x1y3 true) +(= i13x4y4 false) +(= i3x4y1 true) +(= i5x3y4 true) +(= i21x3y5 true) +(= i28x4y0 false) +(= i22x3y5 true) +(= i14x3y6 true) +(= i2x3y5 true) +(= i29x4y6 false) +(= i12x2y2 true) +(= i30x3y3 false) +(= i17x5y2 false) +(= i4x3y5 true) +(= i11x3y3 false) +(= i30x3y5 true) +(= i14x5y4 true) +(= i8x5y2 true) +(= i25x4y0 false) +(= i9x4y4 false) +(= i4x3y0 true) +(= i3x4y3 true) +(= i11x2y6 false) +(= i18x3y5 true) +(= i12x4y0 true) +(= i11x3y5 true) +(= i28x4y3 false) +(= i14x3y2 true) +(= i16x5y3 true) +(= i6x5y4 true) +(= i2x3y4 true) +(= i19x5y4 false) +(= i1x6y4 true) +(= i15x5y2 true) +(= i1x3y4 true) +(= i3x2y5 true) +(= i20x5y4 false) +(= i23x0y2 true) +(= i23x2y5 false) +(= i3x4y6 true) +(= i6x4y4 false) +(= i7x2y1 false) +(= i26x4y5 false) +(= i25x4y1 false) +(= i10x2y2 true) +(= i23x2y1 true) +(= i9x6y3 true) +(= i8x3y1 false) +(= i13x1y3 true) +(= i14x2y0 false) +(= i7x4y5 false) +(= i15x1y2 true) +(= i21x2y1 true) +(= i1x2y6 true) +(= i17x2y6 true) +(= i12x1y2 true) +(= i22x1y2 true) +(= i12x5y4 true) +(= i1x6y3 true) +(= i25x2y4 false) +(= i25x4y5 false) +(= i7x3y4 true) +(= i10x3y1 false) +(= i25x4y2 false) +(= i18x0y4 false) +(= i26x5y3 false) +(= i11x2y4 true) +(= i10x2y1 false) +(= i18x2y3 true) +(= i24x2y4 false) +(= i29x2y5 false) +(= i28x2y5 true) +(= i11x4y2 true) +(= i7x3y2 true) +(= i16x4y5 false) +(= i27x0y3 false) +(= i16x6y3 false) +(= i19x3y2 true) +(= i20x5y2 false) +(= i12x3y6 true) +(= i22x3y6 false) +(= i27x2y1 false) +(= i13x3y4 false) +(= i24x3y1 false) +(= i10x6y2 true) +(= i0x3y5 true) +(= i21x5y4 false) +(= i17x0y4 false) +(= i7x0y4 true) +(= i8x6y2 true) +(= i10x1y3 true) +(= i11x3y2 true) +(= i24x4y3 false) +(= i13x4y5 false) +(= i13x6y2 false) +(= i25x5y3 false) +(= i13x5y2 true) +(= i13x6y4 true) +(= i15x2y2 true) +(= i31x2y6 false) +(= i25x1y2 false) +(= i18x0y3 true) +(= i29x2y4 true) +(= i0x2y5 true) +(= i15x4y5 false) +(= i16x2y1 false) +(= i29x4y2 false) +(= i30x3y1 false) +(= i28x5y3 false) +(= i13x4y1 false) +(= i13x4y3 true) +(= i22x5y2 false) +(= i14x0y3 true) +(= i20x6y3 false) +(= i7x2y2 true) +(= i22x2y6 true) +(= i18x4y2 true) +(= i10x4y3 true) +(= i24x3y2 false) +(= i16x4y2 true) +(= i20x4y5 false) +(= i24x2y6 true) +(= i17x0y3 true) +(= i26x2y2 false) +(= i31x3y2 false) +(= i23x2y4 false) +(= i18x0y2 true) +(= i24x2y0 false) +(= i5x2y6 true) +(= i25x1y4 true) +(= i29x3y3 false) +(= i13x5y3 true) +(= i17x1y2 true) +(= i27x2y5 false) +(= i22x5y4 false) +(= i8x2y6 true) +(= i30x2y5 false) +(= i6x6y2 true) +(= i28x4y6 false) +(= i3x6y4 true) +(= i29x2y2 false) +(= i22x5y3 false) +(= i26x3y4 false) +(= i11x0y2 true) +(= i6x3y2 true) +(= i11x2y2 true) +(= i0x3y3 false) +(= i1x4y1 true) +(= i11x4y0 true) +(= i12x0y4 true) +(= i10x2y6 false) +(= i28x6y4 false) +(= i17x3y3 false) +(= i20x2y4 false) +(= i4x4y5 true) +(= i5x1y3 true) +(= i0x2y4 true) +(= i15x2y1 false) +(= i26x5y2 false) +(= i25x3y4 false) +(= i3x1y4 true) +(= i26x3y1 false) +(= i8x6y3 true) +(= i19x0y2 true) +(= i11x4y1 false) +(= i19x3y4 false) +(= i28x4y2 false) +(= i2x5y4 true) +(= i23x6y3 false) +(= i21x4y6 false) +(= i10x4y2 true) +(= i26x3y0 false) +(= i6x3y4 true) +(= i25x3y5 true) +(= i17x4y0 true) +(= i27x2y3 true) +(= i29x5y2 false) +(= i12x2y4 false) +(= i0x2y3 true) +(= i24x4y0 false) +(= i13x4y6 true) +(= i31x2y5 false) +(= i30x2y3 false) +(= i4x4y3 true) +(= i14x5y3 true) +(= i7x3y1 false) +(= i17x4y2 true) +(= i22x2y1 true) +(= i0x0y2 true) +(= i11x4y6 true) +(= i7x0y2 true) +(= i4x2y6 true) +(= i22x3y0 false) +(= i9x4y0 false) +(= i23x6y2 false) +(= i9x2y0 true) +(= i16x6y2 false) +(= i15x2y0 false) +(= i29x2y0 false) +(= i2x3y1 true) +(= i5x4y3 false) +(= i3x3y5 true) +(= i9x2y5 true) +(= i27x6y2 false) +(= i22x6y3 false) +(= i1x1y4 true) +(= i23x1y3 true) +(= i5x5y3 true) +(= i17x4y5 false) +(= i17x0y2 true) +(= i18x3y0 false) +(= i6x4y2 true) +(= i24x0y2 true) +(= i0x2y2 true) +(= i7x3y6 true) +(= i20x2y3 false) +(= i31x5y2 false) +(= i22x3y4 false) +(= i1x2y4 true) +(= i16x4y0 true) +(= i19x6y4 false) +(= i8x4y4 false) +(= i19x3y0 false) +(= i30x6y4 false) +(= i22x0y3 true) +(= i4x4y1 false) +(= i29x3y2 false) +(= i8x5y4 true) +(= i5x1y4 true) +(= i29x1y3 false) +(= i7x2y5 true) +(= i10x0y4 true) +(= i5x2y1 false) +(= i8x1y4 true) +(= i13x2y6 false) +(= i14x2y4 true) +(= i22x3y2 true) +(= i22x4y3 false) +(= i8x4y5 false) +(= i24x2y3 true) +(= i7x4y3 true) +(= i7x4y4 true) +(= i5x3y3 false) +(= i28x4y4 false) +(= i3x5y2 true) +(= i30x0y3 false) +(= i10x1y2 true) +(= i8x5y3 true) +(= i0x4y4 true) +(= i3x4y0 true) +(= i31x2y3 false) +(= i18x4y4 false) +(= i6x2y6 true) +(= i28x3y4 false) +(= i16x3y5 true) +(= i19x3y1 false) +(= i22x3y3 false) +(= i24x2y2 false) +(= i24x3y5 true) +(= i5x4y0 false) +(= i12x4y1 false) +(= i17x2y2 true) +(= i28x2y1 false) +(= i16x2y4 true) +(= i24x4y4 false) +(= i6x6y3 true) +(= i8x2y3 true) +(= i3x3y4 true) +(= i22x4y4 false) +(= i1x2y2 true) +(= i5x0y3 true) +(= i8x4y3 true) +(= i20x1y3 true) +(= i21x6y3 false) +(= i5x4y1 false) +(= i8x0y2 true) +(= i19x2y1 false) +(= i21x4y0 true) +(= i23x5y4 false) +(= i15x0y3 true) +(= i10x1y4 false) +(= i29x6y4 false) +(= i5x3y0 true) +(= i13x4y2 true) +(= i27x0y2 false) +(= i17x4y3 true) +(= i26x4y6 false) +(= i10x5y3 true) +(= i29x5y4 false) +(= i18x4y3 true) +(= i4x2y4 true) +(= i1x4y0 true) +(= i10x2y5 false) +(= i25x0y4 false) +(= i5x4y2 true) +(= i30x4y3 false) +(= i2x2y4 true) +(= i25x3y1 false) +(= i3x3y1 false) +(= i12x3y4 false) +(= i15x3y1 false) +(= i2x1y2 true) +(= i22x4y5 false) +(= i17x4y4 true) +(= i6x4y0 false) +(= i17x6y2 false) +(= i18x6y2 false) +(= i5x3y2 true) +(= i7x2y6 true) +(= i21x6y4 false) +(= i25x6y2 false) +(= i2x4y2 false) +(= i31x5y4 false) +(= i3x3y3 true) +(= i14x4y2 true) +(= i19x6y2 false) +(= i25x5y4 false) +(= i19x3y5 true) +(= i5x3y5 true) +(= i7x2y4 true) +(= i15x1y3 true) +(= i16x4y1 false) +(= i3x0y4 true) +(= i8x2y5 true) +(= i13x3y2 true) +(= i25x0y3 true) +(= i5x5y4 true) +(= i13x2y3 true) +(= i20x4y0 true) +(= i4x6y2 true) +(= i21x3y6 false) +(= i22x1y3 true) +(= i1x0y3 true) +(= i1x4y3 false) +(= i8x3y5 true) +(= i25x2y0 false) +(= i13x2y5 false) +(= i4x6y4 true) +(= i4x4y4 true) +(= i20x2y2 false) +(= i21x4y2 false) +(= i4x2y2 true) +(= i31x5y3 false) +(= i15x4y2 true) +(= i28x1y3 false) +(= i25x5y2 false) +(= i7x1y3 true) +(= i13x3y0 false) +(= i16x3y4 false) +(= i23x3y5 true) +(= i0x3y2 true) +(= i15x3y3 false) +(= i1x4y6 true) +(= i2x3y3 true) +(= i19x4y5 false) +(= i7x5y3 true) +(= i6x3y6 true) +(= i19x4y0 true) +(= i4x3y1 false) +(= i16x1y4 false) +(= i27x3y0 false) +(= i13x6y3 false) +(= i17x3y5 true) +(= i6x6y4 true) +(= i0x1y4 true) +(= i23x4y6 false) +(= i23x4y2 false) +(= i16x0y3 true) +(= i17x6y4 false) +(= i29x4y0 false) +(= i31x3y1 false) +(= i13x2y2 true) +(= i15x4y3 true) +(= i18x1y3 true) +(= i12x0y3 true) +(= i15x4y4 true) +(= i31x3y0 false) +(= i11x2y3 true) +(= i3x3y2 true) +(= i15x2y3 true) +(= i27x4y3 false) +(= i27x5y3 false) +(= i22x1y4 true) +(= i19x2y2 true) +(= i31x2y1 false) +(= i21x0y4 false) +(= i18x1y4 false) +(= i10x3y0 true) +(= i18x4y0 true) +(= i3x2y2 true) +(= i5x2y0 true) +(= i10x0y3 true) +(= i9x5y2 true) +(= i0x5y3 true) +(= i15x3y6 true) +(= i18x1y2 true) +(= i31x3y4 false) +(= i19x3y3 false) +(= i30x3y0 false) +(= i27x4y1 false) +(= i9x5y4 true) +(= i4x2y0 true) +(= i26x2y0 false) +(= i3x2y4 true) +(= i30x2y1 false) +(= i22x0y4 false) +(= i3x0y2 true) +(= i15x4y1 false) +(= i9x1y4 false) +(= i26x4y3 false) +(= i6x3y3 false) +(= i8x2y1 false) +(= i17x2y4 true) +(= i19x2y3 true) +(= i22x2y4 false) +(= i31x3y6 false) +(= i7x2y3 true) +(= i29x4y4 false) +(= i0x5y4 true) +(= i21x2y3 false) +(= i30x4y2 false) +(= i4x5y2 true) +(= i11x1y2 true) +(= i22x2y3 false) +(= i3x3y0 true) +(= i17x3y1 false) +(= i6x3y5 true) +(= i26x4y1 false) +(= i3x4y4 true) +(= i29x3y4 false) +(= i25x4y4 false) +(= i4x4y0 false) +(= i14x4y1 false) +(= i19x3y6 false) +(= i8x0y4 true) +(= i23x4y3 false) +(= i21x0y2 true) +(= i6x5y2 true) +(= i25x3y2 false) +(= i16x2y6 true) +(= i6x4y1 false) +(= i14x1y3 true) +(= i29x3y1 false) +(= i0x1y3 true) +(= i13x2y4 false) +(= i18x3y4 true) +(= i0x2y6 true) +(= i2x3y2 true) +(= i28x4y1 false) +(= i2x1y4 true) +(= i0x4y2 true) +(= i28x3y6 false) +(= i6x1y3 true) +(= i18x2y2 true) +(= i29x4y3 false) +(= i30x0y4 false) +(= i2x2y3 true) +(= i15x2y5 false) +(= i8x3y6 true) +(= i19x2y4 false) +(= i20x4y4 false) +(= i3x2y0 true) +(= i28x1y4 true) +(= i22x2y2 false) +(= i6x2y4 true) +(= i31x3y5 false) +(= i5x2y3 true) +(= i13x2y1 false) +(= i16x1y2 true) +(= i1x4y4 true) +(= i15x3y0 false) +(= i20x4y3 true) +(= i21x2y5 false) +(= i25x4y3 false) +(= i7x1y2 true) +(= i24x6y4 false) +(= i9x3y4 true) +(= i19x4y3 true) +(= i9x4y2 true) +(= i5x5y2 true) +(= i23x2y2 true) +(= i26x4y4 false) +(= i4x4y6 true) +(= i28x3y0 false) +(= i14x2y2 true) +(= i5x4y6 true) +(= i21x5y3 false) +(= i5x4y4 true) +(= i5x1y2 true) +(= i5x6y3 true) +(= i5x4y5 true) +(= i19x2y0 false) +(= i15x4y0 true) +(= i16x3y3 false) +(= i11x2y0 false) +(= i9x4y5 false) +(= i2x4y1 false) +(= i8x2y4 true) +(= i9x3y2 true) +(= i16x3y0 false) +(= i19x2y5 false) +(= i30x1y2 false) +(= i18x2y4 true) +(= i30x2y0 false) +(= i1x3y6 true) +(= i10x6y4 false) +(= i17x2y5 false) +(= i28x5y4 false) +(= i12x4y2 true) +(= i14x1y4 false) +(= i29x4y5 false) +(= i1x2y5 true) +(= i2x4y3 true) +(= i7x4y1 false) +(= i1x4y2 true) +(= i24x0y3 true) +(= i10x4y4 false) +(= i6x2y1 false) +(= i7x5y2 true) +(= i8x1y2 true) +(= i8x4y2 true) +(= i10x6y3 true) +(= i14x6y4 true) +(= i10x2y0 true) +(= i23x4y0 false) +(= i28x3y1 false) +(= i10x4y5 false) +(= i31x6y4 false) +(= i19x1y2 true) +(= i7x4y2 true) +(= i16x5y2 true) +(= i24x2y5 false) +(= i24x3y4 false) +(= i2x2y1 true) +(= i15x2y6 false) +(= i2x5y2 true) +(= i23x2y6 true) +(= i30x5y3 false) +(= i3x4y5 true) +(= i10x3y5 true) +(= i27x1y3 false) +(= i26x2y6 true) +(= i20x4y2 true) +(= i2x2y2 true) +(= i22x0y2 true) +(= i19x0y4 false) +(= i9x3y5 true) +(= i24x1y4 true) +(= i21x5y2 false) +(= i5x3y1 false) +(= i20x4y6 false) +(= i30x6y2 false) +(= i18x2y0 false) +(= i31x4y6 false) +(= i17x4y6 false) +(= i27x2y4 true) +(= i2x6y4 true) +(= i26x0y2 false) +(= i30x1y3 false) +(= i14x3y5 true) +(= i28x2y3 false) +(= i31x0y2 false) +(= i28x2y4 false) +(= i12x2y6 false) +(= i4x3y4 true) +(= i31x2y2 false) +(= i7x6y4 false) +(= i8x3y2 true) +(= i11x6y2 true) +(= i17x4y1 false) +(= i29x1y2 false) +(= i12x4y5 false) +(= i27x4y6 false) +(= i22x4y0 false) +(= i2x2y0 true) +(= i9x2y4 false) +(= i3x3y6 true) +(= i11x3y6 true) +(= i11x6y3 true) +(= i9x2y1 false) +(= i12x2y5 false) +(= i23x4y5 false) +(= i27x5y2 false) +(= i23x3y6 false) +(= i31x4y0 false) +(= i8x0y3 true) +(= i23x2y0 false) +(= i28x0y2 false) +(= i20x1y4 true) +(= i0x4y5 true) +(= i6x3y1 false) +(= i12x5y2 true) +(= i12x4y6 true) +(= i18x3y6 false) +(= i3x4y2 false) +(= i2x6y3 true) +(= i5x6y4 true) +(= i21x6y2 false) +(= i1x3y3 true) +(= i16x0y2 true) +(= i11x4y5 false) +(= i26x6y4 false) +(= i31x0y4 false) +(= i20x5y3 false) +(= i25x0y2 false) +(= i31x0y3 false) +(= i10x3y3 false) +(= i10x2y3 true) +(= i27x2y6 true) +(= i11x5y3 true) +(= i2x4y4 true) +(= i16x3y2 true) +(= i19x5y2 false) +(= i1x3y2 true) +(= i21x3y4 false) +(= i10x3y4 true) +(= i21x2y6 true) +(= i30x2y4 false) +(= i28x6y3 false) +(= i27x3y1 false) +(= i12x4y4 false) +(= i22x2y0 false) +(= i15x6y2 false) +(= i29x2y1 false) +(= i6x3y0 true) +(= i11x2y1 false) +(= i23x2y3 false) +(= i10x4y6 true) +(= i18x2y1 false) +(= i10x5y2 true) +(= i16x2y2 true) +(= i2x2y5 true) +(= i7x4y6 true) +(= i25x3y0 false) +(= i17x3y2 true) +(= i31x1y2 false) +(= i22x4y2 true) +(= i26x5y4 false) +(= i24x5y2 false) +(= i0x6y4 true) +(= i17x3y4 false) +(= i29x2y3 false) +(= i21x1y3 true) +(= i23x1y2 true) +(= i21x1y4 true) +(= i5x2y4 true) +(= i25x6y3 false) +(= i11x1y4 false) +(= i20x0y3 true) +(= i16x5y4 false) +(= i28x2y0 false) +(= i5x6y2 true) +(= i15x5y3 true) +(= i31x6y3 false) +(= i1x5y2 true) +(= i17x3y6 false) +(= i18x5y4 false) +(= i13x5y4 true) +(= i16x4y3 true) +(= i6x2y0 true) +(= i25x2y3 true) +(= i19x4y4 false) +(= i3x0y3 true) +(= i30x3y4 true) +(= i4x4y2 true) +(= i18x5y2 false) +(= i21x2y0 false) +(= i29x5y3 false) +(= i11x0y4 true) +(= i31x3y3 true) +(= i7x2y0 true) +(= i20x2y1 true) +(= i0x5y2 true) +(= i14x0y2 true) +(= i19x1y3 true) +(= i11x0y3 true) +(= i20x1y2 true) +(= i25x1y3 true) +(= i30x3y2 false) +(= i16x3y6 false) +(= i4x6y3 true) +(= i8x3y4 false) +(= i31x2y0 false) +(= i20x3y0 false) +(= i29x4y1 false) +(= i0x4y1 true) +(= i14x4y4 false) +(= i0x1y2 true) +(= i2x2y6 true) +(= i26x2y4 true) +(= i23x3y0 false) +(= i14x6y3 false) +(= i16x2y3 true) +(= i19x4y2 true) +(= i31x4y1 false) +(= i20x3y4 false) +(= i31x1y3 false) +(= i22x6y2 false) +(= i25x6y4 false) +(= i17x1y4 false) +(= i30x4y4 false) +(= i9x0y3 true) +(= i0x3y4 true) +(= i20x0y2 true) +(= i23x3y1 false) +(= i3x5y3 false) +(= i26x1y2 false) +(= i11x3y1 false) +(= i9x2y6 true) +(= i14x0y4 false) +(= i14x1y2 true) +(= i20x3y6 false) +(= i14x3y1 false) +(= i9x4y3 true) +(= i27x3y4 false) +(= i27x2y2 false) +(= i15x6y4 false) +(= i12x3y0 false) +(= i12x6y4 false) +(= i26x6y2 false) +(= i17x5y3 false) +(= i23x3y2 false) +(= i12x0y2 true) +(= i18x5y3 false) +(= i8x3y3 false) +(= i2x3y0 true) +(= i15x6y3 false) +(= i0x0y4 true) +(= i23x6y4 false) +(= i4x3y2 true) +(= i4x5y3 false) +(= i9x2y2 true) +(= i30x1y4 false) +(= i28x3y2 false) +(= i0x6y3 true) +(= i7x5y4 false) +(= i21x4y1 true) +(= i8x3y0 true) +(= i15x3y2 true) +(= i27x4y0 false) +(= i15x4y6 true) +(= i13x1y2 true) +(= i12x2y3 true) + diff --git a/a2/src/4/a4.py b/a2/src/4/a4.py index b216b3b..9c5b015 100644 --- a/a2/src/4/a4.py +++ b/a2/src/4/a4.py @@ -1,23 +1,17 @@ #!/bin/env python -#pylint: disable-msg=too-many-locals,invalid-name -"""hi""" +#pylint: disable-msg=too-many-locals,invalid-name,missing-docstring -def generate(): - """Generates the yices code for peg solitaire""" +if __name__ == '__main__': pos = [(x, y) for x in range(7) for y in range(7) if not ((x < 2 and y < 2) or # exclude topleft (x > 4 and y > 4) or # exclude bottomright (x > 4 and y < 2) or # exclude topright (x < 2 and y > 4)) # exclude bottomleft ] - ill_middles = [ - (2, 0), (4, 0), (0, 2), (0, 4), (6, 2), (6, 4), (2, 6), (4, 6)] holes = [(3, 3)] winning = (3, 3) - iterations = len(pos)-len(holes) - posp = [p for p in pos if p not in ill_middles] print """ (benchmark a1.smt :logic QF_UF @@ -39,7 +33,7 @@ def generate(): print ';Iteration {}'.format(i) print '(or' for sx, sy in pos: - for mx, my in posp: + for mx, my in pos: if mx == sx and my == sy: continue for ex, ey in pos: @@ -77,6 +71,3 @@ def generate(): for x, y in pos if (x, y) != winning) print '))' - -if __name__ == '__main__': - generate() -- 2.20.1