[SMT-LIB] [Announcement] Accessing SMT solvers from Haskell, now supporting CVC4

[Levent Erkok]

[Potentially off-topic: Please ignore if you are not interested in
accessing SMT-solvers from Haskell!]

As most list members are no doubt aware, programming-languages
community has been building bridges between high-level PL's and SMT
solvers for quite a while. Haskell, for instance, has several such
bindings. One particular project that targets a seamless integration
between Haskell and SMT solvers via the smt-lib2 interface is SBV,
which previously had connections to Yices and Z3. I'm happy to
announce v2.9 release of the Haskell SBV library:


       http://leventerkok.github.com/sbv/

New in this release is support for the CVC4 SMT solver:
http://cvc4.cs.nyu.edu/web/

This is an exciting development from the Haskell community
perspective: *CVC4 comes with essentially no limit on its use for
research or commercial purposes*! (Direct quote from the CVC4 web-site
cited above.) Consequently, I expect more Haskell folks to explore SMT
solvers in due course.

If you are a member of the SMT-Lib community, but do not particularly
care for Haskell: Then I'm hoping this release will provide an
opportunity for you (or your students) to explore the world of
functional programming by allowing you to script your favorite
SMT-solvers from within a very high-level functional language that has
enjoyed considerable success in both academia and the industry.
Haskell is well suited for both research projects and commercial
applications, and has a vibrant community. Prototyping new ideas in
Haskell with the SMT-solvers being at your finger-tips via the
SMT-Lib2 interface might interest both researchers and practitioners
alike.

Feedback, patches and bug reports are always welcome.

Levent Erkok.