BT

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

| 作者: Jonathan Allen フォローする 609 人のフォロワー , 翻訳者 尾崎 義尚 フォローする 0 人のフォロワー 投稿日 2010年12月1日. 推定読書時間: 1 分 |

原文(投稿日: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のオンラインバージョンを使うことができる。

この記事に星をつける

おすすめ度
スタイル

こんにちは

コメントするには InfoQアカウントの登録 または が必要です。InfoQ に登録するとさまざまなことができます。

アカウント登録をしてInfoQをお楽しみください。

あなたの意見をお聞かせください。

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

このスレッドのメッセージについてEmailでリプライする
コミュニティコメント

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

このスレッドのメッセージについてEmailでリプライする

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

このスレッドのメッセージについてEmailでリプライする

ディスカッション

InfoQにログインし新機能を利用する


パスワードを忘れた方はこちらへ

Follow

お気に入りのトピックや著者をフォローする

業界やサイト内で一番重要な見出しを閲覧する

Like

より多いシグナル、より少ないノイズ

お気に入りのトピックと著者を選択して自分のフィードを作る

Notifications

最新情報をすぐ手に入れるようにしよう

通知設定をして、お気に入りコンテンツを見逃さないようにしよう!

BT