• 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-with-tracking
      • Aignet-simplify-marked-with-tracking
      • Aignet-cnf
      • Aignet-simplify-marked
      • Aignet-complete-copy
      • Aignet-transforms
      • Aignet-eval
      • Semantics
      • 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
  • Math
  • Testing-utilities

• Network

Stype-count

(stype-count type x) counts the number of nodes whose sequential-type is type in the node list x.

Signature

(stype-count type x) → count

Arguments

type — Guard (stypep type).

x — Guard (node-listp x).

Returns

count — Type (natp count).

This is a key function in the logical story of Aignet input, output, and register numbering. See representation for more details.

Definitions and Theorems

Function: stype-count

(defun stype-count (type x)
  (declare (xargs :guard (and (stypep type) (node-listp x))))
  (let ((__function__ 'stype-count))
    (declare (ignorable __function__))
    (cond ((atom x) 0)
          ((equal (stype-fix type) (stype (car x)))
           (+ 1 (stype-count type (cdr x))))
          (t (stype-count type (cdr x))))))

Theorem: natp-of-stype-count

(defthm natp-of-stype-count
  (b* ((count (stype-count type x)))
    (natp count))
  :rule-classes :type-prescription)

Theorem: stype-count-of-cons

(defthm stype-count-of-cons
  (equal (stype-count type (cons a b))
         (if (equal (stype-fix type) (stype a))
             (+ 1 (stype-count type b))
           (stype-count type b))))

Theorem: stype-count-of-atom

(defthm stype-count-of-atom
  (implies (not (consp x))
           (equal (stype-count type x) 0))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: positive-stype-count-implies-consp

(defthm positive-stype-count-implies-consp
  (implies (< 0 (stype-count stype x))
           (consp x))
  :rule-classes :forward-chaining)

Theorem: stype-count-of-stype-fix-type

(defthm stype-count-of-stype-fix-type
  (equal (stype-count (stype-fix type) x)
         (stype-count type x)))

Theorem: stype-count-stype-equiv-congruence-on-type

(defthm stype-count-stype-equiv-congruence-on-type
  (implies (stype-equiv type type-equiv)
           (equal (stype-count type x)
                  (stype-count type-equiv x)))
  :rule-classes :congruence)

Theorem: stype-count-of-node-list-fix-x

(defthm stype-count-of-node-list-fix-x
  (equal (stype-count type (node-list-fix x))
         (stype-count type x)))

Theorem: stype-count-node-list-equiv-congruence-on-x

(defthm stype-count-node-list-equiv-congruence-on-x
  (implies (node-list-equiv x x-equiv)
           (equal (stype-count type x)
                  (stype-count type x-equiv)))
  :rule-classes :congruence)