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

bvredxnor()：对给定位向量的位进行异或运算。

如果我遵循此处给出的示例(example of universal quantifiers with C API)，我不知道应该为函数的参数(位向量)提供哪种类型

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

查看C API中提供的位向量函数，我注意到所有参数的类型都是Z3_ast，所以我想我可以使用相同的泛型类型。但是API中没有生成Z3_ast排序的函数...(写这篇文章我觉得我触及了类型和排序的区别，但它仍然有点不清楚)

解决方案是使用未解释的排序吗？如果是这样的话，在这样做的时候，我会不会因为过度放大类型而失去了模型中的一些精度，而这个人工制品只是为了调试目的？我的意思是，如果我将此函数应用于位向量，会起作用吗？

提前谢谢您，

股份公司

推荐答案

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

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

该属性表示至少有5个不同的位向量值。如果x的定义域的长度至少为3，则为真，否则则不是。因此，声明的有效性取决于域。通常，您也可以将其视为SMTLib一阶特性的限制。

当然，上述情况适用于SMTLib，而不一定适用于Z3。Leo和Co一直走在曲线的前面，Z3确实有很多技巧超出了SMTLib的要求。如果Z3以您所描述的方式支持参数位向量问题的某些概念，那将是一个惊喜。