如何用c++API获取SAT试题中的模型值？ [英] How to get the model value in SAT problems using c++ api?

问题描述

我正在使用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))检查结构是否相等。

这篇关于如何用c++API获取SAT试题中的模型值？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！