Z3 : 关于 Z3 int2bv 的问题? [英] Z3 : Questions About Z3 int2bv?

问题描述

我对 Z3(smt2 格式)操作 int2bv 有点困惑.我写了一个这样的smt2表达式:

I'm a little confused with the Z3 (smt2 format ) operation int2bv . I wrote a such smt2 expression :

(declare-const t1 Int)
(assert (= ((_ int2bv 2) t1) #b11))
(check-sat)
(get-model)

当我用 Z3 解决它时，它得到了:

when I solve it with Z3 ,it got:

sat
(model 
  (define-fun t1 () Int
    0)
)

这样对吗?t1不应该是3吗?我认为 int2bv 操作只是将 int 值转换为等效的 bitvector 值.但好像不是！

Is that correct? Shouldn't t1 be 3? I thought the int2bv operation just transform the int value to the equivalent bitvector value. But it seems not!

谢谢！

推荐答案

int2bv 函数本质上是作为未解释的(如文档中所述)处理的，因此语义不精确.之前有一些关于这些转换函数的问题，它们可能在这里也有帮助:

The int2bv function is essentially handled as uninterpreted (as stated in the documentation), so the semantics are not precise. There have previously been a few questions about those conversion functions, they might be helpful here too:

Z3:int2bv 的异常

使用 Z3 检查溢出

bv-enable-int2bv-propagation 选项

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