Ищете практические примеры использования SMT Z3 (например, DbC) и альтернативы Z3 с открытым исходным кодом?

Я заинтересовался и ищу практические примеры использования SMT Z3 (например, DbC) с кодом и альтернативами с открытым исходным кодом для этого инструмента. Так что, на самом деле, меня интересуют аналогичные инструменты формального решения Z3, но:

  • это должно быть с открытым исходным кодом
  • обеспечить как низкоуровневое (API), так и высокоуровневое (Text Script) взаимодействие
  • поддержка SMT-LIB
  • пригодный (пригодный для использования) в инструментах / написанный на / для языков как Java, python, ruby, Vala, а не Haskell
  • основанные на нем стабильные (практичные) инструменты, такие как проектирование по контракту (DbC), статическая проверка типов и т. д.

Согласно домашней странице SMT-LIB (подробности см. В пакете bit.ly) список решателей SMT 2010 года: "Alt-Ergo, Barcelogic, Beaver, Boolector, CVC3, DPT, MathSAT, OpenSMT, SatEEn, Spear, STP, SWORD, UCLID, VeriT, Yices, Z3."

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

Наконец, любая информация по сравнению ее с возможностями GHC была бы полезной, но только в случае, если есть пример реализации (не языковая "особенность").

Более быстрая информация о Z3 здесь http://bit.ly/bundles/ewiger/1

Источник

2 ответа

Решение

Насколько мне известно, CVC3 наиболее соответствует вашим требованиям в том, что он:

  1. Имеет набор функций, который похож на Z3.
  2. Имеет лицензию в стиле BSD
  3. Является основным решением для ряда существующих проектов.

CVC3 имеет привязки для C++ и Java и, возможно, других языков. В общем, я думаю, что API гораздо сложнее в использовании, чем (текстовый) язык ввода. Это дает дополнительное преимущество: если вы придерживаетесь языка SMT-LIB2, вы можете позже переключиться на другой инструмент, если это станет необходимым. Большая выборка примеров доступна на веб-сайте SMT-LIB.

Источник

Вы спрашивали об альтернативах с открытым исходным кодом для Z3:

Согласно SMT-Wikipedia на 2011-08, у нас есть:

Исходя из этих мер, представляется, что наиболее яркими, хорошо организованными проектами являются OpenSMT, STP и CVC4.

Я просто проверяю это - пока все три кажется разумным, плюс старый CVC -> я имею в виду CVC3.

Источник
Другие вопросы по тегам