From: Mart Lubbers Date: Wed, 23 Dec 2015 16:16:25 +0000 (+0100) Subject: success with 4:) X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=e8ae2d2ff67ae26b7aa020cb0d88c8bbadab9470;p=ar1516.git success with 4:) --- diff --git a/a2/2.tex b/a2/2.tex index 414669b..174dfd6 100644 --- a/a2/2.tex +++ b/a2/2.tex @@ -46,7 +46,7 @@ joining them with logical or operators. The solution described in \autoref{tab:sol2a} is found by \textsc{NuSMV} within $0.29$ seconds. - \begin{table}[ht] + \begin{table}[H] \centering\small \begin{tabular}{rrrrl} \toprule @@ -85,7 +85,7 @@ joining them with logical or operators. The solution described in \autoref{tab:sol2c} is found by \textsc{NuSMV} within $1.8$ seconds. - \begin{table}[ht] + \begin{table}[H] \centering\small \begin{tabular}{rrrrl} \toprule diff --git a/a2/4.tex b/a2/4.tex index 15029d5..9694310 100644 --- a/a2/4.tex +++ b/a2/4.tex @@ -1,2 +1,114 @@ \section{Solving solitaire} -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. + +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} + +\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} + +\subsection{Formalization} +Basically there are two possible formalization techniques we can use. +Formalization per position and formalization per peg. + +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. + +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. + +\begin{lstlisting}[caption={Coordinate system},label={lst:coord}] + 0123456 +0 ooo +1 ooo +2ooooooo +3ooooooo +4ooooooo +5 ooo +6 ooo +\end{lstlisting} + +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\}$. In +this way we can describe the start position, where $i=0$, by the following +formula meaning that all the positions are occupied except for the middle +position with coordinate $(3,3)$: +$$\neg i_0x_3y_3\wedge\bigwedge_{(x,y)\in P\setminus\{(3,3)\}}i_0x_xy_y$$ + +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)\}$ +All iterations following that can be described as the following formula: + +\begin{align} +\bigwedge^{I}_{i=1} + \bigvee_{(sx, sy)\in P}\bigvee_{(mx, my)\in P'} + \bigvee_{(ex, ey)\in P}\Bigl( + & 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) +\end{align} + +To get a trace for a winning game we negate the final condition and add it to +the formula: +$$i_{31}x_3y_3\wedge\bigwedge_{(x,y)\in P\setminus\{(3,3)\}}\neg i_{31}x_xy_y$$ + +\lstinputlisting[caption={Solution for peg solitaire},label={lst:sol}] + {./src/4/a4.tex} diff --git a/a2/ar.tex b/a2/ar.tex index 91fe795..5dabd82 100644 --- a/a2/ar.tex +++ b/a2/ar.tex @@ -3,36 +3,12 @@ \maketitle \tableofcontents -%\setcounter{section}{-1} -%\section{General approach} -%Implementing all the problems by hand in SMT-Lib format would be too much work -%and therefore all problems have an accompanying bash script contains a function -%\lstinline{generate} that generates the SMT-Lib format. The script feeds the -%SMT-Lib format to yices after which the output is feeded to a Python script -%that visualizes the solution. This means that for all problems $p$ for $p\in -%\{1,\ldots, 4\}$ there exist $2$ files. \texttt{ap.bash} that generates the -%solution and \texttt{ap.py} that visualizes the solution. All solving is done -%on the benchmark system listed in Listing~\ref{listing:benchmark}. -% -%\begin{lstlisting}[caption={Benchmark system},label={listing:benchmark}] -%CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor -%RAM: 8GB -% -%Yices: 2.4.1 -%SMT-Lib: 1.2 -%Bash: 4.3.30(1) -%\end{lstlisting} - -\newpage \input{1.tex} -\newpage \input{2.tex} -\newpage \input{3.tex} -\newpage \input{4.tex} \end{document} diff --git a/a2/pre.tex b/a2/pre.tex index 5f0513c..7970698 100644 --- a/a2/pre.tex +++ b/a2/pre.tex @@ -5,9 +5,13 @@ \usepackage{booktabs} % For nice tables \usepackage{enumerate} % For nice tables \usepackage{amsmath} % For nice tables +\usepackage{listings} % For nice tables +\usepackage{float} % For nice tables \everymath{\displaystyle} +\lstset{keepspaces=true,captionpos=b,basicstyle=\ttfamily} + \author{Mart Lubbers (s4109503)} \title{Automated reasoning Assignment 2} \date{\today} diff --git a/a2/src/4.py b/a2/src/4.py deleted file mode 100644 index b0b30f5..0000000 --- a/a2/src/4.py +++ /dev/null @@ -1,32 +0,0 @@ -#!/bin/env python -pegs = [(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 - ] -holes = [(3,3)] -var = ' '.join('p{}: boolean;'.format(i) for i in range(len(pegs))) -init = ' & '.join('p{}={}'.format(i, - 'FALSE' if pegs[i] in holes else 'TRUE') for i in range(len(pegs))) -a1 = '({})==1)'.format('+'.join('toint(p{})'.format(i) for i in range(len(pegs)))) -trans = '' -for i in range(len(pegs)): - current = pegs[i] - top = (current[0], current[1]-1) - bottom = (current[0], current[1]+1) - left = (current[0]-1, current[1]) - right = (current[0]+1, current[1]) - -print """\ -MODULE main -VAR -{} -INIT -{} -TRANS -case {} -{} -LTLSPEC G !({}) -""".format(var, init, trans, win, a1) diff --git a/a2/src/4.smv b/a2/src/4.smv deleted file mode 100644 index 08856c4..0000000 --- a/a2/src/4.smv +++ /dev/null @@ -1,24 +0,0 @@ -MODULE main -VAR -p1: boolean; -p2: boolean; -INIT -p1=TRUE & p2=TRUE & p3=TRUE & -p4=TRUE & p5=TRUE & p6=TRUE & - -p7=TRUE & p8=TRUE & - p9=TRUE & p10=TRUE & p11=TRUE & - p12=TRUE & p13=TRUE & -p14=TRUE & p15=TRUE & - p16=TRUE & p17=TRUE & p18=TRUE & - p19=TRUE & p20=TRUE & -p21=TRUE & p22=TRUE & p23=TRUE & - p24=TRUE & p25=TRUE & p26=TRUE & - p27=TRUE & p28=TRUE & - -p29=TRUE & p30=TRUE & p31=TRUE & -p32=TRUE & p33=TRUE & p34=TRUE -TRANS -next(p1)=TRUE & -next(p2)=TRUE -LTLSPEC G !(p1=FALSE) diff --git a/a2/src/4/4.model b/a2/src/4/4.model new file mode 100644 index 0000000..3b52ae7 --- /dev/null +++ b/a2/src/4/4.model @@ -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 new file mode 100644 index 0000000..b216b3b --- /dev/null +++ b/a2/src/4/a4.py @@ -0,0 +1,82 @@ +#!/bin/env python +#pylint: disable-msg=too-many-locals,invalid-name +"""hi""" + +def generate(): + """Generates the yices code for peg solitaire""" + 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 + :extrapreds ( + {} + ) + :formula + (and\ + """.format('\n\t'.join(' '.join('(i{}x{}y{})'.format(i, x, y) + for x, y in pos) + for i in range(iterations))) + print ';Iteration 0' + print ' '.join('(not i0x{}y{})'.format(x, y) for x, y in holes), + print ' '.join('i0x{}y{}'.format(x, y) + for x, y in pos if (x, y) not in holes) + + + for i in range(1, iterations): + print ';Iteration {}'.format(i) + print '(or' + for sx, sy in pos: + for mx, my in posp: + if mx == sx and my == sy: + continue + for ex, ey in pos: + if (ex == sx and ey == sy)or (ex == mx and ey == my): + continue + if not ((sy == my and my == ey and sx == mx+1 and + mx == ex+1) or + (sy == my and my == ey and sx == mx-1 and + mx == ex-1) or + (sx == mx and mx == ex and sy == my+1 and + my == ey+1) or + (sx == mx and mx == ex and sy == my-1 and + my == ey-1)): + continue + print '(and' + print ('i{0}x{1}y{2} ' + 'i{0}x{3}y{4} ' + '(not i{0}x{5}y{6})').format(i-1, + sx, sy, mx, my, ex, ey) + print ('(not i{0}x{1}y{2}) ' + '(not i{0}x{3}y{4}) ' + 'i{0}x{5}y{6}').format(i, sx, sy, mx, my, ex, ey) + for ox, oy in pos: + if not((ox == sx and oy == sy) or + (ox == mx and oy == my) or + (ox == ex and oy == ey)): + print '(= i{0}x{1}y{2} i{3}x{1}y{2})'.format( + i, ox, oy, i-1), + print ')' + print ')' + + print ';Negated winning condition' + print 'i{}x{}y{}'.format(iterations-1, winning[0], winning[1]), + print ' '.join('(not i{}x{}y{})'.format(iterations-1, x, y) + for x, y in pos if (x, y) != winning) + + print '))' + +if __name__ == '__main__': + generate() diff --git a/a2/src/4/print4.py b/a2/src/4/print4.py new file mode 100644 index 0000000..c0fcfdd --- /dev/null +++ b/a2/src/4/print4.py @@ -0,0 +1,44 @@ +#!/bin/env python +"""hi""" + +import sys +import re + +PAT = r'\(= i(?P\d+)x(?P\d+)y(?P\d+) (?Ptrue|false)\)' + +def print_board(data, tofile): + """Prints a peg solitaire board""" + for yco in range(8): + for xco in range(8): + pos = [d for d in data if d[0] == xco and d[1] == yco] + if not pos: + tofile.write(' ') + else: + tofile.write('.' if pos[0][2] else 'o') + tofile.write('\n') + +def parse(lines, output): + """Parse the model from yices""" + data = {} + for line in lines: + line = line.strip() + match = re.match(PAT, line) + if match: + ite = int(match.group('i')) + if ite not in data: + data[ite] = [] + data[ite].append((int(match.group('x')), int(match.group('y')), + match.group('v') == 'true')) + for _, dat in sorted(data.items()): + print_board(dat, output) + + +if __name__ == '__main__': + if len(sys.argv) == 1: + parse(sys.stdin, sys.stdout) + elif len(sys.argv) == 2: + with open(sys.argv[1], 'r') as fin: + parse(fin, sys.stdout) + else: + with open(sys.argv[1], 'r') as fin, open(sys.argv[2], 'w') as fout: + parse(fin, fout)