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.