• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
      • Representation
        • Aignet-impl
        • Node
        • Network
          • Lookup-id
          • Lookup-stype
          • Aignet-extension-p
          • Aignet-nodes-ok
          • Aignet-outputs-aux
          • Aignet-nxsts-aux
          • Fanin
          • Aignet-outputs
          • Lookup-reg->nxst
          • Aignet-lit-fix
          • Stype-count
          • Aignet-fanins
          • Aignet-nxsts
          • Aignet-idp
          • Aignet-norm
          • Aignet-norm-p
          • Aignet-id-fix
          • Fanin-count
          • Proper-node-listp
          • Fanin-node-p
          • Node-list
          • Aignet-litp
        • Combinational-type
        • Stypep
        • Typecode
      • Aignet-copy-init
      • Aignet-simplify-marked-with-tracking
      • Aignet-cnf
      • Aignet-simplify-with-tracking
      • Aignet-complete-copy
      • Aignet-eval
      • Semantics
      • Aignet-transforms
      • Aignet-simplify-marked
      • Aignet-read-aiger
      • Aignet-write-aiger
      • Aignet-abc-interface
      • Utilities
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Network

Lookup-stype

Core function for looking up an input, output, or register in the logical AIG network by its IO number.

Signature

(lookup-stype n stype aignet) → suffix

Arguments

n — Guard (natp n).

stype — Guard (stypep stype).

aignet — Guard (node-listp aignet).

Returns

suffix — Type (node-listp suffix).

See representation to understand IO numbers and IO lookups.

Definitions and Theorems

Function: lookup-stype

