[c] 단일 곱셈으로 비트 추출

매우 흥미로운 질문과 영리한 속임수.

단일 바이트를 조작하는 간단한 예를 살펴 보겠습니다. 단순화를 위해 부호없는 8 비트 사용 당신의 숫자가 xxaxxbxx당신 이 원한다고 상상해보십시오 ab000000.

이 솔루션은 비트 마스킹과 곱셈의 두 단계로 구성되었습니다. 비트 마스크는 흥미롭지 않은 비트를 0으로 바꾸는 간단한 AND 연산입니다. 위의 경우 마스크가 00100100되고 결과가 00a00b00됩니다.

이제 어려운 부분은로 바꾸는 것입니다 ab.......

곱셈은 ​​시프트 및 덧셈 연산입니다. 핵심은 오버플로가 필요없는 비트를 “이동”하고 원하는 비트를 올바른 위치에 배치하는 것입니다.

4 ( 00000100)를 곱 하면 모든 것이 2 씩 왼쪽으로 이동하여 이동합니다 a00b0000. b위로 이동 하려면 1 (a를 올바른 위치에 유지) + 4 (b를 위로 이동)를 곱해야합니다. 이 합계는 5이며 이전 4와 결합하면 매직 넘버 20 또는 00010100입니다. 원본은 00a00b00마스킹 후 였습니다 . 곱셈은 ​​다음을 제공합니다.

000000a00b000000
00000000a00b0000 +
----------------
000000a0ab0b0000
xxxxxxxxab......

이 방법을 사용하면 더 많은 수와 더 많은 비트로 확장 할 수 있습니다.

당신이 물었던 질문 중 하나는 “이것은 몇 비트라도 가능합니까?” 여러 마스킹 작업이나 곱셈을 허용하지 않는 한 대답은 “아니오”라고 생각합니다. 문제는 “충돌”문제입니다 (예 : 위 문제의 “stray b”). 우리가 이것을 같은 숫자로해야한다고 상상해보십시오 xaxxbxxcx. 이전의 접근 방식에 따르면 {x 2, x {1 + 4 + 16}} = x 42 (oooh-모든 것에 대한 답변)가 필요하다고 생각할 것입니다. 결과:

00000000a00b00c00
000000a00b00c0000
0000a00b00c000000
-----------------
0000a0ababcbc0c00
xxxxxxxxabc......

보시다시피 여전히 작동하지만 “단지”입니다. 여기서 핵심은 모든 비트를 압축 할 수있는 비트 사이에 “충분한 공간”이 있다는 것입니다. 나는 c + d를 얻는 인스턴스를 얻을 수 있기 때문에 c 바로 뒤에 네 번째 비트 d를 추가 할 수 없었습니다.

따라서 공식적인 증거 없이는 다음과 같이 질문의 더 흥미로운 부분에 대답 할 것입니다. “아니오, 이것은 여러 비트에 대해 작동하지 않습니다. N 비트를 추출하려면 원하는 비트 사이에 (N-1) 개의 공백이 필요합니다. 추출하거나 추가 마스크 곱셈 단계를 수행하십시오. “

“비트 사이에 (N-1) 0이 있어야 함”규칙에 대해 생각할 수있는 유일한 예외는 다음과 같습니다. 원본에서 서로 인접한 두 개의 비트를 추출하려면 같은 순서로해도 여전히 할 수 있습니다. 그리고 (N-1) 규칙의 목적을 위해 두 비트로 계산됩니다.

아래 @Ternary의 답변에서 영감을 얻은 또 다른 통찰력이 있습니다 (내 의견 참조). 흥미로운 비트마다 거기에 가야하는 비트를위한 공간이 필요한만큼 오른쪽에 0 만 있으면됩니다. 또한 왼쪽에 결과 비트만큼 왼쪽에 많은 비트가 필요합니다. 따라서 비트 b가 n의 위치 m에서 끝나는 경우 왼쪽에 m-1 0이 있고 오른쪽에 nm 0이 있어야합니다. 특히 비트의 순서가 원래 순서와 순서가 다르면 원래 순서와 비교하여 중요한 개선 사항입니다. 예를 들어 16 비트 워드

a...e.b...d..c..

로 이동할 수 있습니다

abcde...........

