• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
        • Unparameterization
        • Elaborate
        • Addnames
        • Annotate
        • Clean-warnings
          • Vl-interfacelist-clean-warnings
          • Vl-programlist-clean-warnings
          • Vl-packagelist-clean-warnings
          • Vl-modulelist-clean-warnings
          • Vl-configlist-clean-warnings
          • Vl-classlist-clean-warnings
          • Vl-udplist-clean-warnings
          • Vl-design-clean-warnings
          • Vl-clean-warnings
            • Vl-warning-sort
              • Vl-warning-<
          • Vl-program-clean-warnings
          • Vl-package-clean-warnings
          • Vl-interface-clean-warnings
          • Vl-module-clean-warnings
          • Vl-config-clean-warnings
          • Vl-class-clean-warnings
          • Vl-udp-clean-warnings
        • Eliminitial
        • Custom-transform-hooks
        • Problem-modules
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-clean-warnings

Vl-warning-sort

Mergesort warnings using vl-warning-<

Definitions and Theorems

Function: vl-warning-ordered-p

(defun vl-warning-ordered-p (acl2::x)
  (declare (xargs :guard (and t (vl-warninglist-p acl2::x))
                  :stobjs nil))
  (cond ((atom acl2::x) t)
        ((atom (cdr acl2::x)) t)
        ((vl-warning-< (first acl2::x)
                       (second acl2::x))
         (vl-warning-ordered-p (cdr acl2::x)))
        (t (and (not (vl-warning-< (second acl2::x)
                                   (first acl2::x)))
                (vl-warning-ordered-p (cdr acl2::x))))))

Function: vl-warning-merge

(defun vl-warning-merge (acl2::x acl2::y)
  (declare (xargs :stobjs nil
                  :guard (and t (vl-warninglist-p acl2::x)
                              (vl-warninglist-p acl2::y))))
  (cond ((atom acl2::x) acl2::y)
        ((atom acl2::y) acl2::x)
        ((vl-warning-< (car acl2::y)
                       (car acl2::x))
         (cons (car acl2::y)
               (vl-warning-merge acl2::x (cdr acl2::y))))
        (t (cons (car acl2::x)
                 (vl-warning-merge (cdr acl2::x)
                                   acl2::y)))))

Function: vl-warning-merge-tr

(defun vl-warning-merge-tr (acl2::x acl2::y acl2::acc)
  (declare (xargs :stobjs nil
                  :guard (and t (vl-warninglist-p acl2::x)
                              (vl-warninglist-p acl2::y))))
  (cond ((atom acl2::x)
         (revappend-without-guard acl2::acc acl2::y))
        ((atom acl2::y)
         (revappend-without-guard acl2::acc acl2::x))
        ((vl-warning-< (car acl2::y)
                       (car acl2::x))
         (vl-warning-merge-tr acl2::x (cdr acl2::y)
                              (cons (car acl2::y) acl2::acc)))
        (t (vl-warning-merge-tr (cdr acl2::x)
                                acl2::y
                                (cons (car acl2::x) acl2::acc)))))

Function: vl-warning-mergesort-fixnum

(defun vl-warning-mergesort-fixnum (acl2::x len)
 (declare (xargs :stobjs nil
                 :guard (and t (vl-warninglist-p acl2::x)
                             (natp len)
                             (<= len (len acl2::x))))
          (type (signed-byte 30) len))
 (cond
  ((mbe :logic (zp len)
        :exec (eql (the (signed-byte 30) len) 0))
   nil)
  ((eql (the (signed-byte 30) len) 1)
   (list (car acl2::x)))
  (t
    (let*
     ((acl2::len1 (the (signed-byte 30)
                       (ash (the (signed-byte 30) len) -1)))
      (acl2::len2 (the (signed-byte 30)
                       (- (the (signed-byte 30) len)
                          (the (signed-byte 30) acl2::len1))))
      (acl2::part1 (vl-warning-mergesort-fixnum acl2::x acl2::len1))
      (acl2::part2
           (vl-warning-mergesort-fixnum (rest-n acl2::len1 acl2::x)
                                        acl2::len2)))
     (vl-warning-merge-tr acl2::part1 acl2::part2 nil)))))

Function: vl-warning-mergesort-integers

