什麼是選項`rlimit`和`timeout`之間的關係？

Question

有人建議在this Z3 issue comment該選項rlimit要優於timeout：

結合超時與搜索算法使一切 不確定性，所以現在你甚至不需要改變隨機種子 讓它失敗！使用rlimits（(set-option :rlimit <n>)和 類似）的資源邊界的確定方法。

我試圖找到有關rlimit在Z3的幫助（z3 -pd）的更多信息，但說明書中提供只有很短。

具體來說，我有以下問題：

• Q1：什麼樣的 「求解資源」 並不rlimit限制 - 只是時間或還記憶？
• Q2：是:rlimit 1000相當於該解算器必須經過1000毫秒終止:timeout 1000？
• Q3：可以重複設置rlimit（因爲timeout可以）或者只是一次？

Answer 1

A1：不管我們覺得很有意義。我們的想法是算什麼「基本操作」，但我們繼續前進，增加新的「行動」這一定義的變化。不能保證它在不同版本的Z3中保持不變。但是，只要您繼續使用相同的二進制文件，它就是確定性的。

A2：沒有，沒有對等的，但一旦超過了RLIMIT Z3將終止。我們最近一批固定的臭蟲在那裏並沒有終止的，我敢肯定，還有幾個在那裏這些錯誤的地方，但我們會解決，當然他們。

A3：是的，你可以做

... (set-option :rlimit 12345) (check-sat) ...