1. Iago Abal
  2. z3-haskell

Commits

Author Commit Message Date Builds
Iago Abal
Remove trailing spaces #cleanup
Iago Abal
Cabalize examples
Iago Abal
Rename: examples/monad/func_and_array.hs -> FuncModel.hs #cleanup
Iago Abal
Export low-level C API calls to extract function/array models Also, remove a bunch of trailing spaces. #cleanup
Scott West
Adding else part and datatype for function models. The new datatype rolls together the map and else part of a function model.
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
  1. Prev
  2. Next