Commits

Author Commit Message Labels Comments Date
Iago Abal
Add support for solvers to Z3.Monad
Iago Abal
Move Z3Logic datatype to Z3.Base (plus tweaks)
eddy_westbrook
added support for printing ASTs and Exprs
Iago Abal
Remove unused LANGUAGE pragmas
Iago Abal
Add bit-vectors to Z3.Base
Iago Abal
Remove trailing spaces
Iago Abal
unBool: conversion from Z3_bool to Bool
Iago Abal
Trivial merge with Eddy's changeset
em...@rice.edu
changes to support Z3 logics
Iago Abal
Minor clean-up
Iago Abal
Add Z3.Monad: A simple monadic wrapper for Z3.Base
Iago Abal
Add Z3.Opts: a convenient wrapper to Z3 configuration
Iago Abal
Update copyright notice
Iago Abal
Add FlexibleInstances to globally declared extensions
Iago Abal
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.
Iago Abal
Generalize recursive `QExpr' instance
Iago Abal
Remove trailing spaces
Iago Abal
Remove trailing spaces
Iago Abal
Set version to 0.3.0
David Castro
Automated merge with ssh://bitbucket.org/iago/z3-haskell
David Castro
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…
David Castro
mkQuant added in Z3.Lang.Monad.
David Castro
Bugfixes in Z3.Base
Iago Abal
Merge Z3.Base
Iago Abal
Clean up
David Castro
Changed types of mkForall and mkExists in Z3.Base
David Castro
castPtr removed.
David Castro
Existential quantifier.
David Castro
Result datatype simplified in Z3.Base.
David Castro
delModel added.
  1. Prev
  2. Next