z3 - z3 是否通过名称来区分变量？

Question

假设我们有以下代码：

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”是否操作同一个变量？

Answer 1

您似乎将宿主语言 C++ 中存在的编程变量 x与逻辑变量以及Z3 的原因混淆了。并且都表示逻辑变量，并且通过添加约束，您可以给 Z3 一个事实，这会使您的约束无法满足。y abxyax && !ya && !a