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

Re: [PVS-Help] Very slow proveit/PVS proofs



Hi Ben,
There was a bug in that fix, could you try the following replacement?

By the way,(grind) didn't cause the bug for me, it was (model-check),
which is your default for TCCs that don't have "int" in their name - I
don't know if there is a discrepancy between us that I should look into.
Please let me know if there is.

Thanks,
Sam

(in-package :pvs)

(defmethod judgement-types* ((ex branch))
  (multiple-value-bind (then-types then-jdecls)
      (judgement-types* (then-part ex))
    (multiple-value-bind (else-types else-jdecls)
	(judgement-types* (else-part ex))
      (when (or then-types else-types)
	(cond ((equal then-types else-types)
	       (values then-types then-jdecls))
	      ((and (vectorp then-types) (vectorp else-types))
	       (let ((comp-types (join-compatible-vector-types
				  then-types else-types (type ex))))
		 (when comp-types
		   (values comp-types
			   (jdecls-union then-jdecls else-jdecls)))))
	      ;; May have to convert a vector, might be better the other way
	      (t (let* ((ttypes (jtypes-to-types then-types (then-part ex)))
			(etypes (jtypes-to-types else-types (else-part ex)))
			(comp-types (join-compatible-vector-types ttypes etypes (type ex))))
		   (when comp-types
		     (values comp-types
			     (jdecls-union then-jdecls else-jdecls))))))))))


