89 lines
3.2 KiB
Racket
89 lines
3.2 KiB
Racket
#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)
|