Z3_parse_smtlib_string使用問題

Question

在下面的代碼中，我放了一個明顯不能令人滿意的Z3聲明，然後嘗試使用C++/C Z3 API以編程方式查看它。

問題是這段代碼總是觸發輸出的檢查：「SAT ?!」。即明確不可滿足的表達式被確定爲在API調用的當前使用中是可滿足的。

如何獲得此類操作以按預期方式工作？

#include "z3++.h" 
int main(){ 
    z3::context c; 

    std::string testing = "(declare-const p0 Bool)(assert(= p0 true))(assert(= p0 false))(check-sat)"; 

    Z3_ast parsed = Z3_parse_smtlib2_string(c,testing.c_str(),0,0,0,0,0,0); 
    z3::expr e(c, parsed); 

    z3::solver s(c); 
    if(s.check() == z3::sat) 
    std::cout << "SAT?!\n"; 
    return 0; 
} 

Answer 1

Z3在這種情況下是正確的，因爲沒有約束條件被添加到求解器中，因此這是可以滿足的。關鍵部分是這樣的：

Z3_ast parsed = Z3_parse_... 
z3::expr e(c, parsed); 

z3::solver s(c); 
s.add(e); // <--- Add constraints to solver here 
if(s.check() ...