Z3 で仮定を表現する方法はありますか (私は Z3Py ライブラリを使用しています)、エンジンがそれらの有効性をチェックせず、定理の証明のように、それらを基礎となる理論として採用するようにしますか?
たとえば、Real 型の引数を持つ 2 つの単項関数があるとします。すべての入力値について、f1(t) が f2(t) と等しいことを Z3 エンジンに伝えたいと思います。
次のような Z3Py でエンコードされます:
t = Real("t"
)
提示されたコードの問題は、アサーション セットが非常に大きく、量指定子を使用していることです (リアルタイム システムの充足可能性を証明しようとしています)。上記のアサーションを他のアサーションのセットに追加すると、チェック手順が終了しません。
はい、それはあなたが説明したとおりに可能ですが、量指定子になってしまいます。これはもちろん、より難しい問題を解決していることを意味し、Z3 は異なる動作をします (最終的に、完全に異なるソルバーを使用することになる可能性があります。多くのソース コードを共有することさえできます)。
与えられた特定の例では、関数定義 (ForAll x . f(x) = ...) の形式を持っているため、量指定子を安価に削除できます。つまり、f のすべての出現箇所を右手で置き換えることができます。 side であり、量指定子は自明に満たされます。Z3 では、これはマクロ ファインダーによって行われます。マクロ ファインダーは、戦術 (「macro-finder」という名前) として適用されるか、「smt」戦術を使用している場合 (暗黙的に他のものを介して、または直接)、設定できます。 smt.macro_finder=真。