		Search-engine friendly clone of the ACL2 documentation.

Oddexpr-check

Vl-odd-binop-class

Group binary operators into classes.

Signature
(vl-odd-binop-class x) → class
Arguments: x — Guard (vl-op-p x).
Returns: class — Type (symbolp class).

This lets us come up with a basic abstraction for an expression, where, e.g., we treat any kind of shift operation as equivalent, etc.

Definitions and Theorems

Function: vl-odd-binop-class

(defun vl-odd-binop-class (x)
  (declare (xargs :guard (vl-op-p x)))
  (let ((__function__ 'vl-odd-binop-class))
    (declare (ignorable __function__))
    (case x
          ((:vl-binary-times :vl-binary-div
                             :vl-binary-mod :vl-binary-power)
           :mult-class)
          ((:vl-binary-plus) :plus-class)
          ((:vl-binary-minus) :minus-class)
          ((:vl-binary-shl :vl-binary-shr
                           :vl-binary-ashl :vl-binary-ashr)
           :shift-class)
          ((:vl-binary-lt :vl-binary-lte
                          :vl-binary-gt :vl-binary-gte)
           :rel-class)
          ((:vl-binary-eq :vl-binary-neq)
           :cmp-class)
          ((:vl-binary-ceq :vl-binary-cne)
           :ceq-class)
          ((:vl-binary-bitand) :bitand-class)
          ((:vl-binary-xor :vl-binary-xnor)
           :xor-class)
          ((:vl-binary-bitor) :bitor-class)
          ((:vl-binary-logand) :logand-class)
          ((:vl-binary-logor) :logor-class)
          (otherwise nil))))

Theorem: symbolp-of-vl-odd-binop-class

(defthm symbolp-of-vl-odd-binop-class
  (b* ((class (vl-odd-binop-class x)))
    (symbolp class))
  :rule-classes :type-prescription)