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 Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell

-- Aaron Tomb Galois, Inc. (http://www.galois.com) atomb@galois.com Phone: (503) 626-6616 ext. 156 Fax: (503) 350-0833