如何將變量的值轉換爲模型中的int值？

Question

使用模型對象時，我呼叫func_decl get_func_decl (unsigned i)來獲取賦予某個函數（變量）的值。我遇到的問題是將該輸出（這是一個func_decl）並將其轉換爲int。

例如，如果該模型是{x |-> 4, y |-> 12, z |-> 6}，我想獲得的3個變量（4，12和6）的實際int值。

Answer 1

Z3提供了功能Z3_get_numeral_int爲了這個目的：

Z3_bool Z3_API Z3_get_numeral_int(__in Z3_context c, __in Z3_ast v, __out int* i); 

注意，最後一個參數是一個點，如果調用成功，將填充正確值的整數（它會失敗對非數字或數字不能表示爲int）。

也有稱爲Z3_get_numeral_*以獲得不同類型的值的其他功能，例如，UINT64等

此方法適用於常量（即，元數0的func_decls）。爲了得到一個（非零元數）函數定義的項目，下面的函數應使用：

Z3_func_entry Z3_API Z3_func_interp_get_entry(__in Z3_context c, __in Z3_func_interp f, unsigned i);