\myheading{Simple sudoku in SMT using functions and array}

\leveldown{}

\renewcommand{\CURPATH}{puzzles/sudoku/2}

Surely, you may want to use functions and arrays, like you would do in any \ac{PL}.

Arrays in SMT are immutable of course.
You can't modify them.
(There is nothing to modify.)
You can create a new array with a new element stored at some index, or replaced.

But here we will use only \textit{select} operation on arrays.

Also, functions in SMT are more like macros.

\lstinputlisting[style=customsmt]{\CURPATH/sudoku_array.smt}
( \url{\RepoURL/\CURPATH/sudoku_array.smt} )

Let's see how different SMT solvers produce results, dumping array's content:

\begin{lstlisting}[caption=STP]
(model
( define-fun |cells|  (_ BitVec 8) (_ BitVec 4) #x70 #x5 )
( define-fun |cells|  (_ BitVec 8) (_ BitVec 4) #x62 #x1 )
( define-fun |cells|  (_ BitVec 8) (_ BitVec 4) #x38 #x2 )
( define-fun |cells|  (_ BitVec 8) (_ BitVec 4) #x28 #x3 )
( define-fun |cells|  (_ BitVec 8) (_ BitVec 4) #x85 #x4 )

...

( define-fun |cells|  (_ BitVec 8) (_ BitVec 4) #x40 #x9 )
( define-fun |cells|  (_ BitVec 8) (_ BitVec 4) #x84 #x9 )
( define-fun |cells|  (_ BitVec 8) (_ BitVec 4) #x66 #x8 )
( define-fun |cells|  (_ BitVec 8) (_ BitVec 4) #x21 #x7 )
( define-fun |cells|  (_ BitVec 8) (_ BitVec 4) #x63 #x5 )
)
\end{lstlisting}

Some SMT solvers dumps a function that create an array using \textit{store} operations:

\begin{lstlisting}[caption=Z3]
(
  (define-fun cells () (Array (_ BitVec 8) (_ BitVec 4))
    (let ((a!1 (store (store (store ((as const (Array (_ BitVec 8) (_ BitVec 4)))
                                  #x1)
                                #x07
                                #x7)
                         #x18
                         #x3)
                  #x71
                  #x9)))
(let ((a!2 (store (store (store (store a!1 #x38 #x2) #x45 #x3) #x60 #x7)
                  #x65
                  #x8)))
(let ((a!3 (store (store (store (store a!2 #x50 #x6) #x43 #x8) #x12 #x9)
                  #x28
                  #x8)))

...

(let ((a!18 (store (store (store (store a!17 #x21 #x7) #x17 #x2) #x10 #x8)
                   #x03
                   #x3)))
  (store a!18 #x02 #x5))))))))))))))))))))
)
\end{lstlisting}

Some other SMT solvers create an \ac{ITE}-tree, that will behave exactly like the array filled with correct values.
In fact, you can copy and paste this output and use it as a function in your SMT code:

\begin{lstlisting}[caption=Boolector]
(
  (define-fun cells (
   (cells_x0 (_ BitVec 8))) (_ BitVec 4)
    (ite (= cells_x0 (_ bv8 8)) (_ bv4 4)
    (ite (= cells_x0 (_ bv7 8)) (_ bv7 4)
    (ite (= cells_x0 (_ bv6 8)) (_ bv6 4)
    (ite (= cells_x0 (_ bv5 8)) (_ bv9 4)
    (ite (= cells_x0 (_ bv4 8)) (_ bv8 4)
    (ite (= cells_x0 (_ bv3 8)) (_ bv3 4)

...

    (ite (= cells_x0 (_ bv131 8)) (_ bv1 4)
    (ite (= cells_x0 (_ bv130 8)) (_ bv8 4)
    (ite (= cells_x0 (_ bv128 8)) (_ bv2 4)
    (ite (= cells_x0 (_ bv129 8)) (_ bv3 4)
      (_ bv0 4)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)
\end{lstlisting}

\begin{lstlisting}[caption=Bitwuzla]
(
  (define-fun cells ((@x0 (_ BitVec 8))) (_ BitVec 4)
    (ite (= @x0 (_ bv8 8)) (_ bv8 4)
    (ite (= @x0 (_ bv7 8)) (_ bv7 4)
    (ite (= @x0 (_ bv6 8)) (_ bv6 4)
    (ite (= @x0 (_ bv5 8)) (_ bv9 4)
    (ite (= @x0 (_ bv4 8)) (_ bv2 4)
    (ite (= @x0 (_ bv3 8)) (_ bv3 4)
...
    (ite (= @x0 (_ bv131 8)) (_ bv1 4)
    (ite (= @x0 (_ bv130 8)) (_ bv8 4)
    (ite (= @x0 (_ bv128 8)) (_ bv3 4)
    (ite (= @x0 (_ bv129 8)) (_ bv2 4)
      (_ bv0 4)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)
\end{lstlisting}

Unlike Z3, CVC5 dumps a function that constructs array without using \textit{let}, but again, using nested \textit{store} operations:

\begin{lstlisting}[caption=CVC5]
(
(define-fun cells () (Array (_ BitVec 8) (_ BitVec 4)) (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store ((as const (Array (_ BitVec 8) (_ BitVec 4))) #b0000) #b00000010 #b0101) #b00000011 #b0011) #b00010000 #b1000) #b00010111 #b0010) #b00100001 #b0111) #b00100100 #b0001) #b00100110 #b0101) #b00110000 #b0100) #b00110101 #b0101) #b00110110 #b0011) #b01000001 #b0001) #b01000100 #b0111) #b01001000 #b0110) #b01010010 #b0011) #b01010011 #b0010) #b01010111 #b1000) #b01100001 #b0110) #b01100011 #b0101) #b01101000 #b1001) #b01110010 #b0100) #b01110111 #b0011) #b10000100 #b1001) #b10000110 #b0111) #b00000000 #b0001) #b00000001 #b0100) #b00000100 #b0010) #b00000101 #b1001) #b00000110 #b0110) #b00000111 #b0111) #b00001000 #b1000) #b00010001 #b0011) #b00010010 #b1001) #b00010011 #b0110) #b00010100 #b0101) #b00010101 #b0111) #b00010110 #b0001) #b00011000 #b0100) #b00100000 #b0010) #b00100010 #b0110) #b00100011 #b0100) #b00100101 #b1000) #b00100111 #b1001) #b00101000 #b0011) #b00110001 #b1000) #b00110010 #b0111) #b00110011 #b1001) #b00110100 #b0110) #b00110111 #b0001) #b00111000 #b0010) #b01000000 #b1001) #b01000010 #b0010) #b01000011 #b1000) #b01000101 #b0011) #b01000110 #b0100) #b01000111 #b0101) #b01010000 #b0110) #b01010001 #b0101) #b01010100 #b0100) #b01010101 #b0001) #b01010110 #b1001) #b01011000 #b0111) #b01100000 #b0111) #b01100010 #b0001) #b01100100 #b0011) #b01100101 #b0010) #b01100110 #b1000) #b01100111 #b0100) #b01110000 #b0101) #b01110001 #b1001) #b01110011 #b0111) #b01110100 #b1000) #b01110101 #b0110) #b01110110 #b0010) #b01111000 #b0001) #b10000000 #b0011) #b10000001 #b0010) #b10000010 #b1000) #b10000011 #b0001) #b10000101 #b0100) #b10000111 #b0110) #b10001000 #b0101))
)
\end{lstlisting}

Yices does something slightly different:

\begin{lstlisting}[caption=Yices]
(= cells @fun_172)
(function @fun_172
 (type (Array (_ BitVec 8) (_ BitVec 4)))
 (= (@fun_172 #b00000011) #b0011)
 (= (@fun_172 #b00010000) #b1000)
 (= (@fun_172 #b00010111) #b0010)
 (= (@fun_172 #b00100001) #b0111)
 (= (@fun_172 #b00100100) #b0001)

...

 (= (@fun_172 #b10000101) #b0100)
 (= (@fun_172 #b10000111) #b0110)
 (default #b0101))
\end{lstlisting}

\levelup{}