2

出于与此处所述相同的原因（用户定义的未解释函数），我想定义自己的未解释函数

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

如果我按照此处给出的示例（使用 C API 的通用量词示例），我不知道为我的函数的参数提供什么类型（位向量）

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

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

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

先感谢您，

AG。

4

1 回答 1

2

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

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

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

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

于 2012-04-26T16:33:10.237 回答