		Search-engine friendly clone of the ACL2 documentation.

Network

Aignet-nxsts

Signature
(aignet-nxsts aignet) → nxsts
Arguments: aignet — Guard (node-listp aignet).
Returns: nxsts — Type (node-listp nxsts).

Definitions and Theorems

Function: aignet-nxsts

(defun aignet-nxsts (aignet)
  (declare (xargs :guard (node-listp aignet)))
  (let ((__function__ 'aignet-nxsts))
    (declare (ignorable __function__))
    (aignet-nxsts-aux (stype-count :reg aignet)
                      aignet)))

Theorem: node-listp-of-aignet-nxsts

(defthm node-listp-of-aignet-nxsts
  (b* ((nxsts (aignet-nxsts aignet)))
    (node-listp nxsts))
  :rule-classes :rewrite)

Theorem: fanin-count-of-aignet-nxsts

(defthm fanin-count-of-aignet-nxsts
  (b* ((?nxsts (aignet-nxsts aignet)))
    (equal (fanin-count nxsts) 0)))

Theorem: lookup-id-of-aignet-nxsts

(defthm lookup-id-of-aignet-nxsts
  (b* ((?nxsts (aignet-nxsts aignet)))
    (equal (lookup-id k nxsts) nil)))

Theorem: stype-count-of-aignet-nxsts

(defthm stype-count-of-aignet-nxsts
  (b* ((?nxsts (aignet-nxsts aignet)))
    (equal (stype-count stype nxsts)
           (if (equal (stype-fix stype) :nxst)
               (stype-count :reg aignet)
             0))))

Theorem: aignet-nxsts-of-node-list-fix-aignet

(defthm aignet-nxsts-of-node-list-fix-aignet
  (equal (aignet-nxsts (node-list-fix aignet))
         (aignet-nxsts aignet)))

Theorem: aignet-nxsts-node-list-equiv-congruence-on-aignet

(defthm aignet-nxsts-node-list-equiv-congruence-on-aignet
  (implies (node-list-equiv aignet aignet-equiv)
           (equal (aignet-nxsts aignet)
                  (aignet-nxsts aignet-equiv)))
  :rule-classes :congruence)

Theorem: lookup-stype-of-aignet-nxsts

(defthm lookup-stype-of-aignet-nxsts
  (b* ((?nxsts (aignet-nxsts aignet)))
    (implies (not (equal (stype-fix stype) :nxst))
             (equal (lookup-stype k stype nxsts)
                    nil))))

Theorem: lookup-reg->nxst-of-aignet-nxsts

(defthm lookup-reg->nxst-of-aignet-nxsts
  (b* ((?nxsts (aignet-nxsts aignet)))
    (implies (and (<= (fanin-count aignet)
                      (fanin-count rest))
                  (<= (stype-count :reg aignet)
                      (stype-count :reg rest)))
             (equal (lookup-reg->nxst k (append nxsts rest))
                    (if (< (nfix k) (stype-count :reg aignet))
                        (lookup-reg->nxst k aignet)
                      (lookup-reg->nxst k rest))))))

Theorem: aignet-nxsts-of-append-aignet-nxsts

(defthm aignet-nxsts-of-append-aignet-nxsts
  (implies (and (equal (stype-count :reg x)
                       (stype-count :reg rest))
                (<= (fanin-count x) (fanin-count rest)))
           (equal (aignet-nxsts (append (aignet-nxsts x) rest))
                  (aignet-nxsts x))))

Theorem: aignet-nxsts-of-cons

(defthm aignet-nxsts-of-cons
 (equal
  (aignet-nxsts (cons node x))
  (cond
     ((and (equal (stype node) :nxst)
           (< (nxst-node->reg node)
              (stype-count :reg x)))
      (update-nth (- (stype-count :reg x)
                     (+ 1 (nxst-node->reg node)))
                  (nxst-node (aignet-lit-fix (nxst-node->fanin node)
                                             x)
                             (nxst-node->reg node))
                  (aignet-nxsts x)))
     ((equal (stype node) :reg)
      (cons (nxst-node (make-lit (+ 1 (fanin-count x)) 0)
                       (stype-count :reg x))
            (aignet-nxsts x)))
     (t (aignet-nxsts x)))))