z3 - Z3 中的 BitVector - 不同位的函数

Question

我有这段代码来检查其他元素是否包含在集合中。

;; 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)

我的问题是您想将此代码也用于 8 位和 16 位向量，但它不起作用。

例如，如果我将所有 (_ BitVec 6) 替换为 (_ BitVec 8)，则上述代码无法正常工作，因为结果应该是 unsat，但它却是 sat。

好像 6 位向量效果很好。

如何使其适用于不同大小的位向量？

Answer 1

我们还必须调整示例中出现的常量:#b111111、#b000000、(_ bv1 6) 等。话虽这么说，SMT-LIB 2.0 格式对于编写参数问题不是很方便。我认为编程 API 更容易用来编码参数问题。以下是使用 Z3 Python API 编码的相同示例。也可以在线获取 here 。我们可以通过将 SZ = 6 替换为 SZ = 8 或 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()