• 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
            • Svar
            • Least-fixpoint
            • Svex-p
            • Svex-select
            • Svex-alist
              • Svex-alist-p
              • Svex-alist-fix
              • Svex-alist-vars
              • Svex-alist-eval
              • Svex-lookup
              • Svex-fastacons
              • Svex-alist-vals
                • Svex-alist-keys
                • Svex-acons
                • Svex-alist-equiv
                • Svex-fastlookup
              • Svex-equiv
              • Svexlist
              • Svex-call
              • Fnsym
              • Svex-quote
              • Svex-var
              • Svcall-rw
              • Svcall
              • Svex-kind
              • Svcall*
              • Svex-fix
              • Svex-count
              • Svex-1z
              • Svex-1x
              • Svex-z
              • Svex-x
            • 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
    • Svex-alist

    Svex-alist-vals

    Like alist-vals but with proper fty-discipline for svex-alists.

    Signature
    (svex-alist-vals x) → vals
    Arguments
    x — Guard (svex-alist-p x).
    Returns
    vals — Type (svexlist-p vals).

    Definitions and Theorems

    Function: svex-alist-vals

    (defun svex-alist-vals (x)
      (declare (xargs :guard (svex-alist-p x)))
      (let ((__function__ 'svex-alist-vals))
        (declare (ignorable __function__))
        (mbe :logic
             (if (atom x)
                 nil
               (if (mbt (and (consp (car x)) (svar-p (caar x))))
                   (cons (mbe :logic (svex-fix (cdar x))
                              :exec (cdar x))
                         (svex-alist-vals (cdr x)))
                 (svex-alist-vals (cdr x))))
             :exec (strip-cdrs x))))

    Theorem: svexlist-p-of-svex-alist-vals

    (defthm svexlist-p-of-svex-alist-vals
      (b* ((vals (svex-alist-vals x)))
        (svexlist-p vals))
      :rule-classes :rewrite)

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

    (defthm svex-alist-vals-of-svex-alist-fix-x
      (equal (svex-alist-vals (svex-alist-fix x))
             (svex-alist-vals x)))

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

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

    Theorem: member-svex-alist-vals-when-svex-lookup

    (defthm member-svex-alist-vals-when-svex-lookup
      (implies (svex-lookup k x)
               (member (svex-lookup k x)
                       (svex-alist-vals x))))

    Theorem: svex-alist-vals-of-svex-acons

    (defthm svex-alist-vals-of-svex-acons
      (equal (svex-alist-vals (svex-acons k v x))
             (cons (svex-fix v)
                   (svex-alist-vals x))))

    Theorem: len-of-svex-alist-vals

    (defthm len-of-svex-alist-vals
      (equal (len (svex-alist-vals x))
             (len (svex-alist-keys x))))

    Theorem: svex-alist-vals-of-pairlis$

    (defthm svex-alist-vals-of-pairlis$
      (implies (and (equal (len x) (len y))
                    (svarlist-p x))
               (equal (svex-alist-vals (pairlis$ x y))
                      (svexlist-fix y))))