CODEWITHSUNDEEP
z3
Dingbao Xie
Dingbao Xie

Reputation: 736

Does z3 distinguish variables by their names?

Suppose we have the following code:

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();

The executing result of above code is 'unsat sat'; The result shows that z3 regards x and y as the same variable. Does z3 distinguish variables by their names? And if I use the same variable in different places, can I write the code as following:

context c;
solver(s);

function test1(){
   s.add(c.bool_const("a"));
}
function test2(){
   s.add(!c.bool_const("a"));
}

Dose the function 'test1' and 'test2" manipulate the same variable?

Upvotes: 2

Views: 374

Answers (1)

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

You seem to confuse the programming variables x and y that exist in the host language C++ with logical variables a and b that Z3 reasons about. x and y both represent the logical variable a, and by adding x && !y to the constraints you give Z3 the fact a && !a, which makes your constraints unsatisfiable.

Upvotes: 4

Related Questions