任意长度的通用位向量类型

Question

出于与此处所述相同的原因 (user defined uninterpreted function)，我想定义自己的未解释函数

bvredxnor() ：对给定位向量的位进行 xnor。

如果我按照此处给出的示例 (example of universal quantifiers with C API) 我不知道要为我的函数的参数提供什么类型（位向量）

我可以创建一个给定长度的位向量，但我希望它用于任何长度的位向量。

查看 C API 中可用的位向量函数，我注意到所有参数的类型都是 Z3_ast，所以我想我可以使用相同的泛型类型。但是API中没有生成Z3_ast排序的函数......（写这个我感觉我在触摸类型和排序之间的区别，但还是有点不清楚）

是使用未解释排序的解决方案吗？如果是这样，那么在这样做时，我不会通过过度扩大类型来降低模型的精度，而这个人工制品仅用于调试目的吗？我的意思是，如果我将此函数应用于位向量，这会起作用吗？

提前谢谢你，

AG。

Answer 1

SMTLib 确实不 允许具有可变长度的位向量。也就是说，您不能表达在位向量长度上参数化的问题。这样做的原因是，由于基数问题，关于位向量的属性不一定在长度上保持参数化。也就是说，考虑：

exists x0, x1, x2, x3, x4. distinct [x0, x1, x2, x3, x4]

此属性表示至少有 5 个不同的位向量值。如果 x 的域的长度至少为 3，则这是正确的，否则则不然。因此，声明的有效性取决于域。您也可以将其视为一般 SMTLib 一阶性质的限制。

当然，以上适用于 SMTLib，不一定适用于 Z3。 Leo 和 co 一直处于领先地位，Z3 确实有许多超出 SMTLib 要求的技巧。如果 Z3 确实以您描述的方式支持某些参数位向量问题的概念，那将是一个惊喜。