• 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
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Gatesimp

!gatesimp->xor-mode

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

Signature

(!gatesimp->xor-mode xor-mode x) → new-x

Arguments

xor-mode — Guard (gatesimp-xor-mode-p xor-mode).

x — Guard (gatesimp-p x).

Returns

new-x — Type (gatesimp-p new-x).

Definitions and Theorems

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