Z3打印評估結果

Question

在Z3中，我們如何編寫一個程序來獲得評估結果？默認model.eval(expression)將返回評估結果的另一個表達式。如何將結果分配給特定於類型的數據？以下是我想要在我的程序中執行的操作。

int a = model.eval(x + 1) // compiler error 

Answer 1

有時模型不完整。例如，當沒有任何東西取決於x的值時，則Z3可能根本不會分配任何值，即，您可以自由選擇適合您的任何值。 eval函數有第二個參數，當設置爲true時，將啓用模型完成，即eval將用一些合法值（通常爲0）替換那些不關心的項目。

Z3-ints是實際整數，而不是C/C++ - 整數小於2^32-1，所以轉換不會自動執行。如果您知道在您的應用程序中這將始終正常，並且eval將始終返回一個數字，那麼您可以使用Z3_get_numeral_int執行該轉換。