帶非線性算法的Z3性能

我認爲Z3的一部分處理非線性算術時遇到了性能問題。以下是一個簡單的具體Boogie示例，使用Z3（版本4.1）進行驗證需要很長時間（大約3分鐘）才能完成。帶非線性算法的Z3性能

const D: int; 
function f(n: int) returns (int) { n * D } 

procedure test() returns() 
{ 
    var a, b, c: int; 
    var M: [int]int; 
    var t: int; 

    assume 0 < a && 1000 * a < f(1); 
    assume 0 < c && 1000 * c < f(1); 
    assume f(100) * b == a * c; 

    assert M[t] > 0; 
}

看來，問題是由具有的功能的相互作用引起的，對整數變量範圍的假設以及（未知）整數值的乘法。最終的斷言不應該被證明。 Z3似乎並沒有很快失敗，它似乎有辦法以某種方式實例化許多術語，因爲它的內存消耗增長相當快，達到300 MB，此時它放棄了。

我想知道這是否是一個錯誤，或者是否有可能改進啓發式時Z3應當停止搜索目前正試圖解決問題的特定方向。

一個有趣的事情是，通過使用

function {:inline} f(n: int) returns (int) { n * D }

內聯函數使驗證很快終止。背景：這是我們在驗證者聖盃中看到的問題的最小測試用例。在那裏，布吉節目變得更長，可能有多種類似的假設。通常，驗證似乎不會終止。

任何想法？

來源

2012-09-20 stefan

您可以包含/發佈Z3文件嗎？ –

當然。我使用Boogie的/ proverLog選項獲取Z3輸入[無內聯函數]（http://pastebin.com/6HjT9DmC）和[with內聯]（http://pastebin.com/91kxxQrC）。 – stefan

是的，非終止是由於非線性整數算術。 Z3有一個新的非線性求解器，但它適用於「非線性實數算術」，並且只能用於僅使用算術的量詞自由問題（即，在您的示例中沒有未解釋的函數）。因此，在您的示例中使用了舊的算術求解器。該解算器對整數算術的支持非常有限。你對這個問題的分析是正確的。 Z3無法找到非線性整數約束塊的解決方案。請注意，如果我們將f(100) * b == a * c替換爲f(100) * b <= a * c，則Z3會立即返回「未知」答案。

我們可以通過限制Z3中非線性算術推理的數量來避免非終止。對於每個Z3查詢，選項NL_ARITH_ROUNDS=100將最多使用非線性模塊100次。這不是一個理想的解決方案，但至少，我們避免了不終止。

來源

2012-09-21 15:33:24

謝謝，這很有幫助，我會嘗試使用此選項。最終我們想利用Z3的真正支持，這似乎也解決了我們的問題。但這需要布吉首先支持實際。 – stefan

帶非線性算法的Z3性能

回答

相關問題