Z3理論插件分裂到子問題

有時（或多次）它發生的問題是如此之大，以至於Z3解算器有很多超時問題。在這種情況下，我認爲將問題分解爲較小的子問題將會有所幫助。Z3理論插件分裂到子問題

我想在Z3中具體詢問Theory Plugins。

假設我有3個變量A,B and C。我正在爲他們每個人分配價值。假設由於我指定的一些限制，分配的值是A=0和B=1。現在，取決於這些A and B的值，C是用另一組方程計算的，可能不是作爲約束編碼的。在這種情況下，是否可以寫一個理論插件，它會說當A and B分配了某些值，然後回調一些函數返回值C。

我在示例目錄中看到了一個理論示例，但它對我來說不是很清楚。另外我試圖閱讀文檔。

來源

2013-02-19 Raj

理論插件並不是將問題分解爲子問題的理想技術。當我們想要擴展Z3支持的一套理論時，通常會定義一個理論插件。例如，假設我們想要包含一個可以推理字符串的模塊。該模塊將提供新的解釋符號，例如：substring,contains等。 This article描述了用於集合+基數約束的決策過程。這個程序是作爲Z3的理論插件實現的。

這就是說，理論插件目前已被棄用。它們在Z3中仍受支持，但它們與新的Solver API不兼容。要使用插件，我們必須使用舊的（不贊成使用的）API。

這裏有一些相關的職位描述理論插件API的當前狀態Z3：

來源

2013-02-21 00:20:41

Z3理論插件分裂到子問題

回答

相關問題