Как мне получить Z3 для возврата минимальной модели?

Question

Если я даю Z3 формулу, такую ​​как p | q, я ожидал бы, что Z3 вернет p = true, q = не волнует (или с переключением p и q), но вместо этого он, похоже, настаивает на назначении значений как p, так и q (даже если у меня нет завершенного завершения при звонке Eval()). Кроме того, удивляясь этому, тогда мой вопрос заключается в том, что, если p и q не являются простыми опорами. vars, но дорогие выражения, и я знаю, что обычно p или q будут истинными. Есть ли простой способ попросить Z3 вернуть «минимальную» модель и не тратить время на попытки удовлетворить как p, так и q? Я уже пробовал MkITE, но это не имеет значения. Или мне нужно использовать какую-то тактику для обеспечения этого?

спасибо! PS. Я хотел добавить, что я отключил AUTO_CONFIG, но Z3 пытается назначить значения константам в обеих ветвях или: например, в фрагменте ниже. Я хочу, чтобы он назначал либо путь2_2, либо путь2_1 или путь2R_2 и path2R_1, но не оба

(or (and (select a!5 path2_2) a!6 (select a!5 path2_1) a!7) 
     (and (select a!5 path2R_2) a!8 (select a!5 path2R_1) a!9)) 

Answer 1

У Z3 есть функция, называемая распространением релевантности. Это описано в this article. Он делает то, что вы хотите. Обратите внимание, что в большинстве случаев распространение релевантности оказывает негативное влияние на производительность. В наших экспериментах это полезно только для задач, содержащих кванторы (рассуждение квантора настолько дорого, что оно окупается). По умолчанию Z3 будет использовать распространение релевантности в задачах, содержащих кванторы. В противном случае он не будет использовать его. Вот пример того, как включить его, когда проблема не имеет кванторов (пример также доступен онлайн here)

x, y = Bools('x y') 
s = Solver() 
s.set(auto_config=False, relevancy=2) 
s.add(Or(x, y)) 
print s.check() 
print s.model()