Как измерить размер формулы в Z3?
Я работаю в Z3 с очень большими формулами, поэтому не могу их проанализировать (действительно, печатать их сложно). Поэтому я хотел бы провести высокоуровневый анализ, используя инструменты, которые могут быть в Z3.
Конкретно, считайте, что у меня есть формула phi и я ее выполняю simplify(phi). Есть ли способ измерить размер обеих формул? Конечно, есть разные понятия о размере, но есть ли встроенный? По сути, я хочу знать, изменило ли применение simplify(phi) формулу (поскольку я знаю, что использование simplify(phi) ничего не гарантирует [1,2]).
[1] Как упростить Or(Not(y), And(y, Not(x))) до Or(Not(y), Not(x)) с помощью Z3? [2] Упрощение с помощью Z3 не настолько упрощает, как ожидалось
Похоже, стандартного метода не существует. Большое спасибо!!
Ответы 1
Возможно, зонды — это то, что вы ищете.
Зонды позволяют проверять различные меры, связанные с целью в Z3, и реализуется множество различных типов мер по достижению целей. [1]
Предполагая, что вы взаимодействуете с Z3 через API Python, вы можете получить список доступных зондов с помощью команды:
describe_probes()
Вот пример использования зондов в Z3py:
from z3 import *
probe = Probe('num-exprs')
A, B = Bools('A B')
phi = Or(And(A, B), And(A, B))
phi_simple = simplify(phi)
print(probe(phi))
print(probe(phi_simple))
[1] https://microsoft.github.io/z3guide/docs/strategies/probes/
Это интересная идея. Однако в документации предполагается, что проверки применяются к целям, а не к выражениям. Я не уверен, что на самом деле происходит, когда вы используете его так, как вы это делали выше. Возможно, он поступает правильно? И опять же, решает ли это исходный вопрос, остается открытым. Но определенно стоит изучить. Отличная находка!
Привет! Большое спасибо за ответ. В вашем примере это, кажется, работает (результат 4 в phi, тогда как 2 в phi_simple), однако я проверил это на некоторых других примерах и получил очень странные результаты: иногда упрощенный вариант больше исходного. Сейчас я не могу показать пример этого, но могу вам сказать, что я пробовал с другим зондом ('memory'), и он точно такой же, как в оригинальном, так и в упрощенном варианте. Есть ли у вас какие-либо идеи, почему это происходит? Еще раз спасибо!
Цель – это совокупность утверждений. Заглянув в исходный код Z3, я нашел файл src/tactic/probe.cpp, который объясняет, как датчики работают внутри. Проверка «памяти», кажется, возвращает выделенную память z3 независимо от цели, поэтому я думаю, поэтому в обоих случаях она одинакова. «Размер» зонда, похоже, возвращает количество формул, составляющих цель. Зонд «num-exprs», похоже, возвращает соответствующее количество выражений конкретной цели и, похоже, выполняет рекурсивный подсчет каждой формулы, составляющей цель.
Большое спасибо! Тогда есть ли у вас какое-либо представление о том, почему упрощенное фи будет иметь большее количество «num-exprs», чем исходное?
Я думаю, что разница заключается в том, как создается цель. Давайте возьмем в качестве примера формулу A and B and C с логическими переменными A,B,C: у нас будет size = 3, поскольку цель представляет собой объединение трех переменных, и num-exprs = 3, поскольку каждая подформула цели имеет размер 1 (только переменная). В A or B or C у нас будет size = 1, поскольку это соединение только одной формулы, и num-exprs = 5, поскольку оно учитывает 2 выражения для операторов и 3 для переменных. Как подсчитывается «число-выражение» для каждой формулы в цели, описано в файле src/ast/for_each_expr.cpp#L23
Хм... Я могу понять, что size=1 в одном случае и size=3 в другом (из-за цели), но разве num-exprs не должно быть одинаковым в обоих случаях? Я имею в виду, что в обоих случаях у нас есть выражения 2 для операторов (and и or) и 3 для переменных... или это тот случай, когда and не рассматривается как оператор, потому что он скорее является «сочетанием/для целей»? еще раз спасибо
Это именно тот случай, поскольку and — это конъюнктура целей, то три цели будут соответственно A, B и C, теперь мы считаем выражения трёх целей отдельно и суммируем их, но так как есть только переменные, то сумма будет быть 1 + 1 + 1 = 3. Именно поэтому оператор and в данном случае не учитывается при подсчете.
Мне неизвестны какие-либо доступные метрики по умолчанию. Вы можете рассматривать формулу как дерево и подсчитывать количество узлов, ширину и глубину; рассчитать максимальную ширину любого уровня или любой их комбинации. Вопрос в том, будут ли какие-либо из этих показателей полезны. Единственный способ выяснить это — попробовать, поскольку я думаю, что ответ будет зависеть от конкретного приложения. (В stackoverflow.com/a/69966273/936310 есть скелетный код, с которого вы можете начать обход формулы.)