Z3：更好的建模方式？答案

【问题标题】：Z3: A better way to model?Z3：更好的建模方式？
【发布时间】：2011-09-21 17:51:22
【问题描述】：

我有两个 SMT 问题实例。第一个在这里：

http://gist.github.com/1232766

Z3 在我不太好的机器上大约 2 分钟后返回了一个模型，这很棒。我也有这个：

http://gist.github.com/1232769

我已经在这个问题上运行了 z3，但 Z3 没有完成。如果您检查这些文件的内容，您会看到第二个与第一个相同，只是它有一个额外的断言来“拒绝”第一个实例返回的模型。（你可以在它们之间做一个“差异”来了解我的意思。）我碰巧知道这个问题有多个令人满意的模型，我正在尝试使用 z3 来找到所有令人满意的模型。

我知道这可能完全在意料之中，但我很想知道为什么与第一个相比，第二个对 Z3 来说是一个更棘手的问题。有没有更好的方法来制定第二个问题，让 Z3 更轻松？

谢谢..

【问题讨论】：

标签： z3

【解决方案1】：

如果不了解您的应用程序，很难给您一个准确的答案。正如您所建议的，建模在您使用的逻辑中起着重要作用：AUFBV。 Z3采用的策略对整体性能也有很大影响。 Z3 配备了多种内置策略。它有许多可用于影响搜索的参数。 Z3 还有一种策略规范语言。这是一个新功能。我没有宣传它，因为它正在进行中，并且语言很可能会在下一个版本中发生变化。您可以通过执行以下命令访问有关策略语言的更多信息：

(help check-sat-using)
(help-strategy)

话虽如此，Z3 中有一个内置策略似乎对您的问题有效。这是用于逻辑UFBV 的策略。您的问题使用数组，但可以通过将 table0 转换为具有两个参数的函数来避免它们：

(declare-fun table0 ((_ BitVec 64) (_ BitVec 64)) (_ BitVec 8))

并用(table0 s65 t) 替换(select (table0 s65) t) 形式的每个术语，其中t 是任意术语。最后，您还必须在文件开头添加命令(set-logic UFBV)。使用此设置，我设法为您的查询生成 4 个不同的模型。我并没有试图产生更多。每次通话耗时约 75 秒。

【讨论】：

谢谢，切换到 v3.2 并使用 AUFBV 有所帮助。我现在看到大约。每分钟一个解决方案，这是相当不错的。顺便说一句，有没有更好的方法来连续生成“所有”令人满意的模型？到目前为止，我一直在解析第一个模型的结果并生成一个新程序来添加约束以拒绝原始模型，并为每个新模型重新启动 Z3。如果有办法说(get-next-model) 或类似的方式会更好，Z3 将返回不同的模型（如果存在）。
我们没有get-next-model 之类的命令。但是，可以使用 C API 自动执行此功能。顺便说一句，我相信 Philippe Suter (lara.epfl.ch/~psuter) 实现了这个功能。