This is a Julia interface to Z3 - a high performance theorem prover developed at Microsoft Research. Z3 can solve satisfiability modulo theory (SMT) problems.
Prerequisites: Have Z3 installed with shared libraries in your path.
using Z3 A = Var(Integer) # Create an integer-valued variable add!(A - 5 == 10) # Add a constraint check() # Is this problem satisfiable? model(Int, A) # Return a value for A in type Int = i.e. 15
Z3.jl is a relatively lightweight wrapper. By this I mean there's mostly direct access to the C-API, and Z3.jl doesn't prevent Z3 from terminating your program if you use it incorrectly. There are some conveniences however. In particular:
Building expressions (and pretty much everything else) in Z3 all take place within a
Z3.jl provides a Context class which allows you to create a new Context
ctx = Context() ctx = Context(qf_bv) # context under quantifier free bitvector logic
All api functions which need a context (which again is most of them), take a
ctx keyword parameter, e.g.:
ctx = Context() A = Var(Integer; ctx=ctx) B = Var(Integer; ctx=ctx) C = (-)(A, B; ctx=ctx)
This can get quite cumbersome, and so for the common case where you just want to write down an expression, Z3.jl provides a default, globally defined context.
You can access it with
Much like a global context, many operations (particularly those involved in adding and removing constraints) involve a
solver. In Z3.jl solvers are created using the
s = Solver() # Equivalently s = Solver(ctx=global_context()) A = Var(Real) B = Var(Real) add!(A == B; solver = s) check(;solver = s)
Warning: Ensure you don't mix and match variables and assertions with different contexts and solvers or Z3 will probably crash. This is particularly easy to do with arithmetic operations and the global context. One way to ensure you are not usung the global context when you don't mean to is to call disable_global_context!() which will throw an error if you attempt to use it.
For every c type we have a corresponding julia type.
All of these types subtype
For instance in
wrap.jl we have the definition:
@wrap function Z3_mk_eq(ctx::Z3_context,l::Z3_ast,r::Z3_ast) ccall((:Z3_mk_eq,"libz3"),Z3_ast,(Z3_context,Z3_ast,Z3_ast),ctx,l,r) end
Z3_ast is just a typealias alias
This is true for all types that begin with
The corresponding julia type is
@wrap performs some creative metaprogramming to create a new function
Z3_ has been dropped) which will accept the julia types, and treats
context arguments instead as keyword parameters, e.g:
# Return the expression l == r function mk_eq(l::Ast, r::Ast; ctx::Context = global_context()) ... return x::Ast end
Which can be used more conveniently than dealing with the c pointers.
A = Var(Integer) B = Var(Integer) mk_eq(A, B)
3 months ago