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

Re: [PVS-Help] Problems with a bigger lookup table

Hi Ben,

There was another bug exposed by the patch I sent; it took me a while to
make sure there wasn't a deeper problem.  I'm including a replacement
patch below.

More memory won't help with this, as it is hitting an internal error that
would be hard to work around.  I believe if you get more memory, then
Allegro will try to use it, but for me grind finished the proof in
reasonable time (on the other hand, I do have 16G of ram).


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

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

(defun join-minimal-types* (types2 min rem)
  (if (null types2)
      (if rem
	  (cons rem 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))

(defmethod judgement-types* ((ex field-application))
  (if (record-expr? (argument ex))
      (multiple-value-bind (jtypes jdecls)
	  (judgement-types* (beta-reduce ex))
	(remove-judgement-types-of-type (type ex) jtypes jdecls))
      (multiple-value-bind (ajtypes ajdecls)
	  (judgement-types* (argument ex))
	(when ajtypes
	  (if (vectorp ajtypes)
	      (let ((pos (position-if #'(lambda (x) (eq (car x) (id ex)))
		(assert pos)
		(let ((entry (aref ajtypes pos)))
		   (type ex) (cdr entry) (when ajdecls (aref ajdecls pos)))))
	       (type ex)
	       (field-application-types ajtypes ex)
Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

> Is it possible that increasing the available memory to pvs-allegro would help, and if so, what would be
> the recommended method for doing so?
> Best Regards,
> Ben Hocking
> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>     On Nov 24, 2014, at 11:02 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
>     Attached is a much larger example of a lookup table. This is the same size as one used for
>     proprietary purposes, but with the proprietary information replaced with non-properietary numbers
>     that have similar relationships. The purpose of the lookup table is to calculate an efficiency value
>     that is between 0 and 1. The theory generates 3 TCCs, the last of which (LookupTable_2_D_TCC3) is
>     the important one, namely that the result is indeed between 0 and 1. If I attempt the proof
>     strategy (skeep)(skeep)(skeep)(grind), I get the following error:
>     Error: `(#<Judgement posrat_div_posrat_is_posrat>)' is not of the
>            expected type `array'
>       [condition type: type-error]
>     Note that I do not get this error if I just try (grind). This uses the patch previously sent to me
>     by Sam Owre (patch-20141114.lisp), although I do not know if it is related to that patch, or whether
>     the problem would exist without it. While it takes a long time to process with the patch, without
>     it, the time required is so long that I have not attempted to ascertain whether it would actually
>     complete.
>     <example_map.pvs>
>     Best Regards,
>     Ben Hocking
>     ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx