• Top
  • Documentation
  • Books
  • 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
          • Aignet-fanins
          • Stype-count
          • 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
        • Typecode
        • Stypep
      • 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
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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)))))