Nim Z3

"Z3 is a cat with a funny hat" -TheLemonMan

NimZ3 is an early stage Nim binding for the Z3 theorem prover

Documentation

• Module documentation
• Examples

Status

This is still a work in progress and a lot of Z3 is still missing, but the most important basics are available:

• bool, bit vector, int and float types
• solving
• optimization
• simplification

The API uses template magic to hide Z3 contexts and allows normal Nim syntax for defining Z3 model assertions.

Example

z3:
  let x = Int("x")
  let y = Int("y")
  let z = Int("z")
  let s = Solver()
  s.assert 3 * x + 2 * y - z == 1
  s.assert 2 * x - 2 * y + 4 * z == -2
  s.assert x * -1 + y / 2 - z == 0
  s.check_model:
    echo model

Answer:

z -> (- 2)
y -> (- 2)
x -> 1

More examples are available in the tests directory, run with nimble test.

More Z3 info

Some helpful documents and tutorials about Z3:

• Z3 - guide
• Programming Z3

Open questions

Things I'm not sure how to solve yet. Any input appreciated:

• Should there be distinct types for signed and unsigned bit vectors? This would make it easier to implement operators for things like Z3_mk_bvXXX_no_overflow()

• What is a good way to create Z3 consts? The current method of doing let x = Int "x" is redundant and prone to mistakes. Is it better to create some kind of declaration template instead?