z3-encoding

Assertion language embedded in Haskell, based on Z3 solver.

Features

• [x] Primitive types: boolean, integer, double precision float number
• [x] Complex types: set, map, ADT
• [x] Logic primitives and connectives: true, false, conjunction, disjunction, negation, implication
• [x] Logic qualifiers: universal, existential
• [x] Assertions for primitive types: equality, less than
• [x] Assertions for complex types: membership testing
• [ ] Extensible function
• [ ] Extensible assertion
• [x] Static type safety

Usage

1. Install z3, noting its include path and lib path as specified by prefix=
2. git clone https://github.com/izgzhen/z3-encoding
3. Adapt z3-encoding/stack.yaml to your specific condition, esp.:
   • extra-include-dirs
   • extra-lib-dirs

Upstream

Currently, it supports z3 v4.4.1, through a low-level Haskell library z3-haskell.

Also, current version of this package supports the GHC v8.0.1.