Могу ли я получить условия пути от Pex в формате SMT 2?

Question

Могу ли я получить условия пути от Pex в формате SMT 2?

Я использую переменные окружения z3_logdir и z3_loglevel, чтобы Pex регистрировал условия пути в форматах файлов *.z3. Есть ли способ заставить pex экспортировать условия пути в формате SMT 2? или преобразовать формат файла.Z3 в SMT 2?

0

z3 pex

Источник

user1779039 25 июл '13 в 17:27

1 ответ

Решение

Другие вопросы по тегам z3 pex

user1096362 01 авг '13 в 19:18 2013-08-01 19:18 · Accepted Answer · 2013-08-01 19:18

Pex поставляется с DLL для Z3: Microsoft.Z3.dll. Это соответствует Z3 версии 2.5 (это можно загрузить с http://research.microsoft.com/en-us/um/redmond/projects/z3/old/older_z3.html). API в Z3 v 2.5 содержит поддержку синтаксического анализа файлов Z3 во внутреннем формате, и есть функции API для их вывода в SMT-LIB(1). Существует более новая версия Z3 и другие инструменты для преобразования тестов SMT-LIB1 в SMT-LIB2.