BT

最新技術を追い求めるデベロッパのための情報コミュニティ

寄稿

Topics

地域を選ぶ

InfoQ ホームページ ニュース LINQ to Z3、世界最速の定理証明器

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

Leia em Português

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

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

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のオンラインバージョンを使うことができる。

この記事に星をつける

おすすめ度
スタイル

BT