		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Bitand-integer-values

Apply & to integer values [C17:6.5.10/4].

Signature
(bitand-integer-values val1 val2) → resval
Arguments: val1 — Guard (valuep val1).; val2 — Guard (valuep val2).
Returns: resval — Type (valuep resval).

By the time we reach this ACL2 function, the values have already been subjected to the usual arithmetic conversions, so they are promoted arithmetic value with the same type. We put this condition in the guard.

The type of the result is the same as the operands [C17:6.3.1.8/1]. This operation is always well-defined, so it always returns a value (never an error).

Verifying the guards of this function involves showing that logand is in the range of an integer type when its operands are in the range of the same integer type. we use rules to rewrite integer-type-rangep to signed-byte-p and unsigned-byte-p, so that library rules apply about logand returning signed-byte-p or unsigned-byte-p under suitable conditions. To relieve the hypotheses of these library rules, we enable the rules about the accessors of the integer values. The :use hint server to exclude the cases in which the two values have different kinds, which is impossible because the two values have the same type.

Definitions and Theorems

Function: bitand-integer-values

(defun bitand-integer-values (val1 val2)
  (declare (xargs :guard (and (valuep val1) (valuep val2))))
  (declare (xargs :guard (and (value-integerp val1)
                              (value-integerp val2)
                              (value-promoted-arithmeticp val1)
                              (value-promoted-arithmeticp val2)
                              (equal (type-of-value val1)
                                     (type-of-value val2)))))
  (let ((__function__ 'bitand-integer-values))
    (declare (ignorable __function__))
    (b* ((mathint1 (value-integer->get val1))
         (mathint2 (value-integer->get val2)))
      (value-integer (logand mathint1 mathint2)
                     (type-of-value val1)))))

Theorem: valuep-of-bitand-integer-values

(defthm valuep-of-bitand-integer-values
  (b* ((resval (bitand-integer-values val1 val2)))
    (valuep resval))
  :rule-classes :rewrite)

Theorem: bitand-integer-values-of-value-fix-val1

(defthm bitand-integer-values-of-value-fix-val1
  (equal (bitand-integer-values (value-fix val1)
                                val2)
         (bitand-integer-values val1 val2)))

Theorem: bitand-integer-values-value-equiv-congruence-on-val1

(defthm bitand-integer-values-value-equiv-congruence-on-val1
  (implies (value-equiv val1 val1-equiv)
           (equal (bitand-integer-values val1 val2)
                  (bitand-integer-values val1-equiv val2)))
  :rule-classes :congruence)

Theorem: bitand-integer-values-of-value-fix-val2

(defthm bitand-integer-values-of-value-fix-val2
  (equal (bitand-integer-values val1 (value-fix val2))
         (bitand-integer-values val1 val2)))

Theorem: bitand-integer-values-value-equiv-congruence-on-val2

(defthm bitand-integer-values-value-equiv-congruence-on-val2
  (implies (value-equiv val2 val2-equiv)
           (equal (bitand-integer-values val1 val2)
                  (bitand-integer-values val1 val2-equiv)))
  :rule-classes :congruence)