2つのZ3変数に同じ名前を付けることはできないという事実に頼る必要があります。ていることを確認してのものであると、私が使ってきたtuple_example1（）からtest_capi.cでZ3 /例/ Cをしてから、元のコードを変更します：
// some code before that ...
x = mk_real_var(ctx, "x");
y = mk_real_var(ctx, "y"); // originally y is called "y"
// some code after that ...
に：
// some code before that ...
x = mk_real_var(ctx, "x");
y = mk_real_var(ctx, "x"); // but now both x and y are called "x"
// some code after that ...
そして（予想通り）出力は次のように変更されました：
tuple_example1
tuple_sort: (real, real)
prove: get_x(mk_pair(x, y)) = 1 implies x = 1
valid
disprove: get_x(mk_pair(x, y)) = 1 implies y = 1
invalid
counterexample:
y -> 0.0
x -> 1.0
に：
tuple_example1
tuple_sort: (real, real)
prove: get_x(mk_pair(x, y)) = 1 implies x = 1
valid
disprove: get_x(mk_pair(x, y)) = 1 implies y = 1
valid
BUG: unexpected result.
しかし、よく見ると、Z3は実際には失敗したわけではなく、コンソールに出力された単純な（ドライバー）だけであることがわかりました。そこで、私は先に進んで、yを「x」と呼ばれるintソートとして、まったく同じテストを作成しました。驚いたことに、Z3は、種類が異なる場合に、同じ名前の2つの変数を処理できました。
tuple_example1
tuple_sort: (real, real)
prove: get_x(mk_pair(x, y)) = 1 implies x = 1
valid
disprove: get_x(mk_pair(x, y)) = 1 implies y = 1
invalid
counterexample:
x -> 1.0
x -> 0
それは本当に何が起こっているのですか？それとも単なる偶然ですか？どんな助けでも大歓迎です、ありがとう！
一般に、SMT-Libは、種類が異なる限り、変数名の繰り返しを許可します。標準の27ページを参照してください。特に、それは言う：
具体的には、変数は任意のシンボルにすることができ、関数シンボルは任意の識別子（つまり、シンボルまたはインデックス付きシンボル）にすることができます。結果として、識別子が変数として扱われるのか関数シンボルとして扱われるのかを知るために、解析中にコンテキスト情報が必要になります。変数の場合、この情報は、変数を導入する唯一のメカニズムである3つのバインダーによって提供されます。対照的に、関数シンボルは、後で説明するように事前定義されています。すべての関数シンボルfは、1つ以上のランクに個別に関連付けられており、それぞれがfの引数と結果の種類を指定していることを思い出してください。ソートチェックを簡素化するために、用語内の関数シンボルに、その結果ソートσの1つで注釈を付けることができます。このような注釈付き関数記号は、形式の修飾された識別子です（fσとして）。
また、同じドキュメントの31ページで、「あいまいさ」をさらに明確にしています。
一致式のパターンを除いて、用語内のあいまいな関数記号fのすべての出現は、形式の修飾された識別子として出現する必要があります（fσとして）。ここで、σはその出現の意図された出力ソートです。
したがって、SMT-Lib用語では、次のように記述します。
(declare-fun x () Int)
(declare-fun x () Real)
(assert (= (as x Real) 2.5))
(assert (= (as x Int) 2))
(check-sat)
(get-model)
これにより、次のものが生成されます。
sat
(model
(define-fun x () Int
2)
(define-fun x () Real
(/ 5.0 2.0))
)
Cインターフェースで観察しているのは、本質的に同じもののレンダリングです。もちろん、SMT-LibはC APIや他の言語のAPIについて何も述べていないため、インターフェイスによってどの程度の「チェック」が実施されるかは、完全にソルバー固有です。これは、実際にBUGそこの出力に表示される行を説明しています。この時点で、動作は完全にソルバー固有です。
しかし、簡単に言うと、SMT-Libでは、種類が異なる限り、2つの変数に同じ名前を使用することができます。
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加