0
是否有任何有效的方法从位向量中提取位号i
,而i
有Int
数据类型?换句话说,是否有任何有效的smt脚本可以完成以下脚本的功能?如何使用“Int”数据类型的参数从位向量中提取?
(declare-fun int-index() Int)
(assert (and (>= int-index 0) (<= int-index 21)))
(declare-fun bv1() (_ BitVec 22))
(define-fun getbit ((x (_ BitVec 22)) (bv-index (_ BitVec 22))) (_ BitVec 1)
((_ extract 0 0) (bvlshr x bv-index)))
(assert (= #b1 (getbit bv1 ((_ int2bv 22) int-index))))
(check-sat-using (! smt :bv.enable_int2bv true) :print_model true)
在此先感谢您。