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.