[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Auto-rewrites and instantiations
> 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
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
> 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
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.
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: firstname.lastname@example.org