		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

A4vec-eval

Semantics of a4vecs.

Signature
(a4vec-eval x env) → res
Arguments: x — Symbolic 4vec to evaluate.
Guard (a4vec-p x).; env — Environment for aig-eval.
Returns: res — Value of x as a 4vec.
Type (4vec-p res).

Definitions and Theorems

Function: a4vec-eval

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

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

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

Theorem: a4vec-eval-of-a4vec

(defthm a4vec-eval-of-a4vec
  (equal (a4vec-eval (a4vec upper lower) env)
         (4vec (aig-list->s upper env)
               (aig-list->s lower env))))

Theorem: a4vec-eval-of-const

(defthm a4vec-eval-of-const
  (implies (syntaxp (quotep x))
           (equal (a4vec-eval x env)
                  (4vec (aig-list->s (a4vec->upper x) env)
                        (aig-list->s (a4vec->lower x) env)))))

Theorem: a4vec-eval-of-var

(defthm a4vec-eval-of-var
  (implies (syntaxp (symbolp x))
           (equal (a4vec-eval x env)
                  (4vec (aig-list->s (a4vec->upper x) env)
                        (aig-list->s (a4vec->lower x) env)))))

Theorem: a4vec-eval-of-a4vec-fix-x

(defthm a4vec-eval-of-a4vec-fix-x
  (equal (a4vec-eval (a4vec-fix x) env)
         (a4vec-eval x env)))

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

(defthm a4vec-eval-a4vec-equiv-congruence-on-x
  (implies (a4vec-equiv x x-equiv)
           (equal (a4vec-eval x env)
                  (a4vec-eval x-equiv env)))
  :rule-classes :congruence)