Z3 простых чисел

Я пытаюсь изучить z3, и это первая программа, которую я пишу.Z3 простых чисел

В этом упражнении я пытаюсь определить, является ли x простым. Если x является простым, верните SAT, иначе возвратите UNSAT вместе с двумя его факторами.

Вот то, что я до сих пор http://rise4fun.com/Z3/STlX

Моя проблема, я не думаю, что код делает что-нибудь прямо сейчас. Он возвращает SAT для всех, что я делаю. Если я утверждаю, что 7 является простым, он возвращает SAT, если я утверждаю, что 7 не является простым, он возвращает SAT.

Я не уверен, как рекурсия работает в z3, но я видел несколько примеров, и я попытался имитировать, как они сделали рекурсию.

Если вы, ребята, можете взглянуть и наставить мне, где я ошибся, я был бы очень благодарен.

источник

2014-01-23 zsawaf

Пожалуйста, добавьте код к вашему вопросу. Ссылки могут сломаться, и ваш вопрос потеряет некоторую ценность. –

Следующая формула не достичь того, что ваш комментарий указывает:

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

Первая проблема заключается в том, что х, у свободны. Они объявляются как константы раньше. Ваш комментарий говорит, что вы хотите рекурсивно называть делит, увеличивая y до достижения x. Вы можете использовать количественные формулы для определения отношения, которое удовлетворяет этому свойству. Вы должны написать что-то вдоль линий:

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

Вы также должны указать, какие формулы, которые Вы хотите проверить перед вызовом регистрация сат. Поиск простых чисел с использованием решателя SMT, конечно, не будет практичным, но проиллюстрирует некоторые из поведения, которое вы получите, когда Z3 создает кванторы, которые зависят от в проблемной области и могут быть быстрыми или очень дорогими.

источник

2014-01-23 18:04:42

Привет, спасибо, что нашли время, чтобы ответить. я удалил постоянные заявления, я думал, что вы должны были объявить их, вроде как C. Я попытался с помощью ForAll квантора, как уже говорилось выше, однако теперь я продолжаю получать таймаут :( ли у вас есть опыт работы с этим до? http://rise4fun.com/Z3/iQpl – zsawaf

Я так привык к мысли рекурсивно, после того, как несколько часов вмешался, я нашел другой способ его реализовать. Для всех, кто интересуется, вот моя реализация.

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

источник

2014-01-23 22:42:37 zsawaf

BTW, в вашей реализации 'isPrime (n)' на самом деле означает, что '' n' не является простым '. –

Ха-ха-ха да! Я испортил соглашение об именах, но в целом он работал нормально :) Я понимаю, как теперь z3 работает лучше.Благодарим за помощь. – zsawaf

Пожалуйста, включите код в свой ответ. Ссылки могут сломаться, и ваш вопрос потеряет всякую ценность. –

Спасибо за частичное решение! Комплексное решение для 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)))))))

Взял меня больше, чем я хочу признать, чтобы получить это право.

источник

2016-02-26 14:03:31

Z3 простых чисел

ответ

Смежные вопросы