问题标签 [z3]

我正在使用 Z3 构建有界模型检查器。在尝试实施完整性测试时，我遇到了一个奇怪的性能问题。完整性测试必须确保所有状态，每条路径最多包含每个状态一次。如果仍有满足此属性的路径，则 Z3 很快就会给出答案，但是在考虑了所有路径的情况下，Z3 似乎呈指数级缓慢。

我已将测试用例简化为以下内容：

在我的计算机上，这会导致以下运行时间（取决于路径长度）：

• 3：0.057s
• 4：0.561s
• 5：42.602s
• 6：>15m（中止）

如果我从 Int 切换到大小为 64 的位向量，性能会稍微好一些，但似乎仍然呈指数级：

• 3：0.035s
• 4：0.053s
• 5：0.061s
• 6：0.106s
• 7：0.467s
• 8：1.809s
• 9：2m49.074s

奇怪的是，长度为 10 只需要 2m34.197s。如果我切换到更小尺寸的位向量，性能会好一点，但仍然是指数级的。

所以我的问题是：这是可以预料的吗？有没有更好的方法来制定这种“无循环”约束？

Microsoft.Z3.dll 在文件属性中被描述为 Z3 托管 DLL。

Java可以加载dll。它使用 System.loadLibrary 或 System.load 执行此操作，具体取决于程序员的偏好。

如果 Java 设计者还创建了 DLL，则可以使用 javah 来定义导入/导出声明。不幸的是，这不是我的情况。Microsoft 已将 DLL 创建为托管 C# DLL。

我需要一些帮助来获取 C# 声明，例如在Microsoft RISE Z3 托管 API中找到的声明，并对Java 包/类进行原型设计以使调用成功。（我确信 DLL 已加载）。

为方便起见，具体调用由 Microsoft 在 Microsoft.Z3.h 的第 03042 行定义。任何示例代码将不胜感激！

我从我的服务器得到的错误是：

我们有一个在 Azure 中运行的 C# Web 角色，C# 项目调用我们随应用程序部署的 F# dll 中的代码。

当我们使用本地 Azure 模拟器在本地运行时，我们的 F# 代码被调用并运行良好。当它在云中的 Azure 中运行时，我们的 F# 代码在某个时间点失败，并出现以下异常：

无法解析 x 的函数：var(2).Exception: System.IO.FileNotFoundException: 无法加载文件或程序集 'FSharp.Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' 或其依赖项之一。该系统找不到指定的文件。
文件名： Microsoft.FSharp.Text.Lexing.LexBuffer 1.FromArray(char[] s) at Microsoft.FSharp.Text.Lexing.LexBuffer1.FromString(String s) at Marshal.vars@27.GenerateNext(IEnumerable) 的“FSharp.Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a 1&下一个）
警告：程序集绑定日志记录已关闭。要启用程序集绑定失败日志记录，请将注册表值 [HKLM\Software\Microsoft\Fusion!EnableLog] (DWORD) 设置为 1。注意：与程序集绑定失败日志记录相关的一些性能损失。要关闭此功能，请删除注册表值 [HKLM\Software\Microsoft\Fusion!EnableLog]。.将使用默认功能。

我们发现一些帖子表明这是因为：

Windows Azure 以部分信任的方式运行应用程序，作为沙盒执行的一部分。但是，F# 核心库当前已安装到 GAC 中，但没有 AllowPartialTrustedCallers 属性。因此，在构建要在 Azure 中运行的 F# 应用程序时，必须使用 --standalone 静态链接 F# 库。提供的模板可以解决这个问题，但您会注意到以下副作用： • 编译时间比平时长 • 大量引用 • 对“RDManaged.dll”的虚拟引用

http://archive.msdn.microsoft.com/fsharpazure

为了解决这个问题，我们遵循以下建议并将–standalone标志放入 F# 库的构建配置中。

http://www.42spikes.com/post/F-and-Azure.aspx

但是，F# 库不使用此标志进行编译。我们得到这个构建错误：

错误 3 写入二进制“obj\Debug\Analyzer.dll”时出现问题：Microsoft.FSharp.Text.StructuredFormat.Joint 类型的 pass2 出错，错误：您的模块之一需要类型“System.Collections.IStructuralEquatable”在被发射的模块中定义。您可能缺少输入文件 FSC 1 1
Analyzer

这个构建错误可能是因为我们的 F# 项目具有依赖关系吗？它引用了 FSharp.PowerPack.dll 和 Microsoft.Z3.dll，以及我们解决方案中的另一个 C# 库 AnalyzerCommon.dll（它只包含我们的 F# 和 C# 代码实现的通用接口）。

