问题标签 [z3]

我有以下代码

代码应该在第一个（check-sat）返回 unsat 并在第二个（check-sat）返回，但我不知道。

有人可以告诉我有什么问题。我正在使用 Windows 7，使用 cygwin 的 jSMTLIB

谢谢赛义夫

我有以下 SMT-Lib2 脚本：

在 Mac 上运行 Z3 v3.2 时，我得到：

其中指出 s0 = -1 是一个模型。但是，对于 s0 = -1，我们有 s3 = 1 和 s5 = #b0，这使得断言为假。事实上，我很确定上述基准是不能令人满意的。

我在 Z3 输出中注意到的一件事是它为基数约束提供的量化公式。它说：

断言是一个连词，听起来很奇怪；这不应该是一种分离吗？我不确定这是否是问题的根本原因，但听起来确实很可疑。

在使用 SMTLIB 数组时，我注意到 Z3 对理论的理解与我的不同。我使用的是 SMTLIB 数组理论 [0]，可以在官方网站 [1] 上找到。

我认为我的问题最好用一个简单的例子来说明。

第一个数组应在索引 1 处返回 2，对所有其他索引返回 0，第二个数组应在索引 0 处返回 1，在索引 1 处返回 2，对所有其他索引返回 0。在索引 0 处调用select似乎证实了这一点：

Z3sat为两者返回。

正如预期的那样，Z3（如果重要的话，我在 linux-amd64 上使用 3.2 版）unsat在这种情况下回答。接下来，让我们比较这两个数组：

Z3 告诉我sat，我将其解释为“这两个数组比较相等”。但是，我希望这些数组不会比较相等。我基于 SMTLIB 阵列理论，它说：

因此，用简单的英语来说，这意味着“两个数组应该比较相等，当且仅当它们对于所有索引都相等”。有人可以向我解释一下吗？我是否遗漏了什么或误解了理论？如果您对这个问题有任何想法，我将不胜感激。

最好的问候，莱昂

[0] http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2 [1] http://smtlib.org

SMT2 标准（或它的 Z3 扩展）是否提供与 API 调用“check_assumptions”等效的命令？根据Josh Berdine的说法，使用保护文字和 check_assumptions 通常比使用 push-pop 作用域更快。但是，我现在坚持通过 stdio 使用 Z3，并且(check-assumoptions p)只使用 yield unsupported。

我正在使用 Z3 SMT 求解器来解决我在逻辑 QF_BV 中使用 SMTLIB 2 语言表达的问题。

该模型无法满足，我试图让求解器产生一个 unsat-core。

我的模型由几个“强制性”约束组成，我使用assert语句指定它们。

我想要考虑用于 unsat-core 生成的断言已使用(assert (! (EXPR) :named NAME))构造指定。

unsat正如预期的那样，Z3 给了我一个。然而，Z3 似乎总是转储一个由所有命名断言组成的“微不足道”的 unsat-core。

我知道存在我的命名断言的一个子集，它是一个 unsat-core。我使用 Yices SMT 求解器找到了这个核心，它经常给我相对较小的未饱和核心。Yices 模型与 Z3 模型相同（几乎是从 SMT2 到 Yices 输入语言的逐行翻译）。

产生“好”的 unsat 核心是求解器特有的功能，还是我可以做出任何通用的建议/更改来帮助 Z3 给我一个更好的核心？

在 Z3 的最后一个版本中，我没有得到 z3_dbg.dll。还发布吗？

亚历山大。

我想将公式中的所有嵌套量词拉到最外层。我希望以下命令可以在 Z3 中工作，但它们不能：

目的是:pull-nested-quantifiers什么？如何使用 SMT-LIB 或 Z3 API 提取嵌套量词？

是否可以序列化/反序列化 Z3 上下文（来自 C#）？如果没有，是否计划使用此功能？

我认为此功能对于现实世界的应用程序很重要。

对于这个基准：

我越来越：

这是一个已知的问题？（这是在 Linux 和 Mac 上使用 Z3 V3.2。）

带有量词的公式包含trans函数声明。Z3 成功找到模型并打印出来。但它也打印模型中未在模型中任何地方使用的函数trans!1!4464，如 ..。trans!7!4463它是什么？如何禁用此输出？

这是查询：http ://dl.dropbox.com/u/444947/asyn_arbiter_bound_16.smt2 ，这是 Z3 的输出 - http://dl.dropbox.com/u/444947/asyn_arbiter_bound_16_result.txt