Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Make WITH-SMT work (on SBCL) #4

Merged
merged 2 commits into from
Jun 1, 2021
Merged

Make WITH-SMT work (on SBCL) #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3a2d7c0
Make WITH-SMT work (on SBCL)
lukego May 19, 2021
9ace677
Make WITH-SMT use READ-FROM-SMT
lukego May 19, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
10 changes: 7 additions & 3 deletions cl-smt-lib.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
(defpackage :cl-smt-lib/cl-smt-lib
(:nicknames :cl-smt-lib)
(:use :common-lisp :named-readtables :cl-smt-lib/process-two-way-stream)
(:import-from :uiop/launch-program :terminate-process)
(:import-from :uiop/launch-program :terminate-process :wait-process)
(:export
:make-smt
:smt-error
Expand Down Expand Up @@ -76,13 +76,17 @@ case-sensitive smt libv2 format."

(defmacro with-smt ((smt (program &rest args) &optional preserve-case-p)
&body body)
(let ((form (gensym)))
(declare (ignore preserve-case-p))
(let ((form (gensym))
(status (gensym)))
`(with-open-stream (,smt (make-smt ,program ,@args))
(unwind-protect
(progn
,@body
(close (output ,smt))
(loop :for ,form = (read-from-smt ,smt ,preserve-case-p nil :eof)
(let ((,status (wait-process (process ,smt))))
(unless (zerop ,status) (error "SMT solver failed with exit status ~S" ,status)))
(loop :for ,form = (read-from-smt ,smt t nil :eof)
:while (not (equal :eof ,form))
:collect ,form))
;; Ensure the process is terminated.
Expand Down
4 changes: 2 additions & 2 deletions fundamental-two-way-stream.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
(defpackage :cl-smt-lib/fundamental-two-way-stream
(:use :cl :trivial-gray-streams)
(:export :fundamental-two-way-stream))
(:export :fundamental-two-way-stream :input :output))
(in-package :cl-smt-lib/fundamental-two-way-stream)

(defclass fundamental-two-way-stream
Expand All @@ -12,7 +12,7 @@

;;; Trivial-gray-stream generic function customization.
(defmethod stream-read-char ((stream fundamental-two-way-stream))
(read-char (input stream)))
(read-char (input stream) nil :eof))

(defmethod stream-read-char-no-hang ((stream fundamental-two-way-stream))
(read-char-no-hang (input stream)))
Expand Down
5 changes: 4 additions & 1 deletion process-two-way-stream.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,10 @@
(defpackage :cl-smt-lib/process-two-way-stream
(:use :cl :cl-smt-lib/fundamental-two-way-stream :uiop/launch-program)
(:export :process-two-way-stream
:make-process-two-way-stream))
:make-process-two-way-stream
:input
:output
:process))
(in-package :cl-smt-lib/process-two-way-stream)

;;; A process wrapped in a two-way stream.
Expand Down