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

Re: [PVS-Help] turning off rewrite




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?