[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Regarding "replace", "name-replace" w.r.t bv2int


I don't know whether the following is a bug or just a quirk of using bv2int.

The problem is as follows. I have something like 
bv2int(w(x(y(z(arg1,arg2)))))*2^-116 about which I need to prove a certain 
property. The expressions w,x,y,z when used in the fashion shown above 
result in a bitvector of length 118. There are ways to simplify the 
expressions within bv2int which results in

bv2int(fill[63](TRUE) o bv) *2^-116 where bv is of length 55. Next what I 
want to do is to transform it to

bv2int(fill[63](TRUE) o bv)*2^(63 - (d-1))*2^-116 + (2^(63 - (d - 1)) - 
1)*2^-116 and then

subsequently getting it to the form

(2*bv2int(fill[63](TRUE) o bv + 1)*2^-d)/2^53 - 2^-116. Of course, the above 
is true only when

(d-1) = 63.

I have a few lemmas that should allow me to do the replacements. However, I 
noticed that for some reason I am not able to rewrite any of the terms 
involving bv2int in the consequent. I can rewrite the same term in the 
antecedent though. In fact even name-replace does not work for the bv2int 
expression in the consequent. However, also, I noticed that name-replace 
works in the early stages of the proof (namely when most of the expressions 
have not been expanded and rewritten). Same applies for replace as well.

I have checked my specifications for any inconsistencies that might prevent 
the rewrites but they appear to be clean.

Any suggestions on why something like this might occur and how can I work 
around it? I am using PVS 3.2

Thank you,