2

次のコードがあるとします。

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」は同じ変数を操作しますか?

4

1 に答える 1

4

ホスト言語C++に存在するプログラミング変数 x論理変数を混同しているようで、Z3が理由を説明しています。および両方とも論理変数を表し、制約に追加することで Z3 に事実を与え、制約が満たされないようにします。y abxyax && !ya && !a

于 2013-06-21T07:59:11.703 に答える