Генерация минимального ненасыщенного ядра с использованием Z3 Python API

Question

Z3 поддерживает минимальное обнаружение ненасыщенного ядра со следующей опцией.

(set-option :smt.core.minimize true)

как задокументировано здесь .

В документации API упоминается только простое использование отслеживания ненасыщенных ядер. Есть ли способ достичь минимальное обнаружение несоответствующего ядра с помощью Z3 Python API.

Answer 1

Для этой цели вы используете функцию assert_and_track.См. https://github.com/Z3Prover/z3/blob/master/src/api/python/z3/z3.py#L6571-L6599, пример которого приведен в документации.Чтобы указать z3 свести к минимуму количество ядер, используйте:

s.set(':core.minimize', True)

Обратите внимание, что понятие «минимального» ненасыщенного ядра на самом деле не существует;так как у вас может быть два разных набора с одинаковым количеством элементов, оба из которых могут выступать в качестве основного ядра.И, насколько я знаю, z3 не дает никаких гарантий относительно «минимальности», кроме «наилучших усилий».

Также актуально: https://github.com/Z3Prover/z3/issues/888, где тактика и минимизация несоответствующего ядра не совсем хороши.с другими.