问题标签 [bitvector]

我正在处理表示为位向量的集合。最后我看到了像 M & (N-1) 这样的东西。M 和 N 都是集合，都是非空的。

就收藏而言，这意味着什么？

是否可以在 z3Py 中转换BoolRef为一位长？BitVecRef在我的设计中，要求 aBitVecRef从两个其他的比较中返回BitVecRef。这类似于将 pythonbool转换为int. 以下是它的使用示例：

这将是理想的，但(bv1 < bv2)is的类型Boolref，它会引发“排序不匹配”错误。有没有办法将结果转换为可以(bv1 < bv2)断言res等于它的结果？

我是 VHDL 的新手，我正在尝试如下模拟一个块：

1. 它有四个std_logic_vector输入，分别命名为a、和。输入和是有符号数，输入和是无符号数。bcdabcd
2. 它有四个输出，分别名为u、和。输出和 是有符号数，输出和是无符号数。vwxuvwx

3. 输出定义如下：

   u = a + b

   v = a / 2

   w = c * d

   x = c * 2

4. 内部信号是整数。

我能够编译模块和测试台。我遇到的问题是，当我尝试模拟电路时，会显示以下错误消息：

结果，模拟器无法启动。我不明白这条线怎么可能是错误的：

我尝试通过将这一行更改为其他执行相同操作的行，但我在同一行中得到错误。如果我删除此行，第 37 行会报告错误。请给我提示以找出我的错误吗？下面是模块的代码：

我正在尝试在 BitVec 中设置可能允许的字节列表，但我不确定我实际上是否以正确的方式设置了约束。

例如：

让我们调用一个 32 位 BVbv和一个Solver()被调用s：

我希望每个字节都可以是我使用的一个0x2或0x34多个：0xFFExtract()

可悲的是，s.check()回报unsat。

我认为这不是表达这些字节可能是0x2 OR 0x34 OR 0xFF的正确方法。我是否以正确的方式编写了约束，或者我的思维过程完全错误？

我无法理解这两个函数中的位逻辑。

1. 我不知道我们为什么要检查条件（bitVector & mask）== 0。

2. 另外，为什么我们在满足条件时将 bitVector 与掩码进行 OR 运算，否则将 bitVector 与 ~mask 进行 AND 运算？

3. 为什么有一种属性可以“通过从整数中减去一位并将其与原始整数进行与运算来检查是否设置了一位”？

完整代码在这里。

我有一个 RGB 图像，ndarray并希望将它的紧凑抽象计算为位向量，其中每个元素指示像素是否更接近白色。（无需显示此位向量）

我查看了参考资料并找出了一些功能。但到目前为止，我只找到了一种简单的方法来获得ndarray布尔值（这比我的意图多 8 倍）。有没有直接有效的方法来实现我想要的？

到目前为止我所拥有的：

I think I don't understand how BitVecs work in z3. I have written the following code:

I'd expect that this to be "unsat", because there are values inside and outside this range. But when I run s.check(), I get:

This was confusing to me, so I guessed there was overflow involved. But then I tried:

Which confuses me a lot, because it suggests that z3 can model this number using 32 bit BitVecs. Additionally I ran:

Which confused me even more, because it seems clearly incompatible with the second example...

我正在开发一个为用户提供数十万个标志的系统。这些标志在编号上都是连续的，从 0 到 X，无论 X 最终是什么。X 预计会随着时间的推移而增长。我们也期望有很多很多的用户。

我们主要关心的是：

1. 能够快速测试用户是否设置了任何给定的标志。
2. 能够快速设置标志。
3. 能够将数据存储优化到尽可能小的尺寸。

使用 10k 标志，如果我们使用位向量，我们在内存中查看每个用户大约 1k 的数据。这可能太多了。更糟糕的是，这是在 Javascript 中，存储在序列化为 JSON 的文档数据库中，这意味着我们有多个存储选项，但没有一个是我特别喜欢的。

1. 将标志存储为 Uint32Array 对象的 JSON 输出。看起来像："{"0":10,"1":4294967295}"。不幸的是，当标志接近填充状态时，每 4 个字节平均需要 17 个字节，这是内存的 4 倍以上，并且在序列化时会导致大约 5k 的内存。这并不理想。
2. 执行我们自己的 JSON 序列化，使用 base64 以避免数字作为字符串方法的臃肿大小。不幸的是，这为 JSON 输入/输出阶段增加了一个额外的处理步骤，这使事情变得复杂，因为现在我们必须在这个过程中修改我们的数据，这会减慢一切。

所以...暂时搁置位向量的想法。我想知道是否有更好的方法。我考虑使用“范围数组”，例如：

我们可以对这个系统中的数据做一些假设，这就是我采用这种方法的原因：

1. 标志永远不会取消设置。一旦设置，它将保持设置。
2. 标志通常是聚集在一起的。如果设置了标志 X，则很有可能同时设置 X-1 和 X+1。
3. 标志通常会设置为增加的索引值。如果设置了标志 X，则 X-1 比 X+1 更可能被设置，并且 X+1 很可能在不久之后被设置。

因此，由于这些条件，我认为存储范围对象数组可能是最佳解决方案。这样，随着时间的推移，用户的标志最终会浓缩成一个大范围的条目。最理想的情况当然是：

当然，最坏的情况是，如果他们以某种方式设法发现自己​​处于设置其他所有标志的状态。

那会很糟糕。我认为比位向量解决方案差得多。但我们非常有信心这不会发生。

因此，关于快速决定是否设置标志的能力；这只是一个 O(logn) 二进制搜索（因为数组将被排序）；只需找到最接近您的号码的范围对象，检查您的号码是否在该范围内，然后返回。

插入更加棘手。它仍然是二进制搜索，但现在我们正在修改数组。

1. 一个相邻的兄弟插入：最佳方案。我们找到一个范围，其中最小值或最大值与我们插入的数字相差一个，然后简单地减少或增加当前范围的值。O(1)
2. 没有相邻的兄弟节点插入：只需插入一个具有最小值集的新节点。O(n)，因为我们将在数组中向下移动它之后的所有内容。
3. 两个相邻兄弟插入：将最大值更改为右侧兄弟范围的最大值，从数组中删除右侧兄弟范围并将其后的所有内容向左移动。上）。

所以案例 2+3 让我想知道我是否不应该为此尝试使用某种平衡的二叉搜索树。例如，红黑树。

这值得麻烦吗？这是我想太多了吗？

我知道bv2int和int2bv在 Z3 中都作为未解释的函数处理。尽管如此，我仍在寻找解决以下问题的最佳实践：给定一个“小”（< 10 位）位向量索引，如何有效地将其转换为 Int，并在这样的查询中使用：

输出：

谢谢！

有几篇关于在 z3 中将位向量转换为整数（反之亦然）的帖子。例如，请参见此处、 此处和此处。

文档说Z3_mk_bv2int 未被解释：

“......这个函数本质上被视为未解释。所以你不能指望Z3在用这个函数解决约束时精确地反映这个函数的语义......”

但是，我找不到一个无法 反映预期语义的简单示例。例如，每当我使用这样的查询时：

我得到了一个正确的答案（索引应该是 7，它是）

谁能提供一个简单的例子，其中 z3 的 bv2int和/或int2bv失败？谢谢！