Z3中整數的最小值函數

Z3是否支持整數的最小值函數，即返回兩個數的最小值？我沒有在Z3的網站上找到它。Z3中整數的最小值函數

此外，它是否支持某種函數可以返回一組數字的最小值？例如：（assert（= y（min x1 x2 x3 x4 x5））），其中x和y是整數。

謝謝。

來源

2012-06-27 Yin Chen

min是即將浮點理論的保留關鍵字。可以使用define-fun命令來定義宏min2（二進制），min3（三元）等這裏是限定min2，min3和min4一個例子。

http://rise4fun.com/Z3/akWje

的SMT 2.0標準不支持的參數的任意數量的宏。如果您願意，您可以使用其中一個Z3 API來做到這一點。 Python前端非常靈活。這裏是Z3Py中的一個例子。

http://rise4fun.com/Z3Py/Vvp

來源

2012-06-27 06:51:41

非常感謝萊昂納多。我注意到一對或一組數字的min函數不包含在SMT的標準語言中。我只是對應用程序中常見的原因感到好奇。我們可以看到，min是一個反單調函數，即min（S）> min（T），只要S \ subseteq T對於數組S，T，並且在大多數CSP求解器中實現。是否有任何技術原因，例如效率問題或增加複雜程度？ –

不，沒有特殊原因沒有在默認情況下在SMT中。 SMT-Lib標準試圖成爲極簡主義者。由於'min'可以基於支持的運營商來定義，因此它不符合標準。 –

Z3中整數的最小值函數

回答

相關問題