• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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
          • Maybe-litp
          • Lit-list
          • 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
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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.