Nim Z3

First try for a Nim binding for the Z3 theorem prover

Most of Z3 is still missing, but the following works:

• integer and boolean 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 in the tests directory, run with nimble test.

Some helpful documents and tutorials about Z3:

• Z3 - guide
• Programming Z3