Z3Pyライブラリ（Z3Pyライブラリを使用しています）を仮定して、エンジンの妥当性をチェックするのではなく、理論を証明するのと同じように、基礎理論と見なす方法がありますか？Z3またはZ3Pyの前提
たとえば、Real型の引数を持つ2つの単項関数があるとします。私はすべての入力値に対してf1（t）がf2（t）に等しいことをZ3エンジンに伝えたいと思います。
次のようになりますZ3Pyでエンコード：
トン=レアル（ "T"）
assumption1 =のForAll（T、F1（T）= F2（t）を）。
提示されたコードの問題は、私のアサーションセットがかなり大きく、私は量子を使っていることです（私はリアルタイムシステムの充足可能性を証明しようとしています）。上記のアサーションを他のアサーションのセットに追加すると、チェック手順は終了しません。
はい、これは説明のとおりですが、数値限定子になります。これはもちろん、より難しい問題を解決していることを意味し、Z3は異なる動作をします（完全に異なるソルバー多くのソースコードを共有していません）。
与えられた特定の例では、関数定義（ForAll x。f（x）= ...）の形をとっているので、安価に量限定子を取り除くことができます。つまり、fのすべての出現右辺を用いて数量化を行う。 Z3では、これはマクロファインダによって行われます。マクロファインダは、（マクロファインダという名前の）タクティックとして適用されます。または（他の人や直接的に暗黙のうちに）「smt」タクティックを使用している場合は、 smt.macro_finder = true。
私はZ3Pyライブラリを使用していますが、エンジンはその正当性をチェックしていませんが、理論を証明するのと同じようにそれらを基礎理論として捉えています。
実際、Z3に追加するすべてのアサーションは、前提と呼ぶものとして扱われます。 Z3はアサーションの充足可能性をチェックしますが、妥当性をチェックしません。数式Fの有効性をチェックするには、（Fではなく）アサートし、（Fではない）の充足可能性をチェックします。 （Fではない）がunsatの場合、Fは有効です。背景公理がある場合、基本的にBackground => Fの妥当性をチェックしているので、Background &（Fではない）の満足度をチェックすることができます。
クエリでZ3が終了するかどうかは、使用する理論と量子の組み合わせによって異なります。クエリーがより多くの機能を組み合わせるほど、より強くなります。 純粋な線形算術式または多項式実数演算式の場合、 これらはSMT-LIB分類（smtlib.orgを参照）でLRA、LIAおよびNRAと呼ばれます。Z3は最近追加された特殊な決定手順を使用します。