如何使用「Int」數據類型的參數從位向量中提取？

Question

是否有任何有效的方法從位向量中提取位號i，而i有Int數據類型？換句話說，是否有任何有效的smt腳本可以完成以下腳本的功能？

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

在此先感謝您。

Answer 1

不是，您需要創建一個「大」if-then-else術語，對bv-index進行案例分析，然後使用（_ extract index index）函數，其中 「index」必須是不變。