Z3:int2bv 的异常 [英] Z3: an exception with int2bv

问题描述

(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?

I am confused about the exception "int2bv expects one parameter" caused by the code above, how to use function int2bv correctly?

推荐答案

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

This is because int2bv is a parametric function and the SMT2 syntax for these is (_ f p1 p2 ...), so in this case the correct syntax is

((_ int2bv 32) a)

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

Note that int2bv is essentially treated as uninterpreted; the API documentation says:

注意.这个函数本质上被视为未解释的.所以你不能指望 Z3 在用这个函数解决约束时精确地反映这个函数的语义."(来自此处)

"NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function." (from here)

这篇关于Z3:int2bv 的异常的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！