私が理解している限り、Z3 は、量化された線形実数/有理数演算に遭遇すると、Bjørner、IJCAR 2010、および Bjørner と Monniaux による最近の研究で説明されている量指定子の除去の形式を適用します (qe_sat_tactic.cpp少なくとも、そう言っています)。
私は考えていた
「定数」がシンボリックであるという意味で、数式が多線形の場合でも機能するかどうか。例 ∀x, ax≤b ⇒ ax ≤ 0 は、a<0、a=0、a>0 の場合に分けて扱うことができます。これは Weispfenning の仮想置換アプローチを使用して可能ですが、Z3 で最終的に何が実装されたのか (つまり、一般的なアプローチを実装するのか、定数係数に制限されたアプローチを実装するのか) はわかりません。
Z3 で、1 つのモデルだけを解くのではなく、消去の結果を出力できるかどうか。そうするための Z3 戦術があるかもしれませんが、これがどのように要求されるのかわかりません。
Z3 で、上記のように消去を実行できるかどうか、次に、新しい非線形ソルバーを使用してモデルを取得します。繰り返しになりますが、一連の戦術でうまくいくかもしれませんが、これがどのように要求されるのかわかりません。
ありがとう。