Commits

Author Commit Message Labels Comments Date
Iago Abal
Minor documentation fixes
Iago Abal
Add lg2(n) and 2^n axiomatizations for integral types
Iago Abal
Remove the limitation of function's range being a base Z3 type
Iago Abal
Move `compile' to a separate class `Compilable'
Iago Abal
Just support functions up to arity 5
Iago Abal
Let the user to configure some Z3 parameters
Iago Abal
Ignore .cabal~ files
Iago Abal
Ignore cabal-dev folder
David Castro
Z3.Base: with<Context|Config> = withForeignPtr . un<Context|Config>
Iago Abal
Minor tweak
Iago Abal
Add basic support for instantiation patterns
Iago Abal
Add a `divides' operator
Iago Abal
Tweak `implies' operator to rewrite p => (q => r) to p && q => r
Iago Abal
Minor tweak
Iago Abal
Add basic quantifier support to the Z3.Lang high-level API
Iago Abal
Fix/redesign of the TCC apparatus
Iago Abal
Fix 'and_' and 'or_' to avoid creating 'BoolMulti' expressions with no arguments
Iago Abal
Ignore .orig files
David Castro
Minor fixes.
David Castro
Automated merge with ssh://bitbucket.org/iago/z3-haskell
David Castro
* Added uninterpreted functions to Z3.Lang.
David Castro
Added mkApp and mkFuncDecl functions to Z3.Base.
David Castro
Fixed 'set_WELL_SORTED_CHECK' parameter.
David Castro
Added newtype FuncDecl to Z3.Base
David Castro
Added function declaration and application to Z3.Base.C
David Castro
Added checkModel :: IsScalar a => Expr a -> Z3 (Result a). Created models are
Iago Abal
Remove Show (Expr a) and Eq (Expr a) instances for GHC >= 7.4
Iago Abal
Add basic support for universally quantified formulas
Iago Abal
Minor fix
Iago Abal
Restrict dividend to be non-zero
  1. Prev
  2. Next