我正在使用 Z3 Java API 來解決使用該parseSMT2File()方法的 smt 文件。但是，即使我設(shè)置params.add("interactive-mode", true)了 then solver.setParameters(params)，Z3 也會拋出以下錯誤：Exception in thread "main" com.microsoft.z3.Z3Exception: (error "line 276 column 23: model is not available")(error "line 277 column 26: model is not available")(error "line 279 column 15: command is only available in interactive mode, use command (set-option :interactive-mode true)")(error "line 280 column 16: model is not available")
1 回答
滄海一幻覺
TA貢獻1824條經(jīng)驗 獲得超5個贊
parseSMT2File()只解析文件中的斷言，并將它們作為一個表達式返回。它不運行許多命令，包括check-sat，即您還必須調(diào)用check()您添加了斷言的求解器。
添加回答
舉報
0/150
提交
取消