[SMT-LIB] "typecast" for bitvec?

[Jun Koi]

On Thu, Sep 8, 2011 at 12:15 PM, Christopher L Conway
<cconway at cs.nyu.edu> wrote:
> Jun,
>
> You can use concat, e.g.,
>    (assert (= a64 (concat #x00000000 a32)))
>
> Alternatively, if you want sign-extension,
>    (define-fun sign-extend-32-64 ((x (_ BitVec 32))) (_ BitVec 64)
>      (concat (if (= ((_ extract 31 31) x) #b0) #x00000000 #xffffffff) x))
>    (assert (= a64 (sign-extend-32-64 a32))
>

this is awesome, Chris :-)

so here is my code, just in case someone finds that useful.


(set-logic QF_BV)
(declare-fun a64 () (_ BitVec 64))
(declare-fun a32 () (_ BitVec 32))
(define-fun extend-32-64((x (_ BitVec 32))) (_ BitVec 64) (concat #x00000000 x))
(assert (= a64 (extend-32-64 a32)))
(check-sat)


thanks!
Jun