查找部分任務的Z3策略

Question

假設我有一個包含變量w，x，y，z的公式F.

Z3是否有任何策略可以找到F的部分模型，但是部分模型必須包含y和z的賦值。 （我不在乎w和x）。

通過應用這種策略，Z3花費的時間少於查找完整模型的部分模型。

有沒有這樣的策略存在？

Answer 1

這樣做沒有內置的策略。 找到「不關心」的確切集合並不便宜。 此外，如果w和x真的「不在乎」，那麼它們不應該以顯着的方式影響Z3的性能。