2

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

http://gist.github.com/1232766

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

http://gist.github.com/1232769

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

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

谢谢..

4

1 回答 1

2

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

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

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

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

(select (table0 s65) t)并且用(table0 s65 t)where替换形式的每个术语t是一个任意术语。最后,您还必须(set-logic UFBV)在文件开头添加命令。使用此设置,我设法为您的查询生成 4 个不同的模型。我没有尝试产生更多。每个呼叫消耗大约 75 秒。

于 2011-09-21T20:26:16.403 回答