Commits
Author  Commit  Message  Labels  Comments  Approvals  Date 

Add support for solvers to Z3.Monad




Move Z3Logic datatype to Z3.Base (plus tweaks)




added support for printing ASTs and Exprs




Remove unused LANGUAGE pragmas




Add bitvectors to Z3.Base




Remove trailing spaces




unBool: conversion from Z3_bool to Bool




4f0098e
M

Trivial merge with Eddy's changeset





changes to support Z3 logics




Minor cleanup




Add Z3.Monad: A simple monadic wrapper for Z3.Base




Add Z3.Opts: a convenient wrapper to Z3 configuration




Update copyright notice




Add FlexibleInstances to globally declared extensions




Do not link against OpenMP on OS X
In OS X libz3 is statically linked against libgomp.
What is more, apparently default OS X installations do not
provide a shared library for OpenMP: thus the package loading
fails when libgimp.dylib is not found.




Generalize recursive `QExpr' instance




Remove trailing spaces




Remove trailing spaces




Set version to 0.3.0




2e4c35d
M

Automated merge with ssh://bitbucket.org/iago/z3haskell




Generalized quantifiers.
forall :: QExpr t => t > Expr Bool
Example types of class QExpr t:
f :: Expr Integer > Expr Bool
f :: Expr Bool > Expr Bool
...
f :: Expr Integer > Expr Rational > Expr Bool
f :: Expr Integer > Expr Rational > QBody
QBody is the type of a quantified expression body. It is an 'Expr Bool'
annotated with a list [Pattern]:
t :: Expr Bool
t `instanceWhen` [Pat p1, Pat…




mkQuant added in Z3.Lang.Monad.




Bugfixes in Z3.Base




26c9dfe
M

Merge Z3.Base




Clean up




Changed types of mkForall and mkExists in Z3.Base




castPtr removed.




Existential quantifier.




Result datatype simplified in Z3.Base.




delModel added.


