squirrels.smt2

(define-sort MultiSet (T) (Array T Int))

(declare-const squirrels (MultiSet Int))

(assert (= (select squirrels 2) (select squirrels 3) (select squirrels 5) (select squirrels 8) (select squirrels 22) 1))
(assert (= (select squirrels 9) (select squirrels 12) 2))
(assert (= (store (store (store (store (store (store (store squirrels 2 0) 3 0) 5 0) 8 0) 9 0) 12 0) 22 0) ((as const (MultiSet Int)) 0)))

(define-fun round-cond ((s (MultiSet Int))) Bool
            (and
             (>= (select s 2) 0)
             (>= (select s 3) 0)
             (>= (select s 5) 0)
             (>= (select s 8) 0)
             (>= (select s 9) 0)
             (>= (select s 12) 0)
             (>= (select s 22) 0)
             (= (store (store (store (store (store (store (store s 2 0) 3 0) 5 0) 8 0) 9 0) 12 0) 22 0) ((as const (MultiSet Int)) 0))
             (<= (+ (* 2 (select s 2)) (* 3 (select s 3)) (* 5 (select s 5)) (* 8 (select s 8)) (* 9 (select s 9)) (* 12 (select s 12)) (* 22 (select s 22))) 30)))

(define-fun union-subset ((a (MultiSet Int)) (b (MultiSet Int)) (c (MultiSet Int))) Bool
            (and
             (>= (select c 2) (+ (select a 2) (select b 2)))
             (>= (select c 3) (+ (select a 3) (select b 3)))
             (>= (select c 5) (+ (select a 5) (select b 5)))
             (>= (select c 8) (+ (select a 8) (select b 8)))
             (>= (select c 9) (+ (select a 9) (select b 9)))
             (>= (select c 12) (+ (select a 12) (select b 12)))
             (>= (select c 22) (+ (select a 22) (select b 22)))))

(define-fun count-squirrels ((s (MultiSet Int))) Int
            (+ (select s 2) (select s 3) (select s 5) (select s 8) (select s 9) (select s 12) (select s 22)))

(declare-const round1 (MultiSet Int))
(declare-const round2 (MultiSet Int))

(assert (round-cond round1))
(assert (round-cond round2))
(assert (union-subset round1 round2 squirrels))

(maximize (+ (count-squirrels round1) (count-squirrels round2)))
(check-sat)
(get-model)