• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
        • Gatesimp
          • Gatesimp-p
          • !gatesimp->xor-mode
          • !gatesimp->level
          • !gatesimp->hashp
          • Gatesimp-fix
          • Gatesimp->xor-mode
          • Gatesimp->level
          • Gatesimp->hashp
        • Aignet-hash-mux
        • Aignet-hash-xor
        • Aignet-hash-and
        • Aignet-hash-or
        • Aignet-hash-iff
        • Aignet-build
        • Patbind-aignet-build
      • Representation
      • 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

• Aignet-construction

Gatesimp

Structure encoding AIGNET construction settings for how much to try to simplify and whether to use hashing

This is a bitstruct type introduced by fty::defbitstruct, represented as a unsigned 6-bit integer.

Fields

hashp — boolean

level — gatesimp-level

xor-mode — gatesimp-xor-mode

A simple bit-encoded triple of level, hashp, and xor-mode.

The level field is a value between 0 and 4 inclusive, determining how hard to work to simplify new nodes. The numbers corresponding to the levels of simplification found in the paper:

R. Brummayer and A. Biere. Local two-level And-Inverter Graph minimization without blowup. Proc. MEMCIS 6 (2006): 32-38,

The xor-mode field is a value between 0 and 2 inclusive, determining whether to use XOR nodes:

• If 2, XOR nodes can be created using aignet-hash-xor and additionally, if the level is 3 or greater, derived when creating the AND of two nodes of the form (not (and a b)), (not (and (not a) (not b))).
• If 1, XOR nodes will be created when calling aignet-hash-xor, but not derived from existing AND gates.
• If 0, no XOR nodes will be used even when calling aignet-hash-xor, instead implementing the function using AND gates.

The hashp field is a Boolean and determines whether structural hashing is used.

To construct a gatesimp object, use either the constructor function gatesimp or the macro make-gatesimp, with the usual conventions of product types produced by fty::defprod and fty::defbitstruct.

Definitions and Theorems

Function: gatesimp-p

(defun gatesimp-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'gatesimp-p))
    (declare (ignorable __function__))
    (and (mbe :logic (unsigned-byte-p 6 x)
              :exec (and (natp x) (< x 64)))
         (gatesimp-level-p (part-select x :low 1 :width 3))
         (gatesimp-xor-mode-p (part-select x :low 4 :width 2)))))

Theorem: unsigned-byte-p-when-gatesimp-p

(defthm unsigned-byte-p-when-gatesimp-p
  (implies (gatesimp-p x)
           (unsigned-byte-p 6 x)))

Theorem: gatesimp-p-compound-recognizer

(defthm gatesimp-p-compound-recognizer
  (implies (gatesimp-p x) (natp x))
  :rule-classes :compound-recognizer)

Function: gatesimp-fix

