Z3 Python Mod Int Проблема
Я хочу печатать простые числа ниже 20, используя Z3. Следующая программа печатает 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)
Ответы 1
Используя z3 версии 4.10.2, ваша программа отлично работает для меня, выводя:
2
3
19
5
17
11
7
13
которые являются всеми простыми числами меньше 20.
Возможно у вас установлена другая версия?
Обратите внимание, что z3 (или любой другой решатель SMT) не будет эффективен при поиске простых чисел в целом для больших простых чисел. Но для этой задачи ее ограниченный размер позволяет решить задачу полностью. Однако я не удивлюсь, если это изменится в следующем выпуске или даже в следующей сборке: такого рода проблемы просто не подходят для решения с помощью SMT-решателя; и вы, скорее всего, получите unknown в качестве ответа, или решатель будет бесконечно зацикливаться.
Спасибо за ответ. Оказалось у меня Z3 версия старая. Да согласен z3 не подходит для нахождения больших простых чисел, иначе Криптографии может и не быть. ' ./bin/z3 --version Z3 версия 4.5.1 — 64-битная