;; 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)))))