时间戳

首页 > 解决方案 > 在 Z3 中创建可变宽度蒙版约束

z3 - 在 Z3 中创建可变宽度蒙版约束

问题描述

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

有什么想法可以更有效地解决这个问题，或者解决宽度问题吗？

标签： z3smt

解决方案

目前尚不清楚您要做什么，发布实际代码总是更有帮助。但是，根据您的描述，您可以简单地先向左移动，然后再向右移动。这将从底部推动 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 基于一个非常简单的一阶类型系统。所以，是的：几乎所有位向量操作都必须具有与参数完全相同的大小。这是设计使然：可变长度位向量在逻辑中根本不可用，因为它会使它变得无用，因为公式的可满足性取决于您将它们实例化到的实际位大小。

如果这没有帮助，我建议您发布您正在尝试做的事情和您遇到的问题的实际代码片段。例子越具体越好。

推荐阅读