0

データ型を持っているi間にビットベクトルからビット番号を抽出する効率的な方法はありますか? つまり、次のスクリプトが行うことを実行できる効率的な smt スクリプトはありますか?iInt

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

前もって感謝します。

4

1 に答える 1

1

実際には、bv-index でケース分析を行い、(_ extract index index) 関数を使用する「大きな」if-then-else 用語を作成する必要があります。ここで、「index」は定数でなければなりません。

于 2015-09-08T03:25:24.587 に答える