Использовать разные решатели в Z3
Я использую интерфейс Z3 Python для создания формул для моих экспериментов. Затем я отправляю эту формулу решателю Z3. Если я прав, Z3 использует свой собственный решатель!
Как использовать другой SAT/SMT решатель с Z3py?
Способ, который я использую для этого в CBMC (средство проверки ограниченной модели C): Запустите программу и добавьте промежуточное представление DIMAC (в файл), а затем используйте этот файл в качестве входных данных для других решателей SAT. Могу ли я сделать подобные вещи в Z3. Спасибо.
2 ответа
Похоже, вы действительно должны использовать решающий SMT-интерфейс, а не Z3py. Было несколько попыток создать такие интерфейсы с различной степенью поддержки нескольких решателей:
https://github.com/pysmt/pysmt - независимый от Solver API Python для решателей SMT. Я не использовал его сам, но это звучит многообещающе, особенно если вы хотите, чтобы Python был вашим API верхнего уровня.
https://github.com/sosy-lab/java-smt - аналогичный проект, в котором в качестве основного языка используется Java.
http://leventerkok.github.io/sbv/ - моя собственная попытка предоставить независимый от Solver API для использования SMT-решателей, этот написан на Haskell.
Это ни в коем случае не исчерпывающий список. Я уверен, что есть и другие, на разных языках, с разной степенью зрелости. Какой из них выбрать, действительно зависит от предпочтений вашего основного языка и функций, предоставляемых каждой системой; которые могут широко варьироваться.
Все решатели SMT поддерживают формат ввода SMT2, так что вы можете сделать то же самое с Z3 и другими решателями SMT. Z3py может преобразовывать объекты Solver и Goal в строки, совместимые с SMT2 (некоторые сложные объявления переменных, например, некоторые типы данных могут отсутствовать).
Z3py - это специфичный для Z3 API (как видно из названия), он не предоставляет возможности использовать другие решатели SMT.