		Search-engine friendly clone of the ACL2 documentation.

Network

Lookup-reg->nxst

Look up the next-state node that corresponds to particular register node.

Signature
(lookup-reg->nxst reg aignet) → nxst-lit
Arguments: reg — Register number for this register.
Guard (natp reg).; aignet — Guard (node-listp aignet).
Returns: nxst-lit — Type (litp nxst-lit).

Note: This is different from the other lookups: it's by ID of the corresponding RO node, not IO number. I think the asymmetry is worth it though.

Definitions and Theorems

Function: lookup-reg->nxst

(defun lookup-reg->nxst (reg aignet)
  (declare (xargs :guard (and (natp reg) (node-listp aignet))))
  (let ((__function__ 'lookup-reg->nxst))
    (declare (ignorable __function__))
    (cond ((endp aignet) 0)
          ((and (equal (stype (car aignet))
                       (nxst-stype))
                (b* ((ro (nxst-node->reg (car aignet))))
                  (and (nat-equiv reg ro)
                       (< ro (stype-count :reg aignet)))))
           (aignet-lit-fix (nxst-node->fanin (car aignet))
                           aignet))
          ((and (equal (stype (car aignet)) (reg-stype))
                (nat-equiv (stype-count :reg (cdr aignet))
                           reg))
           (make-lit (fanin-count aignet) 0))
          (t (lookup-reg->nxst reg (cdr aignet))))))

Theorem: litp-of-lookup-reg->nxst

(defthm litp-of-lookup-reg->nxst
  (b* ((nxst-lit (lookup-reg->nxst reg aignet)))
    (litp nxst-lit))
  :rule-classes :type-prescription)

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

(defthm aignet-litp-of-lookup-reg->nxst
  (aignet-litp (lookup-reg->nxst reg aignet)
               aignet))

Theorem: lookup-reg->nxst-of-nfix-reg

(defthm lookup-reg->nxst-of-nfix-reg
  (equal (lookup-reg->nxst (nfix reg) aignet)
         (lookup-reg->nxst reg aignet)))

Theorem: lookup-reg->nxst-nat-equiv-congruence-on-reg

(defthm lookup-reg->nxst-nat-equiv-congruence-on-reg
  (implies (nat-equiv reg reg-equiv)
           (equal (lookup-reg->nxst reg aignet)
                  (lookup-reg->nxst reg-equiv aignet)))
  :rule-classes :congruence)

Theorem: lookup-reg->nxst-of-node-list-fix-aignet

(defthm lookup-reg->nxst-of-node-list-fix-aignet
  (equal (lookup-reg->nxst reg (node-list-fix aignet))
         (lookup-reg->nxst reg aignet)))

Theorem: lookup-reg->nxst-node-list-equiv-congruence-on-aignet

(defthm lookup-reg->nxst-node-list-equiv-congruence-on-aignet
  (implies (node-list-equiv aignet aignet-equiv)
           (equal (lookup-reg->nxst reg aignet)
                  (lookup-reg->nxst reg aignet-equiv)))
  :rule-classes :congruence)

Theorem: lookup-reg->nxst-id-bound

(defthm lookup-reg->nxst-id-bound
  (<= (lit->var (lookup-reg->nxst n aignet))
      (fanin-count aignet))
  :rule-classes :linear)

Theorem: lookup-reg->nxst-out-of-bounds

(defthm lookup-reg->nxst-out-of-bounds
  (implies (<= (stype-count :reg aignet) (nfix n))
           (equal (lookup-reg->nxst n aignet) 0)))