Partial merge of integers work; this is simple B&B and some pseudoboolean

infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.

1 files changed, 18 insertions, 1 deletions

diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index c1d46ca65..60cee3937 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -151,7 +151,8 @@ public:
     return *this;
   }
 
-  /** Raise this Integer to the power <code>exp</code>.
+  /**
+   * Raise this Integer to the power <code>exp</code>.
    *
    * @param exp the exponent
    */
@@ -161,6 +162,22 @@ public:
     return Integer( result );
   }
 
+  /**
+   * Return the greatest common divisor of this integer with another.
+   */
+  Integer gcd(const Integer& y) const {
+    mpz_class result;
+    mpz_gcd(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
+    return Integer(result);
+  }
+
+  /**
+   * Return the absolute value of this integer.
+   */
+  Integer abs() const {
+    return d_value >= 0 ? *this : -*this;
+  }
+
   std::string toString(int base = 10) const{
     return d_value.get_str(base);
   }