CODEWITHSUNDEEP
z3bitvector
mmpourhashem
mmpourhashem

Reputation: 91

How to extract from a bit-vector using parameters with "Int" datatype?

Is there any efficient way to extract the bit number i from a bit-vector, while i has Int datatype? In other words, is there any efficient smt script that can do what the following script does?

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

Thank you in advance.

Upvotes: 0

Views: 577

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

Not really, you need to create a "big" if-then-else term that does case analysis on bv-index and then uses the (_ extract index index) function, where "index" has to be a constant.

Upvotes: 1

Related Questions