我正在 UFBV 查询上运行 Z3。目前查询包含2个调用check-sat。
如果我把push 1刚过check-sat，Z3在30秒内解决了查询。如果我不放任何push 1根本没有，因此有两个电话check-sat没有任何push 1他们之间，然后Z3在200秒内解决它。
有趣的。有什么具体原因还是只是巧合？
Z3 3.x拥有基于战术和战术的“策略规范语言”。我还没有“做广告”，因为它正在进行中。
基本思想在此描述幻灯片 http://research.microsoft.com/en-us/um/people/leonardo/cp2011.pdf。
我们针对每种逻辑都有不同的内置策略。这些策略通常不支持增量求解，因为它们可能会应用使用“封闭世界”假设的转换。例如，我们有将 0-1 线性整数算术映射到 SAT 的转换。每当 Z3 检测到用户“想要”增量求解（例如，多个check-sat命令，push&pop命令），它切换到通用求解器。在未来的版本中，我们将提供更多用于控制 Z3 行为的功能。
顺便说一句，如果你有两个连续的(check-sat) (check-sat)命令，Z3不一定进入增量模式。仅当存在时才会进入assert or push两个调用之间的命令。
现在，假设您的查询采用以下形式：(check-sat) <assertions> (check-sat)，您的第二个查询的形式为(check-sat) <assertions> (push) (check-sat)。在这两种情况下，Z3 在第二个时间点都将处于增量模式(check-sat)。但是，行为仍然不一样。增量求解器将断言公式“编译”为内部格式，并且如果push命令已执行。例如，仅当没有用户范围时，它才会使用更有效的二进制子句编码。通过用户范围，我的意思是，数量push命令 - 数量pop命令。这样做是因为更有效的编码中使用的数据结构没有有效的撤消/逆操作。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
