LINQ to Z3,世界上最快的定理证明程序

  • Jonathan Allen
  • 朱永光

2010 年 12 月 1 日

话题:.NET语言 & 开发

微软研究院宣称,Z3 是世界上最快的定理证明程序。Z3 被设计作为其他应用程序的底层工具,它不适合单独使用。而嵌入到定理证明程序中的时候,在大量的项目中都有应用,包括Spec#/BoogiePexYogiVigilanteSLAMF7SAGEVS3FORMULAHAVOC

通过使用 Z3 的.NET 的 API,你可以使用面向对象的风格来编码定理。不过,在Z3 练习指导中演示的一个非常小的问题,都用到了非常多的代码。Bart De Smet 编写了名为LINQ to Z3的包装器,把 OO 风格的 API 包装为查询风格的 API,极大地简化了 Z3 的使用。下面是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 on RiSE4Fun来尝试一下在线版本。

查看英文原文:LINQ to Z3, The World’s Fasted Theorem Prover

.NET语言 & 开发