我创建了大约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 ）（ >= 0 ，）
Or(bound_s'_v'(0) >= 0, bound_s'_v'(0) == -1)
此外，还要求对于某些初始状态，需要绑定：
`bound_s0_v0(0) >= 0`
Description of the exutable file: 在前2-3行中，脚本启动求解器，导入z3，在最后一行中调用 print s.check()
1 回答
Presumbaly，你可以尝试使用求解器'qflia'，因为我的逻辑中没有看到量词 .
Edit:
我试过'qflia'，但它并没有让它更快 . 也许，你也应该尝试其他求解器 .