z3 :: tacticとz3 :: goalの目的

Question

目標を作成して戦術に追加し、戦術からソルバーを作成することができます。

単純にz3 :: solverインスタンスを作成し、それに式を追加することより、このアプローチの利点は何ですか？

Answer 1

戦術は異なる目的を持っています。アサーション/制約を含むゴールを作成し、ゴールの上でTacticを実行すると、その結果が新しい（アサーション/制約）目標の新しいセットになります。ソルバーは充足可能性を判断し、新しい（副）目標を生成しません。

戦術をソルバーに変換して、得られたソルバーが戦術を実行するようにすることができます。結果が決定的（些細な/不満）の場合、結果を返します。戦術によって生成された副目標が決定的でない場合、「未知」を返す。