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

*To*: Hanne Gottliebsen <hago@dcs.st-and.ac.uk>*Subject*: Re: Length of proof*From*: Dave Stringer-Calvert <dave_sc@csl.sri.com>*Date*: Thu, 10 May 2001 09:53:07 -0700*cc*: PVS-help <pvs-help@csl.sri.com>*In-Reply-To*: Message from Hanne Gottliebsen <hago@dcs.st-and.ac.uk> of "Thu, 03 May 2001 10:14:29 BST." <Pine.LNX.4.10.10105031011440.1634-100000@kininvie.dcs.st-and.ac.uk>*Sender*: pvs-help-owner@csl.sri.com

Hanne - The following will give you the number of proof steps for each formula in a given theory, not counting (postpone) steps. Is this what you were looking for? Dave (defun proof-sizes-theory (theory) (let ((th (get-theory theory))) (if th (let ((fmlas (remove-if-not #'formula-decl? (append (formals th) (assuming th) (theory th))))) (if fmlas (progn (mapc #'(lambda (x) (format t "Proof of ~a has size ~a~%" (id x) (justification-size (justification x)))) fmlas) nil) (format t "Theory ~a has no formulas" theory))) (format t "No typechecked theory named ~a" theory)))) (defun justification-size (just) (or (and (or (not just) (eq (car (rule just)) 'POSTPONE)) 0) (1+ (reduce #'+ (mapcar 'justification-size (subgoals just))))))) PVS(72): (proof-sizes-theory "list_props") Proof of length_TCC1 has size 1 Proof of member_TCC1 has size 1 Proof of member_null has size 1 Proof of nth_TCC1 has size 4 Proof of nth_TCC2 has size 4 Proof of nth_TCC3 has size 15 Proof of nth_TCC4 has size 12 Proof of append_TCC1 has size 1 Proof of append_null has size 6 Proof of append_assoc has size 1 Proof of reverse_append has size 4 Proof of reverse_reverse has size 12 Proof of length_append has size 1 Proof of length_reverse has size 3 Proof of list_rep has size 1 Proof of every_append has size 1 Proof of every_disjunct1 has size 1 Proof of every_disjunct2 has size 1 Proof of every_conjunct has size 1 Proof of every_member has size 2

- Prev by Date:
**prove theory with strategy** - Next by Date:
**Re: Length of proof** - Prev by thread:
**Length of proof** - Next by thread:
**Re: Length of proof** - Index(es):