Commits

Author Commit Message Labels Comments Date
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
Iago Abal
Automated merge with ssh://bitbucket.org/iago/z3-haskell
Iago Abal
Increase version number in Cabal file (0.1.1 -> 0.2.0)
Iago Abal
Declare Z3.Lang.Nat in z3.cabal (d'oh!)
Iago Abal
Minor fixes
Iago Abal
Add support for natural arithmetic
Iago Abal
Minor fix
David Castro
Minor cleanum in Z3.Lang.Monad.
Iago Abal
Create a Z3.Lang.Prelude offering the basic functionality of Z3
Iago Abal
Move expressions into a Z3.Lang.Exprs module
  1. Prev
  2. Next