z3 - 目标没有战术支持

Question

我有一些代码，我想在一些策略的帮助下检查它们。由于我有很多 if-then-else 语句，我想应用 elim-term-ite 策略。

我使用了以下策略

(check-sat-using(然后(!简化:arith-lhs true)elim-term-itesolve-eqs lia2pb pb2bv bit-blast sat))

但是，如果我将其错误为 - “目标位于 lia2pb 不支持的片段中”

那么，如果我尝试删除策略 lia2pb 及其旁边的策略，我会收到另一个错误，即 未知“不完整”。

我尝试删除除简化之外的所有策略，但我仍然会收到不完整错误。

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

Answer 1

使用lia2pb (又名线性整数算术到伪 bool 值)，所有整数变量都必须有界。也就是说，它们必须有一个下限和上限。

策略sat仅当输入目标不包含理论原子时才完整。也就是说，目标仅包含 bool 连接词和 bool 常量。如果情况并非如此，那么如果它无法显示(输入的 bool 抽象)目标不可满足，它将返回“未知”。

您可以要求Z3显示lia2pb的输入目标使用以下命令:

(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将替换绑定(bind)变量 x与 y + l_x ，其中y是一个新变量并且 l_x是 x 的下界。例如，在包含 3 <= x 的目标中, x替换为 y+3 ，其中y是一个新的新鲜变量。