Z3 Python Mod Int 问题

Question

我想使用 Z3 打印小于 20 的素数。以下程序打印 2、3、5 和 7，但不打印 11、13、17 或 19。

尽管 isPrime(11)、isPrime(13)、isPrime(17) 或 isPrime(19) 在我的测试中都令人满意，但知道哪里出了问题。

from z3 import *
def isPrime(x):
    y = Int('y')
    return And(x > 1, Not(Exists(y, And(y < x, 1 < y, x % y == 0))))

s = Solver()

x = Int('x')
s.add(isPrime(x))
s.add(x < 20)

while s.check() == sat:
    ans = s.model()[x]
    print(ans)
    s.add(x != ans)

Answer 1

你的程序对我来说工作得很好，输出：

2
3
19
5
17
11
7
13

20以下的所有素数

也许您有旧版本的 z3？

$ z3 --version
Z3 version 4.10.2 - 64 bit

如果是这种情况，请尝试升级。

请注意，对于大素数，z3（或任何其他 SMT 求解器）将 not 通常有效地寻找素数。但是对于这个问题，它的有界大小使得完全解决问题成为可能。