問題タブ [smt]

境界のあるコンテキスト (つまり、すべての基本的な並べ替えはビットベクトル) では、(2-dim) セットを配列としてモデル化します。一部の公理では、この配列を量化する必要があります。このような公理を含めると、ソルバーは不明を返します。構文の観点からは、この種の量指定子は の範囲を超えていますがFOL、ソルバーが境界付けられたコンテキスト情報を認識/使用できることを期待しています。

1. ソルバーが境界付けられたコンテキスト情報を使用しないのはなぜですか?
2. これをソルバーに教える可能性はありますか?

最小限の例を次に示します。

私が理解している限り、Z3 は、量化された線形実数/有理数演算に遭遇すると、Bjørner、IJCAR 2010、および Bjørner と Monniaux による最近の研究で説明されている量指定子の除去の形式を適用します (qe_sat_tactic.cpp少なくとも、そう言っています)。

私は考えていた

1. 「定数」がシンボリックであるという意味で、数式が多線形の場合でも機能するかどうか。例 ∀x, ax≤b ⇒ ax ≤ 0 は、a<0、a=0、a>0 の場合に分けて扱うことができます。これは Weispfenning の仮想置換アプローチを使用して可能ですが、Z3 で最終的に何が実装されたのか (つまり、一般的なアプローチを実装するのか、定数係数に制限されたアプローチを実装するのか) はわかりません。

2. Z3 で、1 つのモデルだけを解くのではなく、消去の結果を出力できるかどうか。そうするための Z3 戦術があるかもしれませんが、これがどのように要求されるのかわかりません。

3. Z3 で、上記のように消去を実行できるかどうか、次に、新しい非線形ソルバーを使用してモデルを取得します。繰り返しになりますが、一連の戦術でうまくいくかもしれませんが、これがどのように要求されるのかわかりません。

ありがとう。

SMTLIB インターフェイスを使用して、Z3 の集合 (和集合、交差など) の理論を定義しようとしています。残念ながら、私の現在の定義では単純なクエリで z3 がハングするため、簡単なオプション/フラグがいくつか欠けていると思います。

パーマリンクはこちら: http://rise4fun.com/Z3/JomY

私が欠けているものについてのヒントはありますか？

また、私が言えることから、集合演算の標準的な SMT-LIB2 エンコーディングはありませんZ3.mk_set_{add,del,empty,...} (これが、量指定子を介してその機能を取得しようとしている理由です)。それとも別のルートがありますか？

ありがとう！

ランジット。

私がやろうとしているのは、すべてのベクトルに行き、各ビットで異なることをすることです。

define-fun LT....私が知りたいのは、私が forall (in )でうまくやっているかどうかです。

結果が予想と一致しないため: S

このリンクにあるコード: http://rise4fun.com/Z3/xrFK

Z3 で次の統計を取得します。

各結果行に使用された指標を知りたいです。

手伝って頂けますか？

Z3 の Python API を使用して量指定子の削除を実行するにはどうすればよいですか? チュートリアルとAPIを確認しましたが、どうにかできませんでした。

存在量指定子を含む式があり、この量指定子が削除されるように、Z3 に新しい式を提供してもらいたいです。私は本質的にこれと同じことをしたい:

Z3で変数を非表示にする方法

ただし、Python インターフェイスを使用します。また、私の式は線形演算です。

ありがとう！

追加: 量指定子の削除を行った後、量指定子のない式を別の式に「追加」します。したがって、戦術を利用する場合、サブゴール (戦術の出力) を線形演算の式に変換する方法はありますか?