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

Lit-negate

Efficiently negate a literal.

Signature
(lit-negate lit) → new-lit
Arguments
lit — Guard (litp lit).
Returns
new-lit — Type (litp new-lit).

Definitions and Theorems

Function: lit-negate$inline

(defun lit-negate$inline (lit)
  (declare (type (integer 0 *) lit))
  (declare (xargs :guard (litp lit)))
  (declare (xargs :split-types t))
  (let ((__function__ 'lit-negate))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((var (lit->var lit))
              (neg (lit->neg lit)))
           (make-lit var (b-not neg)))
         :exec (the (integer 0 *)
                    (logxor (the (integer 0 *) lit) 1)))))

Theorem: litp-of-lit-negate

(defthm litp-of-lit-negate
  (b* ((new-lit (lit-negate$inline lit)))
    (litp new-lit))
  :rule-classes :rewrite)

Theorem: lit->var-of-lit-negate

(defthm lit->var-of-lit-negate
  (b* ((?new-lit (lit-negate$inline lit)))
    (equal (lit->var new-lit)
           (lit->var lit))))

Theorem: lit->neg-of-lit-negate

(defthm lit->neg-of-lit-negate
  (b* ((?new-lit (lit-negate$inline lit)))
    (equal (lit->neg new-lit)
           (b-not (lit->neg lit)))))

Theorem: lit-negate-of-make-lit

(defthm lit-negate-of-make-lit
  (equal (lit-negate (make-lit var neg))
         (make-lit var (b-not neg))))

Theorem: lit-negate-of-lit-negate

(defthm lit-negate-of-lit-negate
  (equal (lit-negate (lit-negate x))
         (lit-fix x)))

Theorem: b-not-not-equal

(defthm b-not-not-equal
  (not (equal (b-not x) x)))

Theorem: lit-negate-not-equal-when-vars-mismatch

(defthm lit-negate-not-equal-when-vars-mismatch
  (implies (not (equal (lit->var x) (lit->var y)))
           (not (equal (lit-negate x) y))))

Theorem: lit-negate-not-equal-when-neg-matches

(defthm lit-negate-not-equal-when-neg-matches
  (implies (equal (lit->neg x) (lit->neg y))
           (not (equal (lit-negate x) y))))

Theorem: equal-of-lit-negate-backchain

(defthm equal-of-lit-negate-backchain
 (implies
  (and
   (syntaxp
    (not
     (or
      (acl2::rewriting-negative-literal-fn
           (cons 'equal
                 (cons (cons 'lit-negate$inline (cons x 'nil))
                       (cons y 'nil)))
           mfc state)
      (acl2::rewriting-negative-literal-fn
           (cons 'equal
                 (cons y
                       (cons (cons 'lit-negate$inline (cons x 'nil))
                             'nil)))
           mfc state))))
   (litp y)
   (equal (lit->var x) (lit->var y))
   (equal (lit->neg x)
          (b-not (lit->neg y))))
  (equal (equal (lit-negate x) y) t)))

Theorem: equal-of-lit->var-negated-hyp

(defthm equal-of-lit->var-negated-hyp
 (implies
  (and
   (syntaxp
        (acl2::rewriting-negative-literal-fn
             (cons 'equal
                   (cons (cons 'lit->var$inline (cons x 'nil))
                         (cons (cons 'lit->var$inline (cons y 'nil))
                               'nil)))
             mfc state))
   (not (equal (lit->neg x) (lit->neg y))))
  (equal (equal (lit->var x) (lit->var y))
         (equal (lit-fix x) (lit-negate y)))))

Theorem: equal-of-lit-negate-component-rewrites

(defthm equal-of-lit-negate-component-rewrites
  (implies (equal (lit-negate x) (lit-fix y))
           (and (equal (lit->var y) (lit->var x))
                (equal (lit->neg y)
                       (b-not (lit->neg x))))))

Theorem: equal-of-b-not-cancel

(defthm equal-of-b-not-cancel
  (equal (equal (b-not x) (b-not y))
         (bit-equiv x y)))

Theorem: equal-of-lit-negate-cancel

(defthm equal-of-lit-negate-cancel
  (equal (equal (lit-negate x) (lit-negate y))
         (equal (lit-fix x) (lit-fix y))))

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

(defthm lit-negate$inline-of-lit-fix-lit
  (equal (lit-negate$inline (lit-fix lit))
         (lit-negate$inline lit)))

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

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

Subtopics

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