2014-09-24 90 views
1

由於previously asked Z3不能提供遞歸函數的模型。然而,是否有可能告訴Z3(最好通過Java API)沒有定義遞歸函數的模型是足夠的(或者確實選擇我感興趣的函數,本質上我不需要非常量函數的模型) ?顯然,這可能會導致查詢返回,儘管某些函數沒有模型。基本上,用戶然後必須確保這些功能確實有一些模型。然而,我認爲Z3或SMT解算器的工作方式並不是真正可以實現的,也就是說,我假設Z3需要遞歸函數的(部分)模型來評估表達式。模型和遞歸函數

回答

1

量詞的MBQI實現並不能很好地處理遞歸函數。 有一件事可能會爲你帶來訣竅:用有界遞歸函數替換遞歸函數定義。您添加一個額外的參數來計算您願意探索該函數的展開次數。每當您在輸入的其餘部分應用遞歸函數時,請設置深度參數。您可以使用代數數據類型的Peano數字或整數。例如,符號自動機工具包使用這種方法。

0

我發現了一篇論文,探討了Nikolaj Bjorner的答案:Amin,Leino和Rompf(2014)的「用SMT解算器進行計算」。此外,我發現Suter,Köksal和Kuncak(2011)的「可滿足模遞歸程序」,其中調用連續遞歸函數,直到可以決定可滿足性爲止。