# Guile Z3 Bindings

This project aims to give GNU 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:

```
autoreconf -fiv
./configure Z3_LIBDIR=/usr/lib
make
```

To install run:

`make install`

To run the tests, run:

`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:

```
(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:

```
(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:

```
,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.