(set-option :produce-models true)
(set-logic ALL)

(declare-datatypes ((Tom 0)) (((Batman) (Jake) (Dibii))))
(declare-datatypes ((Queen 0)) (((Ruby) (Spot) (Starbuck))))
(declare-datatypes ((Activities 0)) (((Lazer) (Sleep) (Ball))))

(declare-datatypes ((QueenPair 0)) 
   (((queenpair (first Queen) (second Queen)))))

(declare-fun QueenPartner (Queen) Tom)
(declare-fun QueenActivity (Queen) Activities)
(declare-fun QueenKittens (Queen) Int)
(declare-fun TomPartner (Tom) Queen)

; Integer constraint
(assert (forall ((q Queen)) (and (>= (QueenKittens q) 1) (<= (QueenKittens q) 3))))

; "Only one dot in each row/col" consistency check.
(assert (forall ((qp QueenPair)) (ite (= (first qp) (second qp))
                                  true
                                  (and
                                  (not (= (QueenPartner (first qp)) (QueenPartner (second qp))))
                                  (not (= (QueenKittens (first qp)) (QueenKittens (second qp))))
                                  (not (= (QueenActivity (first qp)) (QueenActivity (second qp))))
                                  ))))
; All other constraints for Tom are implied if the partner of the partner is the same.
(assert (forall ((t Tom)) (= (QueenPartner (TomPartner t)) t)))

; 1. Batman chose the female who liked to chase a ball, but she was not Starbuck.
(assert (= (QueenActivity (TomPartner Batman)) Ball))
(assert (not (= (TomPartner Batman) Starbuck)))

; 2. Dibii's companion liked to chase the laser light.
(assert (= (QueenActivity (TomPartner Dibii)) Lazer))

; 3. Ruby loved to cuddle up to her male for a long afternoon nap in the sun.
(assert (= (QueenActivity Ruby) Sleep))

; 4. Starbuck had two more kittens than Batman's companion.
(assert (= (QueenKittens Starbuck)
           (+ (QueenKittens (TomPartner Batman)) 2)))

(check-sat)
(get-model)

(echo "
Spot:")
(get-value ((QueenPartner Spot)
            (QueenKittens Spot)
            (QueenActivity Spot)))

(echo "
Ruby:")
(get-value ((QueenPartner Ruby)
            (QueenKittens Ruby)
            (QueenActivity Ruby)))

(echo "
Starbuck:")
(get-value ((QueenPartner Starbuck)
            (QueenKittens Starbuck)
            (QueenActivity Starbuck)))