Skip to content
Nim binding for the Z3 theorem prover
HTML Nim
Branch: master
Clone or download
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
src Deprecated Z3_get_error_msg_ex Dec 14, 2019
tests Dropped s.check_model from most of the tests Feb 27, 2019
README.md Update README Feb 17, 2019
z3.nimble bumped version Feb 12, 2019

README.md

Nim Z3

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

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

Documentation

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:

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?

You can’t perform that action at this time.