Ограничения маркировки в Z3 Python API - PullRequest
Новая
       8

Ограничения маркировки в Z3 Python API

0 голосов
/ 11 мая 2018

Вопрос 1: Как я могу использовать Z3 Python API для добавления ограничений с уникальными метками? Я пытался что-то вроде:

... self.solver.add (self.vm [i]> = 0, 'labelIdx' + str (self.idx)) ...

где self.idx - целое число, которое увеличивается для каждого i, но я получаю:

z3.z3types.Z3Exception: ожидается True, False или логическое выражение Z3. Получил labelIdx0

Что означает, что аргументы add не могут быть строками.

Вопрос 2: Функция unsat_core () работает только с объектами Solver () или также с объектами Optimize (). Должен ли я установить какую-то опцию перед добавлением ограничений. Видимо, здесь [1] это процедура.

Спасибо!

[1] https://rise4fun.com/Z3/smtc_core

1 Ответ

0 голосов
/ 11 мая 2018

Для отслеживания ненасыщенных ядер вам необходимо использовать assert_and_track, см. Здесь: https://z3prover.github.io/api/html/classz3py_1_1_solver.html#ad1255f8f9ba8926bb04e1e2ab38c8c15

Оптимизация и ненасыщенные ядра работают , а не , к сожалению, работают вместе. Это было недавно поднято как проблема, см. Здесь: https://github.com/Z3Prover/z3/issues/1577. Как я понимаю, это не потому, что это не может быть поддержано, скорее они еще не реализовали это. Комментируя этот тикет, вы можете мотивировать их добавить поддержку!

...