		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A4vec-part-select

Signature
(a4vec-part-select lsb width in mask) → partsel
Arguments: lsb — LSB of the select -- may be negative.
Guard (a4vec-p lsb).; width — Width of the range to select.
Guard (a4vec-p width).; in — input to select from.
Guard (a4vec-p in).; mask — Guard (4vmask-p mask).
Returns: partsel — Type (a4vec-p partsel).

Definitions and Theorems

Function: a4vec-part-select

(defun a4vec-part-select (lsb width in mask)
 (declare (xargs :guard (and (a4vec-p lsb)
                             (a4vec-p width)
                             (a4vec-p in)
                             (4vmask-p mask))))
 (let ((__function__ 'a4vec-part-select))
  (declare (ignorable __function__))
  (b* (((a4vec width))
       ((a4vec lsb))
       ((a4vec in))
       (mask (4vmask-fix mask))
       ((when (sparseint-equal mask 0))
        (a4vec-x)))
   (a4vec-ite
    (aig-and (a2vec-p lsb)
             (aig-and (a2vec-p width)
                      (aig-not (aig-sign-s width.upper))))
    (b*
     ((maskwidth
       (and
        (or
         (sparseint-< 0 mask)
         (and
          (not (and (a4vec-constantp width)
                    (a4vec-constantp lsb)))
          (cw
           "Warning: bitblasting variable part select under unbounded mask~%")))
        (+ 1 (sparseint-length mask))))
      (width-limit
           (if maskwidth (min maskwidth
                              (aig-list->s-upper-bound width.upper))
             (aig-list->s-upper-bound width.upper)))
      ((when (eql 0 width-limit))
       (aig-sterm nil))
      (neg-lsb (aig-unary-minus-s lsb.upper))
      (shift.upper (aig-head-of-concat neg-lsb (aig-sterm t)
                                       in.upper width-limit))
      (shift.lower (aig-head-of-concat neg-lsb (aig-sterm nil)
                                       in.lower width-limit)))
     (a4vec-zero-ext width (a4vec shift.upper shift.lower)
                     mask))
    (a4vec-x)))))

Theorem: a4vec-p-of-a4vec-part-select

(defthm a4vec-p-of-a4vec-part-select
  (b* ((partsel (a4vec-part-select lsb width in mask)))
    (a4vec-p partsel))
  :rule-classes :rewrite)

Theorem: a4vec-part-select-correct

(defthm a4vec-part-select-correct
  (4vec-mask-equiv (a4vec-eval (a4vec-part-select lsb width in mask)
                               env)
                   (4vec-part-select (a4vec-eval lsb env)
                                     (a4vec-eval width env)
                                     (a4vec-eval in env))
                   mask))

Theorem: a4vec-part-select-of-a4vec-fix-lsb

(defthm a4vec-part-select-of-a4vec-fix-lsb
  (equal (a4vec-part-select (a4vec-fix lsb)
                            width in mask)
         (a4vec-part-select lsb width in mask)))

Theorem: a4vec-part-select-a4vec-equiv-congruence-on-lsb

(defthm a4vec-part-select-a4vec-equiv-congruence-on-lsb
  (implies (a4vec-equiv lsb lsb-equiv)
           (equal (a4vec-part-select lsb width in mask)
                  (a4vec-part-select lsb-equiv width in mask)))
  :rule-classes :congruence)

Theorem: a4vec-part-select-of-a4vec-fix-width

(defthm a4vec-part-select-of-a4vec-fix-width
  (equal (a4vec-part-select lsb (a4vec-fix width)
                            in mask)
         (a4vec-part-select lsb width in mask)))

Theorem: a4vec-part-select-a4vec-equiv-congruence-on-width

(defthm a4vec-part-select-a4vec-equiv-congruence-on-width
  (implies (a4vec-equiv width width-equiv)
           (equal (a4vec-part-select lsb width in mask)
                  (a4vec-part-select lsb width-equiv in mask)))
  :rule-classes :congruence)

Theorem: a4vec-part-select-of-a4vec-fix-in

(defthm a4vec-part-select-of-a4vec-fix-in
  (equal (a4vec-part-select lsb width (a4vec-fix in)
                            mask)
         (a4vec-part-select lsb width in mask)))

Theorem: a4vec-part-select-a4vec-equiv-congruence-on-in

(defthm a4vec-part-select-a4vec-equiv-congruence-on-in
  (implies (a4vec-equiv in in-equiv)
           (equal (a4vec-part-select lsb width in mask)
                  (a4vec-part-select lsb width in-equiv mask)))
  :rule-classes :congruence)

Theorem: a4vec-part-select-of-4vmask-fix-mask

(defthm a4vec-part-select-of-4vmask-fix-mask
  (equal (a4vec-part-select lsb width in (4vmask-fix mask))
         (a4vec-part-select lsb width in mask)))

Theorem: a4vec-part-select-4vmask-equiv-congruence-on-mask

(defthm a4vec-part-select-4vmask-equiv-congruence-on-mask
  (implies (4vmask-equiv mask mask-equiv)
           (equal (a4vec-part-select lsb width in mask)
                  (a4vec-part-select lsb width in mask-equiv)))
  :rule-classes :congruence)