[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(TRUE) o bv) *2^-116 where bv is of length 55. Next what I
want to do is to transform it to
bv2int(fill(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(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