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

• Make-lit

Make-lit^

Same as make-lit, but with a type declaration that the input variable is 31 bits unsigned.

Signature

(make-lit^ var neg) → *

Arguments

var — Guard (varp var).

neg — Guard (bitp neg).

Definitions and Theorems

Function: make-lit^$inline

(defun make-lit^$inline (var neg)
 (declare (type (unsigned-byte 31) var)
          (type bit neg))
 (declare (xargs :guard (and (varp var) (bitp neg))))
 (declare (xargs :guard (unsigned-byte-p 31 var)
                 :split-types t))
 (let ((__function__ 'make-lit^))
  (declare (ignorable __function__))
  (mbe :logic (make-lit var neg)
       :exec (the (unsigned-byte 32)
                  (logior (the (unsigned-byte 32)
                               (ash (the (unsigned-byte 31) var) 1))
                          (the bit neg))))))

Theorem: make-lit^$inline-of-var-fix-var

(defthm make-lit^$inline-of-var-fix-var
  (equal (make-lit^$inline (var-fix var) neg)
         (make-lit^$inline var neg)))

Theorem: make-lit^$inline-var-equiv-congruence-on-var

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

Theorem: make-lit^$inline-of-bfix-neg

(defthm make-lit^$inline-of-bfix-neg
  (equal (make-lit^$inline var (bfix neg))
         (make-lit^$inline var neg)))

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

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