问题标签 [z3]

我正在使用 z3 进行研究，但遇到以下问题。我正在分析包含数组和未解释函数的可满足公式的模型。我想检查特定的数组条目。

在 z3 指南的示例中，可以访问这些值。
例如，对于像这样的问题

一个人得到答案

表示my_arrayat 位置的0值为1。

但是，我得到的答案看起来像

这根本不是很有帮助。

此外，在模型的开头，我得到一个如下所示的块：

我不太明白这个的意思，但不知何故，这似乎与我的问题有关，因为指南中的简单示例没有出现类似的块。有谁知道是什么触发了 z3 的这种行为或如何避免这种行为？

经过一些实验，我发现了一个表现出不良行为的“最小”示例。它似乎与在索引表达式中使用未解释的函数有关。

z3对此的回应是：

我已经用 z3 分析了 QF_AUFLIA 中的一个公式。结果是sat。返回的模型(get-model)包含以下几行：

根据我对 SMTLIBv2 语言的理解，这个语句是畸形的。=只能应用于相同类型的参数。但是，2有 sortInt和false有 sort Bool。

当我将这两行反馈给 z3 时，它同意我的说法：

这是一个错误吗？

如果不是，我应该如何解释(= 2 false)？

安装 Z3 V3.1 后，以下 SMT-LIB 代码不起作用。在我的早期版本（Z3 V2.19）中已经相当不错了。

我需要在上面的代码中更改什么才能在 3.1 版本中运行它。

根据INI 参数列表，应该有一个布尔警告标志，但通过在 Z3 3.2 (x64_mt) 中设置它

拼写和. unsupported_WARNINGwarning

文档是否已过时或我在这里做错了什么？

[编辑]

根据Z3 2.17 的发行说明，该选项应通过以下方式设置

但尝试

产量

我有一个快速的问题。我编写了一个简单的程序（使用 Z3 NET API）并得到如下输出。

程序（部分）：

输出：

我想知道我是否可以将“else -> true”设为假（即“else -> false”）。

对于 Z3 2.x，我使用了 SMTLib2 命令

获取 Z3 运行的统计信息。使用 Z3 3.2 我得到

对于上述情况，以及

Z3 回复

获取统计信息的新方法是什么（除了 /st 命令行选项）？

作为一个有效的选项，但 Z3 3.2 再次回复

我正在使用带有 c api 的 Z3。是否可以找出给定Z3_ast变量是否对应于or_b1_b2下面的子句？

谢谢

我有一个文件包含：

并且，根据在线教程，在这个文件上运行 z3 应该返回：

所以我知道这是合法的 Z3 输入。但是，每当我运行“z3 [option]”时，无论我选择什么选项，我得到的都是错误消息——包括没有。有人能告诉我如何在输入文件上正确调用 Z3 吗？

问候。

给定一个任意命题公式 PHI（对某些变量的线性约束），确定每个变量的（近似）上限和下限的最佳方法是什么？

有些变量可能是无界的。在这种情况下，算法应该得出结论，这些变量没有上限/下限。

例如，PHI = (x=3 AND y>=1)。x 的上限和下限均为 3。y 的下限为 1，并且 y 没有上限。

这是一个非常简单的例子，但有没有一般的解决方案（可能使用 SMT 求解器）？

我正在尝试使用 Z3 SMT Solver 证明以下内容：((x*x) + x) = ((~x * ~x) + ~x). 这是正确的，因为 c 编程语言中的溢出语义。

现在我编写了以下 smt-lib 代码：

z3 的输出是：

现在我的问题是：为什么结果“不满意”？我的代码中的简化命令表明可以获得有效的分配，以便 myfun1 和 myfun2 具有相同的结果。

我的代码有问题还是z3中的错误？

请任何人都可以帮助我。谢谢