• Top
  • Documentation
  • Books
  • 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-number-of-phases
        • Stv->outs
        • 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
  • Math
  • Testing-utilities

• 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)))