• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
        • Defstv
        • Stv-compile
        • Symbolic-test-vector-format
        • Stv-implementation-details
        • Compiled-stv-p
        • Stv-run-for-all-dontcares
        • Stv-run
        • Stv-process
        • Stv-run-check-dontcares
        • Symbolic-test-vector-composition
        • Stv-expand
        • Stv-easy-bindings
        • Stv-debug
        • Stv-run-squash-dontcares
        • Stvdata-p
        • Stv-doc
        • Stv2c
          • Stv2c-opts-p
          • Stv2c-c-symbol-names
          • Stv2c-outs-structdef
          • Stv2c-ins-structdef
          • Stv2c-c-symbol-name
          • Stv2c-header
          • Stv2c-main
        • Stv-widen
        • Stv-out->width
        • Stv-in->width
        • Stv->outs
        • Stv-number-of-phases
        • Stv->ins
        • Stv-suffix-signals
        • Stv->vars
      • Esim-primitives
      • E-conversion
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Stv2c

Stv2c-c-symbol-names

(stv2c-c-symbol-names x) maps stv2c-c-symbol-name across a list.

Signature

(stv2c-c-symbol-names x) → *

This is an ordinary std::defprojection.

Definitions and Theorems

Function: stv2c-c-symbol-names-exec

(defun
 stv2c-c-symbol-names-exec (x acc)
 (declare (xargs :guard t))
 (let
  ((__function__ 'stv2c-c-symbol-names-exec))
  (declare (ignorable __function__))
  (if (consp x)
      (stv2c-c-symbol-names-exec (cdr x)
                                 (cons (stv2c-c-symbol-name (car x))
                                       acc))
      acc)))

Function: stv2c-c-symbol-names-nrev

(defun stv2c-c-symbol-names-nrev (x nrev)
       (declare (xargs :stobjs (nrev)))
       (declare (xargs :guard t))
       (let ((__function__ 'stv2c-c-symbol-names-nrev))
            (declare (ignorable __function__))
            (if (atom x)
                (nrev-fix nrev)
                (let ((nrev (nrev-push (stv2c-c-symbol-name (car x))
                                       nrev)))
                     (stv2c-c-symbol-names-nrev (cdr x)
                                                nrev)))))

Function: stv2c-c-symbol-names

(defun
 stv2c-c-symbol-names (x)
 (declare (xargs :guard t))
 (let
   ((__function__ 'stv2c-c-symbol-names))
   (declare (ignorable __function__))
   (mbe :logic (if (consp x)
                   (cons (stv2c-c-symbol-name (car x))
                         (stv2c-c-symbol-names (cdr x)))
                   nil)
        :exec
        (if (atom x)
            nil
            (with-local-nrev (stv2c-c-symbol-names-nrev x nrev))))))

Theorem: stv2c-c-symbol-names-nrev-removal

(defthm stv2c-c-symbol-names-nrev-removal
        (equal (stv2c-c-symbol-names-nrev x nrev)
               (append nrev (stv2c-c-symbol-names x)))
        :rule-classes ((:rewrite)))

Theorem: stv2c-c-symbol-names-exec-removal

(defthm stv2c-c-symbol-names-exec-removal
        (equal (stv2c-c-symbol-names-exec x acc)
               (revappend (stv2c-c-symbol-names x)
                          acc))
        :rule-classes ((:rewrite)))

Theorem: stv2c-c-symbol-names-of-take

(defthm stv2c-c-symbol-names-of-take
        (implies (<= (nfix n) (len x))
                 (equal (stv2c-c-symbol-names (take n x))
                        (take n (stv2c-c-symbol-names x))))
        :rule-classes ((:rewrite)))

Theorem: set-equiv-congruence-over-stv2c-c-symbol-names

(defthm set-equiv-congruence-over-stv2c-c-symbol-names
        (implies (set-equiv x y)
                 (set-equiv (stv2c-c-symbol-names x)
                            (stv2c-c-symbol-names y)))
        :rule-classes ((:congruence)))

Theorem: subsetp-of-stv2c-c-symbol-names-when-subsetp

(defthm subsetp-of-stv2c-c-symbol-names-when-subsetp
        (implies (subsetp x y)
                 (subsetp (stv2c-c-symbol-names x)
                          (stv2c-c-symbol-names y)))
        :rule-classes ((:rewrite)))

Theorem: member-of-stv2c-c-symbol-name-in-stv2c-c-symbol-names

(defthm member-of-stv2c-c-symbol-name-in-stv2c-c-symbol-names
        (implies (member k x)
                 (member (stv2c-c-symbol-name k)
                         (stv2c-c-symbol-names x)))
        :rule-classes ((:rewrite)))

Theorem: stv2c-c-symbol-names-of-rev

(defthm stv2c-c-symbol-names-of-rev
        (equal (stv2c-c-symbol-names (rev x))
               (rev (stv2c-c-symbol-names x)))
        :rule-classes ((:rewrite)))

Theorem: stv2c-c-symbol-names-of-list-fix

(defthm stv2c-c-symbol-names-of-list-fix
        (equal (stv2c-c-symbol-names (list-fix x))
               (stv2c-c-symbol-names x))
        :rule-classes ((:rewrite)))

Theorem: stv2c-c-symbol-names-of-append

(defthm stv2c-c-symbol-names-of-append
        (equal (stv2c-c-symbol-names (append a b))
               (append (stv2c-c-symbol-names a)
                       (stv2c-c-symbol-names b)))
        :rule-classes ((:rewrite)))

Theorem: cdr-of-stv2c-c-symbol-names

(defthm cdr-of-stv2c-c-symbol-names
        (equal (cdr (stv2c-c-symbol-names x))
               (stv2c-c-symbol-names (cdr x)))
        :rule-classes ((:rewrite)))

Theorem: car-of-stv2c-c-symbol-names

(defthm car-of-stv2c-c-symbol-names
        (equal (car (stv2c-c-symbol-names x))
               (and (consp x)
                    (stv2c-c-symbol-name (car x))))
        :rule-classes ((:rewrite)))

Theorem: stv2c-c-symbol-names-under-iff

(defthm stv2c-c-symbol-names-under-iff
        (iff (stv2c-c-symbol-names x) (consp x))
        :rule-classes ((:rewrite)))

Theorem: consp-of-stv2c-c-symbol-names

(defthm consp-of-stv2c-c-symbol-names
        (equal (consp (stv2c-c-symbol-names x))
               (consp x))
        :rule-classes ((:rewrite)))

Theorem: len-of-stv2c-c-symbol-names

(defthm len-of-stv2c-c-symbol-names
        (equal (len (stv2c-c-symbol-names x))
               (len x))
        :rule-classes ((:rewrite)))

Theorem: true-listp-of-stv2c-c-symbol-names

(defthm true-listp-of-stv2c-c-symbol-names
        (true-listp (stv2c-c-symbol-names x))
        :rule-classes :type-prescription)

Theorem: stv2c-c-symbol-names-when-not-consp

(defthm stv2c-c-symbol-names-when-not-consp
        (implies (not (consp x))
                 (equal (stv2c-c-symbol-names x) nil))
        :rule-classes ((:rewrite)))

Theorem: stv2c-c-symbol-names-of-cons

(defthm stv2c-c-symbol-names-of-cons
        (equal (stv2c-c-symbol-names (cons a b))
               (cons (stv2c-c-symbol-name a)
                     (stv2c-c-symbol-names b)))
        :rule-classes ((:rewrite)))

Theorem: string-listp-of-stv2c-c-symbol-names

(defthm string-listp-of-stv2c-c-symbol-names
        (string-listp (stv2c-c-symbol-names x)))