логика — Где узнать об API для проверки теорем z3 для c ++?
Я хочу изучить API-интерфейсы z3 для c ++ и узнать, как их использовать в программе на c ++. Я пытался найти учебник, но не смог.
Где я могу это узнать? Любой учебник или что-то?
Благодарю.
Решение
Дистрибутив Z3 содержит пример API Z3 C ++.
Пример расположен по адресу examples/c++/example.cpp, Вы также можете найти его в Интернете Вот.
Z3 C ++ API — это просто тонкий слой поверх Z3 C API. Он в основном предоставляет интеллектуальные указатели для управления объектами Z3 и перегружает операторы, чтобы упростить создание выражений. Вы можете найти документацию по этим API Вот.
Замечание: гораздо проще изучить API Z3 с помощью Python. Учебник по Z3 на основе Python доступен Вот.
Другие решения
Других решений пока нет …