顯示Z3推斷量詞的模式

我想看看Z3在我的公式中用於一些量詞的模式。顯示Z3推斷量詞的模式

This comment表明它可能是可能的，但我找不到更多的細節。

如何讓Z3打印此信息？

目前，您只能通過調試模式下的調試跟蹤打印此信息，沒有方便的方式以可讀的方式顯示該信息。它仍然在待辦事項列表中，我已經開始在單獨的分支中添加一些內容，但仍然需要時間才能方便使用。 –

@ChristophWintersteiger你能告訴我如何在調試模式下執行它（即使它不可讀）嗎？ –

我找到了一種使用Z3調試版本的方法。我仍然希望有朝一日能夠在正常建設中實現。 –

基於來自克里斯托夫一個helpful comment，我發現，在調試模式下建立Z3（在生成過程中傳遞到-dmk_make.py），然後使-v:10命令行來推斷圖案所得Z3打印上。

2017-08-24 17:49:01

推斷模式的打印輸出是最近添加的，僅用於調試。實現這一目標的方式和輸出格式很可能很快發生變化，所以不要依賴它。（另外，它只打印推斷的模式，可能不是全部） –

感謝您的警告。我打算只用於調試，所以這些限制並不是什麼大問題。 –

回答