gist/racket/icebreaker/icebreaker.rkt

#lang curly-fn rosette

(require syntax/parse/define
         (for-syntax racket/syntax))

;; house is represented by actual number
;; people, places, pets represented by symbolic variable
(define-for-syntax *data*
  '((name martin ramsey sandra turner walter)
    (place london kansas france taipei mumbai)
    (pet robins tigers whales ferret poodle)))

;; create a solver and define all the symbolic variables
(define-simple-macro (define-symbols/solver solver:id)
  ;; generate list of ids, bound to calling lexical context, with a syntax prop determining the
  ;; category
  #:with (ids ...) (for*/list ([row (in-list *data*)] [val (in-list (rest row))])
                     (syntax-property (format-id #'solver "~a" val) 'icebreaker:cat (first row)))
  ;; create the symbolic define expressions
  #:with (defs ...) (for/list ([id (in-list (syntax-e #'(ids ...)))])
                      #`(define-symbolic #,id integer?))
  ;; create initial constraints
  #:with (stmts ...) (let ([groups (group-by #{syntax-property % 'icebreaker:cat }
                                             (syntax-e #'(ids ...)))])
                       (append (for*/list ([grp (in-list groups)] [id (in-list grp)])
                                 ;; all in [1, 5]
                                 #`(void (solver (<= 1 #,id 5))))
                               (for/list ([grp (in-list groups)])
                                 ;; no two in the same category are equal
                                 #`(void (solver (mutually-exclusive #,@grp))))))
  (begin
    ;; incremental solver
    (define solver (solve+))
    defs ...
    stmts ...))

(define-symbols/solver inc)

;; helper for defining the statements of one person (2 true, 1 lie)
(define-simple-macro (define-statements solver:expr sfirst:expr ssecond:expr sthird:expr)
  (void
    (solver (or (and sfirst ssecond (not sthird))
                (and sfirst (not ssecond) sthird)
                (and (not sfirst) ssecond sthird)))))

;; helper for defining a mutually exclusive set of symbolic and concrete values
(define-simple-macro (mutually-exclusive options:expr ...)
  #:with (stxs ...) (for/list ([combo (in-combinations (syntax-e #'(options ...)) 2)])
                      #`(not (= #,(first combo) #,(second combo))))
  (and stxs ...))

;; helper for asserting that 2 houses are at a certain distance apart
(define-simple-macro (at-distance v1:expr v2:expr dist:expr)
  (= dist (abs (- v1 v2))))

;; the rules
;; martin
(define-statements inc
  (mutually-exclusive 1 ramsey ferret poodle kansas)
  (and (at-distance turner whales 4) (not (= turner whales)))
  (and (= walter france) (not (= walter ferret))))

;; ramsey
(define-statements inc
  (and (at-distance martin london 4) (not (= martin london)))
  (and (= sandra london) (not (= sandra ferret)))
  (= walter (sub1 ramsey)))

;; sandra
(define-statements inc
  (= sandra robins)
  (at-distance whales france 2)
  (= walter taipei))

;; turner
(define-statements inc
  (not (= turner kansas))
  (= turner tigers)
  (and (= ramsey robins) (at-distance ramsey turner 3)))

;; walter
(define-statements inc
  (mutually-exclusive walter poodle 2)
  (mutually-exclusive walter sandra robins mumbai taipei)
  (and (= turner kansas) (not (= turner 1))))

(define solution (inc #t))
(displayln solution)