		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

4vec->a4vec

Convert a plain 4vec into a symbolic a4vec.

Signature
(4vec->a4vec x) → res
Arguments: x — Guard (4vec-p x).
Returns: res — Type (a4vec-p res).

This is used, e.g., to create the initial a4vecs for any quoted constants in the svex we are bit-blasting.

Definitions and Theorems

Function: 4vec->a4vec

(defun 4vec->a4vec (x)
  (declare (xargs :guard (4vec-p x)))
  (let ((__function__ '4vec->a4vec))
    (declare (ignorable __function__))
    (b* (((4vec x)))
      (a4vec (aig-i2v x.upper)
             (aig-i2v x.lower)))))

Theorem: a4vec-p-of-4vec->a4vec

(defthm a4vec-p-of-4vec->a4vec
  (b* ((res (4vec->a4vec x)))
    (a4vec-p res))
  :rule-classes :rewrite)

Theorem: 4vec->a4vec-correct

(defthm 4vec->a4vec-correct
  (equal (a4vec-eval (4vec->a4vec x) env)
         (4vec-fix x)))

Theorem: 4vec->a4vec-of-4vec-fix-x

(defthm 4vec->a4vec-of-4vec-fix-x
  (equal (4vec->a4vec (4vec-fix x))
         (4vec->a4vec x)))

Theorem: 4vec->a4vec-4vec-equiv-congruence-on-x

(defthm 4vec->a4vec-4vec-equiv-congruence-on-x
  (implies (4vec-equiv x x-equiv)
           (equal (4vec->a4vec x)
                  (4vec->a4vec x-equiv)))
  :rule-classes :congruence)