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

Re: [PVS-Help] turning off rewrite



David,

The AUTO-REWRITE- should work as you said - could you send me your specs
so I can try and diagnose this?

Thanks,
Sam

David Naumann <naumann@cs.stevens.edu> wrote:

> Hi Shankar,
> 
> So I see in *Auto-Rewrites* that after install-rewrites this function <=
> is installed, which confirms the problem.  What I want to do is prevent
> any rewriting with this definition.  Isn't that what the AUTO_REWRITE-
> declaration is for?
> 
> --dave
> 
> On Sat, 22 Jul 2006, Natarajan Shankar wrote:
> 
> > Dave:
> >  The Emacs command M-x show-auto-rewrites should show you the active
> > rewrites in the *Auto-Rewrites* buffer.  You can use the stop-rewrite prover
> > command on the rewrite as named in the *Auto-Rewrites* buffer to stop it.
> >
> > To stop the recursive rewriting loop, you need to arrange the definition so
> > that the measure decreases whenever the top conditional is resolved.
> >
> > -Shankar
> >
> >> I have a recursively defined relation named <= on a datatype which I don't
> >> want to use as a rewrite.  Following the definition of <= I declare
> >>
> >>    AUTO_REWRITE- <= : [dty,dty -> bool]
> >>
> >> But grind on sequents involving <= seems to diverge rewriting it:
> >>
> >>    Warning: Rewriting depth = 50; Rewriting with <=
> >>
> >> I tried (stop-rewrite "myTheoryname.<=") which yields
> >>
> >>    classtableSig.<= is not an auto-rewrite
> >>
> >> How do I determine the installed rewrites, and more importantly uninstall
> >> this one?
> >
>