[YICES-HELP] Re: [YICES] Question about bitshift

[Bruno Dutertre]

Sanjai Narain wrote:
> The following specification:
> 
> (define-type vm (scalar host))
> (define-type vm_port (scalar e0))
> (define mask::(->  vm vm_port int))
> (assert (=(bv-shift-left0 0b11111111111111111111111111111111 (mask host 
> e0)) 0b11111111111111111111111111111000))
> (check)
> 
> run with "yices -e -tc spec.lisp" gives: Error: [spec.lisp, line(4), 
> column(62), position(163)]: argument must be a number. It insists that 
> the number of left shifts be fixed, not variable. I expect to get the 
> solution (mask host e0) = 3. Any way around this? Thanks. -- Sanjai
> 

Sanjai,

To do what you want, you can define a general bv-shift function,
using if-then-else(s):

(define bv-shift32::(-> (bitvector 32) nat (bitvector 32))
   (lambda (u::(bitvector 32) n::nat)
     (if (= n 0) u
     (if (= n 1) (bv-shift-left0 u 1)
     etc,

There is a significant cost of using such nested if-then-else,
but that should work.

Bruno