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.