有趣的是，F# 代码被调用并且运行良好，直到它到达代码的某个部分——一个使用 FSharp.PowerPack.dll 的公式解析器。

任何提示将非常感谢。

谢谢，山姆

如何显示量词消除的结果？
z3 似乎对以下输入感到满意

但它返回的结果与输出相同。

谢谢

这是我使用 z3 执行的 SMT-LIB 2.0 基准测试：

我预计结果是sat，至少有一个模型，其中ZPZ的幂集（整数）是一个谓词，用于测试整数在Z的子集（排序的元素）中的成员资格。MSPZ

但是z3回答了unsat。

你能帮我理解这个结果吗？具体来说，z3 如何解释 sort Int？它真的被认为是无限的吗？那么动态声明的排序（这里是排序PZ）呢？

我目前正在尝试使用 Z3 作为用合金（一种关系逻辑/语言）编写的规范的有界引擎。我使用 UFBV 作为目标语言。

我使用 Z3 选项检测到问题(set-option :pull-nested-quantifiers true)。

对于两个语义相同的 SMT 规范 Spec1 和 Spec2，Z3 超时（200 秒）以证明 Spec1 但证明 Spec2。

Spec1 和 Spec2 之间的唯一区别是它们具有不同的函数标识符（因为我使用 java 哈希名称）。这可能与错误有关吗？

我想分享和讨论的第二个观察是iffUFBV 上下文中的 " " 运算符。(set-logic UFBV)如果已设置，则不支持此运算符。我的解决方案是改用“=”，但如果操作数包含深度嵌套的量词并且pull-nested-quantifiers设置了“”，则此方法效果不佳。另一个节省的解决方案是使用双重暗示。

现在的问题是：对于 UFBV 中的“”模型是否还有其他更好的解决方案iff，因为我认为，使用双重暗示通常会丢失可用的语义信息以进行改进/简化。

http://i12www.ira.uka.de/~elghazi/tmp/

你可以找到：spec1和spec2两个（我认为）语义相同的 SMT 规范，以及spec3一个使用“=”来建模“ iff”的 SMT 规范，z3 超时。

例如，在下面的代码中，路径条件将为x>0 && x+1>0. 但是由于x>0暗示x+1>0，z3 或 pex API 中是否有任何方法只能获取x>0而不是两者兼而有之。

谢谢

如何在 Z3 中将位向量漂亮地打印为带符号的小数？

我正在从事一个项目，其重点是使用术语重写来解决/简化固定大小的位向量算术问题，这对于一些决策过程（例如基于位爆破的决策过程）的前一步很有用。重写这个术语可能完全解决问题，或者产生一个更简单的等效问题，因此两者的结合可以带来相当大的加速。

我知道许多 SMT 求解器都实施了这种策略（例如 Boolector、Beaver、Alt-Ergo 或 Z3），但很难找到详细描述这些重写步骤的论文/技术报告/等。一般来说，我只找到作者在几段中描述这种简化步骤的论文。我想找到一些详细解释术语重写使用的文档：提供规则示例，讨论 AC 重写和/或其他等式公理的便利性，重写策略的使用等。

目前，我刚刚找到了技术报告A Decision Procedure for Fixed-Width Bit-Vectors，它描述了 CVC Lite 执行的规范化/简化步骤，我想找到更多这样的技术报告！我还找到了一张关于STP 中术语重写的海报，但这只是一个简短的总结。

我已经访问了那些 SMT 求解器的网站，并在他们的出版物页面中进行了搜索...

我将不胜感激任何参考或任何解释如何在当前版本的知名 SMT 求解器中使用术语重写。我对 Z3 特别感兴趣，因为它看起来拥有最智能的简化阶段之一。例如，Z3 3.* 引入了一个新的位向量决策过程，但不幸的是，我找不到任何描述它的论文。

Assume that I have asserted some formula P and, after checking satisfiability, obtained from Z3 a partial model for it, let's call it M.

Now, would it be possible to test whether another formula Q can be satisfied by extending, if necessary, the current model M. That is, I want to check whether the formula P and Q is satisfiable but fixing the values that have been assigned by the current partial model.

Alternatively, is it possible to ask Z3 to “complete” a specific partial model? (That is, I still want to obtain partial models; but, in a few cases, I would like to be able to extend a partial model so that I can then evaluate some arbitrary formula Q which might contain constants/functions not assigned by the current model)