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

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



Hi Ben,
The patch had one other problem with it, it was calling one of the new
functions I made for you from the wrong place.  Could you replace it with
the following?  I believe this fixes both the earlier problem you sent and
the smooth_is_bounded proof (though grind doesn't finish the proof - let
me know if you believe it should).

And please don't worry about sending too much - if you see something wrong
in PVS (or even merely annoying), I want to know about it.

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-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,
> 
> I managed to uncover a different error, using a nice simple theory:
> example: THEORY                                                            
> BEGIN                                                                      
> 
>   smooth(divisor: real, new_val: real, old_val: real): real =              
>     (new_val - old_val) / max(divisor, 1) + old_val                        
> 
>   smooth_is_bounded: THEOREM                                               
>     FORALL(divisor: real, new_val: real, old_val: real):                   
>       LET result = smooth(divisor, new_val, old_val) IN                    
>         min(new_val, old_val) <= result AND result <= max(new_val, old_val)
> 
> END example                                                                
> 
> 
> If I try to prove “smooth_is_bounded” using (grind), I get the error:
> Error: the assertion (= (length types1) (length types2)) failed.
>   [condition type: simple-error]
> 
> Please let me know if I’m spamming you, and thanks for all of your help.
> 
> Best Regards,
> Ben Hocking
> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx