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

Re: Proof status of theorems in batch mode



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
> ----------------------------------------------------------