		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

A4veclist-eval-gl

Signature
(a4veclist-eval-gl x env) → res
Arguments: x — Guard (a4veclist-p x).
Returns: res — Type (4veclist-p res).

Definitions and Theorems

Function: a4veclist-eval-gl

(defun a4veclist-eval-gl (x env)
 (declare (xargs :guard (a4veclist-p x)))
 (let ((__function__ 'a4veclist-eval-gl))
  (declare (ignorable __function__))
  (b*
   ((aiglist
     (time$
      (a4veclist->aiglist x)
      :msg
      "; SV bit-blasting: a4veclist->aiglist: ~st sec, ~sa bytes.~%"))
    (bitlist
     (time$
        (aig-eval-list aiglist env)
        :msg
        "; SV bit-blasting: aig-eval-list: ~st sec, ~sa bytes.~%")))
   (time$ (4veclist-from-bitlist x bitlist)
          :msg "; bits->4vecs: ~st sec, ~sa bytes.~%"))))

Theorem: 4veclist-p-of-a4veclist-eval-gl

(defthm 4veclist-p-of-a4veclist-eval-gl
  (b* ((res (a4veclist-eval-gl x env)))
    (4veclist-p res))
  :rule-classes :rewrite)

Theorem: a4veclist-eval-gl-correct

(defthm a4veclist-eval-gl-correct
  (equal (a4veclist-eval-gl x env)
         (a4veclist-eval x env)))

Theorem: a4veclist-eval-redef

(defthm a4veclist-eval-redef
  (equal (a4veclist-eval x env)
         (a4veclist-eval-gl x env)))

Theorem: a4veclist-eval-gl-of-a4veclist-fix-x

(defthm a4veclist-eval-gl-of-a4veclist-fix-x
  (equal (a4veclist-eval-gl (a4veclist-fix x)
                            env)
         (a4veclist-eval-gl x env)))

Theorem: a4veclist-eval-gl-a4veclist-equiv-congruence-on-x

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