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

[Sam Owre <owre@csl.sri.com>]

Hi Nikhil,

What you're describing sure sounds like a bug to me.  Could you please
send me your specs, and a brief description of how to recreate the
problem?

Thanks,
Sam Owre

Nikhil D. Kikkeri <nikhil23@hotmail.com> wrote:

> From: "Nikhil D. Kikkeri" <nikhil23@hotmail.com>
> To: pvs-help@csl.sri.com
> Date: Thu, 29 Jun 2006 01:24:35 +0530
> Subject: [PVS-Help] Regarding "replace", "name-replace"  w.r.t bv2int
> 
> Hi--
> 
> 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,
> 
> rgds
> -Nikhil
> 
> 
> ---
> http://engr.smu.edu/~nikhil