Guile Z3 Bindings ================= This project aims to give [GNU Guile](https://gnu.org/software/guile) users a very simple library to use Z3, the theorem prover. Z3 itself is able to read files formated in SMT-LIB2, which is a s-expression format. Instead of writting files and calling Z3, this library offers you all the benefits of using guile to produce your expressions in software. How to Build Guile Z3 --------------------- Guile Z3 needs Z3 and guile of course, as well as the usual suspects: * autotools * make * pkg-config From this repo, run the following: ```bash autoreconf -fiv ./configure Z3_LIBDIR=/usr/lib make ``` To install run: ```bash make install ``` To run the tests, run: ```bash make check ``` How to Use Guile Z3 ------------------- As a very simple example, we can try to find solutions for the following equation system: ``` / | x + 2y = 20 | x - y = 2 \ ``` This can be done with guile-z3: ```scheme (use-modules (z3)) (run-with-z3 (lambda (context) (z3-eval context '((set-option :produce-models true) (set-logic QF_LIA) (declare-fun x () Int) (declare-fun y () Int) (assert (= (+ x (* 2 y)) 20)) (assert (= (- x y) 2)) (check-sat))))) ``` And Z3 tells us there is a solution! But what is it? We can get the solution with: ```scheme (use-modules (z3)) (run-with-z3 (lambda (context) ;; First, we check that we can find a solution. Z3 will build an example ;; after check-sat. (let ((sat? (equal? (z3-eval context '((set-option :produce-models true) (set-logic QF_LIA) (declare-fun x () Int) (declare-fun y () Int) (assert (= (+ x (* 2 y)) 20)) (assert (= (- x y) 2)) (check-sat))) 'sat))) ;; Then, outside of Z3, we can do something with the result. Here, we ;; check that a solution can be found. (if sat? ;; If we find one, we ask one to Z3 and we get a nice association list ;; as a result. (let ((solution (z3-eval context '((get-value (x y)))))) (format #t "A solution is x=~a and y=~a~%" (assoc-ref solution 'x) (assoc-ref solution 'y))) ;; Otherwise, we tell the user the equation is not satisfiable. (format #t "unsat~%"))))) ``` Of course, we pass Z3 actual s-expressions, so we can use all the quote-unquote magick we are used to! Interactive Z3 Session ---------------------- To start an interactive Z3 session through the Guile REPL, use this command: ```scheme ,use (z3) ; use guile-z3 ,z3 ; start a Z3 repl! ``` Quick Reference --------------- ### Procedure (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. ### Procedure (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.