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

Question

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

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

如果我按照此处给出的示例( 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 和他的同事一直处于领先地位，而 Z3 确实有许多超出 SMTLib 要求的技巧。如果 Z3 确实按照您所描述的方式支持参数位向量问题的一些概念，那将是一个惊喜。