Z3 4.0 Z3_parse_smtlib2_string

我通過C API/JNA/Scala使用Z3與SMT2，似乎工作得很好。Z3 4.0 Z3_parse_smtlib2_string

我想嘗試增量式求解。所以剛開始我用Z3_parse_smtlib2_string翻譯一下：

(declare-fun x() Int) 
(assert (>= x 0)) 
(check-sat) 
(get-model)

然後我回來的Z3_ast，把它變成一個求解器通過Z3_solver_assert，與Z3_solver_check檢查，並通過恢復模型Z3_solver_get_model （如果檢查返回可滿足，在這個例子中就是這種情況）。到目前爲止沒有問題。

但是，當我想還斷言是這樣的：

(assert (= x 1))

我被卡住的地方Z3_parse_smtlib2_string被稱爲點，因爲它抱怨，x是一個未知的常數。如果我添加申報 - 樂趣到第二個片段我得到一個無效的參數錯誤。這個變量不應該存在於環境中嗎？我是否需要設置其他參數Z3_parse_smtlib2_string？我怎樣才能從預先解析的公式中獲得這些結果？

也使用(set-option :global-decls true)沒有工作，因爲Z3告訴我，這個選項的值不能在初始化後修改。

有沒有人有線索如何解決這個問題？

來源

2012-06-15 MattKay

無恥插件：你有沒有試過[https://github.com/psuter/ScalaZ3](https://github.com/psuter/ScalaZ3）？（披露：我是主要作者）。 – Philippe

Z3_parse_smtlib2_string可以作爲額外的參數列表現有的排序和常量。第二次給你打電話時，你可以告訴它你已經知道x代表什麼了。

要恢復聲明的常量並從第一個解析階段進行排序，可以使用Z3_get_smtlib_num_decls,Z3_get_smtlib_decl以及類似的排序。

來源

2012-06-15 12:36:05 Philippe

Mh ..我有點接受這個答案作爲正確的答案。難道僅當調用Z3_parse_smtlib_string或Z3_parse_smtlib_file時，Z3_get_smtlib_X函數才能工作，如評論所述？因爲我得到錯誤：解析器（數據）不可用... – MattKay

它使用_Z3_parse_smtlib_string_ – MattKay

時正常工作我找到了解決此問題的方法：我沒有得到我需要的信息（func decls和func名稱）來自解析器，但來自模型：_Z3_model_get_const_decl_，_Z3_model_get_func_decl_和_Z3_model_get_decl_name_ 這些是已棄用的API的一部分。但正如我所看到的，這是使用SMTLIB2進行增量求解的唯一方法。還是有人有另一個建議？ – MattKay

Z3 4.0 Z3_parse_smtlib2_string

回答

相關問題