查詢命題模型

Question

我正在瀏覽Z3的OCaml API http://research.microsoft.com/en-us/um/redmond/projects/z3/ml/Z3.html尋找一種訪問求解器返回的模型的方法，該模型滿足簡單的命題公式，即。只使用Z3的SAT部分，而不是「T」部分。 p或q可能會返回一個模型p = true，q = false。我能找到的最接近的是solver_get_model，它返回一個模型。但是我找不到任何訪問模型的方式，因爲模型類型看起來不透明。我確實看到了一個用於獲得與函數符號（model_get_func_interp）相關的解釋的函數，但這並不是我想要的，即使這樣我也看不到如何處理返回的信息（func_interp），因爲這似乎也是一種不透明的類型。關於我唯一能看到的另一種方式是將模型轉換爲字符串。這是唯一的方法嗎？

感謝

Answer 1

（公平的警告：我沒有用OCaml的API自己，所以我部分地我與C API經驗猜測這一點。）

看看的功能：

val model_get_const_interp : context -> model -> func_decl -> ast 

值以通爲context和model應該是清楚的。現在你可能會想知道爲什麼當你真正在尋找一個常量的值時，你需要通過func_decl。問題是，在SMT世界中，特別是在Z3中，常量就像沒有參數的函數一樣（因此文檔中顯示了前提條件get_arity c a == 0）。

這將返回一個（選項類型）的AST。下一步是檢查AST對true或false。這樣做的一個方法是調用該函數

val get_decl_kind : context -> func_decl -> decl_kind 

然後，您可以將結果與OP_TRUE和OP_FALSE比較。

需要注意的是另一種方式來查詢模型是使用

val model_eval : context -> model -> ast -> bool -> ast option 

您可以通過任何AST這一功能（如對∧¬q等），並以同樣的方式讀出結果。