(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-fun QueenPartner (Queen) Tom)
(declare-fun QueenActivity (Queen) Activities)
(declare-fun QueenKittens (Queen) Int)
(declare-fun TomPartner (Tom) Queen)

; Integer constraint
(assert (and 
    (>= (QueenKittens Ruby) 1) (<= (QueenKittens Ruby) 3)
    (>= (QueenKittens Spot) 1) (<= (QueenKittens Spot) 3)
    (>= (QueenKittens Starbuck) 1) (<= (QueenKittens Starbuck) 3)))

; "Only one dot in each row/col" consistency check.
(assert (and
    (not (= (QueenPartner Ruby) (QueenPartner Spot)))
    (not (= (QueenPartner Ruby) (QueenPartner Starbuck)))
    (not (= (QueenPartner Spot) (QueenPartner Starbuck)))
    (not (= (QueenKittens Ruby) (QueenKittens Spot)))
    (not (= (QueenKittens Ruby) (QueenKittens Starbuck)))
    (not (= (QueenKittens Spot) (QueenKittens Starbuck)))
    (not (= (QueenActivity Ruby) (QueenActivity Spot)))
    (not (= (QueenActivity Ruby) (QueenActivity Starbuck)))
    (not (= (QueenActivity Spot) (QueenActivity Starbuck)))))

; All other constraints for Tom are implied if the partner of the partner is the same.
(assert (and
    (= (QueenPartner (TomPartner Batman)) Batman)
    (= (QueenPartner (TomPartner Jake)) Jake)
    (= (QueenPartner (TomPartner Dibii)) Dibii)))

; 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)))