		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expr-constp

Check if an expression is constant.

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

This concept is described in [C:6.6], which does not provide a detailed definition, but here we define a notion that should be at least as strict as that (possibly stricter), for our current C subset.

Definitions and Theorems

Function: expr-constp

(defun expr-constp (e)
 (declare (xargs :guard (exprp e)))
 (let ((__function__ 'expr-constp))
  (declare (ignorable __function__))
  (expr-case e
             :ident nil
             :const t
             :arrsub nil
             :call nil
             :member nil
             :memberp nil
             :postinc nil
             :postdec nil
             :preinc nil
             :predec nil
             :unary (and (member-eq (unop-kind e.op)
                                    '(:plus :minus :bitnot :lognot))
                         (expr-constp e.arg))
             :cast (expr-constp e.arg)
             :binary (and (member-eq (binop-kind e.op)
                                     '(:mul :div
                                            :rem :add
                                            :sub :shl
                                            :shr :lt
                                            :gt :le
                                            :ge :eq
                                            :ne :bitand
                                            :bitxor :bitior
                                            :logand :logor))
                          (expr-constp e.arg1)
                          (expr-constp e.arg2))
             :cond (and (expr-constp e.test)
                        (expr-constp e.then)
                        (expr-constp e.else)))))

Theorem: booleanp-of-expr-constp

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

Theorem: expr-constp-of-expr-fix-e

(defthm expr-constp-of-expr-fix-e
  (equal (expr-constp (expr-fix e))
         (expr-constp e)))

Theorem: expr-constp-expr-equiv-congruence-on-e

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