次のコードがあるとします。
context c;
solver s(c);
expr x=c.bool_const("a");
expr y=c.bool_const("a");
expr z=c.bool_const("b");
s.add(x&&!y);
std::cout<<s.check();
s.reset();
s.add(x&&!z);
std::cout<<s.check();
上記のコードの実行結果は「unsat sat」です。結果は、z3 が x と y を同じ変数と見なしていることを示しています。z3 は変数を名前で区別しますか? また、同じ変数を別の場所で使用する場合、次のようにコードを記述できますか。
context c;
solver(s);
function test1(){
s.add(c.bool_const("a"));
}
function test2(){
s.add(!c.bool_const("a"));
}
関数「test1」と「test2」は同じ変数を操作しますか?