问题描述
我对 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:
bv-enable-int2bv-propagation 选项
这篇关于Z3 : 关于 Z3 int2bv 的问题?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!