• 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
            • 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
  • Math
  • Testing-utilities

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