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
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
\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}
\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}
\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}
+++ /dev/null
-#!/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)
+++ /dev/null
-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)
--- /dev/null
+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)
+
--- /dev/null
+#!/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()
--- /dev/null
+#!/bin/env python
+"""hi"""
+
+import sys
+import re
+
+PAT = r'\(= i(?P<i>\d+)x(?P<x>\d+)y(?P<y>\d+) (?P<v>true|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)
repositories / ar1516.git / commitdiff