Z3 C++，如何解析smt競爭不核心實例

Question

我想用c + + api（版本Z3 4.1.0.0）Z3，即我試圖解析從smt競爭不核心軌道的實例。 我寫（基於實施例）以下代碼：

context c; 
Z3_ast f; 
f = Z3_parse_smtlib2_file(c, "smtlib_uc/QF_IDL/queens_bench/n_queen/queen3-1.smt2.uc.smt2", 0, 0, 0, 0, 0, 0); 
expr r = to_expr(c, f); 
solver s(c); 
s.add(r); 
std::cout << s << "\n"; 

但我得到以下錯誤：

（錯誤「行1列34：錯誤設定 '：產生-不飽和度，芯' ，選項值初始化後不能被修改「）

（錯誤‘線220列15：不飽和度芯未啓用施工，使用命令（設置選項：產生-不飽和度型磁芯真）’）

意外的錯誤：解析錯誤

有誰知道如何解決這個問題？

Answer 1

Z3_parse_smtlib*函數僅用於解析公式;因此，很多選項都不適用於他們。

您可以簡單地刪除輸入文件中的(set-option :produce-unsat-cores true)行，並在初始化context時設置該選項。您可以通過使用Z3_solver_get_unsat_core來檢索不存在的核心。

如果你不想修改輸入文件，你應該使用Z3二進制代替。這些選項將用Z3二進制文件成功解析。