我看到在使用了一個有趣的技術，答案到另一個問題，并想好一點理解。我們給了一個無符號的64位整數，我們對以下位感興趣：1.......2.......3.......4.......5.......6.......7.......8.......具體來說，我們希望將它們移動到前八位，如下所示：12345678........................................................我們不在乎由指示的位的值.，也不必保留它們。該溶液是屏蔽掉不需要的位，并且乘以結果0x2040810204081。事實證明，這可以解決問題。這種方法有多普遍？可以使用這種技術來提取位的任何子集嗎？如果不是，那么如何確定該方法是否適用于特定的一組位？最后，如何找到正確的（a？）乘法器以提取給定的位？
3 回答
飲歌長嘯
TA貢獻1951條經驗 獲得超3個贊
確實，這是一個非常有趣的問題。我要花兩分錢，就是說，如果您可以通過位向量理論上的一階邏輯來說明這樣的問題，那么定理證明就是您的朋友，并且可以為您提供非?？斓慕鉀Q方案您問題的答案。讓我們重新陳述定理所要問的問題：
“存在一些64位常量'mask'和'multiplicand'，因此對于所有64位位向量x，在表達式y =（x＆mask）*被乘數中，我們的y.63 == x.63 ，y.62 == x.55，y.61 == x.47，等等?！?/p>
如果該句子實際上是一個定理，則確實是常量“掩碼”和“被乘數”的某些值滿足此屬性。因此，讓我們用定理證明者可以理解的東西（即SMT-LIB 2輸入）來表述一下：
(set-logic BV)
(declare-const mask (_ BitVec 64))
(declare-const multiplicand (_ BitVec 64))
(assert
(forall ((x (_ BitVec 64)))
(let ((y (bvmul (bvand mask x) multiplicand)))
(and
(= ((_ extract 63 63) x) ((_ extract 63 63) y))
(= ((_ extract 55 55) x) ((_ extract 62 62) y))
(= ((_ extract 47 47) x) ((_ extract 61 61) y))
(= ((_ extract 39 39) x) ((_ extract 60 60) y))
(= ((_ extract 31 31) x) ((_ extract 59 59) y))
(= ((_ extract 23 23) x) ((_ extract 58 58) y))
(= ((_ extract 15 15) x) ((_ extract 57 57) y))
(= ((_ extract 7 7) x) ((_ extract 56 56) y))
)
)
)
)
(check-sat)
(get-model)
現在讓我們問定理證明者Z3這是否是一個定理：
z3.exe /m /smt2 ExtractBitsThroughAndWithMultiplication.smt2
結果是：
sat
(model
(define-fun mask () (_ BitVec 64)
#x8080808080808080)
(define-fun multiplicand () (_ BitVec 64)
#x0002040810204081)
)
答對了！它會在0.06秒內重現原始帖子中給出的結果。
從更一般的角度來看，我們可以將其視為一階程序綜合問題的一個實例，這是一個新興的研究領域，有關該領域的論文很少發表。搜索"program synthesis" filetype:pdf應該可以幫助您入門。
互換的青春
TA貢獻1797條經驗 獲得超6個贊
乘法器中的每個1位用于將其中一位復制到其正確位置：
1已經在正確的位置，因此請乘以0x0000000000000001。2必須向左移動7位，因此我們乘以0x0000000000000080（設置了位7）。3必須向左移動14位位置，因此我們乘以0x0000000000000400（設置了位14）。以此類推，直到
8必須向左移動49位，因此我們乘以0x0002000000000000（設置了位49）。
乘數是各個位的乘數之和。
這之所以起作用，是因為要收集的位不太緊密，因此在我們的方案中不屬于一起的位的乘法要么超出64位，要么落入較低的無關位部分。
請注意，原始編號中的其他位必須為0。這可以通過用AND操作屏蔽它們來實現。
- 3 回答
- 0 關注
- 612 瀏覽
添加回答
舉報
0/150
提交
取消