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

Re: Auto-rewrites and instantiations


Tamarah -

> PROBLEM 1 : auto-rewriting hangs.
> 
> 
> After using (auto-rewrite -4 -5) and then assert I get infrequent '
> responses of 
> 
> Warning: Rewriting depth = 50; Rewriting with activeRes_execute_5$1
> Warning: Rewriting depth = 100; Rewriting with activeRes_execute_5$1
> 5116296 bytes have been tenured, next gc will be global.
> See the documentation for variable EXCL:*GLOBAL-GC-BEHAVIOR* for more informati
> on.


Here, you have a rewrite that is always enabled after the rewriting has
been performed - ie. it rewrites to something that is rewritable using
the same rule.  Hence the 'rewriting depth' messages.  In your example of
activeRes_execute_5$1, the conclusion will always match the hypothesis.

You can interrupt the prover from the rewriting loop by C-c C-c followed
by (restore) at the Lisp prompt, and you will be returned to the previous
sequent.


> In another example I let this continue and got lots of rewriting messages.
> At a certain point PVS indicated "signal" and I found that the PVS process had 
> died.


This is usally a symptom that PVS has used up all the virtual memory on
your machine, which is fatal.


> PROBLEM 2 : Instantiation
> 
> My question is why doesn't (inst? :ifmatch best) give me an instantiation which
> doesn't generate TCCs since one exists?


As Shankar said in an earlier message to you, we intend to implement a new
flag on inst? which will only allow instantiation where no TCC subgoals
are generated - this has now been logged on the PVS suggestions list.

To clarify the current behavior - it is a little confusing for :if-match
best, as not all generated TCCs are returned to the user, as the prover
tries to discharge them automatically.  So, although using a specific
instantiation with (inst) you get no TCC subgoals, there may have been a
TCC generated but auto-discharged.  Hence "fewest TCCs" really means
fewest TCCs after typechecking, and not fewest TCCs after the prover has
attempted a simple proof of them.

Dave

---
Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory,
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA.
Phone: (650) 859-3291    Fax: (650) 859-2844   Email: dave_sc@csl.sri.com