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

[Sanjai Narain]

Thanks, Bruno. Best regards. -- Sanjai

Bruno Dutertre wrote:
> 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