计算 Int 集的总和

Question

使用 CVC4 的集合论(版本 1.8-预发行版 [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

正如 Patrick 所提到的，在 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)))))

如果基数不固定;我不认为你可以编码它，除非域是有限的(或从无限域的有限子集中提取(，如帕特里克所描述的那样。

希望对您有所帮助！

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

这可能不是很有效。