0

我有以下代码： (declare-const L4 (_ BitVec 6)) (declare-const L1 (_ BitVec 6)) (declare-const L0 (_ BitVec 6)) (declare-const l2 (_ BitVec 6) ))

(assert (= l2 (_ bv8 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
    (= (bvand (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
    ;; 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))) 

;; 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
    (or (= L0 Empty)
        (= L1 Empty)
        (exists ((min (_ BitVec 6))) (and (is_minimal min L1) (LT_l L0 min)))))

(assert (not (= L0 Empty)))
(assert (not (= L1 Empty)))
(assert (not (= L4 Empty)))
(assert (LT_l L4 l2))
(assert (LT L0 L1))
(check-sat)
(get-model)
(assert (LT L1 L0))
(check-sat)

当我运行此代码时，我得到的模型是： sat (model (define-fun min!0 () (_ BitVec 6) #b000011) (define-fun L1 () (_ BitVec 6) #b001000) (define-fun L0 () (_BitVec 6) #b000100) (define-fun L4 () (_BitVec 6) #b000100) (define-fun l2 () (_BitVec 6) #b001000) ) unsat

为什么结果min是：

(define-fun min!0 () (_ BitVec 6)
    #b000011)

而不是 b001000，因为 L1 的最小值是这个而不是 b000011。

有人可以解释一下吗？

最后，我定义了函数 Lt_l 来检查 S x < l 中的所有 x 是否存在，但现在我想做 GT_l 来检查 S l < x 中的所有 x 是否存在。我有以下代码：

(define-fun GT_l ((S (_ BitVec 6)) (l (_ BitVec 6))) Bool
    (= (bvand (bvneg (bvshl (_ bv0 6) l)) S) Empty))

但这不起作用为什么？

谢谢

4

1 回答 1

1

在您的示例中，您使用位向量表示集合。例如，位向量#b101000表示集合{5, 3}。输出(define-fun L1 () (_ BitVec 6) #b001000)本质上是说那L1是 "set" {3}。一种可能的混淆是位向量被用来表示集合和元素。位向量min!0表示一个元素。输出(define-fun min!0 () (_ BitVec 6) #b000011)说的min!0是 value 3，它确实是 中的“最小值” L1。

于 2013-05-23T15:35:11.233 回答