Re: Length of proof

[Dave Stringer-Calvert <dave_sc@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