问题标签 [bitvector]

比较两个位向量的最有效方法是什么？在 Objective-C 中，我使用 CFBitVectors 并简单地比较两者中的每一位：

哪个工作正常，但我不确定是否有更有效的方法来使用位运算符。

是否有任何用于位向量（QF_BV 逻辑）的工具，它将象征性地执行操作并根据位向量的符号值返回输出，以便我可以根据需要对它们应用我自己的计算？或者是否有任何 SMT 求解器可以在位爆破后提取变量的符号值？例如：

让，

1. X[3:0], Y[3:0], Z[4:0], W[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. 打印 Y[3:0]
8. W[4:0] <- Y[3:0] + 0000
9. 打印 W[4:0]
10. …………

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

假设我有以下约束

如何在stp的c/c++接口中编写相应的代码？我的应用程序需要解决与此类似的约束集。任何帮助表示赞赏。

我正在尝试编写一个函数，该函数接受三个位向量，表示从位置 1-9 开始数独谜题的行、列和块中使用的数字。一个单元格只能使用未使用的数字，并且该函数应该返回所有向量中的数字是否强制一种可能性或是否存在多种可能性。我认为这意味着我必须合并所有三个向量，然后确定结果模式中“未设置”位的位置。

然而，我的函数在 gdb 中似乎并没有返回正确的掩码，即使它是受到这个推导的启发：http: //graphics.stanford.edu/~seander/bithacks.html#MaskedMerge

我正在尝试将一组合并到两组中，然后将第三组合并到前一个合并中，得出最终合并中 1 的数量，然后减去它以得出有多少个 0。

然后，我编写了以下函数：

完全初学者在深端跳跃。这是我在此的头一篇博文。

我是一名大型机程序员，试图加入 1990 年代并学习一些面向对象的编程（目前对我来说是希腊语）。请原谅我下面的基本解释。

我正在开发一个应用程序，该应用程序需要为 Sql Server DB 上的人员保留可用性日历。由于我可以有数万（或更多）行，我希望尽可能高效而不浪费空间。

对 C# 来说完全是绿色的，我遇到了 BitVector 32，并意识到如果我简单地忽略 0 位，我将在每个月的每一天都有一个布尔值（True/False 来描述每个人的可用性）（32 位代表 31一个月中的几天，还有一些留在二月等）。

这处理一个月，但我可以创建一个包含 12 个 bitvector32 值的数组，并将全年覆盖在 48 个字节中（bitvector32 使用 4 个字节 X 12 个月）。

通过隔离各个位来实例化和填充 bitvector32 结构没有问题。然后，我将 availability.data 传递给一个方法，将其写入定义为 Int 值的 Sql Server 表：

我的问题是我的下一个程序，我需要读取这个整数值并将其转换或转换（？）回 Bitvector32 格式。

我试过这个：

但我收到错误“无法将类型'int'隐式转换为'System.Collections.Specialized.Bitvector32”

我正处于确定这个过程的边缘，我怀疑它是一个简单的关键字或演员，但我一直没能找到它。有任何想法吗？

另外，这是正确的方法吗？我不想一整年都做一个会占用多余空间的布尔数组。

任何输入将不胜感激。

我正在尝试为我的 SQL Server 数据库上的数千人有效地存储和访问一个布尔值（表示“可用性”）。他们会给我他们不可用的日期，我需要代表他们并根据时间表以编程方式处理它们。

换句话说，我需要能够跟踪每个人一年中每一天的可用性（简单的是/否或真/假就足够了）。

我遇到了 Bitvector32 结构并让它工作得很好（参见背景链接：如何在我的 C# 程序中将 SQL Server 'Int' 字段转换为 'BitVector32'？）。我能够创建它，将它作为 int 写入我的数据库，然后将它恢复到我的 C# 程序中。

问题是，我希望能够通过 SQL 访问此结构中包含的布尔值，但我做不到。

我的下一个选项是只为我当时需要的指定日期创建一个布尔值数组（24 次出现），并将其存储在我的 sql 服务器表中以包含每个人的 Y/N。但是，作为新手，我听说 SQL Server 不处理数组。唯一的选择是在 SQL Server 中定义 24 个唯一命名的“位”字段，并从我的 C# 布尔数组中加载它们。这看起来很丑陋。

有没有人看到更好的解决方案或者我很接近？

我有一个位向量，我想将它的一部分复制到另一个向量（例如，为简单起见，复制到另一个向量的开头）。请注意，所有位可能需要在某个方向上移动（或者更确切地说，旋转），而不仅仅是第一个元素，因为每个字节内的位对齐方式会发生变化。

为清楚起见，假设签名是：

并且该数据以字节存储，因此没有字节序问题，并且低位首先出现在向量中。我们可以使签名更复杂以适应其他假设，但暂时不要介意。

所以，

• 是否有一些硬件支持这样做（我的意思是在 x86 或 x86_64 CPU 上）？
• 是否有此功能的一些标准/惯用/广泛使用的实现（或类似的东西）？

以下代码导致 SIGSEV

如果signed==false，那么就不会发生问题。

我在 MAC OS X 上运行 Z3。

有任何想法吗？

我有四个位向量的集合，例如：

我想获得在给定位向量的 0、1、2、3 或 4 中设置的那些位的掩码。因此 m0 将是未在四个位向量中的任何一个中设置的位的掩码，m3 是在恰好三个位向量中设置的那些位的掩码，等等：

使用按位运算符找到这些掩码的最快方法是什么？

我假设这些对 0 位和 4 位的操作最少：

对于其他选项，我不太确定我的方法操作最少：

这是计算这些掩码的最快方法还是我可以做得更快（在更少的操作中）？

在大多数情况下，我需要这些面具中的一个或几个，而不是同时使用所有这些面具。

（注意，实际上我会为 64 位或 128 位向量执行此操作。这可能无关紧要，但我在 32 位 x86 平台上的 C 中执行此操作。）

: 变量 x 定义为 int 排序方式 (declare-const x Int)

有什么方法可以将 x 转换为位向量排序吗？因为有时 x 涉及到 int 理论无法处理的 &、|、^ 等位操作。

我不想在开始时将变量 x 定义为位向量，因为我认为 int 理论支持的操作（例如，+、-、*、/）除了位操作之外的运行速度比位向量中支持的操作快得多。

所以实际上，我想根据需要将 int 排序转换为位向量排序或 vesa 。

谢谢。

陈婷