		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod-wiresearch-smartpivot

Signature
(elab-mod-wiresearch-smartpivot wire mininst minoffset maxinst maxoffset) → pivotinst
Arguments: wire — Guard (natp wire).; mininst — Guard (natp mininst).; minoffset — Guard (natp minoffset).; maxinst — Guard (natp maxinst).; maxoffset — Guard (natp maxoffset).
Returns: pivotinst — Type (natp pivotinst).

Definitions and Theorems

Function: elab-mod-wiresearch-smartpivot

(defun elab-mod-wiresearch-smartpivot
       (wire mininst minoffset maxinst maxoffset)
  (declare (xargs :guard (and (natp wire)
                              (natp mininst)
                              (natp minoffset)
                              (natp maxinst)
                              (natp maxoffset))))
  (declare (xargs :guard (and (< (+ 1 mininst) maxinst)
                              (<= minoffset wire)
                              (< wire maxoffset))))
  (let ((__function__ 'elab-mod-wiresearch-smartpivot))
    (declare (ignorable __function__))
    (b* ((maxinst (mbe :logic (pos-fix maxinst)
                       :exec maxinst))
         (mininst (lnfix mininst))
         (maxoffset (lnfix maxoffset))
         (minoffset (lnfix minoffset))
         (guess (+ 1 mininst
                   (floor (* (- maxinst mininst)
                             (- wire minoffset))
                          (- maxoffset minoffset)))))
      (min (+ -1 maxinst)
           (max (+ 1 mininst) guess)))))

Theorem: natp-of-elab-mod-wiresearch-smartpivot

(defthm natp-of-elab-mod-wiresearch-smartpivot
  (b* ((pivotinst (elab-mod-wiresearch-smartpivot
                       wire
                       mininst minoffset maxinst maxoffset)))
    (natp pivotinst))
  :rule-classes :type-prescription)

Theorem: elab-mod-wiresearch-smartpivot-lower-bound

(defthm elab-mod-wiresearch-smartpivot-lower-bound
  (implies (< (+ 1 (nfix mininst)) (nfix maxinst))
           (< (nfix mininst)
              (elab-mod-wiresearch-smartpivot
                   wire
                   mininst minoffset maxinst maxoffset)))
  :rule-classes :linear)

Theorem: elab-mod-wiresearch-smartpivot-upper-bound

(defthm elab-mod-wiresearch-smartpivot-upper-bound
  (implies (< (+ 1 (nfix mininst)) (nfix maxinst))
           (< (elab-mod-wiresearch-smartpivot
                   wire
                   mininst minoffset maxinst maxoffset)
              (nfix maxinst)))
  :rule-classes :linear)