如何使用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(m.eval(x)==true) 
    std::cout<<"x is true"; 

是否有人知道如何做到這一點？提前致謝。

Answer 1

有一個函數「eq」可用於檢查兩個術語之間的結構相等性。 過載==會創建一個新的術語，但eq（m.eval（e），c.bool_val（true））將檢查結構是否相等。