SAKAI Masahiro - HaskellSMT Diff

Haskellで使えるSMT関係のライブラリ他のメモ。

=　パーサ・プリンタ

== smt-lib

* ((<URL:http://hackage.haskell.org/package/smt-lib>))
* ((<URL:https://github.com/tomahawkins/smt-lib.git>))

パーサとプリンタ。
数年以上メンテナンスされていない。

== Hsmtlib

後述

== Smtlib / SmtLib

* ((<URL:https://github.com/MfesGA/Smtlib>))
* ((<URL:http://hackage.haskell.org/package/SmtLib>))

Hsmtlibのパーサとプリンタ部分を切り出したものだと思う。
自分のtoysmtではとりあえずこれを使ってみたが、色々不都合があり結局ローカルに色々書き換えたものを使っている。
プルリクエストも色々と送っているが、あまり取り込んでもらえていない。

= 幾つかのSMTソルバを呼び出すためのライブラリ

== Hsmtlib

* ((<URL:http://hackage.haskell.org/package/Hsmtlib>))
* ((<URL:https://github.com/MfesGA/Hsmtlib>))

パーサも含まれているたが、それはSmtlibに切り出された模様。

== sbv

* ((<URL:http://hackage.haskell.org/package/sbv>))

割とHaskellっぽいインターフェースを工夫している模様。

== smtlib2

* ((<URL:http://hackage.haskell.org/package/smtlib2>))
* ((<URL:https://github.com/hguenther/smtlib2.git>))

== simple-smt

* ((<URL:http://hackage.haskell.org/package/simple-smt>))
* ((<URL:https://github.com/yav/simple-smt>))

= 特定のSMTソルバを呼び出すためのライブラリ

== z3

* ((<URL:http://hackage.haskell.org/package/z3>))
* ((<URL:http://bitbucket.org/iago/z3-haskell>))

== bindings-yices

* ((<URL:http://hackage.haskell.org/package/bindings-yices>))
* ((<URL:http://github.com/pepeiborra/bindings-yices>))

== yices-easy

* ((<URL:http://hackage.haskell.org/package/yices-easy>))

== yices-painless

* ((<URL:http://hackage.haskell.org/package/yices-painless>))
* ((<URL:http://code.haskell.org/~dons/code/yices-painless/>))

= Haskellで書かれたSMTソルバ

== Smooth

* ((<URL:http://hackage.haskell.org/package/Smooth>))

== nano-smt

* ((<URL:https://github.com/UCSD-PL/nano-smt>))

== toysolver (toysmt)

* ((<URL:http://hackage.haskell.org/package/toysolver>))
* ((<URL:https://github.com/msakai/toysolver>))