数式を解くときにZ3にどこから始めるべきかを教えてください。

Question

私は現在、Z3に与えられたアサーションに多数の不等式と等価が含まれている状況を扱っています。それらは、等価で使用される変数に値を割り当てることによって式を解くことが最も効率的であるように、互いに依存している。

Z3のヒューリスティックスを変更して、ソルバがこれらの公式で常に「開始」するようにする方法はありますか？

私の推測では、最初に言及した同値を含む目標を処理する戦術を使用することでしょう。その後、他のアサーションを続行し、必要に応じてプロセス全体を再開します。

しかし、これを実装する方法がわかりません。式の集合からカスタム目標を作成するにはどうすればよいですか？

Answer 1

あなたが望む数式の最初のセットをアサートし、次にcheck-satを発行し、次のセットを発行してcheck-satを発行することができます。必要に応じて繰り返します。また、プッシュポップを使用して、必要に応じてこれらのポイントに戻ることもできます。

このように複数のチェック・サットを発行すると、ソルバーはあなたがその時点までアサートした数式を探索することになります。これが実際にあなたが望むものを実際に達成するかどうかは、数式がどのように見えるか、ソルバーが各check-sat呼び出しでどのくらい派生できるかによって決まります。