1

我有一些代码，我想通过一些策略来检查它们。由于我有很多if-then-else陈述，我想应用elim-term-ite策略。

我使用了以下策略

(check-sat-using (then (! simplify :arith-lhs true) elim-term-ite solve-eqs lia2pb pb2bv bit-blast sat))

但是，如果我对此有错误 -"goal is in a fragment unsupported by lia2pb"

因此，如果我尝试删除策略lia2pb和它们旁边的策略，我会收到另一个错误unknown "incomplete"。

我试图删除除 之外的所有策略simplify，但是我仍然会收到incomplete错误消息。

我应该尝试什么来帮助 sat 求解器解决问题？我应该尝试其他策略吗？

4

1 回答 1

2

要使用lia2pb（又名线性整数算术到伪布尔），所有整数变量都必须有界。也就是说，它们必须有一个下限和上限。

sat只有当输入目标不包含理论原子时，该策略才是完整的。也就是说，目标仅包含布尔连接词和布尔常量。如果不是这种情况，那么如果它不能显示（输入的布尔抽象）目标是不可满足的，它将返回“未知”。

lia2pb您可以使用以下命令让 Z3 显示输入目标：

(apply (then (! simplify :arith-lhs true) elim-term-ite solve-eqs)

如果您的某些公式包含无界整数变量，您可以构建一个尽可能减少到 SAT 的策略，否则调用通用求解器。这可以使用or-else组合器来完成。这是一个例子：

(check-sat-using (then (! simplify :arith-lhs true) elim-term-ite solve-eqs 
                       (or-else (then lia2pb pb2bv bit-blast sat)
                                smt)))

编辑：该策略lia2pb还假设每个有界整数变量的下限为零。在实践中这不是一个大问题，因为我们可以normalize-bounds在应用之前使用该策略lia2pb。该策略normalize-bounds将用 替换绑定变量x，y + l_x其中y是一个新变量，l_x是 x 的下限。例如，在包含 的目标中3 <= x，x被替换为y+3，其中y是一个新的新鲜变量。

于 2012-09-18T16:59:57.187 回答