diff --git a/racket/icebreaker/README.md b/racket/icebreaker/README.md new file mode 100644 index 0000000..8e35199 --- /dev/null +++ b/racket/icebreaker/README.md @@ -0,0 +1,2 @@ +see: + diff --git a/racket/icebreaker/icebreaker.rkt b/racket/icebreaker/icebreaker.rkt new file mode 100644 index 0000000..75dfa8d --- /dev/null +++ b/racket/icebreaker/icebreaker.rkt @@ -0,0 +1,88 @@ +#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)