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