z3 - 部分割り当てを見つけるための Z3 タクティック

Question

変数 w、x、y、z を含む数式 F があるとします。

F の部分モデルを見つける Z3 の戦術はありますが、部分モデルには y と z の割り当てが含まれている必要があります。(w と x は気にしません。)

この戦術を適用することで、Z3 は完全なモデルを見つけるよりも部分的なモデルを見つけるのに費やす時間が短くなります。

そのような戦術は存在しますか？

Answer 1

それを行うための組み込みの戦術はありません。「ドントケア」の正確なセットを見つけるのは安くはありません。さらに、wとxが本当に「ドント ケア」である場合、それらは Z3 のパフォーマンスに大きな影響を与えるべきではありません。