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

Question

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

• он должен быть открытым исходным кодом
• обеспечивает как низкий уровень (API) и высокий уровень (текст сценарии) взаимодействия
поддержка
• SMT-LIB
• подходит (использовать) в инструментах/написанными в/для языков, как Java, Python, Ruby, Вала и не Haskell
• имеет стабильные (используемые на практике) инструменты, основанные на нем, как дизайн по контракту (DbC), проверка статического типа и т. д.

По SMT-LIB домашней страницы (см bit.ly свертка для деталей) список 2010 SMT решателей: «Alt-Ergo, Barcelogic, Beaver, Boolector, CVC3, ДПТ, MathSAT, OpenSMT, сатин, Копье, STP, SWORD, UCLID, veriT, Yices, Z3. "

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

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

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

Answer 1

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

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

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

Answer 2

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

Согласно SMT-Wikipedia в 2011-08, мы имеем:

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

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