目标不受战术支持 [英] Goal Unsupported by Tactic

问题描述

我有一些代码，我想借助一些策略进行检查.由于我有很多 if-then-else 语句，我想应用 elim-term-ite 策略.

I have some code, which I want to check with help of some tactics. Since I have lot of if-then-else statements, I want to apply elim-term-ite tactic.

我使用了以下策略

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

但是，如果我的错误是 - 目标位于 lia2pb 不支持的片段中"

However, if I an error with this as - "goal is in a fragment unsupported by lia2pb"

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

So then, if I try to remove the tactics lia2pb and the ones next to them, I get another error as unknown "incomplete".

我尝试删除除 simplify 之外的所有策略，但是我仍然会收到 incomplete 错误.

I tried to remove all the tactics except for the simplify, however I would still get an incomplete error.

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

What is that I should try to help the sat solver solve the problem? Should I try another tactics?

推荐答案

要使用 lia2pb(也就是伪布尔的线性整数算术)，所有整数变量都必须有界.也就是说，它们必须有下限和上限.

To use lia2pb (aka linear integer arithmetic to pseudo-boolean), all integer variables must be bounded. That is, they must have a lower and upper bound.

策略 sat 仅在输入目标不包含理论原子时才完整.也就是说，目标只包含布尔连接词和布尔常量.如果不是这种情况，那么如果它不能显示(输入的布尔抽象)目标是不可满足的，它将返回unknown".

The tactic sat is only complete if the input goal does not contain theory atoms. That is, the goal contains only Boolean connectives and Boolean constants. If that is not the case, then it will return "unknown" if it cannot show the (Boolean abstraction of the input) goal to be unsatisfiable.

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

You can ask Z3 to display the input goal for lia2pb by using the following command:

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

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

If some of your formulas contain unbounded integer variables, you can build a strategy that reduces to SAT when possible, and invokes a general purpose solver otherwise. This can be accomplished using the or-else combinator. Here is an example:

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

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

The tactic lia2pb also assumes that the lower bound of every bounded integer variable is zero. This is not a big problem in practice, since we can use the tactic normalize-bounds before applying lia2pb. The tactic normalize-bounds will replace a bound variable x with y + l_x, where y is a fresh variable and l_x is the lower bound for x. For example, in a goal containing 3 <= x, x is replaced with y+3, where y is a new fresh variable.

这篇关于目标不受战术支持的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！