如何在 z3 中声明任意大小的位向量的谓词？

Question

我尝试在 z3 中定义一些关于位向量的规则时遇到了问题。如果我尝试用 z3

解决以下文件

(declare-rel FunnyFun ((_ BitVec 64)))
(declare-var A (_ BitVec 64))
(declare-var B (_ BitVec 64))
(rule (=> (= B (bvadd A #x0000000000000001))
    (FunnyFun B)))

(declare-rel q1 ())

(rule (=> (FunnyFun #x0000000000000001) q1))

(query q1)

我收到错误

(error "query failed: Rule contains infinite sorts in rule <null>:
FunnyFun(#0) :- 
 (= (:var 0) (bvadd (:var 1) #x0000000000000001)).
")

有趣的是，当使用较小的位宽时，z3 立即给出了预期的结果 (sat)：

(declare-rel FunnyFun ((_ BitVec 60)))
(declare-var A (_ BitVec 60))
(declare-var B (_ BitVec 60))
(rule (=> (= B (bvadd A #x000000000000001))
    (FunnyFun B)))

(declare-rel q1 ())

(rule (=> (FunnyFun #x000000000000001) q1))

(query q1)

这是一个错误还是我遗漏了一些约束（我假设 BitVec 可以有任意位宽）？

我尝试了不同的 z3 版本（4.6.0、4.8.3 和 4.8.5），它们都显示了这种行为。

Answer 1

此限制是设计使然。看这里：https://github.com/Z3Prover/z3/issues/1698

如何在 z3 中声明任意大小的位向量的谓词？

How to declare predicates over arbitrary sized bit bit vectors in z3?

z3