z3 - 在使用和不使用推送调用的情况下对 UFBV 上的 Z3 进行增量调用

Question

我正在 UFBV 查询上运行 Z3。当前查询包含 2 个调用 check-sat。如果我将 push 1 放在 check-sat 之后，Z3 将在 30 秒内解决查询。如果我根本不放置任何 push 1 ，因此有两个调用 check-sat 之间没有任何 push 1 ，那么 Z3 解决200秒内完成。有趣的。有什么具体原因还是只是巧合？

Answer 1

Z3 3.x拥有基于战术和战术的“策略规范语言”。我还没有“做广告”，因为它正在进行中。基本思想在slide deck中有描述。 。我们针对每种逻辑都有不同的内置策略。这些策略通常不支持增量求解，因为它们可能会应用使用“封闭世界”假设的转换。例如，我们有将 0-1 线性整数算术映射到 SAT 的转换。每当 Z3 检测到用户“想要”增量求解(例如，多个 check-sat 命令、push 和 pop 命令)时，它就会切换到通用求解器。在未来的版本中，我们将提供更多用于控制 Z3 行为的功能。

顺便说一句，如果您有两个连续的 (check-sat) (check-sat)命令，Z3不一定进入增量模式。仅当有 assert 时才会进入或push两个调用之间的命令。

现在，假设您的查询采用以下形式:(check-sat) <assertions> (check-sat) ，您的第二个查询的形式为 (check-sat) <assertions> (push) (check-sat) 。在这两种情况下，Z3 在第二个 (check-sat) 时都将处于增量模式。 。但是，行为仍然不一样。增量求解器将断言公式“编译”为内部格式，并且如果 push 则其行为会受到影响。命令已执行。例如，仅当没有用户范围时，它才会使用更有效的二进制子句编码。通过用户范围，我的意思是 push 的数量命令 - 数量 pop命令。这样做是因为更有效的编码中使用的数据结构没有有效的撤消/逆操作。