\myheading{SMT solver}
\label{SMT_popcount}

\leveldown{}

Can we do the same using SMT solver?

Here I am encoding popcount64a() function and also its "naive" counterpart in SMT-LIB language:

\begin{lstlisting}[style=customsmt]
(declare-fun c0 () (_ BitVec 64)) (assert (= c0 (_ bv0 64))) ; always 0
(declare-fun c1 () (_ BitVec 64)) (assert (= c1 (_ bv1 64))) ; always 1

(declare-fun m1  () (_ BitVec 64)) (assert (= m1 #x5555555555555555))
(declare-fun m2  () (_ BitVec 64)) (assert (= m2 #x3333333333333333))
(declare-fun m4  () (_ BitVec 64)) (assert (= m4 #x0f0f0f0f0f0f0f0f))
(declare-fun m8  () (_ BitVec 64)) (assert (= m8 #x00ff00ff00ff00ff))
(declare-fun m16 () (_ BitVec 64)) (assert (= m16 #x0000ffff0000ffff))
(declare-fun m32 () (_ BitVec 64)) (assert (= m32 #x00000000ffffffff))

...

(assert (= a_x1  (bvadd (bvand a_x m1)   (bvand (bvlshr a_x  (_ bv1 64)) m1))))
(assert (= a_x2  (bvadd (bvand a_x1 m2)  (bvand (bvlshr a_x1 (_ bv2 64)) m2))))
(assert (= a_x3  (bvadd (bvand a_x2 m4)  (bvand (bvlshr a_x2 (_ bv4 64)) m4))))
(assert (= a_x4  (bvadd (bvand a_x3 m8)  (bvand (bvlshr a_x3 (_ bv8 64)) m8))))
(assert (= a_x5  (bvadd (bvand a_x4 m16) (bvand (bvlshr a_x4 (_ bv16 64)) m16))))
(assert (= a_out (bvadd (bvand a_x5 m32) (bvand (bvlshr a_x5 (_ bv32 64)) m32))))

; popcount64(): the naive way:
; (x>>0)&1 + (x>>1)&1 + (x>>2)&1 + ...

(assert (= naive_out
(bvadd 
       (bvand (bvlshr naive_x (_ bv0 64)) (_ bv1 64))
       (bvand (bvlshr naive_x (_ bv1 64)) (_ bv1 64))

       ...
       
       (bvand (bvlshr naive_x (_ bv62 64)) (_ bv1 64))
       (bvand (bvlshr naive_x (_ bv63 64)) (_ bv1 64))
)))

...

(assert (= naive_x a_x)) (assert (not (= naive_out a_out)))
\end{lstlisting}

Kernighan's unrolled function a bit tougher:

\begin{lstlisting}[style=customsmt]
(declare-fun kern_x0 () (_ BitVec 64))
(declare-fun kern_x1 () (_ BitVec 64))
(assert (= kern_x1 (ite (= kern_x0 c0) kern_x0 (bvand kern_x0 (bvsub kern_x0 c1)))))
(declare-fun kern_x2 () (_ BitVec 64))
(assert (= kern_x2 (ite (= kern_x1 c0) kern_x1 (bvand kern_x1 (bvsub kern_x1 c1)))))

...

(declare-fun kern_x63 () (_ BitVec 64))
(assert (= kern_x63 (ite (= kern_x62 c0) kern_x62 (bvand kern_x62 (bvsub kern_x62 c1)))))
(declare-fun kern_x64 () (_ BitVec 64))
(assert (= kern_x64 (ite (= kern_x63 c0) kern_x63 (bvand kern_x63 (bvsub kern_x63 c1)))))

; be sure x==0 upon the function exit...
;(assert (not (= kern_x64 c0)))

(declare-fun kern_out () (_ BitVec 64))

; add 1 to kern_out each time if kern_xX!=0:
(assert (= kern_out (bvadd
	(ite (= kern_x0 c0) c0 c1) (ite (= kern_x1 c0) c0 c1) (ite (= kern_x2 c0) c0 c1) (ite (= kern_x3 c0) c0 c1)
	(ite (= kern_x4 c0) c0 c1) (ite (= kern_x5 c0) c0 c1) (ite (= kern_x6 c0) c0 c1) (ite (= kern_x7 c0) c0 c1)

	...
	
	(ite (= kern_x56 c0) c0 c1) (ite (= kern_x57 c0) c0 c1) (ite (= kern_x58 c0) c0 c1) (ite (= kern_x59 c0) c0 c1)
	(ite (= kern_x60 c0) c0 c1) (ite (= kern_x61 c0) c0 c1) (ite (= kern_x62 c0) c0 c1) (ite (= kern_x63 c0) c0 c1)
)))

...

(assert (= naive_x kern_x0)) (assert (not (= naive_out kern_out)))
\end{lstlisting}

Again, we can prove here that the last state of "x" would always be zero.

Maybe I encoded the problem in a wrong way, but this time, both CVC4 and Z3 stuck and couldn't solve anything
withing ~15 minutes timeout.
However, Boolector can prove it for ~1 minute.

Of course, I could misunderstood something.

\myheading{SMT arrays}

Now what about array encoding?

\begin{lstlisting}[style=customsmt]
;int popcount64_table(uint64_t x)
;{
;	uint64_t tbl[16]={0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4};
;	uint64_t rt=0;
;	rt=rt+tbl[(x>>(0*4))&0xf];
;	rt=rt+tbl[(x>>(1*4))&0xf];
;...

; fill table of constants:
(declare-const tbl (Array (_ BitVec 64) (_ BitVec 64)))
(assert (= tbl (store tbl (_ bv0 64) (_ bv0 64))))
(assert (= tbl (store tbl (_ bv1 64) (_ bv1 64))))
...
(assert (= tbl (store tbl (_ bv14 64) (_ bv3 64))))
(assert (= tbl (store tbl (_ bv15 64) (_ bv4 64))))

(declare-fun tbl_x () (_ BitVec 64))
(declare-fun tbl_out () (_ BitVec 64))

;	rt=rt+tbl[(x>>(0*4))&0xf];
;	rt=rt+tbl[(x>>(1*4))&0xf];
;	...
(assert (= tbl_out
(bvadd
       (select tbl (bvand (bvlshr tbl_x (_ bv0 64)) (_ bv15 64)))
       (select tbl (bvand (bvlshr tbl_x (_ bv4 64)) (_ bv15 64)))
       ...
       (select tbl (bvand (bvlshr tbl_x (_ bv56 64)) (_ bv15 64)))
       (select tbl (bvand (bvlshr tbl_x (_ bv60 64)) (_ bv15 64)))
)))
\end{lstlisting}

Here we use "store" function to populate array.
At each line, tbl is reassigned.
We then use "select" function to address elements of the array.

Arrays are implemented in SMT solvers using \ac{UF}, but logically, you can think about them
as about chains of ITE's (if-then-else).
Or like a switch() construct found in many popular PLs.

Even more, Boolector during model generation ("get-model"), shows arrays as ITE chains:

\begin{lstlisting}
  (define-fun f (
   (f_x0 (_ BitVec 64))) (_ BitVec 64)
    (ite (= f_x0 #b0000000000000000000000000000000000000000000000000000000000000000) #b0000000000000000000000000000000000000000000000000000000000000000
    (ite (= f_x0 #b0000000000000000000000000000000000000000000000000000000000000001) #b0000000000000000000000000000000000000000000000000000000000000001

...
    
    (ite (= f_x0 #b0000000000000000000000000000000000000000000000000000000000001111) #b0000000000000000000000000000000000000000000000000000000000000100
      #b0000000000000000000000000000000000000000000000000000000000000000)))))))))))))))))
\end{lstlisting}

(We see here that the default value is 0, it's like "default" in "switch()" statement.)

As well as Z3:

\begin{lstlisting}
  (define-fun f ((x!0 (_ BitVec 64))) (_ BitVec 64)
    (ite (= x!0 #x0000000000000003) #x0000000000000002
    (ite (= x!0 #x0000000000000004) #x0000000000000001
    ...
    (ite (= x!0 #x0000000000000002) #x0000000000000001
    (ite (= x!0 #x0000000000000009) #x0000000000000002
      #x0000000000000000))))))))))))))))
\end{lstlisting}

You can think about "select" function as if it simply evaluates internal ITE chain.
And "store" function simply prepends new ITE in front of an array (or ITE chain) returning a new array (or chain).

Anyway, this version Boolector can solve for ~15 seconds, Z3 for ~7 minutes and CVC4 is stuck.

\myheading{Uninterpreted functions}

Since my array is a constant one, I can try to implement it using \ac{UF}.

Here f() acts like the "select" function.
And it's populated like: \verb|assert f(0) is 0, f(1) is 1 ... f(15) is (4)|

\begin{lstlisting}[style=customsmt]
(declare-fun f ((_ BitVec 64)) (_ BitVec 64))
(assert (= (f (_ bv0 64)) (_ bv0 64)))
(assert (= (f (_ bv1 64)) (_ bv1 64)))
...
(assert (= (f (_ bv14 64)) (_ bv3 64)))
(assert (= (f (_ bv15 64)) (_ bv4 64)))

(declare-fun f_x () (_ BitVec 64))
(declare-fun f_out () (_ BitVec 64))

;	rt=rt+f((x>>(0*4))&0xf);
;	rt=rt+f((x>>(1*4))&0xf);
;	...
(assert (= f_out
(bvadd
       (f (bvand (bvlshr f_x (_ bv0 64)) (_ bv15 64)))
       (f (bvand (bvlshr f_x (_ bv4 64)) (_ bv15 64)))
       ...
       (f (bvand (bvlshr f_x (_ bv56 64)) (_ bv15 64)))
       (f (bvand (bvlshr f_x (_ bv60 64)) (_ bv15 64)))
)))
\end{lstlisting}

Boolector and Z3 can solve this for ~10-15 seconds, CVC4 is stuck.

\myheading{Moral of the story}

SAT/SMT solvers are highly capricious for various types of input.
So it's good idea to try several of them.
And of course, I probably misunderstood something, don't know yet, what exactly.

\levelup{}