[SMT][Z3] Can rand() generate 3 consecutive zeroes?

I was thinking about this: can rand() generate 10 consecutive zeroes? There is an example in my book. In short - yes, if the result is modulo divided by 10.

The example was written in Z3Py (Python's API to Z3). This time I'll try to translate it to SMT-LIB v2 using uninterpreted functions (UF's) and arrays.

Version 1

Look at this (version 1):

(set-logic QF_BV)
(set-info :smt-lib-version 2.0)

;(declare-const const1 (_ BitVec 32)) ; Z3's syntax
(declare-fun const1 () (_ BitVec 32))
(assert (= const1 (_ bv214013 32)))
;(declare-const const2 (_ BitVec 32)) ; Z3's syntax
(declare-fun const2 () (_ BitVec 32))
(assert (= const2 (_ bv2531011 32)))

(declare-fun state1 () (_ BitVec 32))
(declare-fun state2 () (_ BitVec 32))
(declare-fun state3 () (_ BitVec 32))
(declare-fun state4 () (_ BitVec 32))

(assert (= (bvadd (bvmul state1 const1) const2) state2))
(assert (= (bvadd (bvmul state2 const1) const2) state3)) ; isn't it redundant?
(assert (= (bvadd (bvmul state3 const1) const2) state4)) ; isn't it redundant?

(assert (= (bvurem (bvand (bvlshr state2 (_ bv16 32)) #x00007fff) (_ bv1000 32)) (_ bv0 32)))
(assert (= (bvurem (bvand (bvlshr state3 (_ bv16 32)) #x00007fff) (_ bv1000 32)) (_ bv0 32))) ; isn't it redundant?
(assert (= (bvurem (bvand (bvlshr state4 (_ bv16 32)) #x00007fff) (_ bv1000 32)) (_ bv0 32))) ; isn't it redundant?

; two correct solutions:
;(assert (not (= state1 #xf3cbf334)))
;(assert (not (= state1 #x73cbf334)))

(check-sat)
(get-model)

QF_BV logic means "quantifier free, bitvector".

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

Version 2

SMT solvers don't have functions in general sense. These are UF's (uninterpreted functions), functions that has no body. This is a bit unusual concept for a programmer accustomed to languages derived from Algol or Lisp.

However, in SMT world, you describe behaviour of uninterpreted functions using additional constraints. This is what I did (version 2):

(set-logic UFBV)
(set-info :smt-lib-version 2.0)

(declare-fun const1 () (_ BitVec 32))
(assert (= const1 (_ bv214013 32)))
(declare-fun const2 () (_ BitVec 32))
(assert (= const2 (_ bv2531011 32)))

(declare-fun rand ((_ BitVec 32)) (_ BitVec 32))
(assert (forall ((x (_ BitVec 32)))
        (= (rand x) (bvadd (bvmul x const1) const2))))

(declare-fun state1 () (_ BitVec 32))
(declare-fun state2 () (_ BitVec 32))
(declare-fun state3 () (_ BitVec 32))
(declare-fun state4 () (_ BitVec 32))

(assert (= (rand state1) state2))
(assert (= (rand state2) state3))
(assert (= (rand state3) state4))

(declare-fun get_result ((_ BitVec 32)) (_ BitVec 32))
(assert (forall ((x (_ BitVec 32)))
        (= (get_result x) (bvurem (bvand (bvlshr x (_ bv16 32)) #x00007fff) (_ bv1000 32)))))

(assert (= (get_result state2) (_ bv0 32)))
(assert (= (get_result state3) (_ bv0 32)))
(assert (= (get_result state4) (_ bv0 32)))

(check-sat)
(get-model)

This gives 0xf3cbf334 or 0x73cbf334 -- both values if supplied to srand() in MSVC would result in 3 consecutive "rand() % 1000 == 0". (Read more.)

Take a closer look:

...

(declare-fun rand ((_ BitVec 32)) (_ BitVec 32))
(assert (forall ((x (_ BitVec 32)))
        (= (rand x) (bvadd (bvmul x const1) const2))))

...

(assert (= (rand state1) state2))
(assert (= (rand state2) state3))

...

(declare-fun get_result ((_ BitVec 32)) (_ BitVec 32))
(assert (forall ((x (_ BitVec 32)))
        (= (get_result x) (bvurem (bvand (bvlshr x (_ bv16 32)) #x00007fff) (_ bv1000 32)))))

(assert (= (get_result state2) (_ bv0 32)))

...

In Plain English, this means "for all (32-bit) X's, rand(x)'s value is always equal to (bvadd (bvmul X const1) const2))))". This is First-Order Logic. "For all" is universal quantifier, usually denoted as an "A" letter upside down: $\forall$.

Since quantifiers exists in the example, another SMT logic is to be used: UFBV (UF stands for uninterpreted functions, BV stands for bitvector, but notice we dropped the "QF_" prefix).

UF's are then "called", as in Lisp language: "(function_name arg1 arg2 ...)".

And ever more. You can say that SMT solvers have no idea about variables. Can you get rid of them? For example, in C/C++ you can use this function for $\Pi$ constant instead of accessing a constant variable or using preprocessor macro:

double PI ()
{
	return 3.1415926;
};
In SMT world, you don't declare variables, you declare argumentless functions that value is either fixed:
...
(declare-fun const1 () (_ BitVec 32))
(assert (= const1 (_ bv214013 32)))
...

... or it's "connected" to another expression/function's value/etc. This is why variables are declared using "declare-fun" directive. (However, Z3 support "declare-const" directive, which is merely a syntactic sugar.)

Version 3

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

;(set-logic AUFBV) ; Boolector can't parse this
(set-info :smt-lib-version 2.0)

(declare-fun const1 () (_ BitVec 32))
(assert (= const1 (_ bv214013 32)))
(declare-fun const2 () (_ BitVec 32))
(assert (= const2 (_ bv2531011 32)))

(declare-fun rand ((_ BitVec 32)) (_ BitVec 32))
(assert (forall ((x (_ BitVec 32)))
        (= (rand x) (bvadd (bvmul x const1) const2))))

(declare-const states (Array (_ BitVec 4) (_ BitVec 32)))

(declare-fun init () (_ BitVec 32))
(assert (= init (select states #x1)))

(assert (= states (store states #x2 (rand (select states #x1)))))
(assert (= states (store states #x3 (rand (select states #x2)))))
(assert (= states (store states #x4 (rand (select states #x3)))))

(declare-fun get_result ((_ BitVec 32)) (_ BitVec 32))
(assert (forall ((x (_ BitVec 32)))
        (= (get_result x) (bvurem (bvand (bvlshr x (_ bv16 32)) #x00007fff) (_ bv1000 32)))))

(assert (= (get_result (select states #x2)) (_ bv0 32)))
(assert (= (get_result (select states #x3)) (_ bv0 32)))
(assert (= (get_result (select states #x4)) (_ bv0 32)))

(check-sat)
(get-model)

Here we use the "AUFBV" SMT logic: same as in the version 2, but "A" means "arrays".

I used arrays before. One way of thinking about them as about immutable data structures. You can't write to array. But you can create a new array based on an old array with one element altered. This is what "store" operations does.

Here I recreate a "states" array 3 times:

...
(declare-const states (Array (_ BitVec 4) (_ BitVec 32)))

(assert (= states (store states #x2 (rand (select states #x1)))))
(assert (= states (store states #x3 (rand (select states #x2)))))
(assert (= states (store states #x4 (rand (select states #x3)))))
...

The last "version" of the array that has been created during the 3rd "assert" is then "used" using "select" directive:

...
(assert (= (get_result (select states #x2)) (_ bv0 32)))
(assert (= (get_result (select states #x3)) (_ bv0 32)))
(assert (= (get_result (select states #x4)) (_ bv0 32)))
...

Version 4

We can get rid of "store" operations by this:
...
(assert (= (select states #x2) (rand (select states #x1))))
(assert (= (select states #x3) (rand (select states #x2))))
(assert (= (select states #x4) (rand (select states #x3))))
...

But this slows down everything significantly for Z3 and Boolector. But CVC4 works faster. I don't know, why.

Performance

I've heard rumours that arrays support is still slow in SMT. Hard to say. Yes, SAT/SMT solvers' performance is still highly unpredictable. But it's not that bad.

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...

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

| SMT-solver      |  v1 | v2  | v3  |  v4 |
|-----------------+-----+-----+-----+-----|
| STP 2.3.3       |   4 | **  | **  |  ** |
| Boolector 3.2.0 |  17 | 29  | 7   |  10 |
| CVC4 1.8        |  22 | 26* | 14* |  5* |
| Z3 4.8.8        |  26 | 64  | 20  | 134 |
| MK85            | 230 |     |     |     |

*) CVC4 reports "unknown", but produces correct results.
**) I could't manage STP to run on these versions.

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:

#include <stdio.h>
#include <stdlib.h>

int main()
{
	for (unsigned int seed=0; ; seed++)
	{
		unsigned int t=seed;
		t=t*214013 + 2531011;
		unsigned int a1=((t>>16)&0x7fff) % 1000;
                if (a1!=0)
                        continue;
		t=t*214013 + 2531011;
		unsigned int a2=((t>>16)&0x7fff) % 1000;
                if (a2!=0)
                        continue;
		t=t*214013 + 2531011;
		unsigned int a3=((t>>16)&0x7fff) % 1000;
                if (a3==0)
                {
        		printf ("seed: 0x%x\n", seed);
	        	exit(0);
                };
                if (seed==0xffffffff)
                        break;
	};
};

If compiled with 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!

The files

Here.


Please drop me email about bug(s) and/or suggestion(s): dennis@yurichev.com