我正在使用Z3的C++API来解决SAT问题。 当问题确定后，我想得到所有变量的可满足性赋值。 我发现打印变量的值很容易，如以下代码所示：

context c;
solver s(c);
expr x=c.bool_const("x");
s.add(x);
if(s.check()==sat){
     model m=s.get_model();
      std::cout<<"x:"<<m.eval(x);
}

但问题是我需要在‘if’条件语句中使用它。 例如：

if(m.eval(x)==true)
     std::cout<<"x is true";

有人知道怎么做吗？提前谢谢。

推荐答案

有一个函数"eq"可用于检查两个术语之间的结构等价性。 重载==创建一个新术语，但eq(m.val(E)，c.bool_val(True))检查结构是否相等。