		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), given the guard.

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)))
  (declare (xargs :guard (vl-expr-p x)))
  (let ((__function__ 'vl-condcheck-negate))
    (declare (ignorable __function__))
    (if (and (not (vl-fast-atom-p x))
             (eq (vl-nonatom->op x)
                 :vl-unary-bitnot))
        (first (vl-nonatom->args x))
      (make-vl-nonatom :op :vl-unary-bitnot
                       :args (list x)))))

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

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