Using the set theory of CVC4 (version 1.8-prerelease [git master a90b9e2b]) I have defined a set of integers with a fixed cardinality
(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 then gives me one correct model
sat
(model
(define-fun A () (Set Int) (union (union (union (union (singleton 0) (singleton 1)) (singleton (- 1))) (singleton 2)) (singleton (- 2))))
)
Is there a way to ask for the sum of the integers in set A?
As Patrick mentioned, these sorts of operations over arbitrary sets (like summing them up) is just not possible in SMTLib. However, you've more information: You know that the cardinality of the set is 5, so you can encode the summation indirectly.
The trick is to construct a set of the required cardinality explicitly and sum those elements. Obviously this only works well if the set is small enough, but you can "generate" the code automatically from a high-level API if necessary. (Hand coding it would be difficult!)
The below works with z3; Unfortunately CVC4 and Z3 differ in the function names for Sets a bit:
(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))
This produces:
$ 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))))
For CVC4, the encoding is similar:
(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))
For which, cvc4 produces:
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)))))
If the cardinality isn't fixed; I don't think you can code this up unless the domain is finite (or drawn from a finite subset of an infinite domain) as Patrick described.
Hope that helps!