		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Bitxor-integer-values

Apply ^ to integer values [C:6.5.11/4].

Signature
(bitxor-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 [C:6.3.1.8/1]. This operation is always well-defined, so it always returns a value (never an error).

The guard verification of this function is similar to bitand-integer-values; see that function documentation for details on this.

Definitions and Theorems

Function: bitxor-integer-values

(defun bitxor-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__ 'bitxor-integer-values))
    (declare (ignorable __function__))
    (b* ((mathint1 (value-integer->get val1))
         (mathint2 (value-integer->get val2)))
      (value-integer (logxor mathint1 mathint2)
                     (type-of-value val1)))))

Theorem: valuep-of-bitxor-integer-values

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

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

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

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

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

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

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

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

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