Комментарии 9
Автор - большой молодец! За Why3 ничего не расскажете?@ymnспс
А кто-нибудь когда-нибудь видел истории успеха использования SMT-решателей на реальных задачах? А не вот на этих игрушках. Я пару раз пытался использовать z3 в задачах на коллизии к очень плохим алгоритмам хеширования, и они просто зависали на проверке выполнимости. Или, во всяком случае, оказывалось быстрее придумать, накодить и дождаться вывода алгоритма с частичным перебором под конкретную задачу, чем ждать пока ее решит солвер (и хрен его знает, вывел бы он какой-нибудь разультат за еще пару часов, или пришлось бы ждать 10^30 лет).
Интересно. Можете показать код? Есть ли в ваших формулах кванторы?
Увы, нет. Это было больше 5 лет назад. Я тогда только узнал про SMT-решатели, и подумал, вот здорово, можно ж руками ничего не делать, оно само. Оказалось, что нет. С тех пор я немного переквалифицировался и новых задач, для которых мог бы пригодиться солвер, у меня не было.
Но, насколько я помню, проблемы там начнутся даже если вы захотите с помощью решателя просто инвертировать матрицу над кольцом вычетов, начиная с очень малых значений размерности матрицы. Понятно, что это можно и без всяких решателей сделать, но просто как пример очень простой задачи, которую оно не осилит. (Один из тех хешей как раз какие-то упоротые операции над матрицами делал)
Challenge accepted! Попробую инвертировать матрицу над кольцом вычетов, напишу если получится.
Набросал программу: https://github.com/vzhn/z3-inv-matrix. Действительно, матрицы 3x3 считаются достаточно бодро, но для 5x5 я уже не дождался ответа. Скорее всего дело в операции mod, с ней теория арифметики перестает быть линейной, что делает задачу трудной для z3. Есть такой ответ на SO: https://stackoverflow.com/a/66785785.
Да, например, широко используется в статическом анализе кода для проверки сходимости путей выполнения
А кто-нибудь когда-нибудь видел истории успеха использования SMT-решателей на реальных задачах?
Например "Checking Firewall Equivalence with Z3" и "Using Z3 Theorem Prover to analyze RBAC", "Semantic-based Automated Reasoning for AWS Access Policies using SMT".
Парсим строки с SMT-решателем