You may want to take a look at this, as well:
http://www.sivity.net/projects/smt-yices
Aaron
On Jul 23, 2009, at 5:32 PM, Ahn, Ki Yung wrote:
http://hackage.haskell.org/package/yices
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.
--
Ahn, Ki Yung
_______________________________________________
Haskell mailing list
hask...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
--
Aaron Tomb
Galois, Inc. (http://www.galois.com)
at...@galois.com
Phone: (503) 626-6616 ext. 156
Fax: (503) 350-0833
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
