Popularity
5.0
Stable
Activity
0.0
Stable
5
2
3

Monthly Downloads: 5
Programming language: Haskell
License: MIT License
Tags: Language    

z3-encoding alternatives and similar packages

Based on the "Language" category.
Alternatively, view z3-encoding alternatives based on common mentions on social networks and blogs.

Do you think we are missing an alternative of z3-encoding or a related project?

Add another 'Language' Package

README

z3-encoding

Join the chat at https://gitter.im/izgzhen/z3-encoding

Build Status

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.