Skip to content
This repository has been archived by the owner. It is now read-only.

izgzhen/z3-encoding

master
Switch branches/tags
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

z3-encoding

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

Build Status

Assertion language embedded in Haskell, based on Z3 solver.

Features

  • Primitive types: boolean, integer, double precision float number
  • Complex types: set, map, ADT
  • Logic primitives and connectives: true, false, conjunction, disjunction, negation, implication
  • Logic qualifiers: universal, existential
  • Assertions for primitive types: equality, less than
  • Assertions for complex types: membership testing
  • Extensible function
  • Extensible assertion
  • 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.

About

High-level assertion encoding to Z3 solver

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published