Filtering...

aignet-exec

books/centaur/aignet/aignet-exec
other
(in-package "AIGNET$C")
other
(local (include-book "aignet-exec-thms"))
other
(include-book "std/util/defredundant" :dir :system)
other
(set-enforce-redundancy t)
other
(include-book "litp")
other
(include-book "snodes")
other
(include-book "std/util/define" :dir :system)
other
(defredundant :names (const-type gate-type
    in-type
    aignet
    aignet-sizes-ok
    id->slot
    id->slot0
    id->slot1
    id->slot$
    set-snode->fanin
    update-node-slot
    update-node-slot0
    update-node-slot1
    update-node-slot$
    maybe-grow-nodes
    maybe-grow-ins
    maybe-grow-regs
    maybe-grow-outs
    set-innum->id
    innum->id
    set-regnum->id
    regnum->id
    set-outnum->fanin
    outnum->fanin
    lit->phase
    count-nodes
    add-node
    add-in
    add-out
    add-reg
    aignet-add-in
    aignet-add-reg
    aignet-add-and
    aignet-add-xor
    aignet-add-out
    aignet-set-nxst
    aignet-rollback
    aignet-clear
    aignet-init
    id-existsp))