• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
      • Config-p
      • Logical-story
      • Dimacs
      • Gather-benchmarks
      • Cnf
        • Litp
          • Lit-negate-cond
            • Lit-negate-cond^
          • Lit-negate
          • Make-lit
          • Lit-equiv
          • Lit->var
          • Lit->neg
          • Lit-list
          • Maybe-litp
          • Lit-fix
          • Lit-list-list
        • Varp
        • Env$
        • Eval-formula
        • Max-index-formula
        • Max-index-clause
        • Formula-indices
        • Clause-indices
      • Satlink-extra-hook
      • Sat
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Lit-negate-cond

Lit-negate-cond^

Same as lit-negate-cond, but with a type declaration that the input literal is 32 bits unsigned.

Signature

(lit-negate-cond^ lit neg) → *

Arguments

lit — Guard (litp lit).

neg — Guard (bitp neg).

Definitions and Theorems

Function: lit-negate-cond^$inline

(defun lit-negate-cond^$inline (lit neg)
  (declare (type (unsigned-byte 32) lit)
           (type bit neg))
  (declare (xargs :guard (and (litp lit) (bitp neg))))
  (declare (xargs :guard (unsigned-byte-p 32 lit)
                  :split-types t))
  (let ((__function__ 'lit-negate-cond^))
    (declare (ignorable __function__))
    (mbe :logic (lit-negate-cond lit neg)
         :exec (the (unsigned-byte 32)
                    (logxor neg (the (unsigned-byte 32) lit))))))

Theorem: lit-negate-cond^$inline-of-lit-fix-lit

(defthm lit-negate-cond^$inline-of-lit-fix-lit
  (equal (lit-negate-cond^$inline (lit-fix lit)
                                  neg)
         (lit-negate-cond^$inline lit neg)))

Theorem: lit-negate-cond^$inline-lit-equiv-congruence-on-lit

(defthm lit-negate-cond^$inline-lit-equiv-congruence-on-lit
  (implies (lit-equiv lit lit-equiv)
           (equal (lit-negate-cond^$inline lit neg)
                  (lit-negate-cond^$inline lit-equiv neg)))
  :rule-classes :congruence)

Theorem: lit-negate-cond^$inline-of-bfix-neg

(defthm lit-negate-cond^$inline-of-bfix-neg
  (equal (lit-negate-cond^$inline lit (bfix neg))
         (lit-negate-cond^$inline lit neg)))

Theorem: lit-negate-cond^$inline-bit-equiv-congruence-on-neg

(defthm lit-negate-cond^$inline-bit-equiv-congruence-on-neg
  (implies (bit-equiv neg neg-equiv)
           (equal (lit-negate-cond^$inline lit neg)
                  (lit-negate-cond^$inline lit neg-equiv)))
  :rule-classes :congruence)