目标没有战术支持

我有一些代码，我想在一些策略的帮助下检查它们。因为我有很多if-then-else声明，我要申请elim-term-ite tactic.

我使用了以下策略

(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 error.

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

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

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

您可以要求 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)))

EDIT:战术lia2pb还假设每个有界整数变量的下界为零。这在实践中并不是一个大问题，因为我们可以使用这个策略normalize-bounds申请之前lia2pb。战术normalize-bounds将替换绑定变量x with y + l_x, where y是一个新变量并且l_x是 x 的下界。例如，在包含以下内容的目标中3 <= x, x被替换为y+3, where y是一个新的新鲜变量。