在 Z3 中创建可变宽度蒙版约束答案

【问题标题】：Creating a variable width mask constraint in Z3在 Z3 中创建可变宽度蒙版约束
【发布时间】：2019-06-24 11:00:07
【问题描述】：

我想在位向量 (X) 上创建一个约束，将另一个位向量屏蔽到其n 最低有效位。我希望这尽可能高效。到目前为止，我尝试将第二个位向量表示为：1<<n - 1，其中n 是另一个位向量。这给了我两个问题：

首先，它大大降低了求解器的速度
其次，可能与第一个有关，我无法将n 的宽度设置为小于X 的宽度。如果我这样做，它会在 n 上出现类型错误而失败。

有什么更有效的方法来解决这个问题，或者解决宽度问题吗？

【问题讨论】：

标签： z3 smt

【解决方案1】：

不清楚您要做什么，发布实际代码总是更有帮助。但是，根据您的描述，您可以简单地先向左移动，然后再向右移动。这将从底部推动 0，然后将它们放下；确保位向量具有最少的n 位。您移动的数量应等于bitsize - n，其中bitsize 是位向量的长度，n 是您要保留的最低有效位的数量。假设您正在处理 64 位向量，它看起来像：

(declare-const n (_ BitVec 64))
(declare-const x (_ BitVec 64))
(define-fun amnt () (_ BitVec 64) (bvsub #x0000000000000040 n))
(define-fun maskedX () (_ BitVec 64) (bvlshr (bvshl x amnt) amnt))

（常量 #x0000000000000040 是您在 SMT-lib 中将 64 写为 64 位位向量常量的方式。）请注意，这隐含地假设 n 最多为 64：如果这不是真的，那么减法将环绕，您将获得不同的约束。我假设您的系统中已经存在一个约束，即 n 最多是您正在处理的位向量大小。

关于效率：确实没有明显的方法可以使这样的位向量约束变得快或慢：这实际上取决于您周围还有哪些其他约束。因此，在不了解您的问题的任何其他信息的情况下，无法确定这是否是实现您想要的最佳方式。当存在符号值时，考虑 SMTLib 中的“速度”通常是没有帮助的，有很多因素会影响求解器的效率。

关于类型：SMTLib 基于一个非常简单的一阶类型系统。所以，是的：几乎所有位向量操作都必须具有与参数完全相同的大小。这是设计使然：可变长度的位向量在逻辑中根本不可用，因为它会使它变得无用，因为公式的可满足性取决于您将它们实例化为的实际位大小。

如果这没有帮助，我建议您发布一个实际代码 sn-p，说明您正在尝试执行的操作以及您遇到的问题。例子越具体越好。

【讨论】：