计算一个整数集的总和

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

如果您知道集合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)
           )
))

这可能不是很有效。