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

*To*: pvs-help@csl.sri.com*Subject*: Re: Proof status of theorems in batch mode*From*: Sam Owre <owre@csl.sri.com>*Date*: Wed, 21 Jun 2000 14:37:51 -0700*cc*: pvs-help@csl.sri.com*Delivery-Date*: Wed Jun 21 14:38:29 2000*In-reply-to*: Your message of "Wed, 21 Jun 2000 16:12:19 CDT." <39512FB3.B4F8C0C9@ittc.ukans.edu>

Hi, I suspect what you want is something like (defun my-status (theory-name) (dolist (fdecl (all-decls (get-theory theory-name))) (when (formula-decl? fdecl) ;;; Whatever you want to do with fdecl ))) This loops through all the declarations of theory theory-name. Obviously this is for Lisp, not Emacs. The get-theory function returns the theory object if it has already been typechecked, and returns nil if it hasn't. You can use ge-typechecked-theory if you want your function to typecheck it if it needs to, in which case an error will be reported if it cannot be found. All-decls takes a theory and appends the formals, assuming, and theory part of the theory object. Note that IMPORTINGs are mixed in there as well, and these have no id slot (so replacing the formula-decl? test above with (eq (id fdecl) '|F1|) will only work if there are no importings in the theory). Hope this helps, Sam Owre > Date: Wed, 21 Jun 2000 16:12:19 -0500 > From: Makarand <makarand@ittc.ukans.edu> > X-Accept-Language: en > To: pvs-help@csl.sri.com > Subject: Proof status of theorems in batch mode > > HI, > I am looking for a function that tells me the status of a > theorem (whether proved or not). i.e. given a PVS theory: > > A_theory: THEORY > BEGIN > F1: Theorem P(x) > F2: Theorem Q(x) > End A_theory > > I prove F1 and F2 using my proof strategies and now i need to know if > they succeeded. > I need to do this from within a lisp function of my own > as i am running pvs in batch. > > The functions like (STATUS-PVS-FILE) or (STATUS-PROOF-THEORY) > don't help much because i need to interpret (and not just display) > the proof status's of the theorems in my theory. is there a way to write > these buffers > into some file which i can then read again to interpret the proof > status. Surely there is an easier way. > I was looking at (PROVED? FDECL) and (UNPROVED? FDECL) which serve my > prupose, > but then i had trouble getting the right argument. > what and how can i access FDECL? > > Note:- This is all in PVS batch mode so i need a solution that > is noninteractive. > Thanks again. > > ********************************************************** > Makarand Patil > System Level Design Group > Call:- (785) 864 3041 > ----------------------------------------------------------

**References**:**Proof status of theorems in batch mode***From:*Makarand <makarand@ittc.ukans.edu>

- Prev by Date:
**Proof status of theorems in batch mode** - Next by Date:
**Help!** - Prev by thread:
**Proof status of theorems in batch mode** - Next by thread:
**pvs batch mode** - Index(es):