\myheading{Can rand() generate 100 consecutive zeroes? (SMT-LIB versions)}

\leveldown{}

Let's implement this in terms of SMT-LIB language.

\myheading{Version 1: unrolled}

\lstinputlisting[style=customsmt]{\CURPATH/1_unrolled.smt}

\TT{QF\_BV} logic means "quantifier free, bitvector".

So far so good, but a bit redundant.
Can we wrap these redundant parts into function(s)?

\myheading{Version 2: functions}

We can define functions in SMT-LIB language:

\lstinputlisting[style=customsmt]{\CURPATH/2_func.smt}

\myheading{Version 3: function + array}

Now arrays.
You see, declaring many "state" variables is also redundant.
Can't we use arrays here?

\lstinputlisting[style=customsmt]{\CURPATH/3_array_func.smt}

Here we use the \TT{QF\_ABV} SMT logic: same as in \TT{QF\_BV}, but \TT{A} means \textit{arrays}.

We use arrays also in this example: \ref{SMT_popcount}.

Here we define relationships between various elements of array:

\begin{lstlisting}
(assert (= (PRNG_step (select states #x1)) (select states #x2)))
(assert (= (PRNG_step (select states #x2)) (select states #x3)))
(assert (= (PRNG_step (select states #x3)) (select states #x4)))
\end{lstlisting}

Here we \textit{read} from array:

\begin{lstlisting}
(assert (= (PRNG_get_result_modulo_1000 (select states #x2)) (_ bv0 32)))
(assert (= (PRNG_get_result_modulo_1000 (select states #x3)) (_ bv0 32)))
(assert (= (PRNG_get_result_modulo_1000 (select states #x4)) (_ bv0 32)))
\end{lstlisting}

\myheading{Version 4: \ac{UF} + array}

We can also define function using \ac{UF}.
These functions that has no body.
This is a bit unusual concept for a programmer accustomed to languages derived from Algol or Lisp.

However, you can describe behaviour of \ac{UF} using additional constraints.

\lstinputlisting[style=customsmt]{\CURPATH/4_array_UF.smt}

Take a closer look:

\begin{lstlisting}[style=customsmt]
(assert (forall ((x (_ BitVec 32)))
        (= (rand x) (bvadd (bvmul x const1) const2))))
\end{lstlisting}

In Plain English, this means:
"for all (32-bit) X's, rand(x)'s value is always equals to (bvadd (bvmul X const1) const2))))".

This is First-Order Logic.
"For all" is an \textit{universal quantifier}, usually denoted as an "A" letter upside down: $\forall$.

Since quantifiers exists in the example, another SMT logic is to be used:
\TT{AUFBV} (A stands for Arrays, UF for \ac{UF}, BV stands for bitvector, but notice we dropped the \TT{QF\_} prefix).

UF's are then \textit{called}, as in Lisp language: "(function\_name arg1 arg2 ...)".

\myheading{Performance}

(Time in seconds, running on my relic Intel Core 2 Duo T9400, clocked at 2.13GHz.)

\iffalse
| SMT-solver          | v1 (unrolled) | v2 (functions) | v3 (function + array) | v4 (UF + array) |
|---------------------+---------------+----------------+-----------------------+-----------------|
| STP 2.3.3           |           3.6 |            3.6 |                   5.6 |               * |
| Boolector 3.2.1     |             8 |              8 |                     5 |             3.5 |
| CVC4 1.9-prerelease |            21 |             21 |                    16 |               5 |
| Z3 4.8.9            |            23 |             23 |                    26 |             133 |
| Yices 2.6.2         |             6 |              6 |                    11 |               * |
| MK85                |           209 |                |                       |                 |
\fi

\begin{center}
  \begin{tabular}{ | l | l | l | l | l | }
    \hline
SMT-solver          & v1 (unrolled) & v2 (functions) & v3 (function + array) & v4 (UF + array) \\ \hline
STP 2.3.3           &           3.6 &            3.6 &                   5.6 &               * \\
Boolector 3.2.1     &             8 &              8 &                     5 &             3.5 \\
CVC4 1.9-prerelease &            21 &             21 &                    16 &               5 \\
Z3 4.8.9            &            23 &             23 &                    26 &             133 \\
Yices 2.6.2         &             6 &              6 &                    11 &               * \\
MK85                &           209 &              * &                     * &               * \\
    \hline
  \end{tabular}
\end{center}

*) Couldn't manage to run it

Also, since the first version of the example is that simple,
my toy-level bitblaster (MK85, that is based on picosat SAT solver) can solve it,
slower by factor of 10x then others, but still...

\myheading{Bruteforce}

But what about bruteforce?
Yes, you can solve this problem using simple bruteforce.
32-bit search space is small enough.
But... this is what I can do in pure C:

\lstinputlisting[style=customc]{\CURPATH/BF.c}

If compiled with \TT{GCC -O3}, it will run for 12 seconds on the same CPU.
Faster than Z3 and CVC4, but slower than STP and Boolector!
Modulo division is a heavy operation, but it seems, these SMT solvers can find ways to cut the search space!

\myheading{The files}

\url{\RepoURL/\CURPATH}

\levelup{}