		Search-engine friendly clone of the ACL2 documentation.

Network

Fanin

(fanin which aignet) gets the specified fanin from the first node of the input network and fixes it to be a valid fanin literal of the rest of the network.

Signature
(fanin which aignet) → lit
Arguments: which — Guard (bitp which).; aignet — Guard (node-listp aignet).
Returns: lit — Type (litp lit).

Definitions and Theorems

Function: fanin

(defun
    fanin (which aignet)
    (declare (xargs :guard (and (bitp which) (node-listp aignet))))
    (declare (xargs :guard (and (consp aignet)
                                (or (eq (ctype (stype (car aignet)))
                                        :output)
                                    (eq (ctype (stype (car aignet)))
                                        :gate)))))
    (let ((__function__ 'fanin))
         (declare (ignorable __function__))
         (aignet-lit-fix (if (eq (ctype (stype (car aignet)))
                                 :output)
                             (co-node->fanin (car aignet))
                             (if (bit->bool which)
                                 (gate-node->fanin1 (car aignet))
                                 (gate-node->fanin0 (car aignet))))
                         (cdr aignet))))

Theorem: litp-of-fanin

(defthm litp-of-fanin
        (b* ((lit (fanin which aignet)))
            (litp lit))
        :rule-classes :type-prescription)

Theorem: fanin-id-lte-fanin-count

(defthm fanin-id-lte-fanin-count
        (b* ((satlink::?lit (fanin which aignet)))
            (<= (lit-id lit)
                (fanin-count (cdr aignet))))
        :rule-classes :linear)

Theorem: fanin-id-lte-fanin-count-strong

(defthm fanin-id-lte-fanin-count-strong
        (b* ((satlink::?lit (fanin which aignet)))
            (implies (and (consp aignet)
                          (fanin-node-p (car aignet)))
                     (< (lit-id lit) (fanin-count aignet))))
        :rule-classes :linear)

Theorem: aignet-litp-of-fanin

(defthm aignet-litp-of-fanin
        (b* ((satlink::?lit (fanin which aignet)))
            (aignet-litp lit aignet)))

Theorem: aignet-litp-in-extension-of-fanin

(defthm aignet-litp-in-extension-of-fanin
        (b* ((satlink::?lit (fanin which aignet)))
            (implies (aignet-extension-p new aignet)
                     (aignet-litp lit new))))

Theorem: fanin-of-cons

(defthm fanin-of-cons
        (equal (fanin which (cons node aignet))
               (aignet-lit-fix (if (eq (ctype (stype node)) :output)
                                   (co-node->fanin node)
                                   (if (bit->bool which)
                                       (gate-node->fanin1 node)
                                       (gate-node->fanin0 node)))
                               aignet)))

Theorem: fanin-of-bfix-which

(defthm fanin-of-bfix-which
        (equal (fanin (bfix which) aignet)
               (fanin which aignet)))

Theorem: fanin-bit-equiv-congruence-on-which

(defthm fanin-bit-equiv-congruence-on-which
        (implies (bit-equiv which which-equiv)
                 (equal (fanin which aignet)
                        (fanin which-equiv aignet)))
        :rule-classes :congruence)

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

(defthm fanin-of-node-list-fix-aignet
        (equal (fanin which (node-list-fix aignet))
               (fanin which aignet)))

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

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