簡単なSMTソルバの実装ができた。 https://github.com/msakai/toysolver/commit/dc72520ad3d5902d8e2733f9adbb2574e1e8723b
先日の #ProofSummit での発表「SAT/SMTソルバの仕組み」 http://www.slideshare.net/sakai/satsmt をキッカケに、放置気味だった実装を再開して、ようやくある程度のところまで実装できたのだった。個々の構成要素はある程度既に実装してあったのだけれど、ちゃんと繋げるようにして繋ぐのが大変だった。
まだサポートしているのはSMT(EUF ∪ LRA)のみで、かつ実装はまだまだ不完全で機能も足らないけれど、例えば以下の様な例が動いている。
------
solver <- SMT.newSolver
a <- SMT.declareConst solver "a" SBool
x <- SMT.declareConst solver "x" SReal
y <- SMT.declareConst solver "y" SReal
SMT.assert solver $ ite a (2*x + (1/3)*y .<=. -4) (1.5 * y .==. -2*x)
SMT.assert solver $ (x .>. y) .||. (a .<=>. (3*x .<. -1 + (1/5)*(x + y)))
SMT.checkSAT solver -- True
------
solver <- SMT.newSolver
x <- SMT.declareConst solver "x" SBool
f <- SMT.declareFun solver "f" [SBool] SBool
SMT.assert solver $ f true .==. true
SMT.assert solver $ notB (f x)
SMT.checkSAT solver -- True
SMT.assert solver x
SMT.checkSAT solver -- False
------
solver <- SMT.newSolver
a <- SMT.declareConst solver "a" SBool
x <- SMT.declareConst solver "x" SU
y <- SMT.declareConst solver "y" SU
f <- SMT.declareFun solver "f" [SU] SU
SMT.assert solver $ a .||. (x .==. y)
SMT.assert solver $ f x ./=. f y
SMT.checkSAT solver -- True
SMT.assert solver $ notB a
SMT.checkSAT solver -- False
------
solver <- SMT.newSolver
x <- SMT.declareConst solver "x" SU
y <- SMT.declareConst solver "y" SU
f <- SMT.declareFun solver "f" [SU] SU
SMT.assert solver $ f x ./=. f y
SMT.checkSAT solver -- True
SMT.pushContext solver
SMT.assert solver $ x .==. y
SMT.checkSAT solver -- False
SMT.popContext solver
SMT.checkSAT solver -- True