• 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

• Gatesimp

!gatesimp->hashp

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

Signature

(!gatesimp->hashp hashp x) → new-x

Arguments

hashp — Guard (booleanp hashp).

x — Guard (gatesimp-p x).

Returns

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

Definitions and Theorems

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