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

Question

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

• Это должно быть открытым источником
• Предоставить как низкоуровневый (API), так и высокий уровень взаимодействия (текстовых сценариев)
• Поддержка SMT-Lib
• Подходит (для использования) в инструментах / написано в / для языков как Java, Python, Ruby, Vala и нет Haskell.
• Имеет стабильные (пригодные для использования на практике) инструменты на основе него, как дизайн по контракту (DBC), проверки статического типа и т. Д.

Согласно домашней странице SMT-Lib (см. Bit.ly Builly для деталей) Список SMT Rolvers 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.

Answer 1

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

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

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

Answer 2

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

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

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

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