		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expr-zerop

Check if an expression is zero.

Signature
(expr-zerop expr) → yes/no
Arguments: expr — Guard (exprp expr).
Returns: yes/no — Type (booleanp yes/no).

There are syntactically different expressions in C that evaluate to ``zero'' in a broad sense. For now we only include the octal integer constant 0 without suffixes and with just one digit. So this operation is very limited in scope, but sufficient for its current usage (elsewhere).

Definitions and Theorems

Function: expr-zerop

(defun expr-zerop (expr)
  (declare (xargs :guard (exprp expr)))
  (b* (((unless (expr-case expr :const)) nil)
       (const (expr-const->const expr))
       ((unless (const-case const :int)) nil)
       ((iconst iconst)
        (const-int->iconst const))
       ((when iconst.suffix?) nil)
       ((unless (dec/oct/hex-const-case iconst.core :oct))
        nil)
       ((dec/oct/hex-const-oct doh)
        iconst.core)
       ((unless (= doh.leading-zeros 1)) nil)
       ((unless (= doh.value 0)) nil))
    t))

Theorem: booleanp-of-expr-zerop

(defthm booleanp-of-expr-zerop
  (b* ((yes/no (expr-zerop expr)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: expr-zerop-of-expr-fix-expr

(defthm expr-zerop-of-expr-fix-expr
  (equal (expr-zerop (expr-fix expr))
         (expr-zerop expr)))

Theorem: expr-zerop-expr-equiv-congruence-on-expr

(defthm expr-zerop-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (expr-zerop expr)
                  (expr-zerop expr-equiv)))
  :rule-classes :congruence)