Z3命名允許綁定在API

Question

我使用Z3從API，我正在尋找一種方法來調試我的約束。我的代碼編譯和Z3運行在我的約束上，但是我的約束有些問題。我希望看看我給Z3確定什麼是錯誤或缺失的限制，但我不知道如何以一種非常可讀的方式做到這一點。問題是使用像SMTLIB_DUMP_ASSERTIONS這樣的工具不會在任何綁定變量中提供有意義的名稱。由於我有很多重複使用相同的表達式，幾乎所有的東西都被一個生成的變量限制了。

是否有任何方法來轉儲輸入約束文件，其中let-bound變量具有我已分配的名稱？我不特別在乎格式是什麼，但SMTLIB 1或2會很好。

Answer 1

不，您不能提供名稱以讓變量由Z3 AST打印機自動創建。 一個可能的解決方案是編寫您自己的AST打印機。在Z3發行版中，我們有一個示例應用程序examples/c/test_capi.c。它包含以下功能：

void display_ast(Z3_context c, FILE * out, Z3_ast v) 

它顯示瞭如何實現一個簡單的AST打印機。這個例子非常簡單，但它是一個起點。