问题标签 [bitvector]

我正在研究验证机器代码程序。由于许多现代 SMT 求解器有效地支持数组，我计划在我们的验证工具中使用它们。我正在玩 z3，我注意到对公式的微小更改会导致超时。

以下是我使用的两个示例：

1) http://rise4fun.com/Z3/e4Ci *公式：= (array_32_8_0_1_0 == array_32_8_0_0_0) And (EBP_1_1_0 == EBP_1_0_0) And (Not(array_32_8_0_1_0[EBP_1_1_0 - 0] == array_32_8_0_1_0[EBP_1_0_0])) * 对于这个例子，我感到不安，这很好！

2) http://rise4fun.com/Z3/t8aT *公式：= (array_32_8_0_1_0 == array_32_8_0_0_0) 和 (EBP_1_1_0 == EBP_1_0_0) 和 (Not(array_32_8_0_1_0[EBP_1_1_0 - 1] == array_32_8_0_1_0[EBP_1_0_0])) * 对于这个例子，我得到了一个超时。在我的机器上用 z3.exe 运行一个小时也没有给我任何东西。此示例与 (1) 几乎相同，只是数组访问涉及线性表达式。（看第 16 行 temp-var-4 的定义）

为什么会这样？它是否与位向量和数组理论的结合有关？

这是Gayle Laakmann McDowell在《 Cracking the Coding Interview》一书中的问题之一：

实现一个算法来确定一个字符串是否具有所有唯一字符。如果你不能使用额外的数据结构怎么办？

作者写道：

我们可以通过使用位向量来减少空间使用量。我们将假设，在下面的代码中，字符串只是小'a'写到'z'. 这将允许我们只使用一个 int。

作者有这个实现：

假设我们摆脱了“字符串只是小写'a'通过'z'”的假设。相反，字符串可以包含任何类型的字符，如 ASCII 字符或 Unicode 字符。

是否有与作者的解决方案一样有效的解决方案（或接近与作者的解决方案一样有效的解决方案）？

相关问题：

• 检测字符串是否具有唯一字符：将我的解决方案与“Cracking the Coding Interview？”进行比较
• 解释使用位向量来确定是否所有字符都是唯一的
• 字符串唯一字符
• 实现算法以确定字符串是否具有所有唯一字符
• 确定一个字符串是否具有所有唯一字符？

我有一个函数，它需要一个大小为 2kB 的缓冲区并将某些内容加载到其中。我可以假设该功能正常工作，但我无法对其进行测试。

函数原型是

Unsigned long 是我要加载的块的数量（每个块的大小固定为 2kB），缓冲区是加载内容的地方。

现在我必须逐位遍历缓冲区并找到等于 1 的第一位。

为了确保缓冲区大小为 2kB，我做了一个变量

但是我如何通过字符数组逐位迭代？

这样的事情可以吗？

基本上，如果if条件有效，我只是担心？我可以像那样做'&'吗？

我在使用 common lisp 计算两个位向量之间的距离时遇到问题。

我对 lisp 很陌生，这是我的人工智能作业的最后一道作业问题，我相信我遇到的问题是语法问题。

这是问题：

在由 1 和 0 的列表表示的相同长度的两个位向量之间编写递归函数 DISTANCE。例如，

（距离'（1 0 1 1）'（0 1 0 1））

答案：3

讨论如果向量的长度不同，必须做什么。

据我了解，两个位向量之间的距离只是对两者进行异或运算，然后计算 1。

使用该示例，我们将有 1011 ^ 0101 = 1110 等于 3。

假设这是计算距离的正确方法，那么我的问题是找到一种在 lisp 中进行 XOR 的方法，以及使其递归。

如何获取两个列表并将它们放入我可以使用的格式logxor （如图所示），然后计算结果列表中的 1？

在尝试这样做(logxor '(1 0 1 1) '(0 1 0 1))时，它告诉我 '(1 0 1 1) 不是整数，因此它似乎logxor不适用于列表，这让我不知所措。

您可以提供的任何帮助将不胜感激

谢谢！

我正在使用 C 中的位向量。我的位向量是unsigned long long's。对于大量向量，我需要知道奇偶校验，即 1 的位数，是偶数还是奇数。

确切的值并不重要，只是奇偶校验。我想知道是否有比计算数量和检查更快的方法。我试着想些什么，但什么也找不到。

我希望它如何工作的一个简短示例：

你好计算机科学世界，

我试图回答这个问题。。

位向量只是位数组（0 和 1）。长度为 m 的位向量比 m 指针数组占用的空间少得多。描述如何使用位向量来表示一组没有卫星数据的动态不同元素。字典操作应该在 O(1) 时间内运行。

我的想法是可以使用位向量来存储元素的内存位置，并且由于我们假设没有两个元素具有相同的键，我们可以使用散列函数来存储内存位置并在 O(1) 时间内访问它.

位向量是否存储内存位置？

如果没有，谁能引导我到应许之地。

谢谢

理想情况下，可以“或”表示为位向量的两个数字，但我做不到。请告诉代码中是否有错误或其他问题

给出的错误是

从这个错误中，我了解到 Or 只能用于 bool 变量。我的问题是如何或为 BitVectors

我想对一些 SMT 求解器进行基准测试，而 SMT-LIB 基准存储库 [1,2] 似乎是一个不错的起点。

但是，该链接已关闭至少几天。有谁知道我可以找到这些基准的其他地方吗？

[1] http://www.smtlib.org/

[2] http://smtexec.org/exec/smtlib-portal-benchmarks.php

编辑：

基准现在在这里：

[1] http://smtlib.cs.uiowa.edu/benchmarks.shtml

我想使用 Z3 对位向量进行推理。除了可满足性决定之外，我还想要位向量的符号表示，以便我可以根据需要对它们应用我自己的计算。例如：

让，

1. X[3:0], Y[3:0], Z[4:0] 被声明为位向量而不初始化任何值
2. 打印 X[3:0]
3. X[3:0] <- X[3:0] >> 1（逻辑移位）
4. 打印 X[3:0]
5. Z[4:0] <- X[3:0] + Y[3:0]
6. 打印 Z[4:0]
7. …………

所需的输出（像这样的符号）：

使用Z3可以做到这一点吗？

我在我的软件中做了很多位向量操作。例如：假设我需要存储有关候选人“n”的布尔信息，我执行以下操作：

我在阅读该信息时遵循类似的程序：

同时，我还将information_vector写入磁盘并再次读取。现在，我正在尝试解决一个让我做噩梦的错误，让我觉得 Endianess 可能是这里的罪魁祸首，但我无法解释。有什么办法可以查吗？这种位向量操作通常是安全的并且跨架构吗？

我还看到，在代码的某处，我在另一个位向量中为同一候选者设置了一些其他信息：

我通常通过对这些位向量进行与运算来找到一组共同的属性。