使用正确的策略加速 z3-solver答案

【问题标题】：Speed z3-solver up with right tactics使用正确的策略加速 z3-solver
【发布时间】：2013-09-16 15:04:14
【问题描述】：

我创建了大约 20k 个约束，在我的机器上解决它们大约需要 3 分钟。我有不同类型的约束，下面我给出例子并解释它们。我将断言上传到http://filebin.ca/vKcV1gvuGG3。

我有兴趣解决更大的约束系统，因此我想加快这个过程。我想问一下您是否对如何更快地解决它们有建议，例如通过使用适当的策略。从关于策略的教程中我知道了策略，但我似乎没有通过应用策略获得积极的差异......

li 是树的标签。第一种类型对标签的值进行了限制。标签值通常介于 10-20 个不同的值之间。

Or(l6 == 11, Or(l6 == 0, l6 == 1, l6 == 2, l6 == 3, l6 == 4,
      l6 == 5, l6 == 6, l6 == 7, l6 == 8, l6 == 9, l6 == 10))

第二种类型将不同的标签相互关联。

Implies(l12 == 0, Or(l10 == 2, l10 == 5, l10 == 7, l10 == 8, l10 == 10,
           False, False))

第三种类型定义和关联函数f: Int --> Int（或f: BitVector --> BitVector，不完整），其中bound_{s, v}只是一个函数名，n是一个节点的ID。目标是找到对函数bound 的满意分配。

Implies(And(bound_s_v (18) >= 0, l18 == 0),
        And(bound_s_v (19) >= 0,
            bound_s_v (19) >=
            bound_s_v (18),
            bound_s_v (26) >= 0,
            bound_s_v (26) >=
            bound_s_v (18)))

最后一种类型确定是否需要绑定 (>= 0) 或不需要 (== -1, )

Or(bound_s'_v'(0) >= 0, bound_s'_v'(0) == -1)

还有一个要求，即对于某些初始状态，需要绑定：

`bound_s0_v0(0) >= 0`

exutable 文件的描述：在前 2-3 行脚本启动求解器，导入 z3 并在最后一行调用 print s.check()

【问题讨论】：

您发布的文件被截断。我们无法执行它。声明丢失。比如不包含l6等的声明
感谢您的评论！我现在使文件可执行。

标签： z3 z3py

【解决方案1】：

大概，您可以尝试使用求解器“qflia”，因为我在您的逻辑中看不到量词。

编辑：

我尝试了“qflia”，但它并没有让它更快。也许，您也应该尝试其他求解器。

【讨论】：