How do I get Z3 to return minimal model?

问题:

If I give Z3 a formula like p | q, I would expect Z3 to return p=true, q=don't care (or with p and q switched) but instead it seems to insist on assigning values to both p and q (even though I don't have completion turned on when calling Eval()). Besides being surprised at this, my question then is what if p and q are not simple prop. vars but expensive expressions and I know that typically either p or q will be true. Is there an easy way to ask Z3 to return a "minimal" model and not waste its time trying to satisfy both p and q? I already tried MkITE but that makes no difference. Or do i have to use some kind of tactic to enforce this?

thanks! PS. I wanted to add that I have turned off AUTO_CONFIG, yet Z3 is trying to assign values to constants in both branches of the or: eg in the snippet below I want it to assign either to path2_2 and path2_1 or to path2R_2 and path2R_1 but not both

   (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))

回答1:

Z3 has a feature called relevancy propagation. It is described in this article. It does what you want. Note that, in most cases relevancy propagation has a negative impact on performance. In our experiments, it is only useful for problems containing quantifiers (quantifier reasoning is so expensive that it is pays off). By default, Z3 will use relevancy propagation in problems that contain quantifiers. Otherwise, it will not use it. Here is an example on how to turn it on when the problem does not have quantifiers (the example is also available online 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()