由於previously asked Z3不能提供遞歸函數的模型。然而,是否有可能告訴Z3(最好通過Java API)沒有定義遞歸函數的模型是足夠的(或者確實選擇我感興趣的函數,本質上我不需要非常量函數的模型) ?顯然,這可能會導致查詢返回,儘管某些函數沒有模型。基本上,用戶然後必須確保這些功能確實有一些模型。然而,我認爲Z3或SMT解算器的工作方式並不是真正可以實現的,也就是說,我假設Z3需要遞歸函數的(部分)模型來評估表達式。模型和遞歸函數
Q
模型和遞歸函數
1
A
回答
1
量詞的MBQI實現並不能很好地處理遞歸函數。 有一件事可能會爲你帶來訣竅:用有界遞歸函數替換遞歸函數定義。您添加一個額外的參數來計算您願意探索該函數的展開次數。每當您在輸入的其餘部分應用遞歸函數時,請設置深度參數。您可以使用代數數據類型的Peano數字或整數。例如,符號自動機工具包使用這種方法。
0
我發現了一篇論文,探討了Nikolaj Bjorner的答案:Amin,Leino和Rompf(2014)的「用SMT解算器進行計算」。此外,我發現Suter,Köksal和Kuncak(2011)的「可滿足模遞歸程序」,其中調用連續遞歸函數,直到可以決定可滿足性爲止。
相關問題
- 1. Typescript - 遞歸函數類型
- 2. Ackermann函數和遞歸
- 3. SQL函數和遞歸
- 4. 遞歸函數和pthreads
- 5. Lwt和遞歸函數
- 6. 遞歸函數求和
- 7. 遞歸函數
- 8. 遞歸函數
- 9. 函數遞歸
- 10. 遞歸函數
- 11. 遞歸函數
- 12. 遞歸函數
- 13. 遞歸函數
- 14. 遞歸函數
- 15. 遞歸函數
- 16. 遞歸函數
- 17. CakePhp:模型遞歸關聯和查找
- 18. 遞歸函數的返回類型
- 19. Swift遞歸函數,返回類型Closure
- 20. 遞歸函數返回類型錯誤
- 21. C++類型推斷遞歸函數
- 22. 具有模式的Scala遞歸函數
- 23. 流星 - 模板遞歸函數onrendered
- 24. 找出遞歸函數的模式
- 25. Python遞歸函數不遞歸
- 26. 如何從遞歸遞歸函數
- 27. 尾遞歸函數
- 28. 遞歸函數C++
- 29. 遞歸函數Python
- 30. 遞歸strcpy函數