Z3のユニークな変数名

Question

2つのZ3変数 がでなく、が同じ名前であるという事実に頼る必要があります。 は 、その確かに私はz3/examples/cにtest_capi.cからtuple_example1()を使用してから、元のコードを変更しました：

// 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 ... 

と、（予想通り）出力はから変更：

// 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 ... 

へ：

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 

が本当に何が起こっているということですか？それともちょうど偶然でしょうか？ ご協力いただきありがとうございます！

Answer 1

一般に、SMT-Libは、異なるソートを持つ限り、繰り返しのある変数名を許可します。 the standardの27ページを参照してください。特に、それは言う：

機能シンボル は任意の識別子（すなわち、シンボル又はシンボルインデックス付き）であってもよいしながら具体的には、変数は、任意のシンボルであることができます。結果として、 のように、識別子が変数または関数として扱われるかどうかを理解するために、構文解析中に文脈情報が必要です シンボル。変数の場合、この情報は変数を導入する唯一のメカニズムである3つのバインダーによって提供されます。対照的に、機能 は、あらかじめ定義されています（後で説明します）。 各関数シンボルfは、1つ以上の ランクに個別に関連付けられ、それぞれがfの引数と結果のソートを指定することを思い出してください。 にソートチェックを簡略化するために、用語内の関数シンボルには、その結果のソートσの1つを持つ という注釈を付けることができます。そのような注釈付き機能記号は、形式の修飾識別子（fσとして） です。また

thusly同じ文書、それをさらに明確化「曖昧」の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つの変数に同じ名前の変数を使用できます。