失败的 qfnra-nlsat 阻止了其他策略？

Question

使用 Z3 4.4.1 或 master，以下输入给出 unknown：

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)

(assert (and (> x 0) (< x 10)))
(assert (and (> y 0) (< y 10)))
(assert (and (> z 0) (< z 10)))
(assert (= (* z z) (+ (* x x) (* y y))))

(check-sat-using (or-else qfnra-nlsat smt))

如果我调换qfnra-nlsat和smt策略的顺序，那么Z3就会returnsat，这才是正确的解法。它现在的工作方式，我基本上被迫在策略的最后使用 qfnra-nlsat 。但是，这对我来说不是最佳选择。

以上行为是错误吗？似乎 qfnra-nlsat 对模型留下了一些不需要的更改，而我希望如果 qfnra-nlsat 失败，模型将保持不变。

Answer 1

试试看

     (check-sat-using (and-then qfnra-nlsat smt))

这很微妙： qfnra-nlsat 策略无法确定公式是否可满足，因为公式使用整数（并且模型 qfnra-nlsat 找到了实数的解）。因此，它充当空操作并产生与它相同的子目标。 or-else 列表中第一个没有抛出异常的策略成为决定结果的策略。所以 qfnra-nlsat 决定不能降低目标。

通过使用 and-then，您基本上是在使用第一个 qfnra-nlsat 来降低目标。如果成功，它要么不产生子目标，要么产生一个公式为 "false" 的子目标。 smt 策略知道如何处理这些情况，其中可以非常有效地处理 sat 和 unsat 情况。

还有其他选择。特别是，如果你想使用 or-else 作为一些更大的备选方案的一部分，方法是：

 (check-sat-using (or-else (and-then qfnra-nlsat fail) (and-then smt fail)))

如果 qfnra-nlsat 创建了非真非假子目标，则会导致失败。然后在失败时应用 smt 策略。

失败的 qfnra-nlsat 阻止了其他策略？

Failed qfnra-nlsat prevents other tactics?

z3