magpie.rkt

#lang rosette/safe
(require rosette/lib/angelic
         (only-in racket/base syntax->datum))

(define-syntax-rule (define-distinct v x ...)
 (begin
  (define x v) ...
  (assert (distinct? x ...))))
(define-syntax-rule (list-choices x ... sol)
  (list (list (evaluate x sol) (syntax->datum #'x)) ...))

(define houses '(1 2 3 4 5))
(define (left-of?  h1 h2) (= (+ h1 1) h2))
(define (right-of? h1 h2) (= h1 (+ h2 1)))
(define (adjacent? h1 h2) (or (right-of? h1 h2) (left-of? h1 h2)))

(define-distinct (choose* 1 2 3 4 5) poet editor critic writer journalist)
(define-distinct (choose* 1 2 3 4 5) red blue green white yellow)
(define-distinct (choose* 1 2 3 4 5) bicycle motorcycle pedestrian car)
(define-distinct (choose* 1 2 3 4 5) bullfinch tit canary parrot magpie)
(define-distinct (choose* 1 2 3 4 5) milk cacao tea coffee tomato-juice)

(define solution
 (solve
  (begin
   (assert (eq? poet bicycle))
   (assert (eq? editor red))
   (assert (eq? critic 1))
   (assert (adjacent? critic blue))
   (assert (eq? motorcycle 3))
   (assert (right-of? green white))
   (assert (eq? green pedestrian))
   (assert (eq? milk bullfinch))
   (assert (adjacent? cacao tit))
   (assert (eq? yellow tea))
   (assert (adjacent? canary tea))
   (assert (eq? writer coffee))
   (assert (eq? car tomato-juice))
   (assert (eq? journalist parrot)))))
(define magpie-in (evaluate magpie solution))
(assoc magpie-in (list-choices poet editor critic writer journalist solution)) ; '(5 writer)
(second (assoc magpie-in (list-choices red blue green white yellow solution))) ; 'green