我一直在尝试使用Z3来证明某些SIMD矢量化，在尝试对有条件地在位或通道(例如Intel_mm_shuffle_epi8(周围移动的SIMD操作建模时遇到了问题
当我尝试将符号high和low与似乎不受支持的Extract一起使用时，会出现问题：
assert a.sort() == BitVecSort(128)
assert b.sort() == BitVecSort(128)
Extract( Extract(i+3,i,b)*8+7, Extract(i+3,i,b)*8, a)
中的结果
z3.z3types.Z3Exception: Symbolic expressions cannot be cast to concrete Boolean values.
问题似乎有两个方面：
Z3似乎不支持象征性大小的BitVecs
>>> a = Int('a')
>>> b = BitVec('b', a)
ctypes.ArgumentError: argument 2: <class 'TypeError'>: wrong type
会很整洁，但唉。因此，Extract需要能够知道其返回值的精确BitVec排序，并要求high和low都是具体的，尽管看起来唯一真正的要求应该是simplify(high - low)产生具体的值。
正确的做法是什么？
SMTLib位向量逻辑仅针对具体的位大小进行定义。这不仅仅是一个疏忽：这是逻辑的一个基本限制：没有一个决策过程可以决定比特向量公式的正确性，因为比特向量公式可以根据符号大小而变化。典型的例子是：
x <= 7
如果CCD_ 10是大小<3，那么以上都是真的，否则就不是了。如果这看起来是人为的，请考虑以下内容：
x*x <= x+x+x
同样，如果x是2比特宽，这是真的，但如果它是3比特宽，则不是真的。因此，SMTLib要求所有比特向量大小在规范时都是具体的。请注意，可以编写适用于任意位大小的高级程序，但一旦它们被渲染并发送到解算器，所有位向量大小都必须是已知的具体常数。
关于您关于Extract的问题。严格地说，你们是对的，最终长度的具体性就足够了。但是z3py是SMTLib之上的薄层，它并没有做这样的简化。"具体性"要求源自对相应SMTLib功能的类似限制：
All function symbols with declaration of the form ((_ extract i j) (_ BitVec m) (_ BitVec n)) where - i, j, m, n are numerals - m > i ≥ j ≥ 0, - n = i - j + 1 "
请参阅此处：http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml请注意，由于这个原因，甚至逻辑本身也被称为"FixedSizeBitVectors"，而不仅仅是"BitVectors"。
然而，提取一个固定大小的块并不难，只需通过lo进行右移，并屏蔽/提取所需的比特数量：
((_ extract 7 0) (bvlshr x lo))
如果你的块大小不是恒定的，那么你又一次进入了符号位向量大小的世界，SMTLib出于我上面提到的原因避免了这种情况。(这也是为什么extract将具体整数作为自变量，并用有趣的SMTLib表示法来表示自变量是具体值的原因。(
如果你必须使用"符号"字号，你最好的办法是编写你的程序，并通过确保每种情况下的字号都是具体的来分别证明你感兴趣的每个"符号"大小。(本质上是为您感兴趣的所有尺寸进行案例分割。(
是的，high/low需要是常量，这样得到的类型才是静态已知的。您可以使用shift和/或mask来执行您想要的操作，不过您需要固定输出的最大大小。