비록 e와 b 사이에 하나의 공간, d와 c 사이에 2 개, 다른 것 사이에 3 개의 공간이 있지만 N-1에게 무슨 일이 있었나요? 이 경우 a...e“하나의 블록”이됩니다. 여기에 1을 곱하여 올바른 위치에있게되므로 “무료로 e를 얻습니다”. b와 d의 경우도 마찬가지입니다 (b는 오른쪽에 세 개의 공백이 필요하고 d는 왼쪽에 같은 세 개의 공백이 필요함). 따라서 매직 넘버를 계산할 때 중복이 있음을 알 수 있습니다.

a: << 0  ( x 1    )
b: << 5  ( x 32   )
c: << 11 ( x 2048 )
d: << 5  ( x 32   )  !! duplicate
e: << 0  ( x 1    )  !! duplicate

분명히,이 숫자들을 다른 순서로 원한다면, 더 많은 간격을 두어야 할 것입니다. 우리는 다음과 같은 (N-1)규칙을 재구성 할 수있다 : “비트 사이에 최소한 (N-1) 개의 공백이 있거나 항상 최종 결과의 비트 순서를 알고있는 경우 비트 b가 m의 위치에 있으면 n, 왼쪽에는 m-1, 오른쪽에는 nm가 0이어야합니다. “

@Ternary는 “목표 영역의 오른쪽에”비트를 추가 할 수있는 비트, 즉 우리가 찾고있는 비트가 모두 비트 일 때이 규칙이 제대로 작동하지 않는다고 지적했습니다. 16 비트 워드에서 5 개의 꽉 채워진 비트로 위에서 설명한 예를 계속하십시오.

a...e.b...d..c..

간단히하기 위해 비트 위치의 이름을 지정합니다. ABCDEFGHIJKLMNOP

우리가 할 수학은

ABCDEFGHIJKLMNOP

a000e0b000d00c00
0b000d00c0000000
000d00c000000000
00c0000000000000 +
----------------
abcded(b+c)0c0d00c00

지금까지, 우리는 아래에 아무것도 생각 abcde(위치 ABCDE@Ternary 지적으로 문제가되지 있지만, 사실, 경우 것입니다) b=1, c=1, d=1다음 (b+c)위치에 G약간 위치로 수행하게됩니다 F것을 의미 (d+1)위치 F에 약간 수행됩니다 E– 우리 결과는 버릇입니다. c곱셈으로 인해 가장 중요하지 않은 비트에서 0으로 채워지는 패딩이 발생하기 때문에 가장 중요하지 않은 관심 비트 ( 이 예제에서) 오른쪽의 공간 은 중요하지 않습니다.

따라서 (m-1) / (nm) 규칙을 수정해야합니다. “정확하게 (nm) 사용되지 않은 비트가 오른쪽에있는 비트가 두 개 이상인 경우 (위의 예에서 패턴의 마지막 비트는 계산하지 않음-“c “) 규칙을 강화해야합니다. 반복적으로 그렇게하십시오!

우리는 (nm) 기준을 만족하는 비트 수뿐만 아니라 (n-m + 1)에있는 비트 수도 살펴 봐야합니다. 그 숫자를 Q0 (정확히 n-m다음 비트), Q1 ( n-m + 1), 최대 Q (N-1) (n-1). 그러면 우리는

Q0 > 1
Q0 == 1 && Q1 >= 2
Q0 == 0 && Q1 >= 4
Q0 == 1 && Q1 > 1 && Q2 >=2
... 

이것을 보면 간단한 수학적 표현을 쓰면

W = N * Q0 + (N - 1) * Q1 + ... + Q(N-1)

결과는 W > 2 * NRHS 기준을 1 비트 증가시켜야합니다 (n-m+1). 이 시점에서 작업은 안전합니다 W < 4. 그래도 문제가 해결되지 않으면 기준을 한 번 더 늘리십시오.

위의 내용을 따르면 대답에 먼 길을 갈 것이라고 생각합니다 …

답변

(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.exe /m /smt2 ExtractBitsThroughAndWithMultiplication.smt2

sat
(model
  (define-fun mask () (_ BitVec 64)
    #x8080808080808080)
  (define-fun multiplicand () (_ BitVec 64)
    #x0002040810204081)
)

  a00b000c
+ 0b000c00
+ 00c00000
= abc.....

  a0b0000c
+ 0b0000c0
+ 00c00000
= abX.....

  a000b0c0
+ 0b0c0000
+ b0c00000
= Xbc.....

  a000bc000d
+ 0bc000d000
+ 000d000000
= abcd000000

  a000b00c000d
+ 0b00c000d000
+ 00c000d00000
+ 000d00000000
= abcdX.......

+ a0000b00c000d00
+ 0b00c000d000000
+ 00c000d00000000
+ 000d00000000000
= abcd...0X......