Z3素数

Question

我正在努力学习z3，这是我写的第一个程序。

在本练习中，我将尝试确定x是否为质数。如果x是质数，则返回SAT，否则返回UNSAT及其两个因数。

这是我到目前为止所拥有的http://rise4fun.com/Z3/STlX

我的问题是，我认为代码现在什么也做不了。无论我做什么，它都会返回SAT。也就是说，如果我断言7是质数，它返回SAT，如果我断言7不是质数，它返回SAT。

我不确定z3中的递归是如何工作的，但我看过一些示例，并尝试模仿它们是如何进行递归的。

如果你们能够看一看，并告诉我哪里错了，我会非常感激的。

Answer 1

我非常习惯递归地思考，在篡改了几个小时之后，我找到了另一种方法来实现它。对于任何感兴趣的人，这里是我的实现。

http://rise4fun.com/Z3/1miFN

Answer 2

以下公式不能达到您的注释指定的效果：

; recursively call divides on y++ 
;; as long as y < x
;; Change later to y < sqrt(x)
(declare-fun hasFactors (Int Int) Bool)
(assert
   (and (and (not (divides x y)) 
      (not (hasFactors x (+ y 1)))) (< y x))
)

第一个问题是x，y是自由的。它们在之前被声明为常量。你的注释说你想递归地调用divides，递增y直到它达到x。你可以使用量化的公式来指定一个满足这个属性的关系。你必须写一些类似这样的东西：

   (assert (forall ((x Int) (y Int)) (iff (hasFactors x y) (and (< y x) (or (divides y x) (hasFactors x (+ y 1))))))

在调用check-sat.之前，您还必须指定要检查的公式。使用SMT求解器查找质数当然不实用，但将演示Z3实例化量词时的一些行为，这取决于问题域和编码可能很快，也可能非常昂贵。

Answer 3

感谢你的部分解决方案！isPrime的完整解决方案是：

http://rise4fun.com/Z3/jBr0

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

花了我更多的时间去承认它是正确的。