		Search-engine friendly clone of the ACL2 documentation.

Condcheck

Vl-condcheck-negate

Smartly negate a canonicalized expression.

Signature
(vl-condcheck-negate x) → new-x
Arguments: x — Guard (vl-expr-p x).
Returns: new-x — Type (vl-expr-p new-x).

We assume X is already canonicalized in the sense of vl-condcheck-fix. We "smartly" negate it so that, e.g., A becomes ~A, but ~A becomes A instead of ~~A.

Definitions and Theorems

Function: vl-condcheck-negate

(defun vl-condcheck-negate (x)
  (declare (xargs :guard (vl-expr-p x)))
  (let ((__function__ 'vl-condcheck-negate))
    (declare (ignorable __function__))
    (let ((dumb (make-vl-unary :op :vl-unary-bitnot
                               :arg x)))
      (vl-expr-case x :vl-unary
                    (if (vl-unaryop-equiv x.op :vl-unary-bitnot)
                        x.arg
                      dumb)
                    :otherwise dumb))))

Theorem: vl-expr-p-of-vl-condcheck-negate

(defthm vl-expr-p-of-vl-condcheck-negate
  (b* ((new-x (vl-condcheck-negate x)))
    (vl-expr-p new-x))
  :rule-classes :rewrite)

Theorem: vl-condcheck-negate-of-vl-expr-fix-x

(defthm vl-condcheck-negate-of-vl-expr-fix-x
  (equal (vl-condcheck-negate (vl-expr-fix x))
         (vl-condcheck-negate x)))

Theorem: vl-condcheck-negate-vl-expr-equiv-congruence-on-x

(defthm vl-condcheck-negate-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-condcheck-negate x)
                  (vl-condcheck-negate x-equiv)))
  :rule-classes :congruence)