• 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-cond^
          • Lit-negate
          • 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
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Litp

Lit-negate-cond

Efficiently negate a literal.

Signature

(lit-negate-cond lit c) → new-lit

Arguments

lit — Guard (litp lit).

c — Guard (bitp c).

Returns

new-lit — Type (litp new-lit).

When c is 1, we negate lit. Otherwise, when c is 0, we return lit unchanged.

Definitions and Theorems

Function: lit-negate-cond$inline

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

Theorem: litp-of-lit-negate-cond

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

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

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

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

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

Theorem: lit-negate-cond-of-make-lit

(defthm lit-negate-cond-of-make-lit
        (equal (lit-negate-cond (make-lit var neg) c)
               (make-lit var (b-xor c neg))))

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

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

Theorem: lit-negate-cond-not-equal-when-neg-mismatches

(defthm lit-negate-cond-not-equal-when-neg-mismatches
        (implies (not (equal (lit->neg x)
                             (b-xor c (lit->neg y))))
                 (not (equal (lit-negate-cond x c) y))))

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

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

Theorem: equal-of-lit-negate-cond-backchain

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

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

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

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

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

Theorem: lit-negate-cond$inline-of-bfix-c

(defthm lit-negate-cond$inline-of-bfix-c
        (equal (lit-negate-cond$inline lit (bfix c))
               (lit-negate-cond$inline lit c)))

Theorem: lit-negate-cond$inline-bit-equiv-congruence-on-c

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

Subtopics

Lit-negate-cond^

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