		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A4vec-concat

Symbolic version of 4vec-concat.

Signature
(a4vec-concat w x y mask) → res
Arguments: w — Width argument to the concat.
Guard (a4vec-p w).; x — Low bits to concatenate.
Guard (a4vec-p x).; y — High bits to concatenate.
Guard (a4vec-p y).; mask — Care mask for the result.
Guard (4vmask-p mask).
Returns: res — Type (a4vec-p res).

As a special consideration, we use the care mask to try to avoid creating enormous vectors when given a huge width argument.

Definitions and Theorems

Function: a4vec-concat

(defun a4vec-concat (w x y mask)
 (declare (xargs :guard (and (a4vec-p w)
                             (a4vec-p x)
                             (a4vec-p y)
                             (4vmask-p mask))))
 (let ((__function__ 'a4vec-concat))
  (declare (ignorable __function__))
  (b*
   (((a4vec w))
    ((a4vec x))
    ((a4vec y))
    (mask (4vmask-fix mask))
    ((when (sparseint-equal mask 0))
     (a4vec-x))
    ((when (sparseint-< 0 mask))
     (b* ((width (+ 1 (sparseint-length mask))))
      (a4vec-ite
       (aig-and (a2vec-p w)
                (aig-not (aig-sign-s w.upper)))
       (b*
        ((upper (aig-head-of-concat w.upper x.upper y.upper width))
         (lower (aig-head-of-concat w.upper x.lower y.lower width)))
        (a4vec upper lower))
       (a4vec-x)))))
   (and
    (not (a4vec-constantp w))
    (cw
     "Warning: bitblasting variable-width concat under unbounded mask~%"))
   (a4vec-ite
      (aig-and (a2vec-p w)
               (aig-not (aig-sign-s w.upper)))
      (b* ((shift w.upper)
           (xmask (aig-lognot-s (aig-ash-ss 1 (aig-sterm t) shift)))
           (yshu (aig-ash-ss 1 y.upper shift))
           (yshl (aig-ash-ss 1 y.lower shift)))
        (a4vec (aig-logior-ss (aig-logand-ss xmask x.upper)
                              yshu)
               (aig-logior-ss (aig-logand-ss xmask x.lower)
                              yshl)))
      (a4vec-x)))))

Theorem: a4vec-p-of-a4vec-concat

(defthm a4vec-p-of-a4vec-concat
  (b* ((res (a4vec-concat w x y mask)))
    (a4vec-p res))
  :rule-classes :rewrite)

Theorem: a4vec-concat-correct

(defthm a4vec-concat-correct
  (4vec-mask-equiv (a4vec-eval (a4vec-concat n x y mask)
                               env)
                   (4vec-concat (a4vec-eval n env)
                                (a4vec-eval x env)
                                (a4vec-eval y env))
                   mask))

Theorem: a4vec-concat-of-a4vec-fix-w

(defthm a4vec-concat-of-a4vec-fix-w
  (equal (a4vec-concat (a4vec-fix w) x y mask)
         (a4vec-concat w x y mask)))

Theorem: a4vec-concat-a4vec-equiv-congruence-on-w

(defthm a4vec-concat-a4vec-equiv-congruence-on-w
  (implies (a4vec-equiv w w-equiv)
           (equal (a4vec-concat w x y mask)
                  (a4vec-concat w-equiv x y mask)))
  :rule-classes :congruence)

Theorem: a4vec-concat-of-a4vec-fix-x

(defthm a4vec-concat-of-a4vec-fix-x
  (equal (a4vec-concat w (a4vec-fix x) y mask)
         (a4vec-concat w x y mask)))

Theorem: a4vec-concat-a4vec-equiv-congruence-on-x

(defthm a4vec-concat-a4vec-equiv-congruence-on-x
  (implies (a4vec-equiv x x-equiv)
           (equal (a4vec-concat w x y mask)
                  (a4vec-concat w x-equiv y mask)))
  :rule-classes :congruence)

Theorem: a4vec-concat-of-a4vec-fix-y

(defthm a4vec-concat-of-a4vec-fix-y
  (equal (a4vec-concat w x (a4vec-fix y) mask)
         (a4vec-concat w x y mask)))

Theorem: a4vec-concat-a4vec-equiv-congruence-on-y

(defthm a4vec-concat-a4vec-equiv-congruence-on-y
  (implies (a4vec-equiv y y-equiv)
           (equal (a4vec-concat w x y mask)
                  (a4vec-concat w x y-equiv mask)))
  :rule-classes :congruence)

Theorem: a4vec-concat-of-4vmask-fix-mask

(defthm a4vec-concat-of-4vmask-fix-mask
  (equal (a4vec-concat w x y (4vmask-fix mask))
         (a4vec-concat w x y mask)))

Theorem: a4vec-concat-4vmask-equiv-congruence-on-mask

(defthm a4vec-concat-4vmask-equiv-congruence-on-mask
  (implies (4vmask-equiv mask mask-equiv)
           (equal (a4vec-concat w x y mask)
                  (a4vec-concat w x y mask-equiv)))
  :rule-classes :congruence)