Как активировать частичный режим в Z3py?

Question

Я использую привязки Python в Z3, и мне любопытно, ускоряет ли частичный режим мою модель.Однако, кажется, нет способа сделать это в Python.(set_param(...), похоже, не имеет параметра для него)

Я подумал о переходе на pySMT , поскольку он утверждает, что поддерживает частичный режим для Z3, но я бы предпочел оставить Z3Py.

Дополнительный вопрос: будет ли мне полезен частичный режим? Я моделирую память компьютера в массивах и хочу, чтобы Z3 игнорировал записи, на которые никогда не ссылаются.

Answer 1

Вот как вы можете установить частичные модели:

from z3 import *

print get_param('model.partial')
set_param('model.partial', True)
print get_param('model.partial')

Это печатает:

false
true

По поводу вашего бонусного вопроса: я сомневаюсь, что частичные модели купят вам что-нибудь.Решатели SMT обычно находят модель в случае sat и затем завершают модель по мере необходимости.Часть «поиск модели» обычно является дорогостоящим действием, а не завершением модели.Но это, конечно, зависит от вашей конкретной проблемы;так что не мешало бы попробовать.