Z3 prime numbers

Question

我正在尝试学习Z3，这是我编写的第一个程序。

在此练习中，我试图确定x是否是素数。如果X是Prime，则返回SAT，否则，将返回UNSAT与其两个因素一起返回。

这是我到目前为止的http://rise4fun.com/z3/stlx

我的问题是我不认为代码现在正在做任何事情。它返回我做什么。即，如果我断言7是Prime，它将返回SAT，如果我断言7不是Prime，则返回SAT。

我不确定递归如何在Z3中起作用，但是我已经看到了一些示例，我试图模仿他们如何进行递归。

如果你们能够看一看并指示我出错的地方，我将非常感谢。

Answer 1

以下公式无法实现您的评论指定的内容：

; 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是免费的。他们以前被宣布为常数。您的评论说，您想递归地调用鸿沟，将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 2

我习惯于递归思考，在篡改几个小时后，我找到了另一种实施方法。对于任何有兴趣的人，这是我的实施。

http://rise4fun.com/z3/1mifn

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)))))))

让我多于我承认正确的。