• 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

• Litp

Make-lit

Construct a literal with the given var and neg.

Signature

(make-lit var neg) → lit

Arguments

var — Guard (varp var).

neg — Guard (bitp neg).

Returns

lit — Type (litp lit).

Definitions and Theorems

Function: make-lit$inline

(defun make-lit$inline (var neg)
  (declare (type (integer 0 *) var)
           (type bit neg))
  (declare (xargs :guard (and (varp var) (bitp neg))))
  (declare (xargs :split-types t))
  (let ((__function__ 'make-lit))
    (declare (ignorable __function__))
    (the (integer 0 *)
         (logior (the (integer 0 *)
                      (ash (the (integer 0 *) (var-fix var))
                           1))
                 (the bit (lbfix neg))))))

Theorem: litp-of-make-lit

(defthm litp-of-make-lit
  (b* ((lit (make-lit$inline var neg)))
    (litp lit))
  :rule-classes (:rewrite :type-prescription))

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)

Theorem: lit->var-of-make-lit

(defthm lit->var-of-make-lit
  (equal (lit->var (make-lit var neg))
         (var-fix var)))

Theorem: lit->neg-of-make-lit

(defthm lit->neg-of-make-lit
  (equal (lit->neg (make-lit var neg))
         (bfix neg)))

Theorem: make-lit-identity

(defthm make-lit-identity
  (equal (make-lit (lit->var lit) (lit->neg lit))
         (lit-fix lit)))

Theorem: equal-of-make-lit

(defthm equal-of-make-lit
  (equal (equal a (make-lit var neg))
         (and (litp a)
              (equal (lit->var a) (var-fix var))
              (equal (lit->neg a) (bfix neg)))))

Subtopics

Make-lit^

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