(defun lookup-stype (n stype aignet)
       (declare (xargs :guard (and (natp n)
                                   (stypep stype)
                                   (node-listp aignet))))
       (let ((__function__ 'lookup-stype))
            (declare (ignorable __function__))
            (cond ((endp aignet) (node-list-fix aignet))
                  ((and (equal (stype (car aignet))
                               (stype-fix stype))
                        (equal (stype-count stype (cdr aignet))
                               (lnfix n)))
                   (node-list-fix aignet))
                  (t (lookup-stype n stype (cdr aignet))))))

Theorem: node-listp-of-lookup-stype

(defthm node-listp-of-lookup-stype
        (b* ((suffix (lookup-stype n stype aignet)))
            (node-listp suffix))
        :rule-classes :rewrite)

Theorem: lookup-stype-of-nfix-n

(defthm lookup-stype-of-nfix-n
        (equal (lookup-stype (nfix n) stype aignet)
               (lookup-stype n stype aignet)))

Theorem: lookup-stype-nat-equiv-congruence-on-n

(defthm lookup-stype-nat-equiv-congruence-on-n
        (implies (nat-equiv n n-equiv)
                 (equal (lookup-stype n stype aignet)
                        (lookup-stype n-equiv stype aignet)))
        :rule-classes :congruence)

Theorem: lookup-stype-of-stype-fix-stype

(defthm lookup-stype-of-stype-fix-stype
        (equal (lookup-stype n (stype-fix stype)
                             aignet)
               (lookup-stype n stype aignet)))

Theorem: lookup-stype-stype-equiv-congruence-on-stype

(defthm lookup-stype-stype-equiv-congruence-on-stype
        (implies (stype-equiv stype stype-equiv)
                 (equal (lookup-stype n stype aignet)
                        (lookup-stype n stype-equiv aignet)))
        :rule-classes :congruence)

Theorem: lookup-stype-of-node-list-fix-aignet

(defthm lookup-stype-of-node-list-fix-aignet
        (equal (lookup-stype n stype (node-list-fix aignet))
               (lookup-stype n stype aignet)))

Theorem: lookup-stype-node-list-equiv-congruence-on-aignet

(defthm lookup-stype-node-list-equiv-congruence-on-aignet
        (implies (node-list-equiv aignet aignet-equiv)
                 (equal (lookup-stype n stype aignet)
                        (lookup-stype n stype aignet-equiv)))
        :rule-classes :congruence)

Theorem: stype-count-of-cdr-lookup-stype

(defthm
   stype-count-of-cdr-lookup-stype
   (implies (< (nfix n) (stype-count stype aignet))
            (equal (stype-count stype
                                (cdr (lookup-stype n stype aignet)))
                   (nfix n))))

Theorem: car-of-lookup-stype

(defthm car-of-lookup-stype
        (implies (< (nfix n) (stype-count stype aignet))
                 (equal (stype (car (lookup-stype n stype aignet)))
                        (stype-fix stype))))

Theorem: lookup-stype-in-bounds

(defthm lookup-stype-in-bounds
        (iff (consp (lookup-stype n stype aignet))
             (< (nfix n)
                (stype-count stype aignet))))

Theorem: lookup-stype-aignet-extension-p

(defthm lookup-stype-aignet-extension-p
        (aignet-extension-p aignet (lookup-stype n stype aignet)))

Theorem: lookup-stype-of-stype-count

(defthm lookup-stype-of-stype-count
        (implies (and (aignet-extension-p new orig)
                      (equal (stype (car orig))
                             (stype-fix stype))
                      (not (equal (stype-fix stype)
                                  (const-stype))))
                 (equal (lookup-stype (stype-count stype (cdr orig))
                                      stype new)
                        (node-list-fix orig))))

Theorem: lookup-stype-in-extension

(defthm lookup-stype-in-extension
        (implies (and (aignet-extension-binding)
                      (consp (lookup-stype n stype orig)))
                 (equal (lookup-stype n stype new)
                        (lookup-stype n stype orig))))

Theorem: lookup-stype-in-extension-inverse

(defthm lookup-stype-in-extension-inverse
        (implies (and (aignet-extension-bind-inverse)
                      (consp (lookup-stype n stype orig)))
                 (equal (lookup-stype n stype orig)
                        (lookup-stype n stype new))))

Theorem: stype-of-lookup-stype

(defthm stype-of-lookup-stype
        (implies (consp (lookup-stype n stype aignet))
                 (equal (stype (car (lookup-stype n stype aignet)))
                        (stype-fix stype))))

Theorem: stype-of-lookup-stype-split

(defthm stype-of-lookup-stype-split
        (equal (stype (car (lookup-stype n stype aignet)))
               (if (consp (lookup-stype n stype aignet))
                   (stype-fix stype)
                   :const)))

Theorem: aignet-extension-simplify-lookup-stype-when-counts-same

(defthm aignet-extension-simplify-lookup-stype-when-counts-same
        (implies (and (aignet-extension-binding)
                      (equal (stype-count stype new)
                             (stype-count stype orig)))
                 (equal (lookup-stype n stype new)
                        (lookup-stype n stype orig))))

Theorem: aignet-extension-simplify-lookup-stype-inverse

(defthm aignet-extension-simplify-lookup-stype-inverse
        (implies (and (aignet-extension-bind-inverse)
                      (consp (lookup-stype n stype orig)))
                 (equal (lookup-stype n stype orig)
                        (lookup-stype n stype new))))

Theorem: lookup-stype-out-of-bounds

(defthm lookup-stype-out-of-bounds
        (implies (<= (stype-count stype aignet) (nfix n))
                 (equal (lookup-stype n stype aignet)
                        nil)))

Theorem: consp-of-lookup-stype

(defthm consp-of-lookup-stype
        (implies (natp n)
                 (equal (consp (lookup-stype n stype aignet))
                        (< (nfix n)
                           (stype-count stype aignet)))))

Theorem: stype-count-of-lookup-stype-split

(defthm stype-count-of-lookup-stype-split
        (equal (stype-count stype (lookup-stype n stype aignet))
               (if (< (nfix n) (stype-count stype aignet))
                   (+ 1 (nfix n))
                   0)))

Theorem: stype-count-of-lookup-stype

(defthm
   stype-count-of-lookup-stype
   (implies (< (nfix n) (stype-count stype aignet))
            (equal (stype-count stype (lookup-stype n stype aignet))
                   (+ 1 (nfix n)))))