		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svex-apply-aig

Signature
(svex-apply-aig fn args terms mask) → res
Arguments: fn — Guard (fnsym-p fn).; args — Guard (a4veclist-p args).; terms — Guard (svexlist-p terms).; mask — Guard (4vmask-p mask).
Returns: res — Type (a4vec-p res).

Definitions and Theorems

Function: svex-apply-aig

(defun svex-apply-aig (fn args terms mask)
  (declare (xargs :guard (and (fnsym-p fn)
                              (a4veclist-p args)
                              (svexlist-p terms)
                              (4vmask-p mask))))
  (let ((__function__ 'svex-apply-aig))
    (declare (ignorable __function__))
    (b* ((fn (fnsym-fix fn))
         (args (a4veclist-fix args))
         (res (svex-apply-aig-cases fn args terms mask)))
      (a4vec-mask mask res))))

Theorem: a4vec-p-of-svex-apply-aig

(defthm a4vec-p-of-svex-apply-aig
  (b* ((res (svex-apply-aig fn args terms mask)))
    (a4vec-p res))
  :rule-classes :rewrite)

Theorem: svex-apply-aig-correct

(defthm svex-apply-aig-correct
 (implies
  (and
    (fnsym-p fn)
    (bind-free '((a4env . env)) (a4env))
    (equal
         (a4veclist-eval vals aigenv)
         (4veclist-mask
              argmasks
              (svexlist-eval x (svex-a4vec-env-eval a4env aigenv))))
    (svex-argmasks-okp (svex-call fn x)
                       mask argmasks))
  (equal
   (a4vec-eval (svex-apply-aig fn vals x mask)
               aigenv)
   (4vec-mask
        mask
        (svex-apply
             fn
             (svexlist-eval x
                            (svex-a4vec-env-eval a4env aigenv)))))))

Theorem: svex-apply-aig-of-fnsym-fix-fn

(defthm svex-apply-aig-of-fnsym-fix-fn
  (equal (svex-apply-aig (fnsym-fix fn)
                         args terms mask)
         (svex-apply-aig fn args terms mask)))

Theorem: svex-apply-aig-fnsym-equiv-congruence-on-fn

(defthm svex-apply-aig-fnsym-equiv-congruence-on-fn
  (implies (fnsym-equiv fn fn-equiv)
           (equal (svex-apply-aig fn args terms mask)
                  (svex-apply-aig fn-equiv args terms mask)))
  :rule-classes :congruence)

Theorem: svex-apply-aig-of-a4veclist-fix-args

(defthm svex-apply-aig-of-a4veclist-fix-args
  (equal (svex-apply-aig fn (a4veclist-fix args)
                         terms mask)
         (svex-apply-aig fn args terms mask)))

Theorem: svex-apply-aig-a4veclist-equiv-congruence-on-args

(defthm svex-apply-aig-a4veclist-equiv-congruence-on-args
  (implies (a4veclist-equiv args args-equiv)
           (equal (svex-apply-aig fn args terms mask)
                  (svex-apply-aig fn args-equiv terms mask)))
  :rule-classes :congruence)

Theorem: svex-apply-aig-of-svexlist-fix-terms

(defthm svex-apply-aig-of-svexlist-fix-terms
  (equal (svex-apply-aig fn args (svexlist-fix terms)
                         mask)
         (svex-apply-aig fn args terms mask)))

Theorem: svex-apply-aig-svexlist-equiv-congruence-on-terms

(defthm svex-apply-aig-svexlist-equiv-congruence-on-terms
  (implies (svexlist-equiv terms terms-equiv)
           (equal (svex-apply-aig fn args terms mask)
                  (svex-apply-aig fn args terms-equiv mask)))
  :rule-classes :congruence)

Theorem: svex-apply-aig-of-4vmask-fix-mask

(defthm svex-apply-aig-of-4vmask-fix-mask
  (equal (svex-apply-aig fn args terms (4vmask-fix mask))
         (svex-apply-aig fn args terms mask)))

Theorem: svex-apply-aig-4vmask-equiv-congruence-on-mask

(defthm svex-apply-aig-4vmask-equiv-congruence-on-mask
  (implies (4vmask-equiv mask mask-equiv)
           (equal (svex-apply-aig fn args terms mask)
                  (svex-apply-aig fn args terms mask-equiv)))
  :rule-classes :congruence)