Можно ли клонировать Z3_context?

Question

Мне это нужно для пошагового решения в контексте символического исполнения (Кли). В точках разветвления символьных путей выполнения необходимо разбить решающий контекст на 2 части: с истинными и ложными условиями. Конечно, есть обходной путь - создать пустой контекст и воспроизвести все ограничения.

Есть ли способ разделить Z3_context? Планируете ли вы добавить такую ​​функциональность?

Примечание

разделения контекста можно избежать, если использовать символическое исследование в глубину, то есть исследовать текущий путь выполнения, пока он не достигнет "конца", и, следовательно, этот путь больше не будет исследоваться в будущем. В этом случае достаточно набрать pop , пока не будет достигнута точка ветвления, и продолжить исследовать другую ветвь условия. Но в случае Klee многие символические пути исследуются «одновременно» (исследование истинных и ложных ветвей чередуется), поэтому вам нужно решающее переключение контекстного решателя (в каждом методе есть аргумент Z3_context) и ветвление (для этого нет методов, это то что мне нужно).

Спасибо!

Answer 1

Нет, текущая версия Z3 (3.2) не поддерживает эту функцию. Мы понимаем, что это важная возможность, и эквивалентная функция будет доступна в следующем выпуске. Идея состоит в том, чтобы отделить понятия контекста и решателя. В следующем выпуске у нас будут API для создания (и копирования) решателей. Таким образом, вы сможете использовать разные решатели для каждой ветви поиска. В двух словах, Context используется для управления / создания выражений Z3, а Solver - для проверки их соответствия

Answer 2

Подход, который я сейчас использую для такого рода вещей, состоит в том, чтобы утверждать формулы типа p => A вместо A, где p - свежий булевский литерал.Затем в моем клиенте я поддерживаю связь между списком защитных литералов, которые соответствуют каждой ветви, и использую check_assumptions ().В моей ситуации мне удавалось оставить все формулы, выделенные во время каждого поиска, кроме YMMV.Даже для исследований глубины я, кажется, получаю гораздо больше пошагового повторного использования, чем при использовании push / pop.