A tiny example for launching the Z3 process and interact with S-expression in SMTLIB syntax

solver.rkt

#lang racket/base

(require racket/match)

(provide current-solver-path
         call-with-solver
         solve)

(define current-solver-path (make-parameter (find-executable-path "z3")))

(define (call-with-solver action)
  (define-values (proc solverout solverin no-err-pipe)
    (subprocess #f #f 'stdout (current-solver-path) "-in"))

  (define (terminate-solver!)
    (when solverout (close-input-port solverout))
    (when solverin (close-output-port solverin))
    (subprocess-kill proc #t))

  (define (do-send! s-expr)
    (displayln s-expr solverin)
    (flush-output solverin))

  (define (do-recv!)
    (read solverout))

  (define results
    (with-handlers ([exn:fail? (λ (e)
                                 (terminate-solver!)
                                 (raise e))])
      (call-with-values
       (λ () (action do-send! do-recv!))
       (λ results results))))

  (terminate-solver!)
  (apply values results))

(define (solve prog)
  (call-with-solver
   (λ (do-send! do-recv!)

     (for ([s-expr (in-list prog)])
       (do-send! s-expr))

     (do-send! '(check-sat))

     (define is-sat (do-recv!))

     (cond
       [(equal? is-sat 'sat)
        (do-send! '(get-model))
        (define model (do-recv!))
        (match model
          [`(model
             (define-fun ,vars () ,typs ,vals)
             ...)
           (for/hash ([var (in-list vars)]
                      [val (in-list vals)])
             (values var val))]
          [else
           (error 'solve "cannot parse model ~a\n  input: ~a" model prog)])]
       [(equal? is-sat 'unsat)
        #f]
       [else
        (error 'solve "unknown result ~a\n  input: ~a" is-sat prog)]))))

(module+ test
  (require rackunit)

  (check-equal?
   (call-with-solver
    (λ (do-send! do-recv!)
      (do-send! '(check-sat))
      (do-recv!)))
   'sat)

  (check-equal?
   (solve
    '((declare-const x Int)
      (assert (= (* x 2) (+ x 10)))))
   '#hash((x . 10))))