#z3 #smt
#z3 #smt
Вопрос:
Я только что загрузил тесты для сортировки seq и регулярных выражений (используя z3-4.3.2). В чем может быть проблема, когда я получаю неизвестный результат после запуска «membership_1.smt2»?
Я не указал никаких дополнительных параметров командной строки. Согласно тесту, это должно привести к sat, но unknown печатается без какой-либо модели.
Спасибо
Редактировать:
Далее я заметил, что «перезапуск» не распознается. Связано ли это с версией z3 или вы просто забыли параметр командной строки?
Комментарии:
1. Вы правы, команда «перезапустить» не распознана, и команда «повторно объединить» тоже не распознана.
Ответ №1:
Во-первых, я не знаю, где OP или комментатор нашли пример ввода «membership_1.smt2». Я проверил тесты SMT-LIB и источник Z3, S3 и Z3-str и не смог его найти.
В любом случае, проблема заключалась в том, что OP тестировал бенчмарк, написанный либо для S3, либо для Z3-str, и запускал его с неизмененной версией Z3. S3 и Z3-str требуют модифицированной версии Z3 для обработки этих расширений. Это описано на веб-сайте S3 [S3: решатель символьных строк для анализа веб-безопасности,http://www.comp.nus.edu.sg /~ trinhmt/ S3/, доступ 4 августа 2016]:
Модифицированная версия решателя Z3
- Исходный код модифицированного Z3 доступен здесь.
- Мы модифицируем Z3, чтобы обеспечить взаимодействие между теорией струн и теорией арифметики.
Эти недавно добавленные методы API позволяют нам запрашивать длину строковой переменной и взаимосвязь между длиной различных строковых переменных, как показано в нашей статье CCS’14.
Наша модифицированная версия Z3 также используется Z3-str GROUP для интеграции теории целых чисел / струн.
Повторное использование (неизмененного) исходного кода Z3 не показывает совпадений для «повторного запуска» или «повторного объединения». Повторное использование модифицированной версии показывает, что эти нажатия определены в lib/seq_decl_plugin.cpp of z3-source-060115.zip .