是否支持Z3路線圖上的遞歸函數？

Question

6月28日將「define-fun-rec」語法添加到標準中。 CVC4支持它。我很好奇，目前是否支持解決遞歸函數的約束？謝謝。

Answer 1

當然。

請注意，您可以使用Z3通過將它們的合約編碼爲Horn子句來推斷遞歸函數。 Z3中有幾個Horn子句後端。 另外，程序驗證系統，特別是Boogie，非常適合推理遞歸程序。 代替的語法支持，你可以按照速記在 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf建議， 第58頁也可以使用其他間接編碼，當然，在 模式找到在SMT遞歸函數，http://smt2015.csl.sri.com/wp-content/uploads/2015/06/2015-Reynolds-Blanchette-Tinelli-Model-Finding-for-Recursive-Functions-in-SMT.pdf