问题标签 [smt]

我计划在 C 代码的符号执行方面进行一些实验，使用现成的 SMT 求解器，并想知道使用哪个求解器；例如，查看 SMT 竞赛的参赛者，仅采用开源系统，将其范围缩小到 Beaver、Boolector、CVC3、OpenSMT、Sateen、Sonolar、STP、Verit；这仍然是一个很长的清单。

试图进一步缩小范围，我注意到一些系统宣传处理位向量算术的能力，而其他系统只宣传处理一般整数算术的能力。原则上，前者对于 C 是正确的，其中变量是机器字，而不是无界整数。它在实践中有多大的不同？如果您尝试使用通用整数系统来完成此类工作，会发生什么情况？以下情况之一是否适用？

1. 位向量系统的效率稍高一些，但您可以使用其中任何一个，没问题。

2. 您可以使用稍作调整的通用整数系统。

3. 一般整数系统适用于有符号整数（因为溢出的结果未定义），但会给出无符号的错误答案。

4. 一般的整数系统对于机器字算术来说是不正确的，我可以将我的短名单减少到只有那些提供位向量算术的系统。

5. 还有什么……？

我试图尽可能具体地提出一个问题，但如果有人可以提出任何其他标准来缩小列表范围，那就太好了！

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

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

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

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

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

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

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

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

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

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

我正在尝试使用 Z3 来推理子字符串，并且遇到了一些不直观的行为。当被问及“xy”是否出现在“xy”中时，Z3 返回“sat”，但当被问及“x”是否在“x”中或“x”是否在“xy”中时，它返回“未知”。

我评论了以下代码来说明这种行为：

现在问题已经成立，我们尝试找到子字符串：

如果我们改为搜索findMeXYin xy，求解器会按预期返回“sat”。看起来，由于求解器可以处理“xy”的查询，它应该能够处理“x”的查询。此外，如果搜索findMeX='x'in 'xy='xy'，它会返回“未知”。

任何人都可以提出解释，或者在 SMT 求解器中表达这个问题的替代模型吗？

我正在使用 Z3 的 QBVF 求解器，想知道是否可以从存在断言中提取值。也就是说，假设我有以下内容：

这基本上说有一个“最少”的 16 位无符号值。那么，我可以说：

Z3-3.0 愉快地回应：

这真的很酷。但我想做的是能够通过 get-value 提取该模型的各个部分。不出所料，以下似乎都不起作用

在每种情况下，Z3 都正确地抱怨没有这样的常数。(check-sat)显然，Z3 拥有该信息，正如对呼叫的响应所证明的那样。有没有办法通过get-value或其他机制自动访问存在值？

谢谢..

你能告诉我如何在 z3 SMT-LIB 2.0 基准测试中命名断言吗？我更喜欢使用 SMT-LIB 的标准语法，但由于 z3 似乎不理解它，我只是在寻找一个使用 z3 的语法。需要获得带有标签的未饱和核心。

这是我测试的基准测试示例：

由于矛盾（x < y 和 y <= x），我期待 unsat 核心 {hyp4, hyp5}，但 z3 返回：

我知道 z3 不理解这种命名方式，但我在 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。如果我切换到更小尺寸的位向量，性能会好一点，但仍然是指数级的。

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

这是我使用 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 超时。