訂單理論的定製理論解答？

我的程序，反應有限狀態系統的有界合成器，生成SMT查詢以註釋（未解釋）系統和規範的產品自動機。本質上它是一個模型檢查與未解釋的功能。如果註釋存在=> Z3找到的模型滿足規範。所述查詢包含：訂單理論的定製理論解答？

數據類型（以編碼系統的狀態和一個規範自動機）
> =（大於），>（嚴格）（以指定的自動機系統*規格的狀態的排名函數，其被用於搜索與壞狀態的套索）或者換句話說，該自動機的狀態的順序，其中
與布爾域和範圍未解釋功能
所有條款是喇叭子句

一種examp樂是https://dl.dropboxusercontent.com/u/444947/posts/full_arbiter2.smt2 （「FORALL」用於編碼「不關心」輸入功能）

目前查詢需要從整數算術嚴格大於>運營商（即排名函數具有Int範圍）。

問題：是否值得在Z3中爲這種查詢開發一個自定義理論求解器？它可以利用基於DFS的lassos搜索，這可能比整數理論解算器（或diff-neg tactic）更快。

或Z3已經有效地處理了這個？（高效率意味着「可以與基於圖形的套索搜索相比」）。

來源

2013-07-22 Ayrat

算術不是基準的瓶頸。我們可以通過使用

valgrind --tool=callgrind z3 full_arbiter2.smt2 
kcachegrind

Valgrind的和kcachegrind在大多數Linux發行版提供檢查。所以，如果你實施一個求解理論的求解器，我認爲你不會得到顯着的性能改進。一個瓶頸是數據類型理論。如果使用位向量對類型Q和T進行編碼，則可能會提高性能。另一個瓶頸是量詞推理。您在調用Z3之前是否嘗試過展開它們？在Z3中，qe（量詞消除）策略將基本上擴展布爾量詞。我用

(check-sat-using (then qe smt))

來源

2013-07-23 00:08:30

thaanks更換

(check-sat)

有一個小加速！收集數據需要一段時間。簡而言之：1）'qe'（和手動擴展）幫助很多（〜10x）2）爲什麼數據類型是瓶頸？ 3）切換到bv並沒有真正的幫助。請參閱此「報告」：https://dl.dropboxusercontent.com/u/444947/posts/stackoverflow_orders_theory/profile_of_synthesis_queries.html – Ayrat

數據類型是使用遞歸結構（例如樹和列表）來實現的。該實現會影響搜索引擎做出選擇的方式。例如，給定一個列表項「t」。它會總是首先猜測't'是'nil'。沒有針對枚舉類型等有限數據類型的優化。有幾個用戶報告說，在你的公式中用於編碼類似'Q'和'T'的枚舉類型時，它們表現不佳。他們報告說，當他們用位向量（或帶有明確邊界的整數）替換數據類型時，他們得到了很好的加速。用整數進行嘗試可能是值得的。 –

（更新了表）在這些小例子中，'int'和'bv'與'dt'相似，但我會記住你的建議，謝謝！ – Ayrat

訂單理論的定製理論解答？

回答

相關問題