(defun gatesimp-fix (x)
 (declare (xargs :guard (gatesimp-p x)))
 (let ((__function__ 'gatesimp-fix))
  (declare (ignorable __function__))
  (mbe
   :logic
   (loghead
    6
    (logapp
     1 (part-select x :width 1 :low 0)
     (logapp
          3
          (gatesimp-level-fix (part-select x :width 3 :low 1))
          (gatesimp-xor-mode-fix (part-select x :width 2 :low 4)))))
   :exec x)))

Theorem: gatesimp-p-of-gatesimp-fix

(defthm gatesimp-p-of-gatesimp-fix
  (b* ((fty::fixed (gatesimp-fix x)))
    (gatesimp-p fty::fixed))
  :rule-classes :rewrite)

Theorem: gatesimp-fix-when-gatesimp-p

(defthm gatesimp-fix-when-gatesimp-p
  (implies (gatesimp-p x)
           (equal (gatesimp-fix x) x)))

Function: gatesimp-equiv$inline

(defun gatesimp-equiv$inline (x acl2::y)
  (declare (xargs :guard (and (gatesimp-p x)
                              (gatesimp-p acl2::y))))
  (equal (gatesimp-fix x)
         (gatesimp-fix acl2::y)))

Theorem: gatesimp-equiv-is-an-equivalence

(defthm gatesimp-equiv-is-an-equivalence
  (and (booleanp (gatesimp-equiv x y))
       (gatesimp-equiv x x)
       (implies (gatesimp-equiv x y)
                (gatesimp-equiv y x))
       (implies (and (gatesimp-equiv x y)
                     (gatesimp-equiv y z))
                (gatesimp-equiv x z)))
  :rule-classes (:equivalence))

Theorem: gatesimp-equiv-implies-equal-gatesimp-fix-1

(defthm gatesimp-equiv-implies-equal-gatesimp-fix-1
  (implies (gatesimp-equiv x x-equiv)
           (equal (gatesimp-fix x)
                  (gatesimp-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: gatesimp-fix-under-gatesimp-equiv

(defthm gatesimp-fix-under-gatesimp-equiv
  (gatesimp-equiv (gatesimp-fix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: gatesimp

(defun gatesimp (hashp level xor-mode)
  (declare (xargs :guard (and (booleanp hashp)
                              (gatesimp-level-p level)
                              (gatesimp-xor-mode-p xor-mode))))
  (let ((__function__ 'gatesimp))
    (declare (ignorable __function__))
    (b* ((hashp (bool->bit hashp))
         (level (mbe :logic (gatesimp-level-fix level)
                     :exec level))
         (xor-mode (mbe :logic (gatesimp-xor-mode-fix xor-mode)
                        :exec xor-mode)))
      (logapp 1 hashp (logapp 3 level xor-mode)))))

Theorem: gatesimp-p-of-gatesimp

(defthm gatesimp-p-of-gatesimp
  (b* ((gatesimp (gatesimp hashp level xor-mode)))
    (gatesimp-p gatesimp))
  :rule-classes :rewrite)

Theorem: gatesimp-of-bool-fix-hashp

(defthm gatesimp-of-bool-fix-hashp
  (equal (gatesimp (acl2::bool-fix hashp)
                   level xor-mode)
         (gatesimp hashp level xor-mode)))

Theorem: gatesimp-iff-congruence-on-hashp

(defthm gatesimp-iff-congruence-on-hashp
  (implies (iff hashp hashp-equiv)
           (equal (gatesimp hashp level xor-mode)
                  (gatesimp hashp-equiv level xor-mode)))
  :rule-classes :congruence)

Theorem: gatesimp-of-gatesimp-level-fix-level

(defthm gatesimp-of-gatesimp-level-fix-level
  (equal (gatesimp hashp (gatesimp-level-fix level)
                   xor-mode)
         (gatesimp hashp level xor-mode)))

Theorem: gatesimp-gatesimp-level-equiv-congruence-on-level

(defthm gatesimp-gatesimp-level-equiv-congruence-on-level
  (implies (gatesimp-level-equiv level level-equiv)
           (equal (gatesimp hashp level xor-mode)
                  (gatesimp hashp level-equiv xor-mode)))
  :rule-classes :congruence)

Theorem: gatesimp-of-gatesimp-xor-mode-fix-xor-mode

(defthm gatesimp-of-gatesimp-xor-mode-fix-xor-mode
  (equal (gatesimp hashp
                   level (gatesimp-xor-mode-fix xor-mode))
         (gatesimp hashp level xor-mode)))

Theorem: gatesimp-gatesimp-xor-mode-equiv-congruence-on-xor-mode

(defthm gatesimp-gatesimp-xor-mode-equiv-congruence-on-xor-mode
  (implies (gatesimp-xor-mode-equiv xor-mode xor-mode-equiv)
           (equal (gatesimp hashp level xor-mode)
                  (gatesimp hashp level xor-mode-equiv)))
  :rule-classes :congruence)

Function: gatesimp-equiv-under-mask

(defun gatesimp-equiv-under-mask (x x1 mask)
  (declare (xargs :guard (and (gatesimp-p x)
                              (gatesimp-p x1)
                              (integerp mask))))
  (let ((__function__ 'gatesimp-equiv-under-mask))
    (declare (ignorable __function__))
    (fty::int-equiv-under-mask (gatesimp-fix x)
                               (gatesimp-fix x1)
                               mask)))

Function: gatesimp->hashp

(defun gatesimp->hashp (x)
  (declare (xargs :guard (gatesimp-p x)))
  (mbe :logic
       (let ((x (gatesimp-fix x)))
         (bit->bool (part-select x :low 0 :width 1)))
       :exec (bit->bool (the (unsigned-byte 1)
                             (logand (the (unsigned-byte 1) 1)
                                     (the (unsigned-byte 6) x))))))

Theorem: booleanp-of-gatesimp->hashp

(defthm booleanp-of-gatesimp->hashp
  (b* ((hashp (gatesimp->hashp x)))
    (booleanp hashp))
  :rule-classes :rewrite)

Theorem: gatesimp->hashp-of-gatesimp-fix-x

(defthm gatesimp->hashp-of-gatesimp-fix-x
  (equal (gatesimp->hashp (gatesimp-fix x))
         (gatesimp->hashp x)))

Theorem: gatesimp->hashp-gatesimp-equiv-congruence-on-x

(defthm gatesimp->hashp-gatesimp-equiv-congruence-on-x
  (implies (gatesimp-equiv x x-equiv)
           (equal (gatesimp->hashp x)
                  (gatesimp->hashp x-equiv)))
  :rule-classes :congruence)

Theorem: gatesimp->hashp-of-gatesimp

(defthm gatesimp->hashp-of-gatesimp
  (equal (gatesimp->hashp (gatesimp hashp level xor-mode))
         (acl2::bool-fix hashp)))

Theorem: gatesimp->hashp-of-write-with-mask

(defthm gatesimp->hashp-of-write-with-mask
 (implies
  (and
   (fty::bitstruct-read-over-write-hyps x gatesimp-equiv-under-mask)
   (gatesimp-equiv-under-mask x acl2::y fty::mask)
   (equal (logand (lognot fty::mask) 1) 0))
  (equal (gatesimp->hashp x)
         (gatesimp->hashp acl2::y))))

Function: gatesimp->level

(defun gatesimp->level (x)
 (declare (xargs :guard (gatesimp-p x)))
 (mbe
     :logic
     (let ((x (gatesimp-fix x)))
       (part-select x :low 1 :width 3))
     :exec (the (unsigned-byte 3)
                (logand (the (unsigned-byte 3) 7)
                        (the (unsigned-byte 5)
                             (ash (the (unsigned-byte 6) x) -1))))))

Theorem: gatesimp-level-p-of-gatesimp->level

(defthm gatesimp-level-p-of-gatesimp->level
  (b* ((level (gatesimp->level x)))
    (gatesimp-level-p level))
  :rule-classes :rewrite)

Theorem: gatesimp->level-of-gatesimp-fix-x

(defthm gatesimp->level-of-gatesimp-fix-x
  (equal (gatesimp->level (gatesimp-fix x))
         (gatesimp->level x)))

Theorem: gatesimp->level-gatesimp-equiv-congruence-on-x

(defthm gatesimp->level-gatesimp-equiv-congruence-on-x
  (implies (gatesimp-equiv x x-equiv)
           (equal (gatesimp->level x)
                  (gatesimp->level x-equiv)))
  :rule-classes :congruence)

Theorem: gatesimp->level-of-gatesimp

(defthm gatesimp->level-of-gatesimp
  (equal (gatesimp->level (gatesimp hashp level xor-mode))
         (gatesimp-level-fix level)))

Theorem: gatesimp->level-of-write-with-mask

(defthm gatesimp->level-of-write-with-mask
 (implies
  (and
   (fty::bitstruct-read-over-write-hyps x gatesimp-equiv-under-mask)
   (gatesimp-equiv-under-mask x acl2::y fty::mask)
   (equal (logand (lognot fty::mask) 14)
          0))
  (equal (gatesimp->level x)
         (gatesimp->level acl2::y))))

Function: gatesimp->xor-mode

(defun gatesimp->xor-mode (x)
 (declare (xargs :guard (gatesimp-p x)))
 (mbe
     :logic
     (let ((x (gatesimp-fix x)))
       (part-select x :low 4 :width 2))
     :exec (the (unsigned-byte 2)
                (logand (the (unsigned-byte 2) 3)
                        (the (unsigned-byte 2)
                             (ash (the (unsigned-byte 6) x) -4))))))

Theorem: gatesimp-xor-mode-p-of-gatesimp->xor-mode

(defthm gatesimp-xor-mode-p-of-gatesimp->xor-mode
  (b* ((xor-mode (gatesimp->xor-mode x)))
    (gatesimp-xor-mode-p xor-mode))
  :rule-classes :rewrite)

Theorem: gatesimp->xor-mode-of-gatesimp-fix-x

(defthm gatesimp->xor-mode-of-gatesimp-fix-x
  (equal (gatesimp->xor-mode (gatesimp-fix x))
         (gatesimp->xor-mode x)))

Theorem: gatesimp->xor-mode-gatesimp-equiv-congruence-on-x

(defthm gatesimp->xor-mode-gatesimp-equiv-congruence-on-x
  (implies (gatesimp-equiv x x-equiv)
           (equal (gatesimp->xor-mode x)
                  (gatesimp->xor-mode x-equiv)))
  :rule-classes :congruence)

Theorem: gatesimp->xor-mode-of-gatesimp

(defthm gatesimp->xor-mode-of-gatesimp
  (equal (gatesimp->xor-mode (gatesimp hashp level xor-mode))
         (gatesimp-xor-mode-fix xor-mode)))

Theorem: gatesimp->xor-mode-of-write-with-mask

(defthm gatesimp->xor-mode-of-write-with-mask
 (implies
  (and
   (fty::bitstruct-read-over-write-hyps x gatesimp-equiv-under-mask)
   (gatesimp-equiv-under-mask x acl2::y fty::mask)
   (equal (logand (lognot fty::mask) 48)
          0))
  (equal (gatesimp->xor-mode x)
         (gatesimp->xor-mode acl2::y))))

Theorem: gatesimp-fix-in-terms-of-gatesimp

(defthm gatesimp-fix-in-terms-of-gatesimp
  (equal (gatesimp-fix x)
         (change-gatesimp x)))

Function: !gatesimp->hashp

(defun !gatesimp->hashp (hashp x)
  (declare (xargs :guard (and (booleanp hashp) (gatesimp-p x))))
  (mbe :logic
       (b* ((hashp (bool->bit hashp))
            (x (gatesimp-fix x)))
         (part-install hashp x :width 1 :low 0))
       :exec (the (unsigned-byte 6)
                  (logior (the (unsigned-byte 6)
                               (logand (the (unsigned-byte 6) x)
                                       (the (signed-byte 2) -2)))
                          (the (unsigned-byte 1)
                               (bool->bit hashp))))))

Theorem: gatesimp-p-of-!gatesimp->hashp

(defthm gatesimp-p-of-!gatesimp->hashp
  (b* ((new-x (!gatesimp->hashp hashp x)))
    (gatesimp-p new-x))
  :rule-classes :rewrite)

Theorem: !gatesimp->hashp-of-bool-fix-hashp

(defthm !gatesimp->hashp-of-bool-fix-hashp
  (equal (!gatesimp->hashp (acl2::bool-fix hashp)
                           x)
         (!gatesimp->hashp hashp x)))

Theorem: !gatesimp->hashp-iff-congruence-on-hashp

(defthm !gatesimp->hashp-iff-congruence-on-hashp
  (implies (iff hashp hashp-equiv)
           (equal (!gatesimp->hashp hashp x)
                  (!gatesimp->hashp hashp-equiv x)))
  :rule-classes :congruence)

Theorem: !gatesimp->hashp-of-gatesimp-fix-x

(defthm !gatesimp->hashp-of-gatesimp-fix-x
  (equal (!gatesimp->hashp hashp (gatesimp-fix x))
         (!gatesimp->hashp hashp x)))

Theorem: !gatesimp->hashp-gatesimp-equiv-congruence-on-x

(defthm !gatesimp->hashp-gatesimp-equiv-congruence-on-x
  (implies (gatesimp-equiv x x-equiv)
           (equal (!gatesimp->hashp hashp x)
                  (!gatesimp->hashp hashp x-equiv)))
  :rule-classes :congruence)

Theorem: !gatesimp->hashp-is-gatesimp

(defthm !gatesimp->hashp-is-gatesimp
  (equal (!gatesimp->hashp hashp x)
         (change-gatesimp x :hashp hashp)))

Theorem: gatesimp->hashp-of-!gatesimp->hashp

(defthm gatesimp->hashp-of-!gatesimp->hashp
  (b* ((?new-x (!gatesimp->hashp hashp x)))
    (equal (gatesimp->hashp new-x)
           (acl2::bool-fix hashp))))

Theorem: !gatesimp->hashp-equiv-under-mask

(defthm !gatesimp->hashp-equiv-under-mask
  (b* ((?new-x (!gatesimp->hashp hashp x)))
    (gatesimp-equiv-under-mask new-x x -2)))

Function: !gatesimp->level

(defun !gatesimp->level (level x)
  (declare (xargs :guard (and (gatesimp-level-p level)
                              (gatesimp-p x))))
  (mbe :logic
       (b* ((level (mbe :logic (gatesimp-level-fix level)
                        :exec level))
            (x (gatesimp-fix x)))
         (part-install level x :width 3 :low 1))
       :exec (the (unsigned-byte 6)
                  (logior (the (unsigned-byte 6)
                               (logand (the (unsigned-byte 6) x)
                                       (the (signed-byte 5) -15)))
                          (the (unsigned-byte 4)
                               (ash (the (unsigned-byte 3) level)
                                    1))))))

Theorem: gatesimp-p-of-!gatesimp->level

(defthm gatesimp-p-of-!gatesimp->level
  (b* ((new-x (!gatesimp->level level x)))
    (gatesimp-p new-x))
  :rule-classes :rewrite)

Theorem: !gatesimp->level-of-gatesimp-level-fix-level

(defthm !gatesimp->level-of-gatesimp-level-fix-level
  (equal (!gatesimp->level (gatesimp-level-fix level)
                           x)
         (!gatesimp->level level x)))

Theorem: !gatesimp->level-gatesimp-level-equiv-congruence-on-level

(defthm !gatesimp->level-gatesimp-level-equiv-congruence-on-level
  (implies (gatesimp-level-equiv level level-equiv)
           (equal (!gatesimp->level level x)
                  (!gatesimp->level level-equiv x)))
  :rule-classes :congruence)

Theorem: !gatesimp->level-of-gatesimp-fix-x

(defthm !gatesimp->level-of-gatesimp-fix-x
  (equal (!gatesimp->level level (gatesimp-fix x))
         (!gatesimp->level level x)))

Theorem: !gatesimp->level-gatesimp-equiv-congruence-on-x

(defthm !gatesimp->level-gatesimp-equiv-congruence-on-x
  (implies (gatesimp-equiv x x-equiv)
           (equal (!gatesimp->level level x)
                  (!gatesimp->level level x-equiv)))
  :rule-classes :congruence)

Theorem: !gatesimp->level-is-gatesimp

(defthm !gatesimp->level-is-gatesimp
  (equal (!gatesimp->level level x)
         (change-gatesimp x :level level)))

Theorem: gatesimp->level-of-!gatesimp->level

(defthm gatesimp->level-of-!gatesimp->level
  (b* ((?new-x (!gatesimp->level level x)))
    (equal (gatesimp->level new-x)
           (gatesimp-level-fix level))))

Theorem: !gatesimp->level-equiv-under-mask

(defthm !gatesimp->level-equiv-under-mask
  (b* ((?new-x (!gatesimp->level level x)))
    (gatesimp-equiv-under-mask new-x x -15)))

Function: !gatesimp->xor-mode

(defun !gatesimp->xor-mode (xor-mode x)
  (declare (xargs :guard (and (gatesimp-xor-mode-p xor-mode)
                              (gatesimp-p x))))
  (mbe :logic
       (b* ((xor-mode (mbe :logic (gatesimp-xor-mode-fix xor-mode)
                           :exec xor-mode))
            (x (gatesimp-fix x)))
         (part-install xor-mode x
                       :width 2
                       :low 4))
       :exec (the (unsigned-byte 6)
                  (logior (the (unsigned-byte 6)
                               (logand (the (unsigned-byte 6) x)
                                       (the (signed-byte 7) -49)))
                          (the (unsigned-byte 6)
                               (ash (the (unsigned-byte 2) xor-mode)
                                    4))))))

Theorem: gatesimp-p-of-!gatesimp->xor-mode

(defthm gatesimp-p-of-!gatesimp->xor-mode
  (b* ((new-x (!gatesimp->xor-mode xor-mode x)))
    (gatesimp-p new-x))
  :rule-classes :rewrite)

Theorem: !gatesimp->xor-mode-of-gatesimp-xor-mode-fix-xor-mode

(defthm !gatesimp->xor-mode-of-gatesimp-xor-mode-fix-xor-mode
  (equal (!gatesimp->xor-mode (gatesimp-xor-mode-fix xor-mode)
                              x)
         (!gatesimp->xor-mode xor-mode x)))

Theorem: !gatesimp->xor-mode-gatesimp-xor-mode-equiv-congruence-on-xor-mode

(defthm
 !gatesimp->xor-mode-gatesimp-xor-mode-equiv-congruence-on-xor-mode
 (implies (gatesimp-xor-mode-equiv xor-mode xor-mode-equiv)
          (equal (!gatesimp->xor-mode xor-mode x)
                 (!gatesimp->xor-mode xor-mode-equiv x)))
 :rule-classes :congruence)

Theorem: !gatesimp->xor-mode-of-gatesimp-fix-x

(defthm !gatesimp->xor-mode-of-gatesimp-fix-x
  (equal (!gatesimp->xor-mode xor-mode (gatesimp-fix x))
         (!gatesimp->xor-mode xor-mode x)))

Theorem: !gatesimp->xor-mode-gatesimp-equiv-congruence-on-x

(defthm !gatesimp->xor-mode-gatesimp-equiv-congruence-on-x
  (implies (gatesimp-equiv x x-equiv)
           (equal (!gatesimp->xor-mode xor-mode x)
                  (!gatesimp->xor-mode xor-mode x-equiv)))
  :rule-classes :congruence)

Theorem: !gatesimp->xor-mode-is-gatesimp

(defthm !gatesimp->xor-mode-is-gatesimp
  (equal (!gatesimp->xor-mode xor-mode x)
         (change-gatesimp x :xor-mode xor-mode)))

Theorem: gatesimp->xor-mode-of-!gatesimp->xor-mode

(defthm gatesimp->xor-mode-of-!gatesimp->xor-mode
  (b* ((?new-x (!gatesimp->xor-mode xor-mode x)))
    (equal (gatesimp->xor-mode new-x)
           (gatesimp-xor-mode-fix xor-mode))))

Theorem: !gatesimp->xor-mode-equiv-under-mask

(defthm !gatesimp->xor-mode-equiv-under-mask
  (b* ((?new-x (!gatesimp->xor-mode xor-mode x)))
    (gatesimp-equiv-under-mask new-x x 15)))

Function: gatesimp-debug

(defun gatesimp-debug (x)
  (declare (xargs :guard (gatesimp-p x)))
  (let ((__function__ 'gatesimp-debug))
    (declare (ignorable __function__))
    (b* (((gatesimp x)))
      (cons (cons 'hashp x.hashp)
            (cons (cons 'level x.level)
                  (cons (cons 'xor-mode x.xor-mode)
                        nil))))))

Subtopics

Gatesimp-p

Recognizer for gatesimp bit structures.

!gatesimp->xor-mode

Update the |AIGNET|::|XOR-MODE| field of a gatesimp bit structure.

!gatesimp->level

Update the |AIGNET|::|LEVEL| field of a gatesimp bit structure.

!gatesimp->hashp

Update the |AIGNET|::|HASHP| field of a gatesimp bit structure.

Gatesimp-fix

Fixing function for gatesimp bit structures.

Gatesimp->xor-mode

Access the |AIGNET|::|XOR-MODE| field of a gatesimp bit structure.

Gatesimp->level

Access the |AIGNET|::|LEVEL| field of a gatesimp bit structure.

Gatesimp->hashp

Access the |AIGNET|::|HASHP| field of a gatesimp bit structure.