Блог

В настоящее время у меня есть несколько поверхностное понимание того, как работают решатели SMT (основы алгоритмов, таких как электронное сопоставление, MBQI и индуктивные рассуждения CVC4/5). Однако очень неприятно отлаживать методом проб и ошибок.

Есть ли какие-либо рекомендации по отладке сценариев SMT, в которых широко используются кванторы?

1. Плохо написанный сценарий часто переходит в бесконечный цикл, но я не могу сказать, моя ли это ошибка, или просто требуется слишком много времени, чтобы ответить.
2. Решатели SMT, как правило, скрывают внутренние устройства от пользователей, поэтому довольно сложно понять, почему они застряли. Есть ли какой-нибудь способ распечатать «контекст решения»?

Или, может быть, я неправильно использую решатели SMT? Я должен разработать свой собственный алгоритм проверки, используя только SMT-решатели для локальных решений?

Любая помощь будет признательна!

Это очень субъективный вопрос, и в значительной степени основанный на мнении. Но пара общих замечаний:

• Не программируйте напрямую в SMTLib. Он не предназначен для потребления человеком. Вместо этого используйте API более высокого уровня и создавайте сценарии на языке, с которым вы более знакомы. Существуют привязки, доступные на любом количестве языков, включая C/C /Java/Python/O’Caml/Haskell/Scala и т.д. Просто сделав это, вы избавитесь от большинства мирских ошибок, которые вы совершаете.
• Включите вывод детализации решателя. Возможно, вы сможете заметить закономерности в выводе журнала. К сожалению, это очень специфично для решателя, и его может быть трудно расшифровать; но также может указывать, например, на то, что вы застряли в цикле электронного сопоставления в присутствии кванторов.
• Если для вашей задачи проверки существует собственный алгоритм (тройки Хоара, логика разделения, абстрактная интерпретация и т. Д.), вам сначала нужно применить эти методы и делегировать локальные/под-леммы решателю SMT. Не ожидайте, что решатель SMT сможет выполнять большие доказательства и все, что требует реальной индукции из коробки.
• Попробуйте уменьшить сложность, введя чрезмерные ограничения, и посмотрите, какие из них помогут. Основываясь на ваших выводах, вы могли бы выполнить разбиение на случаи, например, если избыточные ограничения перечисляют достаточно небольшое пространство для поиска.

Опять же, это очень общие замечания, и можно только догадываться, будут ли они применимы к вашей конкретной проблеме. Но я бы начал с программирования в API более высокого уровня, если вы еще этого не делаете.