SMTソルバに関する新しい研究を行うことは、利用可能な問題が決定手続きに直接関係しない多くのトリックと前処理技術を必要とすることから、何度も妨げられています。これらはしばしば未公開であるか、適切に実装し最適化するのに時間がかかります。さらに、さまざまなソルバーの比較と理解が非常に困難になります。問題を前処理するためにZ3を使用できますか？
Z3は問題を起こし、前処理された形式（z3自体が問題を解決するために使用する形式）でダンプするプリプロセッサとして使用できますか？
私はコマンドラインオプションが表示されませんが、これを達成するための方法、戦略、Pythonインターフェイス、さらには余分なコードを書く方法があると思います。
はい、Z3はプリプロセッサとして使用できます。コマンドapplyを使用すると、ユーザーは戦術を適用してSMT 2.0のベンチマークとしてダンプすることができます。ここで（http://rise4fun.com/Z3/eutOでオンラインも入手可能）の例である：上記の例で
(declare-const x Real)
(declare-const y Real)
(assert (forall ((n Real)) (or (< x n) (< n y))))
(assert (= (< x y) (< x 100.0)))
(apply (then qe nnf) :print false :print-benchmark true)
、QE（記号消去）とNNF（否定正規形）戦術は、入力問題に適用されています。
いくつかの追加のポイント：
いくつかの戦術だけequisatisfiable結果を生成します。したがって、得られたベンチマークのモデルは、元の式のモデルである必要はありません。 Z3に関連する「モデルコンバータ」（オプション:print-model-converter true）をダンプするよう依頼することができます。モデル変換器は、Z3によって使用されるステップを符号化して、結果の式のモデルを元の式のモデルに変換する。しかし、モデルコンバーターを印刷する標準はなく、Z3はこれらの記述を読み取ることができません。もちろん、プログラムAPIを使用してすべてを結合することもできます。
戦術の小さなセットは、（飽和結果のみが信頼できる）または近似値（信頼できない結果のみが信頼できる）近似を生成します。それらは、通常、モデル発見または証拠発見に使用されます。 Z3が結果のゴールを表示すると、結果は正確に通知されます（satとunsatは信頼できる）。