Z3能檢查包含遞歸函數的公式的可滿足性嗎？

Question

我正在嘗試一些涉及遞歸函數的a Z3 tutorial的示例。我試過了下面的例子。

1. Fibonacci（第8.3節）
2. IsNat（第8.3節）
3. Inductive（10.5節）出

Z3次對所有的上述實例。但是，該教程似乎暗示只有Inductive不是終止。

Z3能否檢查包含遞歸函數的公式的可滿足性，還是不能處理任何歸納事實？

Answer 1

這些來自Z3教程的例子是爲了說明Z3背後技術的侷限性。

Z3失敗這些例子有兩個原因：

1. 通過Z3產生的模型分配一個解釋用於每個未解釋的函數符號。這些模型可以被視爲功能程序。當前版本不會產生遞歸定義。第一個例子是可以滿足的，但Z3不能爲fib提供解釋，因爲它不支持遞歸定義。 我們計劃在這個方向上擴展Z3。

2. Z3不支持歸納證明。例2和例3是不能令人滿意的，但Z3因爲它不支持歸納證明而失敗。我們也有計劃爲此添加基本支持。

雖然這些項目都在我的TODO列表上，但我今年不會開始研究它們。