解析錯誤Z3_parse_smtlib2_file解析在Z3

我使用Z3 4.1提供的示例文件，我想在我的程序來解析SMT LIB2格式輸入。解析錯誤Z3_parse_smtlib2_file解析在Z3

因此，我首先嚐試使用Z3_parse_smtlib2_file來解析Z3中提供的示例（位於文件夾Z3-4.1/examples/smtlib下）。但是我發現很多解析錯誤，然後我的程序立即退出。我認爲輸入格式應該是正確的。我嘗試使用下面的代碼來解析Z3.2.smt2：

(set-option :auto-config true) 
(set-option :produce-models true) 

(declare-const a Int) 
(declare-fun f (Int Bool) Int) 
(assert (> a 10)) 
(assert (< (f a true) 100)) 
(check-sat)

結果如下：

smt2parser_example 
(error "line 1 column 26: error setting ':auto-config', option value cannot be modified after initialization") 
Error code: 4 
BUG: incorrect use of Z3.

的API調用是這樣的：

fs = Z3_parse_smtlib2_file(ctx, fname, 0, 0, 0, 0, 0, 0);

在哪裏問題是什麼？輸入文件應該沒問題。問題在於Z3_parse_smtlib2_file中的參數嗎？

來源

2012-09-26 Ting Chen

作爲由該錯誤消息指示的，自動配置選項不能一旦Z3上下文被初始化修改。只有少數選項是可變的，並且可以在上下文創建後進行更改，並且不包括自動配置。當行

(set-option :auto-config true)

從它解析正確的輸入文件中刪除。如果應用程序需要的任何選項進行設置，這將是最好將它們直接傳遞給上下文構造，即，通過使config（在C++）或Z3_config（C）中的對象到它。

來源

2012-09-27 18:26:04

克里斯托夫，你是對的。當我刪除行「（set-option：auto-config true）」時，解析器API工作正常。但是我遇到了一個新問題。當我在輸入文件的末尾添加一個新行「（獲取模型）」 Z3_parse_smtlib2_file產生錯誤。該錯誤消息是：smt2parser_example （錯誤「第9行第10列：模型是不可用」）錯誤代碼：4 BUG：不正確使用的Z3。 –

事實上，我也是如此。生產模型選項在這裏被忽略，它應該在構建上下文時被設置。通常，解析函數Z3_parse_smtlib *主要用於解析公式。可以通過將命令行傳遞給Z3二進制文件直接在命令行上執行SMT2腳本。 –

解析錯誤Z3_parse_smtlib2_file解析在Z3

回答

相關問題