MA122

ma122.rkt

#lang rosette
(require rosette/lib/angelic)

(define profession (list 'baker 'carpenter 'driver 'plumber))

(define baker (apply choose* profession))
(define carpenter (apply choose* profession))
(define driver (apply choose* profession))
(define plumber (apply choose* profession))

(define (f-constraints)
  (list (distinct? baker driver carpenter plumber)
        (not (equal? baker 'baker))
        (not (equal? driver 'driver))
        (not (equal? carpenter 'carpenter))
        (not (equal? plumber 'plumber))))

(define (v-constraints)
  (list (equal? baker 'plumber)
        (equal? driver 'baker)
        (! (equal? carpenter 'plumber))
        (! (equal? plumber 'carpenter))))

(define (assigned profession sol)
  (first (filter (lambda (p) (equal? (evaluate p sol) profession))
          (list baker carpenter driver plumber))))

(define (m-solve constraint)
  (define s-solve (solve+))
  (let ([sol (s-solve constraint)])
    (if (sat? sol)
        (letrec ([a-driver (assigned 'driver sol)]
                 [n-sol (s-solve (not (equal? 'driver a-driver)))])
            (cons sol (if (sat? n-sol) (list n-sol) (list))))
        (list))))

(define sol (first (first (filter (lambda (s) (= (length s) 1))
                            (for/list ([t (range 5)])
                              (m-solve (and (apply && (f-constraints))
                                            (= t (length (filter identity (v-constraints)))))))))))

(evaluate (list baker carpenter driver plumber) sol)