• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
        • Rewriting
          • Svex-rewrite
          • Svexlist-rewrite-nrev
          • Svex-args-apply-masks
          • 4veclist-quote
          • Svex-simpconfig-p
          • Svex-rewrite-memo-correct
          • Svex-alist-maybe-rewrite-fixpoint
          • Svexlist-compute-masks
          • Svexlist-rewrite-under-masks
          • Svex-alist-rewrite-fixpoint
          • Svexlist-maybe-rewrite-fixpoint
          • Svexlist-rewrite-fixpoint
          • Svexlist-mask-acons
          • Svexlist-mask-alist/toposort
          • Svex-call-simp
          • Svex-alist-compose
          • Svexlist-rewrite-top
          • Svex-alist-subst
          • Svex-alist-compose-rw
          • Svex-argmasks-lookup
          • Svex-alist-subst-rw
          • Svexlist-mask-acons-rev
          • Svex-mask-lookup
          • Svex-mask-acons
          • Svexlist-mask-alist
          • Svex-alist-rewrite-top
          • Constraintlist-compose
          • Svex-substconfig
          • Svex-simpconfig-fix
          • Svex-subst
          • Svex-rewrite-memo-vars-ok
          • Svex-norm-call
          • Svex-3value-mask
          • Svexlist-count-calls-aux
          • Svex-mask-alist-keys
          • Rewriter-tracing
          • Svex-rewrite-top
          • Svexlist-maskfree-rewrite-nrev
          • Svexlist-multirefs-top
          • Svexlist-count-calls
          • Svex-unify
          • Svexlist-toposort-p
          • Svexlist-maskfree-rewrite-top
          • Svex-alist-compose-nrev
          • Rewriting-concatenations
          • Svex-svex-memo
          • Svex-mask-alist
          • Svex-alist-subst-nrev
          • Svex-simpconfig-fix!
          • Svex-rewrite-rules
        • Svex
        • Bit-blasting
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
        • Values
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Rewriting

Svex-alist-compose

Signature

(svex-alist-compose x a) → xx

Arguments

x — Guard (svex-alist-p x).

a — Guard (svex-alist-p a).

Returns

xx — Type (svex-alist-p xx).

Definitions and Theorems

Function: svex-alist-compose

(defun svex-alist-compose (x a)
  (declare (xargs :guard (and (svex-alist-p x)
                              (svex-alist-p a))))
  (let ((__function__ 'svex-alist-compose))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (mbe :logic
           (if (mbt (and (consp (car x)) (svar-p (caar x))))
               (svex-acons (caar x)
                           (svex-compose (cdar x) a)
                           (svex-alist-compose (cdr x) a))
             (svex-alist-compose (cdr x) a))
           :exec (acl2::with-local-nrev
                      (svex-alist-compose-nrev x a acl2::nrev))))))

Theorem: svex-alist-p-of-svex-alist-compose

(defthm svex-alist-p-of-svex-alist-compose
  (b* ((xx (svex-alist-compose x a)))
    (svex-alist-p xx))
  :rule-classes :rewrite)

Theorem: svex-alist-compose-of-svex-alist-fix-x

(defthm svex-alist-compose-of-svex-alist-fix-x
  (equal (svex-alist-compose (svex-alist-fix x)
                             a)
         (svex-alist-compose x a)))

Theorem: svex-alist-compose-svex-alist-equiv-congruence-on-x

(defthm svex-alist-compose-svex-alist-equiv-congruence-on-x
  (implies (svex-alist-equiv x x-equiv)
           (equal (svex-alist-compose x a)
                  (svex-alist-compose x-equiv a)))
  :rule-classes :congruence)

Theorem: svex-alist-compose-of-svex-alist-fix-a

(defthm svex-alist-compose-of-svex-alist-fix-a
  (equal (svex-alist-compose x (svex-alist-fix a))
         (svex-alist-compose x a)))

Theorem: svex-alist-compose-svex-alist-equiv-congruence-on-a

(defthm svex-alist-compose-svex-alist-equiv-congruence-on-a
  (implies (svex-alist-equiv a a-equiv)
           (equal (svex-alist-compose x a)
                  (svex-alist-compose x a-equiv)))
  :rule-classes :congruence)

Theorem: svex-alist-eval-of-svex-compose

(defthm svex-alist-eval-of-svex-compose
  (equal (svex-alist-eval (svex-alist-compose x subst)
                          env)
         (svex-alist-eval x
                          (append (svex-alist-eval subst env)
                                  env))))

Theorem: vars-of-svex-alist-compose

(defthm vars-of-svex-alist-compose
  (implies
       (and (not (member v (svex-alist-vars x)))
            (not (member v (svex-alist-vars a))))
       (not (member v
                    (svex-alist-vars (svex-alist-compose x a))))))

Theorem: svex-lookup-of-svex-alist-compose

(defthm svex-lookup-of-svex-alist-compose
  (equal (svex-lookup v (svex-alist-compose x a))
         (let ((x-look (svex-lookup v x)))
           (and x-look (svex-compose x-look a)))))