Z3：int2bv 的异常答案

【问题标题】：Z3: an exception with int2bvZ3：int2bv 的异常
【发布时间】：2014-03-11 12:59:29
【问题描述】：

(declare-const a Int)
(declare-const b Int)
(declare-const c (_ BitVec 32))
(declare-const d (_ BitVec 32))

(assert (= b (bv2int c)))
(assert (= c (int2bv a)))

(check-sat)

我对上面代码导致的异常“int2bv 需要一个参数”感到困惑，如何正确使用函数 int2bv？

【问题讨论】：

问题是int2bv 需要一个大小（正在创建的新位向量的长度对应于整数）。但是，用于指定此的旧语法（(assert (= c (int2bv[32] a)))，例如，将 a 转换为 32 位长的位向量）会给出错误 unexpected character（例如：rise4fun.com/Z3/uOPG），因此语法可能已更改。这是旧用法的示例：stackoverflow.com/questions/8719764/…

标签： z3

【解决方案1】：

这是因为 int2bv 是一个参数函数，而这些函数的 SMT2 语法是 (_ f p1 p2 ...)，所以在这种情况下，正确的语法是

((_ int2bv 32) a)

请注意，int2bv 本质上被视为未解释； API 文档说：

“NB。这个函数本质上被视为未解释的。所以你不能指望Z3在用这个函数解决约束时精确地反映这个函数的语义。” （来自here）

【讨论】：