LINQ to Z3、世界最速の定理証明器

作者 Jonathan Allen , 翻訳者 尾崎 義尚 投稿日 2010年12月1日

セクション

デベロップメント

トピック

.NET ,

プログラミング ,

LINQ

共有 |

原文(投稿日：2010/11/29)へのリンク

マイクロソフトリサーチは、Z3は、世界最速の定理証明器であると宣言した。Z3は、ほかのアプリケーションへの低レベルツールとして設計されており、単独では動作しない。定理証明器のホストは、 Spec#/Boogie、Pex、Yogi、Vigilante、SLAM、F7、SAGE、VS3、FORMULA、HAVOCを含む数多のプロジェクトで使用されている。

Z3の.NET APIを使用すると、エンコード定義をオブジェクト指向スタイルで行うことができる。しかしながら、たとえば、Z3チュートリアルの例では小さな問題に関しても、非常に退屈なコードになることを示している。Bart De Smet氏は、OOスタイルのAPIをラップして、LINQ to Z3と呼ばれるクエリスタイルのAPIにし、すばらしく簡易化した。以下の例は、Bart De Smet氏のChannel 9インタビューで提示されていたものである。

  var theorem = from t in ctx.NewTheorem<Symbols<int, int, int, int, int>>()
    where t.X1 - t.X2 >= 1
    where t.X1 - t.X2 <= 3
    where t.X1 == (2 * t.X3) + t.X5
    where t.X3 == t.X5
    where t.X2 == 6 * t.X4
    select t; 
  var solution = theorem.Solve();
  Console.WriteLine("X1 = {0}, X2 = {1}, X3 = {2}, X4 = {3}, X5 = {4}",

Z3のプライマリサポートはWindowsであるが、LinuxバージョンのZ3も存在している。 Z3は、非商用に“Microsoft Research License Agreement”下で利用可能である。RiSE4fun上でZ3のオンラインバージョンを使うことができる。