		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Int-mod

Modulo of signed integer values.

Signature
(int-mod left-operand right-operand) → result
Arguments: left-operand — Guard (intp left-operand).; right-operand — Guard (intp right-operand).
Returns: result — Type (intp result).

This has the usual relation with division [SD: Types: Integers: Modulo], we use rem here.

Definitions and Theorems

Function: int-mod

(defun int-mod (left-operand right-operand)
 (declare (xargs :guard (and (intp left-operand)
                             (intp right-operand))))
 (declare (xargs :guard (not (equal (int->value right-operand) 0))))
 (b* ((size (int->size left-operand))
      (x (int->value left-operand))
      (y (int->value right-operand)))
   (make-int :size (int->size left-operand)
             :value (logext size (rem x y)))))

Theorem: intp-of-int-mod

(defthm intp-of-int-mod
  (b* ((result (int-mod left-operand right-operand)))
    (intp result))
  :rule-classes :rewrite)

Theorem: int-mod-of-int-fix-left-operand

(defthm int-mod-of-int-fix-left-operand
  (equal (int-mod (int-fix left-operand)
                  right-operand)
         (int-mod left-operand right-operand)))

Theorem: int-mod-int-equiv-congruence-on-left-operand

(defthm int-mod-int-equiv-congruence-on-left-operand
  (implies (int-equiv left-operand left-operand-equiv)
           (equal (int-mod left-operand right-operand)
                  (int-mod left-operand-equiv right-operand)))
  :rule-classes :congruence)

Theorem: int-mod-of-int-fix-right-operand

(defthm int-mod-of-int-fix-right-operand
  (equal (int-mod left-operand (int-fix right-operand))
         (int-mod left-operand right-operand)))

Theorem: int-mod-int-equiv-congruence-on-right-operand

(defthm int-mod-int-equiv-congruence-on-right-operand
  (implies (int-equiv right-operand right-operand-equiv)
           (equal (int-mod left-operand right-operand)
                  (int-mod left-operand right-operand-equiv)))
  :rule-classes :congruence)