#z3 #z3py
Вопрос:
Я использую API Python Z3, и у меня есть следующий код для получения неудовлетворительных ядер:
for idx, constr in enumerate(z3constrs): solver.assert_and_track(constr, f'tracker{idx}') Однако решение модели содержит переменные отслеживания:
gt;gt;gt; print(solver.model()) [tracker71 = True, tracker229 = True, rect11_x1 = 35, ...] Есть ли какой-либо способ удалить эти переменные из решения (сохраняя его ModelRef объектом), не запуская решатель дважды?
Ответ №1:
Короткий ответ: Нет. Эти переменные являются частью модели, и поэтому их присутствие важно при использовании solver.model() результата в других вызовах, таких как m.evaluate(expr) . Таким образом, вы не можете «игнорировать» их, сохраняя при этом результат в виде ModelRef .
Но вы можете задать вопрос, зачем вам нужен результат, чтобы быть ModelRef в этом случае? Устраняя переменные-трекеры, вы нарушаете внутренние инварианты о том, как строятся модели. Если ваша задача состоит в том, чтобы просто не отображать их в модели или передавать структуру данных, содержащую все, кроме трекеров, то обычно нужно просто создать список пар и использовать его вместо этого. Вот пример:
from z3 import * a = Int('a') s = Solver() s.assert_and_track(a gt; 3, 'tracker1') s.check() m = s.model() clean_m = [] for d in m.decls(): if not(d.name().startswith("tracker")): clean_m = [(d, m[d])] print(m) print(clean_m) Это печатает:
[tracker1 = True, a = 4] [(a, 4)] Очевидно, что вы можете дополнительно обработать результаты, чтобы придать им любую форму, какую захотите.