Description:

z3

dz3 #
High level bindings to the Z3 SMT solver.
What is Z3? #
Z3 is a state-of-the art theorem prover developed at Microsoft Research. It can be used to solve a wide variety of
constraint problems from basic satisfiability to more complex problems involving quantifiers, non-linear arithmetic,
bit-vectors, and symbolic execution.
Features #
This package provides almost everything exposed by the Z3 C API, but quite a bit has been changed to make it more
idiomatic to Dart, including:

Exception handling
Memory management
Automatic context translation
Useful getters for common types
Class hierarchy for AST nodes
Operator overloading

Usage #

Install Z3 via your package manager.

Windows users can install pre-built binaries from chocolatey:
choco install z3
copied to clipboard

Mac users can install z3 via homebrew:
brew install z3
copied to clipboard

Linux users can install z3 via most package managers:
sudo apt install z3
copied to clipboard



(Optional) Build Z3 from source for debugging

Clone dz3 and its submodules:
git clone --recursive https://github.com/pingbird/dz3
copied to clipboard

Build it using CMake and Ninja:
cd dz3/z3
mkdir cmake-build-debug
cd cmake-build-debug
cmake -G Ninja -DCMAKE_BUILD_TYPE=Debug ../
ninja libz3
copied to clipboard
For more help on building from source see https://github.com/Z3Prover/z3/blob/master/README-CMake.md


Add it to your pubspec.yaml file:
dependencies:
dz3: ^0.1.0
copied to clipboard

Enjoy!

See the dz3_example/bin directory for complete examples.

License

For personal and professional use. You cannot resell or redistribute these repositories in their original state.

Share

• Share on Facebook
• Share on Twitter