Incomplete (no bitvectors) syntax, parser, and inter
process communication to Yices from Haskell through pipe.
Purpose for building and using this library was to generate
test cases from constraints that SMT solvers can solve. I
only used it for that particular purpose, so the code in
general is not yet fully tested. Use at your own risk and
error reports are welcomed. See http://yices.csl.sri.com/ for further information on Yices.
Note: this package does not include Yices. You should get it from the
Yices homepage and install it before using this library.
@ If you already have a better API for Yices or other SMT solvers, and
if you can open the source please upload it to hacakage. That would be
great help for some people.