z3 - Z3 中位向量的成员

Question

我需要知道如何在 z3 中执行以下操作:

对于 L4 中的所有 x 。 x

L0 中的所有 x 和 L1 中的所有 y。 x

(declare-const L4 (_ BitVec 6))
(declare-const L1 (_ BitVec 6))
(declare-const L0 (_ BitVec 6))
(declare-const l2 Int)
(declare-const l1 Int)

断言 L0 和 L1 使得 x < y

(check-sat)

结果是周六

断言 L0 和 L1 使得 y < x

(check-sat)

结果是 UnSat

Answer 1

我假设您正在使用位向量来编码有限集。 因此，这是一种可能的编码(也可以在线使用 here ):

;; You use bit-vectors of size 6. That is, we are encoding sets that are subsets of {0, 1, 2, ... 5}
(declare-const L4 (_ BitVec 6))
(declare-const L1 (_ BitVec 6))
(declare-const L0 (_ BitVec 6))
;; I will also encode l1 and l2 as Bit-Vectors.
;; Thus, I don't need to convert them into Bit-vectors to be able to use them in Bit-vector operations.
(declare-const l1 (_ BitVec 6))
(declare-const l2 (_ BitVec 6))
;; To make the problems more interesting let us assume that l1 and l2 are <= 5
(assert (bvsle l1 (_ bv5 6)))
(assert (bvsle l2 (_ bv5 6)))

;; 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
    ;; Note that: All << l is the set of values greater than l
    ;; In SMT-LIB, bvshl is the left shift operator <<  
    (= (bvand (bvshl All l) S) Empty))

;; We can use shifting to encode the set that contains all values in {0, 1, 2, 3, 4, 5} that greater than or equal to l2
(define-const GE_l2 (_ BitVec 6) (bvshl All l2))
;; To assert that forall x in L4. x < l2, we assert that the intersection of L4 and GE_l2 is empty 
(assert (= (bvand GE_l2 L4) Empty))

(check-sat)
(get-model) 

(define-fun is_in ((e (_ BitVec 6)) (S (_ BitVec 6))) Bool
   ;; True if e is an element of the "set" S.
   ;; That is, it checks whether the (1 << e) && S is 0
   (not (= (bvand (bvshl (_ bv1 6) e) S) Empty))) 

(echo "is_in tests")
;; Test: is 2 in the set {0,3}
(simplify (is_in (_ bv2 6) #b001001))
;; Test: is 0 in the set {0, 3}
(simplify (is_in (_ bv0 6) #b001001))
;; Test: is 3 in the set {0, 3}
(simplify (is_in (_ bv3 6) #b001001))
;; Test: is 4 in the set {0, 3}
(simplify (is_in (_ bv4 6) #b001001))
(echo "end is_in tests")

(define-fun is_minimal ((e (_ BitVec 6)) (S (_ BitVec 6))) Bool
    ;; True if e is the minimal element of S
    (and (is_in e S) ;; S contains e
         ;; (1 << e) - 1 represents the set of elements that are smaller than e
         (= (bvand (bvsub (bvshl (_ bv1 6) e) (_ bv1 6)) S) Empty))) 

(echo "is_minimal tests")
;; is 2 the minimal element in {5, 3}
(simplify (is_minimal (_ bv2 6) #b101000))
;; is 3 the minimal element in {5, 3}
(simplify (is_minimal (_ bv3 6) #b101000))
;; is 4 the minimal element in {5, 3}
(simplify (is_minimal (_ bv4 6) #b101000))
;; is 0 the minimal element in {4, 0}
(simplify (is_minimal (_ bv0 6) #b010001))
;; is 4 the minimal element in {4, 0}
(simplify (is_minimal (_ bv4 6) #b010001))
(echo "end is_minimal tests")

;; To encode that forall x in L0 and forall y in L1. x < y
(define-fun LT ((L0 (_ BitVec 6)) (L1 (_ BitVec 6))) Bool
    ; True if forall x in L0 and forall y in L1, x < y
    ; We encode that by saying that 
    ;    - L0 is empty OR
    ;    - L1 is empty OR
    ;    - Or Let min be the minimal value of L1 and Forall x in L0, x < min
    (or (= L0 Empty)
        (= L1 Empty)
        (exists ((min (_ BitVec 6))) (and (is_minimal min L1) (LT_l L0 min)))))

;; To make the problem non-trivial, let us assume that L0 and L1 are not empty
(assert (not (= L0 Empty)))
(assert (not (= L1 Empty)))
(assert (LT L0 L1))
(check-sat)
(get-model)
(assert (LT L1 L0))
(check-sat)