Add modular arithmetic operators. (#1321)

This adds functions on Integers to compute modular addition, multiplication and inverse.

This is required for the Gaussian Elimination preprocessing pass for BV.

1 files changed, 26 insertions, 0 deletions

diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index c2791af52..0433494cc 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -23,6 +23,7 @@
 #include <cln/input.h>
 #include <cln/integer.h>
 #include <cln/integer_io.h>
+#include <cln/modinteger.h>
 #include <iostream>
 #include <limits>
 #include <sstream>
@@ -165,6 +166,7 @@ public:
   Integer operator*(const Integer& y) const {
     return Integer( d_value * y.d_value );
   }
+
   Integer& operator*=(const Integer& y) {
     d_value *= y.d_value;
     return *this;
@@ -348,6 +350,30 @@ public:
   }
 
   /**
+   * Compute addition of this Integer x + y modulo m.
+   */
+  Integer modAdd(const Integer& y, const Integer& m) const;
+
+  /**
+   * Compute multiplication of this Integer x * y modulo m.
+   */
+  Integer modMultiply(const Integer& y, const Integer& m) const;
+
+  /**
+   * Compute modular inverse x^-1 of this Integer x modulo m with m > 0.
+   * Returns a value x^-1 with 0 <= x^-1 < m such that x * x^-1 = 1 modulo m
+   * if such an inverse exists, and -1 otherwise.
+   *
+   * Such an inverse only exists if
+   *   - x is non-zero
+   *   - x and m are coprime, i.e., if gcd (x, m) = 1
+   *
+   * Note that if x and m are coprime, then x^-1 > 0 if m > 1 and x^-1 = 0
+   * if m = 1 (the zero ring).
+   */
+  Integer modInverse(const Integer& m) const;
+
+  /**
    * Return true if *this exactly divides y.
    */
   bool divides(const Integer& y) const {