Печать внутренних решающих формул в z3

Question

Инструмент доказательства теорем z3 занимает много времени, чтобы решить формулу, с которой, я думаю, она сможет легко справиться. Чтобы лучше понять это и, возможно, оптимизировать мой ввод в z3, я хотел увидеть внутренние ограничения, которые z3 генерирует как часть процесса решения. Как напечатать формулу, которую z3 создает для своих решателей на стороне сервера при использовании z3 из командной строки?

Answer 1

У инструмента командной строки Z3 такой опции нет. Кроме того, Z3 содержит несколько решателей и этапов предварительной обработки. Неясно, какой шаг будет полезен для вас. Исходный код Z3 доступен по адресу https://github.com/Z3Prover/z3. Когда Z3 компилируется в режиме отладки, он предоставляет дополнительную опцию командной строки -tr:<tag>, Эта опция может использоваться для выборочного вывода информации. Например, исходный файл nlsat_solver.cpp содержит следующую инструкцию:

TRACE("nlsat", tout << "starting search...\n"; display(tout); 
               tout << "\nvar order:\n"; 
               display_vars(tout););

Опция командной строки -tr:nlsat даст команду Z3 выполнить указанную выше инструкцию. tout поток вывода трассировки Будет храниться в файле .z3-trace, Источник Z3 полон этих TRACE команды. Поскольку код доступен, мы также можем добавить наши собственные команды трассировки в код.

Если вы опубликуете свой пример, я могу рассказать вам, какие компоненты Z3 используются для предварительной обработки и ее решения. Затем мы можем выбрать, какие "теги" мы должны включить для отслеживания.

РЕДАКТИРОВАТЬ (после публикации ограничений): Ваш пример в смешанной целочисленной и действительной нелинейной арифметике. Новый нелинейный арифметический решатель (nlsat) в Z3 не поддерживает to_int, Таким образом, универсальный решатель Z3 используется для решения вашей проблемы. Хотя этот решатель принимает почти все, он не является полным для нелинейной вещественной арифметики. Нелинейная поддержка этого решателя основана на: интервальном анализе и вычислениях Гробнера. Этот решатель реализован в папке src/smt (в нестабильной ветке). Арифметический модуль реализован в файлах theory_arith*, Хорошая опция командной строки трассировки -tr:after_reduce, Он будет отображать набор ограничений после предварительной обработки. Узким местом является арифметический модуль (theory_arith*).

Дополнительные замечания:

• Проблема в неразрешимом фрагменте: смешанная целая и вещественная нелинейная арифметика. То есть для этого фрагмента невозможно написать звуковой и полный решатель. Конечно, мы можем написать решатель, который решает случаи, которые мы находим на практике. Я считаю, что это возможно продлить nlsat обращаться с to_int,

• Если вы избегаете to_int, вы сможете использовать nlsat, Задача будет в нелинейном вещественном арифметическом фрагменте. Я понимаю, что это может быть трудно, так как to_int кажется ключевым моментом в вашей кодировке.

• Код в "нестабильной" ветке на z3.codeplex.com гораздо лучше организован, чем официальная версия в "основной" ветке. Я скоро сливаю его с веткой "master". Вы можете получить "нестабильную" ветку, если хотите поиграть с исходным кодом.

• "Нестабильная" ветвь использует новую систему сборки. Вы можете создать версию выпуска с поддержкой трассировки. Вам просто нужно использовать опцию -t при создании Makefile.

скрипты Python /mk_make.py -t

• Когда Z3 компилируется в режиме отладки, опция AUTO_CONFIG=false по умолчанию. Таким образом, чтобы воспроизвести поведение режима "релиз", необходимо указать параметр командной строки AUTO_CONFIG=true,