Merge pull request #3 from jamesbornholt/persistent-smtlib

Make smtlib servers persistent.

Author: emina

rosette/solver/smt/cmd.rkt

@@ -1,11 +1,11 @@
 #lang racket
 
 (require racket/syntax 
-         (only-in "smtlib2.rkt" cmd assert check-sat get-model read-solution true false)
+         (only-in "smtlib2.rkt" cmd assert check-sat get-model reset read-solution true false)
          "../../base/term.rkt" "../../base/bool.rkt" "../../base/num.rkt" "../solution.rkt"  "../../base/enum.rkt"
          "env.rkt" "enc.rkt")
 
-(provide encode decode)
+(provide encode decode clear-solver)
 
 ; Given an encoding environment, a list of asserts, and
 ; a solver output port, the encode procedure prints an SMT 
@@ -39,6 +39,13 @@
                         (default-binding const)))))]
     [#f (unsat)]))
 
+; Given a solver input port, the reset procedure prints
+; commands necessary to clear the solver's state to the
+; given port.
+(define (clear-solver port)
+  (cmd [port]
+    (reset)))
+
 (define (default-binding const)
   (match (type-of const)
     [(== @boolean?) #f]

rosette/solver/smt/smt.rkt

@@ -27,11 +27,13 @@
     (define/public assert 
       (lambda in (set! asserts (append asserts (filter-asserts in)))))
 
-    (define/public (clear) 
-      (send server shutdown)
+    (define/public (clear)
+      (send server write clear-solver)
       (set!-values (asserts env) (values '() (make-env))))
 
-    (define/public (shutdown)  (clear))
+    (define/public (shutdown)
+      (clear)
+      (send server shutdown))
 
     (define/public (debug)     (error 'debug "not supported by ~a" this))      
     (define/public (solve-all) (error 'solve-all "not supported by ~a" this))

rosette/solver/smt/smtlib2.rkt

@@ -56,6 +56,8 @@
 (define (get-model)   (print-cmd "(get-model)\n"))
 (define (get-info kw) (print-cmd "(get-info ~a)\n" kw))
 
+(define (reset)       (print-cmd "(reset)\n"))
+
 (define (push n)      (print-cmd "(push ~a)\n" n))
 (define (pop n)       (print-cmd "(pop ~a)\n" n))
 (define (assert expr) (print-cmd "(assert ~a)" expr))