Commits

Author Commit Message Labels Comments Date
Scott West
Adding array evaluation. Evaluation of the array is done by converting an evaluated array into a function interpretation, then using the function interpretation extraction mechanism. The example has been updated to contain a small use of each. Although not a full practical example, it can serve as a simple test and showing how they can be used.
Scott West
Recover interpreted functions from the model. This includes a test case.
Iago Abal
Merge Jeff's changeset lifting arrays to Z3.Monad
Jeff Arenson
Lifted arrays (mkArraySort, mkSelect, mkConstArray, mkMap, mkArrayDefault) into Z3.Monad
Iago Abal
Set version to 0.3.1 (tentative) The goal is to do a minor release extending Z3.Base and Z3.Monad APIs.
Iago Abal
Fix comment style #cleanup
Iago Abal
Low-level support of uninterpreted sorts
Iago Abal
Added tag v0.3.0 for changeset 4d5bc01a240a
Iago Abal
Many documentation fixes
Tags
v0.3.0
Iago Abal
Fix Castable class context: it only makes sense for IsTy types!
Iago Abal
Fix example
Iago Abal
Warn whoever import solver-related stuff that the support is still fragile
Iago Abal
Examples solving the N-queens problem
David Castro
Error Handling in Z3.Base: * mkContext sets a NULL error handler * every function in Z3.Base checks if an error happened and throws a Z3Error exception
David Castro
Error Handling in Z3.Base.C
Iago Abal
Update copyright year
Iago Abal
Rewrite checkModel* machinery to avoid code duplication
Iago Abal
Merge with Eddy's checkModelWithResult bundle
eddy_westbrook
added withModelAndResult
Iago Abal
Fix comment style & remove trailing spaces #cleanup
Iago Abal
Add missing Cast case for tcNat and compileNat #fix
Iago Abal
Support casting from Nat to Integer
Iago Abal
Tweak Z3.Lang argument processing #cleanup
Iago Abal
Remove trailing spaces
Iago Abal
Remove dead code #cleanup
Iago Abal
Merge Eddy's work on casts
eddy_westbrook
added support for casts to the Expr type
Iago Abal
Fix comment style
Iago Abal
Rewrite of checkModel to make expressions be evaluated inside a Model monad This fixes a bug caused by misunderstanding the z3_check_and_get_model API call: every time it is called it *may* return a different model!
Iago Abal
Automated merge with ssh://bitbucket.org/iago/z3-haskell
  1. Prev
  2. Next