对于这个非线性整数算术示例,为什么 Z3 return 未知?

Why does Z3 return unknown for this nonlinear integer arithmetic example?

我有一个简单的非线性整数算术示例,即搜索毕达哥拉斯三元组。根据我在相关问题中阅读的内容(见下文),我希望 Z3 找到解决此问题的方法,但它 returns 'unknown'。这是 SMT-LIB v2 中的示例:

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(declare-fun xSquared () Int)
(declare-fun ySquared () Int)
(declare-fun zSquared () Int)
(declare-fun xSquaredPlusYSquared () Int)

(assert (= xSquared (* x x)))
(assert (= ySquared (* y y)))
(assert (= zSquared (* z z)))
(assert (= xSquaredPlusYSquared (+ xSquared ySquared)))

(assert (and (> x 0) (> y 0) (> z 0) (= xSquaredPlusYSquared zSquared)))

(check-sat)

(exit)

有几个相关问题,最值得注意的是:

除非变量的范围有限,否则 Z3 似乎不会尝试通过位爆破来寻找解决方案。将(check-sat)替换为以下命令即可找到解决方案:

(check-sat-using (then (using-params add-bounds :add-bound-lower -100 :add-bound-upper 100) smt))

或者,可以添加断言语句强制每个变量具有某个有限范围。