(defun join-compatible-vector-types (types1 types2 type)
  (assert (= (length types1) (length types2)))
  (let ((ntypes (make-array (length types1) :initial-element nil)))
    (dotimes (i (length types1))
      (let ((t1 (svref types1 i)))
	(if (and (car t1) (symbolp (car t1)))
	    ;; This is for a record type
	    (let ((t2 (find (car t1) types2 :key #'car))
		  (fld (find (car t1) (fields type) :key #'id)))
	      (assert t2)
	      (assert fld)
	      (setf (aref ntypes i)
		    (if (tc-eq t1 t2)
			t1
			(cons (car t1) (join-minimal-types (cdr t1) (cdr t2))))))
	    ;; Else a tuple type
	    (setf (aref ntypes i)
		  (join-compatible-types t1 (svref types2 i) (nth i (types type)))))))
    ntypes))

;; types1 and types2 are both minimal types lists, and are compatible
;; result is new list of minimal types.
;; 2 has mintypes (even_int, posint), 3 has (odd_int, posint)
;; the result is (posint), as even_int is not a subtype of anything in 
;; Suppose types1 = (a1 b1 c1), so the given ex1 has these minimal types
;;     and types2 = (a2 b2 c2), ex2 has these minimal types
(defun join-minimal-types (types1 types2 &optional rem min)
  (if (null types1)
      (join-minimal-types* types2 min rem)
      (if (member (car types1) types2 :test #'tc-eq)
	  (join-minimal-types (cdr types1)
			      (remove (car types1) types2 :test #'tc-eq)
			      rem (cons (car types1) min))
	  (let ((ty2 (find-if #'(lambda (ty2) (strict-subtype-of? (car types1) ty2)) types2)))
	    (if ty2
		(join-minimal-types (cdr types1) (remove ty2 types2)
				    rem (cons ty2 min))
		(join-minimal-types (cdr types1) types2
				    (if (null rem)
					(car types1)
					(let ((ctype (compatible-type rem (car types1))))
					  (unless (some #'(lambda (mty) (subtype-of? mty ctype))
							min)
					    ctype)))
				    min))))))

(defun join-minimal-types* (types2 min rem)
  (if (null types2)
      (if rem
	  (cons rem min)
	  min)
      (if (and rem (subtype-of? rem (car types2)))
	  (join-minimal-types* (cdr types2) min rem)
	  (join-minimal-types* (cdr types2) min
			       (if (null rem)
				   (car types2)
				   (let ((ctype (compatible-type rem (car types2))))
				      (unless (some #'(lambda (mty) (subtype-of? mty ctype))
						    min)
					ctype)))))))

Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

> Hi Sam,
> 
> It seems that the new patch introduced some problems. I'm now getting errors on many proofs that used to work, usually when I run the (grind) strategy (a personal favorite of mine, I'm afraid).
> 
> Here's a relatively simple theory that generates the message "Error: Attempt to take the car of 256 which is not listp.":
> 
> 
> Here's another pair of theories (LookupTestWithTheorems uses LookupTest), that generates the message "Error: No next method for method":
> 
> 
> 
> I have other theories I can provide that are having these problems, but I believe all of my error messages so far fall into one of those two general camps.
> 
> Best Regards,
> Ben Hocking
> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> 
> 
> 
> 
> > On Nov 15, 2014, at 7:39 PM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> > 
> > Outstanding, Sam. At least for the test 3d-lookup table it worked quickly:
> > ~Tools/Simulink2PVS/com.dci.simulink2pvs
> > ▶ time proveit -is lookup3d.pvs
> > Processing ./lookup3d.pvs. Writing output to file ./lookup3d.summary
> > Proving chain of imported theories
> > Proof summary for theory lookup3d
> >    Theory totals: 3 formulas, 3 attempted, 3 succeeded (6.41 s)
> > Grand Totals: 3 proofs, 3 attempted, 3 succeeded (6.41 s)
> > proveit -is lookup3d.pvs  8.71s user 0.29s system 90% cpu 9.896 total
> > 
> > ~Tools/Simulink2PVS/com.dci.simulink2pvs
> > ▶ time proveit -is ndlookup_with_theorems.pvs
> > Processing ./ndlookup_with_theorems.pvs. Writing output to file ./ndlookup_with_theorems.summary
> > Proving chain of imported theories
> > Proof summary for theory ndlookup_with_theorems
> >    test1.................................untried             [Untried]( n/a s)
> >    Theory totals: 1 formulas, 0 attempted, 0 succeeded (0.00 s)
> > Proof summary for theory ndlookup
> >    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s)
> > Grand Totals: 6 proofs, 5 attempted, 5 succeeded (0.00 s)
> > proveit -is ndlookup_with_theorems.pvs  0.69s user 0.11s system 92% cpu 0.857 total
> > 
> > ~Tools/Simulink2PVS/com.dci.simulink2pvs
> > ▶ pvs ndlookup_with_theorems.pvs 
> > 
> > ~Tools/Simulink2PVS/com.dci.simulink2pvs
> > ▶ time proveit -is ndlookup_with_theorems.pvs
> > Processing ./ndlookup_with_theorems.pvs. Writing output to file ./ndlookup_with_theorems.summary
> > Proving chain of imported theories
> > Proof summary for theory ndlookup_with_theorems
> >    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s)
> > Proof summary for theory ndlookup
> >    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s)
> > Grand Totals: 6 proofs, 6 attempted, 6 succeeded (0.00 s)
> > proveit -is ndlookup_with_theorems.pvs  0.73s user 0.09s system 98% cpu 0.828 total
> > Over the next week I'll have the opportunity to test it with some bigger lookup tables. I'll let you know how that goes.
> > 
> > Thanks again!
> > 
> > Best Regards,
> > Ben Hocking
> > ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> > 
> > 
> > 
> > 
> >> On Nov 15, 2014, at 7:27 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:
> >> 
> >> Hi Ben,
> >> 
> >> I haven't tested it thoroughly, but could you try the following patch and
> >> see if it fixes the problem?  Just put the patch file in a
> >> lib/pvs-patches/ subdirectory of your PVS installation (create it if
> >> needed).
> >> 
> >> Let me know what you find.
> >> Thanks,
> >> Sam
> >> 
> >> <patch-20141114.lisp>
> >> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> >> 
> >>> As a follow-up, I’ve tried the following steps: 1) I separated out the 2-d and 3-d lookup tables. The
> >>> 2-d lookup table has its two TCCs proven in 66 seconds. 2) I tried making the TCC strategy be simply “
> >>> (assert)” using:
> >>> %|- *_TCC* : PROOF
> >>> %|-   (assert)
> >>> %|- QED
> >>> 
> >>> Even so, the 3-d lookup table is still running:
> >>> 
> >>> 
> >>> 
> >>> Best Regards,
> >>> Ben Hocking
> >>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> >>> 
> >>>   On Nov 14, 2014, at 9:13 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> >>> 
> >>>   I’m representing a small 2-d and a small 3-d lookup table in PVS using the following code:
> >>>   <ndlookup.pvs>
> >>> 
> >>>   As you can see the PVS theory is not extremely complex and is only 224 lines (include blank lines).
> >>>   However, it seems to take forever* just to get PVS to discharge the TCCs. Is there anything I can do
> >>>   to help the process?
> >>> 
> >>>   *For the file I’m attaching here, I started the process at 8:56 AM (Japan Standard Time) and it is
> >>>   now 9:13 AM and the proof is still running. I had started a proof yesterday that took hours before I
> >>>   gave up, but I realized that I had some suggested proof strategies other than the default so I
> >>>   removed all such strategies (and deleted the pvs-bin folder just to be safe) and started again. The
> >>>   last several lines of the still-being-modified ndlookup.summary file look like:
> >>>   Context changed to /Users/Dependable/Tools/Simulink2PVS/com.dci.simulink2pvs/
> >>>   Parsing ndlookup
> >>>   ndlookup parsed in 0.17 seconds
> >>>   Typechecking ndlookup;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:;;; Finished GC
> >>>   ;;; GC:%                                                                                            
> >>> 
> >>>   I’m attaching that file in its current state as well in case it helps:
> >>>   <ndlookup.summary>
> >>> 
> >>>   Thank you for any help,
> >>>   Ben Hocking
> >>>   ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> >>> 
> > 
>