----------------------------------------------------------------- how-to-make-patches.txt ----------------------------------------------------------------- The Greve Improvement to Forward Chaining (defthm clock-fn-is-natp (implies (exitpoint (run-fn s k)) (natp (clock-fn s))) :rule-classes (:rewrite :forward-chaining :type-prescription)) (defthm |clock fn is minimal| (implies (and (pre s) (natp n) (exitpoint (run-fn s n))) (<= (clock-fn s) n)) :rule-classes :linear) ----------------------------------------------------------------- Verifying Guards for Too-Many-IFs (mutual-recursion (defun occur-cnt-bounded (term1 term2 a m bound-m) ; Let bound = (+ m bound-m). Return (+ a (* m (occur-cnt term1 term2))) unless ; it exceeds bound, in which case return -1. We assume (<= a bound). ; Occur-cnt is no longer defined, but was defined (as is this function) so as ; not to go inside of quotes, returning a lower bound on the number of times ; term1 occurs in term2. (declare (type (signed-byte 30) a m bound-m)) (the-fixnum (cond ((equal term1 term2) (if (<= a bound-m) (the-fixnum (+ a m)) -1)) ((variablep term2) a) ((fquotep term2) a) (t (occur-cnt-bounded-lst term1 (fargs term2) a m bound-m))))) (defun occur-cnt-bounded-lst (term1 lst a m bound-m) (declare (type (signed-byte 30) a m bound-m)) (the-fixnum (cond ((endp lst) a) (t (let ((new (occur-cnt-bounded term1 (car lst) a m bound-m))) (declare (type (signed-byte 30) new)) (if (eql new -1) -1 (occur-cnt-bounded-lst term1 (cdr lst) new m bound-m))))))) ) (defun too-many-ifs1 (args val lhs rhs ctx) (declare (type (signed-byte 30) lhs rhs)) (cond ((endp args) nil) (t (let ((x (the-fixnum! (count-ifs (car args)) ctx))) (declare (type (signed-byte 30) x)) (cond ((eql x 0) (too-many-ifs1 (cdr args) val lhs rhs ctx)) (t (let ((lhs (occur-cnt-bounded (car args) val lhs x (the-fixnum (- rhs x))))) (declare (type (signed-byte 30) lhs)) (if (eql lhs -1) -1 (too-many-ifs1 (cdr args) val lhs rhs ctx))))))))) (defun too-many-ifs-post-rewrite (args val) ; This function implements the part of the too-many-ifs heuristic after the ; right-hand-side of a definition has been rewritten, to see if that expansion ; is to be kept or thrown away. See the Essay on Too-many-ifs. (let* ((ctx 'too-many-ifs-post-rewrite) (rhs (the-fixnum! (count-ifs-lst args) ctx))) (cond ((int= rhs 0) nil) (t (too-many-ifs1 args val 0 rhs ctx))))) ----------------------------------------------------------------- (mutual-recursion (defun occur-cnt-bounded (term1 term2 a m bound-m) ; Let bound = (+ m bound-m). Return (+ a (* m (occur-cnt term1 term2))) unless ; it exceeds bound, in which case return -1. We assume (<= a bound). ; Occur-cnt is no longer defined, but was defined (as is this function) so as ; not to go inside of quotes, returning a lower bound on the number of times ; term1 occurs in term2. (declare (type (signed-byte 30) a m bound-m) (xargs :measure (acl2-count term2) :ruler-extenders (:lambdas) :guard (and (pseudo-termp term2) (signed-byte-p 30 (+ bound-m m)) (<= 0 a) (<= 0 m) (<= 0 bound-m) (<= a (+ bound-m m))) :verify-guards nil)) (the-fixnum (cond ((equal term1 term2) (if (<= a bound-m) (the-fixnum (+ a m)) -1)) ((variablep term2) a) ((fquotep term2) a) (t (occur-cnt-bounded-lst term1 (fargs term2) a m bound-m))))) (defun occur-cnt-bounded-lst (term1 lst a m bound-m) (declare (type (signed-byte 30) a m bound-m) (xargs :measure (acl2-count lst) :ruler-extenders (:lambdas) :guard (and (pseudo-term-listp lst) (signed-byte-p 30 (+ bound-m m)) (<= 0 a) (<= 0 m) (<= 0 bound-m) (<= a (+ bound-m m))))) (the-fixnum (cond ((endp lst) a) (t (let ((new (occur-cnt-bounded term1 (car lst) a m bound-m))) (declare (type (signed-byte 30) new)) (if (eql new -1) -1 (occur-cnt-bounded-lst term1 (cdr lst) new m bound-m))))))) ) (defun too-many-ifs1 (args val lhs rhs ctx) ; See also too-many-ifs-post-rewrite. ; We assume (<= lhs rhs). (declare (type (signed-byte 30) lhs rhs) (xargs :guard (and (pseudo-term-listp args) (pseudo-termp val) (<= 0 lhs) (<= lhs rhs) (<= (count-ifs-lst args) rhs)))) (cond ((endp args) nil) (t (let ((x (the-fixnum! (count-ifs (car args)) ctx))) (declare (type (signed-byte 30) x)) (cond ((eql x 0) (too-many-ifs1 (cdr args) val lhs rhs ctx)) (t (let ((lhs (occur-cnt-bounded (car args) val lhs x (the-fixnum (- rhs x))))) (declare (type (signed-byte 30) lhs)) (if (eql lhs -1) -1 (too-many-ifs1 (cdr args) val lhs rhs ctx))))))))) (defun too-many-ifs-post-rewrite (args val) ; This function implements the part of the too-many-ifs heuristic after the ; right-hand-side of a definition has been rewritten, to see if that expansion ; is to be kept or thrown away. See the Essay on Too-many-ifs. (declare (xargs :guard (and (pseudo-term-listp args) (pseudo-termp val)))) (let* ((ctx 'too-many-ifs-post-rewrite) (rhs (the-fixnum! (count-ifs-lst args) ctx))) (cond ((int= rhs 0) nil) (t (too-many-ifs1 args val 0 rhs ctx))))) ----------------------------------------------------------------- (verify-termination occur-cnt-bounded) (make-flag occur-cnt-bounded-flg occur-cnt-bounded :flag-var flg :flag-mapping ((occur-cnt-bounded . term) (occur-cnt-bounded-lst . list)) :defthm-macro-name defthm-occur-cnt-bounded :local t) (defthm-occur-cnt-bounded integerp-occur-cnt-bounded (term (implies (and (integerp a) (integerp m)) (integerp (occur-cnt-bounded term1 term2 a m bound-m))) :rule-classes :type-prescription) (list (implies (and (integerp a) (integerp m)) (integerp (occur-cnt-bounded-lst term1 lst a m bound-m))) :rule-classes :type-prescription) :hints (("Goal" :induct (occur-cnt-bounded-flg flg term2 term1 lst a m bound-m)))) (defthm-occur-cnt-bounded signed-byte-p-30-occur-cnt-bounded-flg (term (implies (and (force (signed-byte-p 30 a)) (signed-byte-p 30 m) (signed-byte-p 30 (+ bound-m m)) (force (<= 0 a)) (<= 0 m) (<= 0 bound-m) (<= a (+ bound-m m))) (and (<= -1 (occur-cnt-bounded term1 term2 a m bound-m)) (<= (occur-cnt-bounded term1 term2 a m bound-m) (+ bound-m m)))) :rule-classes :linear) (list (implies (and (force (signed-byte-p 30 a)) (signed-byte-p 30 m) (signed-byte-p 30 (+ bound-m m)) (force (<= 0 a)) (<= 0 m) (<= 0 bound-m) (<= a (+ bound-m m))) (and (<= -1 (occur-cnt-bounded-lst term1 lst a m bound-m)) (<= (occur-cnt-bounded-lst term1 lst a m bound-m) (+ bound-m m)))) :rule-classes :linear) :hints (("Goal" :induct (occur-cnt-bounded-flg flg term2 term1 lst a m bound-m)))) (verify-guards occur-cnt-bounded) (verify-termination too-many-ifs1) ; and guards (verify-termination too-many-ifs-post-rewrite)