;; Guile-Z3
;; Copyright (C) 2020 Julien Lepiller <julien@lepiller.eu>

;; This library is free software; you can redistribute it and/or modify
;; it under the terms of the GNU Lesser General Public License as
;; published by the Free Software Foundation; either version 3 of the
;; License, or (at your option) any later version.
;;                                                                  
;; This library is distributed in the hope that it will be useful, but
;; WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
;; Lesser General Public License for more details.
;;                                                                  
;; You should have received a copy of the GNU Lesser General Public
;; License along with this program; if not, contact:
;;
;; Free Software Foundation           Voice:  +1-617-542-5942
;; 59 Temple Place - Suite 330        Fax:    +1-617-542-2652
;; Boston, MA  02111-1307,  USA       gnu@gnu.org

;;; Commentary:
;;
;; A Guile binding for the Z3 Theorem Prover.
;;
;;; Code:

(define-module (z3)
  #:use-module (system foreign)
  #:use-module (rnrs bytevectors)
  #:use-module (srfi srfi-9)
  #:use-module (system base language)
  #:use-module (system repl command)
  #:use-module (system repl common)
  #:use-module (system repl repl)
  #:export (z3-eval
            run-with-z3))

;;; Dynamic linking to foreign functions
(define libz3 (dynamic-link "@Z3_LIBDIR@/libz3"))

(define z3-mk-config
  (pointer->procedure '* (dynamic-func "Z3_mk_config" libz3) '()))
(define z3-del-config
  (pointer->procedure void (dynamic-func "Z3_del_config" libz3) (list '*)))

(define z3-mk-context
  (pointer->procedure '* (dynamic-func "Z3_mk_context" libz3) (list '*)))
(define z3-del-context
  (pointer->procedure void (dynamic-func "Z3_del_context" libz3) (list '*)))

(define z3-eval-smtlib2-string
  (pointer->procedure '* (dynamic-func "Z3_eval_smtlib2_string" libz3) (list '* '*)))

(define z3-set-error-handler
  (pointer->procedure void (dynamic-func "Z3_set_error_handler" libz3) (list '* '*)))
(define get-error
  (dynamic-func "Z3_get_error_msg" libz3))

;;; Utility function

(define (sexp->string sexp)
  "Converts an s-expression to a string, to be passed to eval-smtlib2"
  (with-output-to-string
    (lambda _
      (write sexp))))

;;; Interface

(define (z3-eval context query)
  "Runs a query as an SMT-LIB2 s-expression in the Z3 context.  See the Z3
manual for more information on the expected format."
  (let* ((query (sexp->string query))
         (ans (z3-eval-smtlib2-string
                context
                (string->pointer
                  (substring query 1 (- (string-length query) 1))))))
    (call-with-input-string (pointer->string ans) read)))

(define (run-with-z3 thunk)
  "Runs a one-argument procedure in a new Z3 context.  The only argument to that
procedure is the newly-created Z3 context."
  (let* ((conf (z3-mk-config))
         (ctx (z3-mk-context conf))
         (_ (z3-set-error-handler ctx get-error)))
    (dynamic-wind
      (lambda () #t)
      (lambda () (thunk ctx))
      (lambda ()
        (z3-del-context ctx)
        (z3-del-config conf)))))

(define-meta-command ((z3 exp) repl)
  "Run exp in custom repl."
  (run-with-z3
    (lambda (context)
      (let* ((scheme (lookup-language 'scheme))
             (new (make-repl
                   (make-language #:name "z3"
                                  #:title "z3"
                                  #:reader (language-reader scheme)
                                  #:evaluator (lambda (exp env)
                                                (z3-eval context (list exp)))
                                  #:printer (language-printer scheme)
                                  #:make-default-environment
                                  (language-make-default-environment scheme)))))
        (repl-option-set! new 'interp #t)
        (run-repl new)))))