Z3/cvc4中是否有任何函數可用於計算底數2的對數？

Question

我想證明一個簡化，涉及計算日誌到基地2.是否有任何可用於z3/cvc4計算它的功能？

Answer 1

簡而言之，支持不能直接用於任何工具中的整數。對於無界整數，存在一個固定常數的Presburger求冪的決策過程。由此可以構造對數函數（反之亦然）。我不是專家，但我的理解是這些是相當複雜的。欲瞭解更多信息：

• http://www.logique.jussieu.fr/~point/papiers/Pres.pdf
• http://dx.doi.org/10.2307/2586704
• https://mathoverflow.net/questions/103896/beyond-presburger-arithmetic

我不知道這些算法的任何現有的實現。

對於有界整數，即x in [a，b]其中a和b是數字，沒有解算器特定的支持，但可以對此進行建模。首先創建一個Integer類型的Skolem常量。然後，您使用斷言力S的解釋：

(and (=> (2^0 <= x < 2^1) (= s 0)) 
    (=> (2^1 <= x < 2^2) (= s 1)) 
    ... 
    (=> (2^i <= x < 2^{i+1}) (s = i)) ; for all 2^i in [a,b] and i >= 0. 
) 

這使得S ^不解釋，如果x < = 0（我認爲這是合理的）。這是非常令人不滿意的，但它是線性的。 （如果有人知道更好的編碼，我很想知道它！）還可以使用量化符對上面的公理編碼有界或無界整數。您首先使用量詞將函數2^i編碼爲未解釋的函數。然後使用2^i函數指定日誌功能。這很可能會導致解算器返回未知數，如果沿着這條路走下去，您可能需要使用量化器模塊的解算器選項。

對於位向量，您需要決定數字是有符號還是無符號。對於長度爲k的無符號值，可以使用右移來模擬這個值。

(=> (bvugt x (_ bv0 k))) (= (bvlshr x s) (_ bv1 k)) 

再次x < = 0（無符號）未被解釋。簽名的位向量類似：

(=> (bvsgt x (_ bv0 k))) (= (bvlshr x s) (_ bv1 k)) 

Answer 2

Alive確實有btw的log2（foo）函數。 它使用類似於Tim提供的線性編碼。