问题标签 [z3]

我对 SMT Z3 使用（如 DbC）的实际示例感兴趣并寻找该工具的代码和开源替代品。所以，其实我对类似的Z3形式求解工具很感兴趣，但是：

• 它必须是开源的
• 提供低级（API）和高级（文本脚本）交互
• 支持 SMT-LIB
• 适用于（可用）工具/编写/用于 Java、python、ruby、Vala 等语言，而不是Haskell
• 有基于它的稳定（在实践中可用）工具，如按合同设计（DbC）、静态类型验证等。

根据 SMT-LIB 主页（详见 bit.ly bundle），2010 年 SMT 求解器列表为：“Alt-Ergo、Barcelogic、Beaver、Boolector、CVC3、DPT、MathSAT、OpenSMT、SatEEn、Spear、STP、SWORD、 UCLID、veriT、Yices、Z3。”

请就在实践中使用它们提供任何反馈（代码示例是最好的）？

最后，将它与 GHC 可能性进行比较的任何信息都是有用的，但前提是存在实现示例（不是语言“功能”）。

更多关于 Z3 的快速信息在这里http://bit.ly/bundles/ewiger/1

我尝试为Z3编译 OCaml 版本，但是当我构建它时，它总是显示一堆错误和警告。

这些是几个错误：

我真的不明白，我只是尝试运行build.cmd，然后发生错误，有人知道吗？

我正在尝试将Z3 SMT 求解器用于我的项目。但是，Visual Studio 版本似乎不匹配，这给我带来了麻烦。我的 Visual Studio 2008 报告说

找不到引用的组件“Microsoft.Z3”。

虽然它确实在安装目录中（C:\Program Files\Microsoft Research\Z3-2.19\bin）。

编译项目时，另一个警告说

已解决的文件有错误的图像、没有元数据或无法访问。无法加载文件或程序集“C:\Program Files\Microsoft Research\Z3-2.19\bin\Microsoft.Z3.dll”或其依赖项之一。此程序集由比当前加载的运行时更新的运行时构建，无法加载。

以及其他错误，说明未找到 Z3 相关类型如上下文、术语等。

这是因为 Z3 的新版本是使用我没有的较新版本的 dotNet 框架编译的吗？我该如何解决这个问题？提前致谢！

PS：我在测试中使用的文件来自Z3教程（pdf），第5章，粘贴在下面。

更新：在对旧的 .msi 安装程序文件进行几次提取后，我发现使用低于 v4 的 dotNet Framework 的 Z3 的最新版本是 Z3 2.11；在这种情况下，我决定使用，而不是暂时更新我的​​ VS2008。

SMTLib2 指令(get-info all-statistics)显示几个数字，例如

为了测试不同的公理化和编码，我想知道这些数字中的哪些适合声明一个 Z3 运行比另一个更好/更有效。

从名字猜我会说num. qa. inst- 量词实例化的数量 - 是一个很好的指标（更低=更好），但其他呢？

我正在尝试一些涉及递归函数的 Z3 教程示例。我已经尝试了以下示例。

1. 斐波那契（第 8.3 节）
2. IsNat（第 8.3 节）
3. 感应式（第 10.5 节）

Z3在上述所有示例中都超时。但是，本教程似乎暗示只有归纳是非终止的。

Z3 是否可以检查包含递归函数的公式的可满足性，或者它不能处理任何归纳事实？

有没有人尝试用 Z3 本身来证明Z3 ？

甚至有可能使用 Z3 来证明 Z3 是正确的吗？

更理论上，是否有可能证明工具 X 是正确的，使用 X 本身？

我在Z3 程序中使用以下规则来s生成 sort 的唯一可能值S。

但是，上面的公式让Z3报如下错误：

确保特定类型的域只有一个值的正确方法是什么？

是否可以标记 Z3 范围（SMTLib2 语法）然后弹回特定范围？例如：

我知道我可以使用 弹出两个范围(pop 2)，但在我的场景中，这意味着我必须跟踪在必须匹配的推-弹出对之间打开的尚未关闭的范围的数量，即必须恢复 Z3 上下文以前存在过(push foo)。

Z3 可以生成 Craig 插值（至少对于命题逻辑？）。我在 Z3 的文档中没有找到它。

我正在使用 Z3 来证明为实时任务系统获得的时间表的稳健性。当我检查这个脚本http://www.cs.ru.nl/~georgeta/script.smt2我得到一个不满意的响应。但是，当我使用 PROOF_MODE=1 选项时，响应是饱和的。在前一种情况下可能会出现什么问题？