;;;; amb-sat-solve.scm
;;;; From "Continuations by example" ..." by Matt Might

(require-extension amb)

(define (implies a b) (or (not a) b))

;; The is not the most efficient implementation,
;; because a continuation is captured for each
;; occurrence of the same variable, instead of
;; one for each variable.

(define-syntax sat-solve
  (syntax-rules (and or implies not)
    ((_ ?formula ?body)
     (sat-solve ?formula ?body ?formula) )

    ((_ (not ?phi) ?body ?assertion)
     (sat-solve ?phi ?body ?assertion) )

    ((_ (and ?phi) ?body ?assertion)
     (sat-solve ?phi ?body ?assertion) )

    ((_ (and ?phi1 ?phi2 ...) ?body ?assertion)
     (sat-solve ?phi1 (sat-solve (and ?phi2 ...) ?body ?assertion)) )

    ((_ (or ?phi) ?body ?assertion)
     (sat-solve ?phi ?body ?assertion) )

    ((_ (or ?phi1 ?phi2 ...) ?body ?assertion)
     (sat-solve ?phi1 (sat-solve (or ?phi2 ...) ?body ?assertion)) )

    ((_ (implies ?phi1 ?phi2) ?body ?assertion)
     (sat-solve ?phi1 (sat-solve ?phi2 ?body ?assertion)) )

    ((_ #t ?body ?assertion)
     ?body )

    ((_ #f ?body ?assertion)
     (amb-failure-continuation) )

    ((_ v ?body ?assertion)
     (let ((v (amb #t #f)))
       (amb-assert ?assertion)
       ?body ) ) ) )


; The following prints (#f #f #t)
(sat-solve (and (implies a (not b))
                 (not a)
                 c)
            (print "a = " a ", b = " b ", c = " c))