CODEWITHSUNDEEP
z3
Wei-Fan Chiang
Wei-Fan Chiang

Reputation: 273

Z3 tactic for finding partial assignment

Suppose that I have a formula F which contains variables w, x, y, z.

Is there any tactic of Z3 that finds a partial model of F, but the partial model must contains assignments for y and z. (I don't care w and x.)

By applying this tactic, Z3 spends less time for finding the partial model than finding a full model.

Is there such tactic exists?

Upvotes: 1

Views: 185

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

There is no built-in tactic for doing that. It is not cheap to find the precise set of "don't cares". Moreover, if w and x are really "don't cares", then they should not affect Z3's performance in a significant way.

Upvotes: 1

Related Questions