使用量詞是否影響Z3的性能？

Question

在回答this question時，Leo建議使用量詞來定義函數。假設我只需要應用函數1次，使用量詞是否影響Z3的性能？

它與我聲明一個沒有參數和沒有量詞的函數（因爲我只使用函數只有一次）的情況相比如何？

Answer 1

您可以嘗試使用選項smt.macro_finder = true將量化的等式轉換爲宏。它默認是關閉的，所以最好爲只應用一次的函數定義宏。這也意味着Z3最終會使用基於一般量詞的求解器。在某些情況下，使用「define-fun」命令由宏定義的函數對於純粹位向量或純粹線性算法的公式非常有用。在這些情況下，Z3使用更高效的設置。例如，Z3使用「相關性」傳播來避免多餘的量詞實例化。相關性傳播帶有其自身的開銷，這對於量化公式來說是可以容忍的，但對於無量化公式而言不是一個好主意。