BitVector in Z3 - functions for different bits

Question

I have this code to check if other elements are contained sets.

;; All is encoding the set that contains {0, 1, 2, 3, 4, 5}
(define-const All (_ BitVec 6) #b111111)
;; Empty is encoding the empty set
(define-const Empty (_ BitVec 6) #b000000)

(define-fun LT_l ((S (_ BitVec 6)) (l (_ BitVec 6))) Bool
    ;; True if for all x in S x < l
    (= (bvand (bvshl All l) S) Empty))

(define-fun GT_l ((l (_ BitVec 6)) (S (_ BitVec 6))) Bool
    ;; True if for all x in S l < x
    (= (bvand (bvnot (bvshl All l)) S) Empty))

(define-fun is_in ((e (_ BitVec 6)) (S (_ BitVec 6))) Bool
   ;; True if e is an element of the "set" S.
   (not (= (bvand (bvshl (_ bv1 6) e) S) Empty)))

(define-fun is_minimal ((e (_ BitVec 6)) (S (_ BitVec 6))) Bool
    (and (is_in e S)
         (= (bvand (bvsub (bvshl (_ bv1 6) e) (_ bv1 6)) S) Empty)))

(define-fun LT ((L0 (_ BitVec 6)) (L1 (_ BitVec 6))) Bool
    ; True if forall x in L0 and forall y in L1, x < y
    (or (= L0 Empty)
        (= L1 Empty)
        (exists ((min (_ BitVec 6))) (and (is_minimal min L1) (LT_l L0 min)))))


(declare-const consoleLock (_ BitVec 6))
(declare-const l1 (_ BitVec 6))
(declare-const l2 (_ BitVec 6)) 

( assert (distinct consoleLock l1 l2 ) )

( assert (or (= l1 (_ bv0 6)) (= l1 (_ bv1 6)) (= l1 (_ bv2 6)) (= l1 (_ bv4 6)) ))
( assert (or (= l2 (_ bv0 6)) (= l2 (_ bv1 6)) (= l2 (_ bv2 6)) (= l2 (_ bv4 6)) ))
( assert (or (= consoleLock (_ bv0 6)) (= consoleLock (_ bv1 6)) (= consoleLock (_ bv2 6)) (= consoleLock (_ bv4 6)) ))


(declare-const L4 (_ BitVec 6))
(declare-const L1 (_ BitVec 6))
(declare-const L0 (_ BitVec 6))
(declare-const L5 (_ BitVec 6))


(assert (LT_l L0 l1))
(assert (LT L0 L1))
(assert (GT_l L1 l1))

(assert (LT_l L4 l2))
(assert (LT L4 L5))
(assert (GT_l L5 l2))

(declare-const T1 (_ BitVec 6))
(assert (= T1 l1))
(assert (LT_l T1 l2))

(declare-const T2 (_ BitVec 6))
(assert (= T2 l2))
(assert (LT_l T2 l1))

(check-sat)
(get-model)

My problem is that you want to use this code also for vectors with 8-bit and 16-bit but it doesn't work.

For example, if I replace all (_ BitVec 6) by (_ BitVec 8), the above code does not work well, because the result should be unsat but it sat.

As if to 6-bit vectors works well.

How can I make it work for different sizes of bit vectors?

Answer 1

We also have to adjust the constant occurring in the example: #b111111, #b000000, (_ bv1 6), etc. That being said, SMT-LIB 2.0 format is not very convenient for writing parametric problems. I think the programmatic API is easier to use to encode parametric problems. Here is the same example encoded using the Z3 Python API. It is also available online here. We can change the size of the bit-vectors by replacing SZ = 6 with SZ = 8 or SZ = 16.

def All(sz):
    return BitVecVal(2**sz - 1, sz)

def Empty(sz):
    return BitVecVal(0, sz)

def LT_l(S, l):
    sz = S.size()
    return (All(sz) << l) & S == Empty(sz)

def GT_l(l, S):
    sz = S.size()
    return (~(All(sz) << l)) & S == Empty(sz)    

def is_in(e, S):
    sz = S.size()
    one = BitVecVal(1, sz)
    return (1 << e) & S != Empty(sz)

def is_minimal(e, S):
    sz = S.size()
    return And(is_in(e, S), ((1 << e) - 1) & S == Empty(sz))

def LT(L0, L1):
    sz = L0.size()
    min = BitVec('min', sz)
    return Or(L0 == Empty(sz), L1 == Empty(sz), Exists([min], And(is_minimal(min, L1), LT_l(L0, min))))

SZ=6
consoleLock = BitVec('consoleLock', SZ)
l1 = BitVec('l1', SZ)
l2 = BitVec('l2', SZ)    

s = Solver()
s.add(Distinct(consoleLock, l1, l2))
s.add(Or(l1 == 0, l1 == 1, l1 == 2, l1 == 4))
s.add(Or(l2 == 0, l2 == 1, l2 == 2, l2 == 4))
s.add(Or(consoleLock == 0, consoleLock == 1, consoleLock == 2, consoleLock == 4))

L4 = BitVec('L4', SZ)
L1 = BitVec('L1', SZ)
L0 = BitVec('L0', SZ)
L5 = BitVec('L5', SZ)

s.add(LT_l(L0, l1))
s.add(LT(L0, L1))
s.add(GT_l(L1, l1))
s.add(LT_l(L4, l2))
s.add(LT(L4, L5))
s.add(GT_l(L5, l2))

T1 = BitVec('T1', SZ)
s.add(T1 == l1)
s.add(LT_l(T1, l2))

T2 = BitVec('T2', SZ)
s.add(T2 == l2)
s.add(LT_l(T2, l1))

print s.check()