无法解释简单的调整如何导致"unknown" Z3结果

Question

我正在学习Z3。我正在使用一些简单的"isPrime"函数，偶然发现了一些难以理解的行为。一个看似"更简单"的内联公式，(> q 1)，导致"未知"，而一个更"复杂"的定义乐趣（宏），(isPrime q)，导致快速解决方案，即使(isPrime q)包含(> q 1)。http://rise4fun.com/Z3/slg2D。

(define-fun isPrime ((x Int)) Bool
  (and (> x 1) (not (exists ((z Int) (y Int)) (and (not (= y x)) (and (not (= z x)) (and (> y 1) (> z 1) (= x (* y z)))))))))
(declare-const q Int)
(declare-const r Int)
(assert (and
  ;with this the '+ 2' variation is sat: 5, 3
  ;(isPrime q)
  (> q 1)
  (> r 1)
  ;always answers sat: 2, 2
  ;(isPrime (+ (* q r) 1))
  ;unknown
  (isPrime (+ (* q r) 2))
))
(check-sat)
(get-model)

Answer 1

量化逻辑是一种高级功能，您应该阅读 Z3 如何解决这些公式，这将使您了解您可以从 Z3 中获得什么。根据我拙见的经验，用量词求解公式是一门微妙的艺术。对你来说显而易见的事情，对 Z3 来说可能并不明显。

你有一个 Z3 将尝试满足的forall量词（你把它写成 not exists ）。我猜 Z3 正在挑选一些q和r然后检查isPrime是否成立，否则它会尝试使用新对，依此类推。如果 Z3 没有做出正确的选择，可能需要一段时间才能找到这样的q和r，所以也许你应该给它更多的时间（在rise4fun上解决问题有一个超时）。

另一种方法可能是帮助 Z3 更多一点。例如，让它知道z和y小于 x 。这样，您就可以为这些变量提供下限和上限。

(define-fun isPrime ((x Int)) Bool
   (and (> x 1) (not (exists ((z Int) (y Int)) (and (< y x) (and (< z x) (and (> y 1) (> z 1) (= x (* y z)))))))))

这对我有用。

更新

引用：

1. 莱昂纳多·德·莫拉关于2012年SAT/SMT暑期学校的演讲（https://es-static.fbk.eu/events/satsmtschool12/）
2. Z3 教程，量词 （http://rise4fun.com/Z3/tutorial/guide）
3. 通用 Z3 教程 （http://research.microsoft.com/en-us/um/redmond/projects/z3/mbqi-tutorial/main.html）