微软研究院宣称，Z3 是世界上最快的定理证明程序。Z3 被设计作为其他应用程序的底层工具，它不适合单独使用。而嵌入到定理证明程序中的时候，在大量的项目中都有应用，包括 Spec#/Boogie 、 Pex 、 Yogi 、 Vigilante 、 SLAM 、 F7 、 SAGE 、 VS3 、 FORMULA 和 HAVOC 。
通过使用 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 来尝试一下在线版本。
暂无签名
最新发布
吴磊畅谈 Silverlight 在中国人寿的应用
2010-10-27
Azure 于今日正式商用收费，不包括中国大陆
2010-02-01
MonoDevelop 正式迈入跨平台时代
2009-09-10
腾讯云云原生提质增效实践精选集 2024
《2024腾讯云云原生提质增效实践精选集》出炉，5大热门技术领域，13个行业精选标杆案例，痛点到解决方案全...
大模型时代的创业机会洞察
WebF 是如何高性能实现 Flutter + Web 融合的
QCon 中国的第 15 年
评论