Я использую z3py. У меня есть предикат над двумя целыми числами, которые необходимо оценить с использованием пользовательского алгоритма. Я пытался реализовать его, но без особого успеха. По-видимому, мне нужно процедурное вложение, которое сейчас устарело. Может ли кто-нибудь сказать мне, как я могу реализовать это в z3py? Я понимаю, что это связано с использованием Тактики, но, боюсь, мне не удалось понять, как их использовать. Я бы тоже не возражал против использования устаревшего способа, пока он работает.
Процедурное вложение в Z3
Ответы (1)
Отсутствует тактика процессуального прикрепления. Все тактики реализованы внутри Z3; можно сочинять тактику извне. Предыдущие версии Z3 показали способ регистрации «пользовательской теории». Это устарело, поскольку (1) исходный код Z3 теперь доступен, поэтому пользователи могут напрямую компилировать свои собственные теории, (2) в абстракции пользовательской теории не было надлежащей поддержки для создания модели. Конечно, вы можете попробовать предыдущие версии Z3 с расширением теории пользователей, но оно не поддерживается.
person
Nikolaj Bjorner
schedule
13.01.2014
@nikolaj-bjorner Можно ли привести руководство для (1)?
- person Francesco Gramano; 02.07.2016
