Рассчитать сумму набора 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

Если вам известны все элементы, которые могут содержаться в наборе 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)
           )
))

Это может быть не очень эффективно.