1

ユーザー理論プラグインで、顧客の並べ替え "T" があり、T に " " を指定して関数 "f" を定義したとします。この関数Z3_func_declは、並べ替え T の引数を取り、並べ替え Int(" Z3_mk_int_sort" によって作成された並べ替え) を返します。返される Int 値には、他の制約もあります。

new_assignment検索では、いくつかのコールバック (またはコールバックなど)で Int 戻り値の具体的な値をキャプチャしてnew_eq、並べ替え T の引数値を解決するために追加のアサーションを作成できるようにしたいと考えています。しかし、問題は、それらのコールバックが呼び出されないことです。検索で。

Z3_contextSAT ソリューションの を調べました。理論演算では、次のことを見ました。

vars: v0 #24 lo: -oo, up: 4, value: 0, occs: 0, atom: 1, int , non-base , shared: 0, activity: 0, unassigned: 0, rel: 1, def: #24

"#24" が私の関数で、"up" に表示されている "4" が私の関数の戻り値の SAT 解です。

私の質問は、検索で値「4」を取得する方法です。のコールバックで #24 の等価クラスでそれを見つけようとしましたfinal_checkが、運がありませんでした。

ありがとう！

4

1 に答える 1

3

残念ながら、Z3 ではそれができません。理論は、他の理論で使用される内部データ構造にアクセスできません。理論は、共有される用語が等しい (等しくない) かどうかだけを知っています。この設計上の決定により、他に影響を与えることなく理論の実装を変更することができます。算数の理論が良い例です。現在の実装をより効率的な実装に置き換えます。新しい実装では、異なるデータ構造が使用されます。上記の例では、 loとupが term の既知の下限と上限#24です。4Z3 がの解釈として (上限) を選択するのは単なる偶然です#24。

また、現行バージョンの Z3 では、モデル構築は Z3 が満足できる問題を確立した後に開始されます。したがって、理論算術によって割り当てられた実際の解釈は、他の理論を助けるために実際に使用することはできません.

于 2012-07-09T18:13:26.600 に答える