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
The API uses template magic to hide Z3 contexts and allows normal Nim syntax for defining Z3 model assertions.
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
z -> (- 2) y -> (- 2) x -> 1
More examples in the tests directory, run with
Some helpful documents and tutorials about Z3: