一次乘法提取位

Question

我看到在使用了一个有趣的技术，答案到另一个问题，并想好一点理解。我们给了一个无符号的64位整数，我们对以下位感兴趣：1.......2.......3.......4.......5.......6.......7.......8.......具体来说，我们希望将它们移动到前八位，如下所示：12345678........................................................我们不在乎由指示的位的值.，也不必保留它们。该溶液是屏蔽掉不需要的位，并且乘以结果0x2040810204081。事实证明，这可以解决问题。这种方法有多普遍？可以使用这种技术来提取位的任何子集吗？如果不是，那么如何确定该方法是否适用于特定的一组位？最后，如何找到正确的（a？）乘法器以提取给定的位？

Answer 1

确实，这是一个非常有趣的问题。我要花两分钱，就是说，如果您可以通过位向量理论上的一阶逻辑来说明这样的问题，那么定理证明就是您的朋友，并且可以为您提供非常快的解决方案您问题的答案。让我们重新陈述定理所要问的问题：

“存在一些64位常量'mask'和'multiplicand'，因此对于所有64位位向量x，在表达式y =（x＆mask）*被乘数中，我们的y.63 == x.63 ，y.62 == x.55，y.61 == x.47，等等。”

如果该句子实际上是一个定理，则确实是常量“掩码”和“被乘数”的某些值满足此属性。因此，让我们用定理证明者可以理解的东西（即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应该可以帮助您入门。

Answer 2

乘法器中的每个1位用于将其中一位复制到其正确位置：

• 1已经在正确的位置，因此请乘以0x0000000000000001。

• 2必须向左移动7位，因此我们乘以0x0000000000000080（设置了位7）。

• 3必须向左移动14位位置，因此我们乘以0x0000000000000400（设置了位14）。

• 以此类推，直到

• 8必须向左移动49位，因此我们乘以0x0002000000000000（设置了位49）。

乘数是各个位的乘数之和。

这之所以起作用，是因为要收集的位不太紧密，因此在我们的方案中不属于一起的位的乘法要么超出64位，要么落入较低的无关位部分。

请注意，原始编号中的其他位必须为0。这可以通过用AND操作屏蔽它们来实现。