new-york-city-guys.rkt

#lang rosette

;; Posted to Coq-Club by Fred Smith, 2016-09-24
;; https://sympa.inria.fr/sympa/arc/coq-club/2016-09/msg00185.html

;; The five-story Manning Building, located in the Wall Streat area of
;; Manhattan, houses the home offices of Matt and four other prominent
;; businessmen.
;;
;; Each man's business is located on a different floor of the building, and each
;; also has a branch office located in a foreign city.  No two have a branch in
;; the same city.  The man who visits his branch in Cairo usually combines his
;; trip with a short vacation.  Each of the five men resides in a different
;; borough of New York City.
;; 
;; From this information and the clues below, can you determine each man's
;; home borough, branch office location, and floor?

(define-symbolic matt-idx
                 rick-idx
                 roland-idx
                 shaun-idx
                 cliff-idx

                 bronx-idx
                 manhattan-idx
                 staten-idx
                 brooklyn-idx
                 queens-idx

                 cairo-idx
                 rome-idx
                 athens-idx
                 paris-idx
                 geneva-idx
  integer?)

(define S
  (solve (begin

    (assert (<= 0 matt-idx      4))
    (assert (<= 0 rick-idx      4))
    (assert (<= 0 roland-idx    4))
    (assert (<= 0 shaun-idx     4))
    (assert (<= 0 cliff-idx     4))

    (assert (<= 0 bronx-idx     4))
    (assert (<= 0 manhattan-idx 4))
    (assert (<= 0 staten-idx    4))
    (assert (<= 0 brooklyn-idx  4))
    (assert (<= 0 queens-idx    4))

    (assert (<= 0 cairo-idx     4))
    (assert (<= 0 rome-idx      4))
    (assert (<= 0 athens-idx    4))
    (assert (<= 0 paris-idx     4))
    (assert (<= 0 geneva-idx    4))

    (let ([all-idx (list matt-idx
                         rick-idx
                         roland-idx
                         shaun-idx
                         cliff-idx)])
      (for* ([(n0 i) (in-indexed all-idx)]
             [(n1 j) (in-indexed all-idx)]
             #:when (not (= i j)))
        (assert (not (= n0 n1)))))

    (let ([all-boro-idx (list bronx-idx
                              manhattan-idx
                              staten-idx
                              brooklyn-idx
                              queens-idx)])
      (for* ([(b0 i) (in-indexed all-boro-idx)]
             [(b1 j) (in-indexed all-boro-idx)]
             #:when (not (= i j)))
        (assert (not (= b0 b1)))))

    (let ([all-branch-idx (list cairo-idx
                                rome-idx
                                athens-idx
                                paris-idx
                                geneva-idx)])
      (for* ([(b0 i) (in-indexed all-branch-idx)]
             [(b1 j) (in-indexed all-branch-idx)]
             #:when (not (= i j)))
        (assert (not (= b0 b1)))))

    ;; 1. Rick's office is one floor below the office of the man who lives in
    ;; the Bronx, which is not on the fourth floor.
    (assert (= (+ rick-idx 1) bronx-idx))
    (assert (not (= 3 bronx-idx)))

    ;; 2. The office of the Staten Island resident is one floor below
    ;; Roland's, who doesn't live in Queens.
    (assert (= (+ staten-idx 1) roland-idx))
    (assert (not (= roland-idx queens-idx)))

    ;; 3. Shaun's office is one floor below the one who visits his branch in Rome.
    (assert (= (+ shaun-idx 1) rome-idx))

    ;; 4. Cliff's branch isn't located in Athens.
    (assert (not (= cliff-idx athens-idx)))

    ;; 5. The man who lives in Manhattan has no branch in Rome.
    (assert (not (= manhattan-idx rome-idx)))

    ;; 6. The Paris branch is not Shaun's.
    (assert (not (= paris-idx shaun-idx)))

    ;; 7. The office of the man who lives in Brooklyn is one floor below that
    ;; of the businessman who visits his branch in Geneva, which is not on
    ;; the fifth floor.
    (assert (= (+ brooklyn-idx 1) geneva-idx))
    (assert (not (= geneva-idx 4)))

    ;; 8. The office of the one who lives in the Bronx is on some floor above
    ;; Roland's.
    (assert (< roland-idx bronx-idx))

    ;; 9. Rick, who has no branch in Geneva, doesn't live in Queens.
    (assert (not (= rick-idx geneva-idx)))
    (assert (not (= rick-idx queens-idx)))

    ;; 10. Neither the Staten Island resident nor the Manhattan resident has
    ;; a branch in Athens.
    (assert (not (= staten-idx athens-idx)))
    (assert (not (= manhattan-idx athens-idx)))
)))

;; -----------------------------------------------------------------------------
;; --- spoilers
;; -----------------------------------------------------------------------------

S
#;
(model
 [matt-idx 4]
 [rick-idx 3]
 [roland-idx 1]
 [shaun-idx 0]
 [cliff-idx 2]
 [bronx-idx 4]
 [manhattan-idx 3]
 [staten-idx 0]
 [brooklyn-idx 1]
 [queens-idx 2]
 [cairo-idx 0]
 [rome-idx 1]
 [athens-idx 4]
 [paris-idx 3]
 [geneva-idx 2])