Я работаю с z3 python api. Когда я решаю ограничения с помощью z3 python api, решатель работает бесконечно, и никаких ошибок не возникает. Но когда одни и те же ограничения сбрасываются в виде формата smtlib2, а затем решаются с помощью исполняемого файла z3, он почти мгновенно дает sat или unsat. Дамп smtlib2 очень большой (около 1000 строк). Хотя при небольшом количестве ограничений z3 api работает нормально. Есть ли ошибка в z3 python api для обработки большого количества ограничений?
Разница в выводе, когда решатель smtlib2 вызывается через z3 python api и непосредственно из исполняемого файла?
Ответы (1)
Это может произойти, например, когда конфигурация между двумя методами отличается (даже незначительно) или когда проблемы не совсем идентичны (например, разный порядок ограничений). Некоторые тактики также недетерминированы (например, они используют таймеры при предварительной обработке), а исполняемый файл оказывается немного быстрее / медленнее. Чтобы диагностировать, что именно вызывает разницу, нам нужно увидеть некоторые из ваших проблем или, по крайней мере, некоторые диагностические данные, например, добавить -v: 10 в командную строку и установить глобальную опцию «многословность» на 10.
person
Christoph Wintersteiger
schedule
10.03.2016
Диагностический вывод из командной строки - pastebin.com/qCaBahqE Диагностический вывод из python api - pastebin.com/YpAf90vb
- person user2408329; 13.03.2016
Как видно из выходных данных, два прогона делают очень разные вещи. Например, у первого включен MBQI, а у другого нет (или настройки вывода были другими). Убедитесь, что вы установили правильное определение логики и / или используете правильную тактику или решатели.
- person Christoph Wintersteiger; 14.03.2016
