z3 - 如何使用 c++ api 获取 SAT 问题中的模型值？

Question

我正在使用 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";

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

Answer 1

有一个函数“eq”可用于检查两个术语之间的结构相等性。重载 == 创建一个新术语，但 eq(m.eval(e),c.bool_val(true)) 检查结构相等性。