		Search-engine friendly clone of the ACL2 documentation.

Fraig

Aignet-maybe-update-refs

Signature
(aignet-maybe-update-refs prev-count aignet-refcounts aignet) → new-refcounts
Arguments: prev-count — Guard (natp prev-count).

Definitions and Theorems

Function: aignet-maybe-update-refs

(defun aignet-maybe-update-refs (prev-count aignet-refcounts aignet)
 (declare (xargs :stobjs (aignet-refcounts aignet)))
 (declare (xargs :guard (natp prev-count)))
 (let ((__function__ 'aignet-maybe-update-refs))
  (declare (ignorable __function__))
  (b* ((aignet-refcounts
            (if (< (u32-length aignet-refcounts)
                   (num-fanins aignet))
                (resize-u32 (max 16 (* 2 (num-fanins aignet)))
                            aignet-refcounts)
              aignet-refcounts))
       ((unless (< (lnfix prev-count)
                   (num-fanins aignet)))
        aignet-refcounts)
       (id (1- (num-fanins aignet))))
   (aignet-case
      (id->type id aignet)
      :gate
      (b* ((aignet-refcounts (set-u32 id 0 aignet-refcounts))
           (id0 (lit-id (gate-id->fanin0 id aignet)))
           (id1 (lit-id (gate-id->fanin1 id aignet)))
           (aignet-refcounts
                (set-u32 id0
                         (nfix (+ 1 (get-u32 id0 aignet-refcounts)))
                         aignet-refcounts)))
        (set-u32 id1
                 (nfix (+ 1 (get-u32 id0 aignet-refcounts)))
                 aignet-refcounts))
      :const aignet-refcounts
      :in aignet-refcounts
      :out aignet-refcounts))))

Theorem: new-refcounts-length-of-aignet-maybe-udpate-refs

(defthm new-refcounts-length-of-aignet-maybe-udpate-refs
 (b*
  ((?new-refcounts
     (aignet-maybe-update-refs prev-count aignet-refcounts aignet)))
  (< (fanin-count aignet)
     (len new-refcounts)))
 :rule-classes :linear)

Theorem: aignet-maybe-update-refs-of-nfix-prev-count

(defthm aignet-maybe-update-refs-of-nfix-prev-count
 (equal
     (aignet-maybe-update-refs (nfix prev-count)
                               aignet-refcounts aignet)
     (aignet-maybe-update-refs prev-count aignet-refcounts aignet)))

Theorem: aignet-maybe-update-refs-nat-equiv-congruence-on-prev-count

(defthm aignet-maybe-update-refs-nat-equiv-congruence-on-prev-count
 (implies
  (nat-equiv prev-count prev-count-equiv)
  (equal
       (aignet-maybe-update-refs prev-count aignet-refcounts aignet)
       (aignet-maybe-update-refs prev-count-equiv
                                 aignet-refcounts aignet)))
 :rule-classes :congruence)