使用和不使用推送调用在 UFBV 上对 Z3 的增量调用 [英] Incremental calls to Z3 on UFBV with and without push calls
问题描述
我在 UFBV 查询上运行 Z3.当前查询包含 2 个调用 check-sat.如果我把 push 1 放在 check-sat 之后，Z3 会在 30 秒内解决查询.如果我根本不放任何 push 1，因此有两次调用 check-sat 没有任何 push 1 之间，那么 Z3 解决它在 200 秒内.有趣的.有什么具体原因还是只是巧合?
I am running Z3 on UFBV queries. Currently the query contains 2 calls check-sat.
If I put push 1 just after check-sat, Z3 solves the query in 30sec. If I don't put any push 1 at all, thus have two calls check-sat without any push 1 between them, then Z3 solves it in 200sec.
Interesting. Any specific reasons or just a coincidence?
推荐答案
Z3 3.x 有一个基于战术和战术的战略规范语言".我还没有做广告"，因为它正在进行中.此幻灯片中描述了基本思想.我们对每种逻辑都有不同的内置策略.这些策略通常不支持增量求解，因为它们可能应用使用封闭世界"假设的转换.例如，我们有将 0-1 线性整数算法映射到 SAT 的转换.每当 Z3 检测到用户想要"增量求解(例如，多个 check-sat 命令、push&pop 命令)，它就会切换到通用求解器.在未来的版本中，我们将提供更多的功能来控制 Z3 的行为.
Z3 3.x has a "strategy specification language" based on tactics and tacticals. I'm not "advertising" that yet because it is working in progress.
The basic idea is described in this slide deck.
We have a different built-in strategy for each logic. The strategies usually do not support incremental solving, because they may apply transformations that use a "closed-world" assumption. Example, we have transformations that map 0-1 linear integer arithmetic into SAT. Whenever Z3 detects that the user "wants" incremental solving (e.g., multiple check-sat commands, push&pop commands), it switches to a general purpose solver. In future versions, we will provide more features for controlling Z3 behavior.
顺便说一句，如果您有两个连续的 (check-sat) (check-sat) 命令，Z3 不一定会进入增量模式.仅当两次调用之间存在 assert 或 push 命令时才会进入.
BTW, if you have two consecutive (check-sat) (check-sat) commands, Z3 not necessarily enters in incremental mode. It will enter only if there is an assert or push command between the two calls.
现在，假设您的查询采用以下形式:(check-sat) ，第二个查询的格式为 (check-sat) .在这两种情况下，Z3 将在第二个 (check-sat) 中处于增量模式.但是，行为仍然不一样.增量求解器将断言的公式编译"为内部格式，如果执行了 push 命令，它的行为会受到影响.例如，仅当没有用户范围时，它才会使用更有效的二进制子句编码.对于用户范围，我的意思是 push 命令的数量 - pop 命令的数量.这样做是因为在更有效的编码中使用的数据结构没有有效的撤消/逆操作.
Now, suppose your query is of the form: (check-sat) <assertions> (check-sat), and your second query is of the form (check-sat) <assertions> (push) (check-sat). In both cases, Z3 will be in incremental mode in the second (check-sat). However, the behavior is still not the same. The incremental solver "compiles" the asserted formulas to an internal format, and its behavior is affected if a push command has been executed. For example, it will use a more efficient encoding of binary clauses only if there is no user scope. By user scope, I mean, the number of push commands - number of pop commands. It does that because the data-structure used in the more efficient encoding does not have an efficient undo/inverse operation.
这篇关于使用和不使用推送调用在 UFBV 上对 Z3 的增量调用的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
