• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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-or
        • Aignet-hash-and
        • Aignet-hash-xor
        • Aignet-hash-iff
        • Aignet-build
        • Patbind-aignet-build
      • Representation
      • 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
  • Testing-utilities
  • Math

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

Theorem: gatesimp-fix-of-gatesimp-fix-x

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

Theorem: gatesimp-fix-gatesimp-equiv-congruence-on-x

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

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

Theorem: gatesimp-equiv-under-mask-of-gatesimp-fix-x

(defthm gatesimp-equiv-under-mask-of-gatesimp-fix-x
        (equal (gatesimp-equiv-under-mask (gatesimp-fix x)
                                          x1 mask)
               (gatesimp-equiv-under-mask x x1 mask)))

Theorem: gatesimp-equiv-under-mask-gatesimp-equiv-congruence-on-x

(defthm
     gatesimp-equiv-under-mask-gatesimp-equiv-congruence-on-x
     (implies (gatesimp-equiv x x-equiv)
              (equal (gatesimp-equiv-under-mask x x1 mask)
                     (gatesimp-equiv-under-mask x-equiv x1 mask)))
     :rule-classes :congruence)

Theorem: gatesimp-equiv-under-mask-of-gatesimp-fix-x1

(defthm gatesimp-equiv-under-mask-of-gatesimp-fix-x1
        (equal (gatesimp-equiv-under-mask x (gatesimp-fix x1)
                                          mask)
               (gatesimp-equiv-under-mask x x1 mask)))

Theorem: gatesimp-equiv-under-mask-gatesimp-equiv-congruence-on-x1

(defthm
     gatesimp-equiv-under-mask-gatesimp-equiv-congruence-on-x1
     (implies (gatesimp-equiv x1 x1-equiv)
              (equal (gatesimp-equiv-under-mask x x1 mask)
                     (gatesimp-equiv-under-mask x x1-equiv mask)))
     :rule-classes :congruence)

Theorem: gatesimp-equiv-under-mask-of-ifix-mask

(defthm gatesimp-equiv-under-mask-of-ifix-mask
        (equal (gatesimp-equiv-under-mask x x1 (ifix mask))
               (gatesimp-equiv-under-mask x x1 mask)))

Theorem: gatesimp-equiv-under-mask-int-equiv-congruence-on-mask

(defthm
     gatesimp-equiv-under-mask-int-equiv-congruence-on-mask
     (implies (int-equiv mask mask-equiv)
              (equal (gatesimp-equiv-under-mask x x1 mask)
                     (gatesimp-equiv-under-mask x x1 mask-equiv)))
     :rule-classes :congruence)

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

Theorem: gatesimp-debug-of-gatesimp-fix-x

(defthm gatesimp-debug-of-gatesimp-fix-x
        (equal (gatesimp-debug (gatesimp-fix x))
               (gatesimp-debug x)))

Theorem: gatesimp-debug-gatesimp-equiv-congruence-on-x

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

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.