Z3實數算術和統計

Question

考慮到使用Z3的實數編碼的問題，Z3 /smt2 /st產生的統計數據可能有助於判斷實數引擎是否「有問題/有很多工作」？

在我的情況下，我有兩個主要等效的問題編碼，都使用實數。然而，編碼中的「小」差異在運行時造成很大的差異，即編碼A需要2：30min並且編碼B 13min。 Z3統計顯示conflicts和quant-instantiations大部分是等效的，但其他的不是，例如grobner,pivots和nonlinear-horner。

這兩種不同的統計信息可用作gist。

EDIT（解決Leo的評論）：

SMT2編碼由兩個版本生成的是〜30K線和其中使用實數的斷言灑遍佈代碼。主要區別在於，編碼B使用大量由不等式界定的範圍從0.0到1.0的未指定的實型常量，例如， 0.0 < r1 < 1.0或0.0 < r3 < 0.75 - r1 - r2，而在編碼中，很多這些未指定的常量已被來自相同範圍的固定實數值替代，例如0.1或0.75 - 0.01。兩種編碼都使用非線性實數算術，例如r1 * (1.0 - r2)。

這兩個編碼中的一些隨機例子可以作爲gist獲得。如上所述，所有發生的變量都是未指定的實數。

PS：是否引入別名爲固定的實際值，例如，

(define-sort $Perms() Real) 
(declare-const $Perms.$Full $Perms) 
(declare-const $Perms.$None $Perms) 
(assert (= $Perms.Zero 0.0)) 
(assert (= $Perms.Write 1.0)) 

造成顯著的性能損失？

Answer 1

新的非線性算術解算器僅用於僅包含算術的問題。由於您的問題使用量詞，因此不會使用新的非線性求解器。因此，Z3將採用基於以下組合的舊方法：Simplex（pivot stat），Groebner Basis（groebner stat）和Interval Propagation（horner stat）。這不是一個完整的方法。 此外，基於你發佈的片段，Groebner基礎不會很有效。這種方法通常對包含很多平等的問題有效。 所以，它可能只是開銷。您可以使用選項NL_ARITH_GB=false將其禁用。 當然，這只是基於你發佈的問題片段的猜測。

編碼A和B之間的差異很大。編碼A本質上是一個線性問題，因爲幾個常量被固定爲實際值。對於線性算術問題，Z3總是完整的。所以，這應該解釋性能的差異。

關於你提到的有關別名的問題，引入別名的首選方法是：

(define-const $Perms.$Zero $Perms 0.0) 
(define-const $Perms.$Write $Perms 1.0) 

Z3還包含使用線性方程消除變量的預處理器。 默認情況下，此預處理器在包含量詞的問題中處於禁用狀態。這個設計決策是由程序驗證工具激發的，這些工具廣泛使用量詞中的觸發器/模式。變量消除過程可能會修改仔細設計的觸發器/模式，並影響總運行時間。你可以在Z3中使用新的策略/策略框架來強制它應用這個預處理器。您可以替換命令

(check-sat) 

與

(check-sat-using (then simplify solve-eqs smt)) 

這種策略是告訴Z3執行簡化器，然後解方程（並消除變量），然後執行默認求解器引擎smt。 您可以在以下tutorial中找到更多關於戰術和戰略的信息。