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