(defun vl-warning-mergesort-integers (acl2::x len)
 (declare (xargs :stobjs nil
                 :guard (and t (vl-warninglist-p acl2::x)
                             (natp len)
                             (<= len (len acl2::x))))
          (type integer len))
 (cond
  ((mbe :logic (zp len)
        :exec (eql (the integer len) 0))
   nil)
  ((eql (the integer len) 1)
   (list (car acl2::x)))
  (t
   (let*
    ((acl2::len1 (the integer (ash (the integer len) -1)))
     (acl2::len2 (the integer
                      (- (the integer len)
                         (the integer acl2::len1))))
     (acl2::part1
          (if (< (the integer acl2::len1)
                 (acl2::mergesort-fixnum-threshold))
              (vl-warning-mergesort-fixnum acl2::x acl2::len1)
            (vl-warning-mergesort-integers acl2::x acl2::len1)))
     (acl2::part2
        (if (< (the integer acl2::len2)
               (acl2::mergesort-fixnum-threshold))
            (vl-warning-mergesort-fixnum (rest-n acl2::len1 acl2::x)
                                         acl2::len2)
          (vl-warning-mergesort-integers (rest-n acl2::len1 acl2::x)
                                         acl2::len2))))
    (vl-warning-merge-tr acl2::part1 acl2::part2 nil)))))

Function: vl-warning-sort

(defun vl-warning-sort (acl2::x)
 (declare (xargs :guard (and t (vl-warninglist-p acl2::x))
                 :stobjs nil))
 (mbe
   :logic
   (cond ((atom acl2::x) nil)
         ((atom (cdr acl2::x))
          (list (car acl2::x)))
         (t (let ((acl2::half (floor (len acl2::x) 2)))
              (vl-warning-merge
                   (vl-warning-sort (take acl2::half acl2::x))
                   (vl-warning-sort (nthcdr acl2::half acl2::x))))))
   :exec
   (let ((len (len acl2::x)))
     (if (< len (acl2::mergesort-fixnum-threshold))
         (vl-warning-mergesort-fixnum acl2::x len)
       (vl-warning-mergesort-integers acl2::x len)))))

Theorem: vl-warning-sort-preserves-duplicity

(defthm vl-warning-sort-preserves-duplicity
  (equal (duplicity acl2::a (vl-warning-sort acl2::x))
         (duplicity acl2::a acl2::x)))

Theorem: vl-warning-sort-creates-comparable-listp

(defthm vl-warning-sort-creates-comparable-listp
  (implies (vl-warninglist-p acl2::x)
           (vl-warninglist-p (vl-warning-sort acl2::x))))

Theorem: vl-warning-sort-sorts

(defthm vl-warning-sort-sorts
  (vl-warning-ordered-p (vl-warning-sort acl2::x)))

Theorem: vl-warning-sort-no-duplicatesp-equal

(defthm vl-warning-sort-no-duplicatesp-equal
  (equal (no-duplicatesp-equal (vl-warning-sort acl2::x))
         (no-duplicatesp-equal acl2::x)))

Theorem: vl-warning-sort-true-listp

(defthm vl-warning-sort-true-listp
  (true-listp (vl-warning-sort acl2::x))
  :rule-classes :type-prescription)

Theorem: vl-warning-sort-len

(defthm vl-warning-sort-len
  (equal (len (vl-warning-sort acl2::x))
         (len acl2::x)))

Theorem: vl-warning-sort-consp

(defthm vl-warning-sort-consp
  (equal (consp (vl-warning-sort acl2::x))
         (consp acl2::x)))

Theorem: vl-warning-sort-is-identity-under-set-equiv

(defthm vl-warning-sort-is-identity-under-set-equiv
  (set-equiv (vl-warning-sort acl2::x)
             acl2::x))

Theorem: vl-warninglist-p-of-vl-warning-sort

(defthm vl-warninglist-p-of-vl-warning-sort
  (implies (force (vl-warninglist-p x))
           (vl-warninglist-p (vl-warning-sort x))))

Theorem: consp-of-vl-warning-sort

(defthm consp-of-vl-warning-sort
  (equal (consp (vl-warning-sort x))
         (consp x)))

Subtopics

Vl-warning-<

A basic, rather arbitrary ordering for warnings.