计算一个 Int Set 的总和

Question

使用 CVC4 的集合论（版本 1.8-prerelease [git master a90b9e2b]）我定义了一组具有固定基数的整数

(set-logic ALL_SUPPORTED)
(set-option :produce-models true)

(declare-fun A () (Set Int))
(assert (= 5 (card A)))

;;(assert (= sum (???)))

(check-sat)
(get-model)

CVC4 然后给了我一个正确的模型

sat
(model
(define-fun A () (Set Int) (union (union (union (union (singleton 0) (singleton 1)) (singleton (- 1))) (singleton 2)) (singleton (- 2))))
)

有没有办法求集合 A 中的整数之和？

Answer 1

正如帕特里克所说，在 SMTLib 中不可能对任意集合进行此类操作（例如对它们求和）。但是，您有更多信息：您知道集合的基数是 5，因此您可以对总和进行间接编码。

诀窍是明确地构造一组所需的基数并对这些元素求和。显然，这只有在集合足够小的情况下才有效，但如果需要，您可以从高级 API 自动“生成”代码。 （手工编码会很困难！）

以下适用于 z3；不幸的是，CVC4 和 Z3 在 Sets 的函数名称上略有不同：

(set-option :produce-models true)

; declare-original set
(declare-fun A () (Set Int))
(assert (= 5 (card A)))

; declare the "elements". We know there are 5 in this case. Declare one for each.
(declare-fun elt1 () Int)
(declare-fun elt2 () Int)
(declare-fun elt3 () Int)
(declare-fun elt4 () Int)
(declare-fun elt5 () Int)

; form the set out of these elements:
(define-fun B () (Set Int) (store (store (store (store (store ((as const (Array Int Bool)) false) elt1 true)
                                                       elt2 true)
                                                elt3 true)
                                         elt4 true)
                                  elt5 true))

; make sure our set is equal to the set just constructed:
(assert (= A B))

; now sum-up the elements
(declare-fun sum () Int)
(assert (= sum (+ elt1 elt2 elt3 elt4 elt5)))

(check-sat)
(get-value (elt1 elt2 elt3 elt4 elt5 sum A))

这会产生：

$ z3 a.smt2
sat
((elt1 0)
 (elt2 1)
 (elt3 3)
 (elt4 6)
 (elt5 7)
 (sum 17)
 (A (let ((a!1 (store (store (store ((as const (Set Int)) false) 0 true) 1 true)
                  3
                  true)))
  (store (store a!1 6 true) 7 true))))

对于CVC4，编码类似：

(set-option :produce-models true)
(set-logic ALL_SUPPORTED)

; declare-original set
(declare-fun A () (Set Int))
(assert (= 5 (card A)))

; declare the "elements". We know there are 5 in this case. Declare one for each.
(declare-fun elt1 () Int)
(declare-fun elt2 () Int)
(declare-fun elt3 () Int)
(declare-fun elt4 () Int)
(declare-fun elt5 () Int)

; form the set out of these elements:
(define-fun B () (Set Int) (union (singleton elt1)
                                  (union (singleton elt2)
                                         (union (singleton elt3)
                                                (union (singleton elt4) (singleton elt5))))))

; make sure our set is equal to the set just constructed:
(assert (= A B))

; now sum-up the elements
(declare-fun sum () Int)
(assert (= sum (+ elt1 elt2 elt3 elt4 elt5)))

(check-sat)
(get-value (elt1 elt2 elt3 elt4 elt5 sum A))

为此，cvc4 产生：

sat
((elt1 (- 4)) (elt2 (- 3)) (elt3 (- 2)) (elt4 (- 1)) (elt5 0) (sum (- 10)) (A (union (union (union (union (singleton 0) (singleton (- 1))) (singleton (- 2))) (singleton (- 3))) (singleton (- 4)))))

如果基数不固定；我认为除非域是有限的（或从无限域的有限子集中提取），否则我认为您无法编写此代码，正如 Patrick 所描述的那样。

希望有帮助！

Answer 2

如果您知道集合A（又名A 的有限超集域）中可能包含的所有元素，则一种选择是

(declare-fun A () (Set Int))
...
(declare-fun sum () Int)
(assert (= sum
           (+
               (ite (member 1 A) 1 0)
               (ite (member 2 A) 2 0)
               ...
               (ite (member k A) k 0)
           )
))

这可能不是很有效。